# Theory Compiler

Up to index of Isabelle/HOL/IMP

theory Compiler
imports Machines
begin

    (*  Title:      HOL/IMP/Compiler.thy
        ID:         $Id: Compiler.thy,v 1.15 2005/06/17 14:13:07 haftmann Exp $
        Author:     Tobias Nipkow, TUM
        Copyright   1996 TUM
    *)

    theory Compiler imports Machines begin

    subsection "The compiler"

    consts compile :: "com => instr list"
    primrec
    "compile \<SKIP> = []"
    "compile (x:==a) = [SET x a]"
    "compile (c1;c2) = compile c1 @ compile c2"
    "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
     [JMPF b (length(compile c1) + 1)] @ compile c1 @
     [JMPF (λx. False) (length(compile c2))] @ compile c2"
    "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
     [JMPB (length(compile c)+1)]"

    subsection "Compiler correctness"

    theorem assumes A: "⟨c,s⟩ -->c t"
    shows "!!p q. ⟨compile c @ p,q,s⟩ -*-> ⟨p,rev(compile c)@q,t⟩"
      (is "!!p q. ?P c s t p q")
    proof -
      from A show "!!p q. ?thesis p q"
      proof induct
        case Skip thus ?case by simp
      next
        case Assign thus ?case by force
      next
        case Semi thus ?case by simp (blast intro:rtrancl_trans)
      next
        fix b c0 c1 s0 s1 p q
        assume IH: "!!p q. ?P c0 s0 s1 p q"
        assume "b s0"
        thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
          by(simp add: IH[THEN rtrancl_trans])
      next
        case IfFalse thus ?case by(simp)
      next
        case WhileFalse thus ?case by simp
      next
        fix b c and s0::state and s1 s2 p q
        assume b: "b s0" and
          IHc: "!!p q. ?P c s0 s1 p q" and
          IHw: "!!p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
        show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
          using b  IHc[THEN rtrancl_trans] IHw by(simp)
      qed
    qed

    text {* The other direction! *}

    inductive_cases [elim!]: "(([],p,s),next) : stepa1"

    lemma [simp]: "(⟨[],q,s⟩ -n-> ⟨p',q',t⟩) = (n=0 ∧ p' = [] ∧ q' = q ∧ t = s)"
    apply(rule iffI)
     apply(erule converse_rel_powE, simp, fast)
    apply simp
    done

    lemma [simp]: "(⟨[],q,s⟩ -*-> ⟨p',q',t⟩) = (p' = [] ∧ q' = q ∧ t = s)"
    by(simp add: rtrancl_is_UN_rel_pow)

    constdefs
     forws :: "instr => nat set"
    "forws instr == case instr of
     SET x a => {0} |
     JMPF b n => {0,n} |
     JMPB n => {}"
     backws :: "instr => nat set"
    "backws instr == case instr of
     SET x a => {} |
     JMPF b n => {} |
     JMPB n => {n}"

    consts closed :: "nat => nat => instr list => bool"
    primrec
    "closed m n [] = True"
    "closed m n (instr#is) = ((∀j ∈ forws instr. j ≤ size is+n) ∧
                            (∀j ∈ backws instr. j ≤ m) ∧ closed (Suc m) n is)"

    lemma [simp]:
     "!!m n. closed m n (C1@C2) =
             (closed m (n+size C2) C1 ∧ closed (m+size C1) n C2)"
    by(induct C1, simp, simp add:add_ac)

    theorem [simp]: "!!m n. closed m n (compile c)"
    by(induct c, simp_all add:backws_def forws_def)

    lemma drop_lem: "n ≤ size(p1@p2)
     ==> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
        (n ≤ size p1 & p1' = drop n p1)"
    apply(rule iffI)
     defer apply simp
    apply(subgoal_tac "n ≤ size p1")
     apply simp
    apply(rule ccontr)
    apply(drule_tac f = length in arg_cong)
    apply simp
    apply arith
    done

    lemma reduce_exec1:
     "⟨i # p1 @ p2,q1 @ q2,s⟩ -1-> ⟨p1' @ p2,q1' @ q2,s'⟩ ==>
      ⟨i # p1,q1,s⟩ -1-> ⟨p1',q1',s'⟩"
    by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm)

    lemma closed_exec1:
     "[| closed 0 0 (rev q1 @ instr # p1);
        ⟨instr # p1 @ p2, q1 @ q2,r⟩ -1-> ⟨p',q',r'⟩ |] ==>
      ∃p1' q1'. p' = p1'@p2 ∧ q' = q1'@q2 ∧ rev q1' @ p1' = rev q1 @ instr # p1"
    apply(clarsimp simp add:forws_def backws_def
                   split:instr.split_asm split_if_asm)
    done

    theorem closed_execn_decomp: "!!C1 C2 r.
     [| closed 0 0 (rev C1 @ C2);
       ⟨C2 @ p1 @ p2, C1 @ q,r⟩ -n-> ⟨p2,rev p1 @ rev C2 @ C1 @ q,t⟩ |]
     ==> ∃s n1 n2. ⟨C2,C1,r⟩ -n1-> ⟨[],rev C2 @ C1,s⟩ ∧
         ⟨p1@p2,rev C2 @ C1 @ q,s⟩ -n2-> ⟨p2, rev p1 @ rev C2 @ C1 @ q,t⟩ ∧
             n = n1+n2"
    (is "!!C1 C2 r. [|?CL C1 C2; ?H C1 C2 r n|] ==> ?P C1 C2 r n")
    proof(induct n)
      fix C1 C2 r
      assume "?H C1 C2 r 0"
      thus "?P C1 C2 r 0" by simp
    next
      fix C1 C2 r n
      assume IH: "!!C1 C2 r. ?CL C1 C2 ==> ?H C1 C2 r n ==> ?P C1 C2 r n"
      assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
      show "?P C1 C2 r (Suc n)"
      proof (cases C2)
        assume "C2 = []" with H show ?thesis by simp
      next
        fix instr tlC2
        assume C2: "C2 = instr # tlC2"
        from H C2 obtain p' q' r'
          where 1: "⟨instr # tlC2 @ p1 @ p2, C1 @ q,r⟩ -1-> ⟨p',q',r'⟩"
          and n: "⟨p',q',r'⟩ -n-> ⟨p2,rev p1 @ rev C2 @ C1 @ q,t⟩"
          by(fastsimp simp add:R_O_Rn_commute)
        from CL closed_exec1[OF _ 1] C2
        obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 ∧ q' = C1' @ q"
          and same: "rev C1' @ C2' = rev C1 @ C2"
          by fastsimp
        have rev_same: "rev C2' @ C1' = rev C2 @ C1"
        proof -
          have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
          also have "… = rev(rev C1 @ C2)" by(simp only:same)
          also have "… =  rev C2 @ C1" by simp
          finally show ?thesis .
        qed
        hence rev_same': "!!p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
        from n have n': "⟨C2' @ p1 @ p2,C1' @ q,r'⟩ -n->
                         ⟨p2,rev p1 @ rev C2' @ C1' @ q,t⟩"
          by(simp add:pq' rev_same')
        from IH[OF _ n'] CL
        obtain s n1 n2 where n1: "⟨C2',C1',r'⟩ -n1-> ⟨[],rev C2 @ C1,s⟩" and
          "⟨p1 @ p2,rev C2 @ C1 @ q,s⟩ -n2-> ⟨p2,rev p1 @ rev C2 @ C1 @ q,t⟩ ∧
           n = n1 + n2"
          by(fastsimp simp add: same rev_same rev_same')
        moreover
        from 1 n1 pq' C2 have "⟨C2,C1,r⟩ -Suc n1-> ⟨[],rev C2 @ C1,s⟩"
          by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
        ultimately show ?thesis by (fastsimp simp del:relpow.simps)
      qed
    qed

    lemma execn_decomp:
    "⟨compile c @ p1 @ p2,q,r⟩ -n-> ⟨p2,rev p1 @ rev(compile c) @ q,t⟩
     ==> ∃s n1 n2. ⟨compile c,[],r⟩ -n1-> ⟨[],rev(compile c),s⟩ ∧
         ⟨p1@p2,rev(compile c) @ q,s⟩ -n2-> ⟨p2, rev p1 @ rev(compile c) @ q,t⟩ ∧
             n = n1+n2"
    using closed_execn_decomp[of "[]",simplified] by simp

    lemma exec_star_decomp:
    "⟨compile c @ p1 @ p2,q,r⟩ -*-> ⟨p2,rev p1 @ rev(compile c) @ q,t⟩
     ==> ∃s. ⟨compile c,[],r⟩ -*-> ⟨[],rev(compile c),s⟩ ∧
         ⟨p1@p2,rev(compile c) @ q,s⟩ -*-> ⟨p2, rev p1 @ rev(compile c) @ q,t⟩"
    by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)

    (* Alternative:
    lemma exec_comp_n:
    "!!p1 p2 q r t n.
     ⟨compile c @ p1 @ p2,q,r⟩ -n-> ⟨p2,rev p1 @ rev(compile c) @ q,t⟩
     ==> ∃s n1 n2. ⟨compile c,[],r⟩ -n1-> ⟨[],rev(compile c),s⟩ ∧
         ⟨p1@p2,rev(compile c) @ q,s⟩ -n2-> ⟨p2, rev p1 @ rev(compile c) @ q,t⟩ ∧
             n = n1+n2"
     (is "!!p1 p2 q r t n. ?H c p1 p2 q r t n ==> ?P c p1 p2 q r t n")
    proof (induct c)
    *)

    text{*Warning:
    @{prop"⟨compile c @ p,q,s⟩ -*-> ⟨p,rev(compile c)@q,t⟩ ==> ⟨c,s⟩ -->c t"}
    is not true! *}

    theorem "!!s t.
     ⟨compile c,[],s⟩ -*-> ⟨[],rev(compile c),t⟩ ==> ⟨c,s⟩ -->c t"
    proof (induct c)
      fix s t
      assume "⟨compile SKIP,[],s⟩ -*-> ⟨[],rev(compile SKIP),t⟩"
      thus "⟨SKIP,s⟩ -->c t" by simp
    next
      fix s t v f
      assume "⟨compile(v :== f),[],s⟩ -*-> ⟨[],rev(compile(v :== f)),t⟩"
      thus "⟨v :== f,s⟩ -->c t" by simp
    next
      fix s1 s3 c1 c2
      let ?C1 = "compile c1" let ?C2 = "compile c2"
      assume IH1: "!!s t. ⟨?C1,[],s⟩ -*-> ⟨[],rev ?C1,t⟩ ==> ⟨c1,s⟩ -->c t"
         and IH2: "!!s t. ⟨?C2,[],s⟩ -*-> ⟨[],rev ?C2,t⟩ ==> ⟨c2,s⟩ -->c t"
      assume "⟨compile(c1;c2),[],s1⟩ -*-> ⟨[],rev(compile(c1;c2)),s3⟩"
      then obtain s2 where exec1: "⟨?C1,[],s1⟩ -*-> ⟨[],rev ?C1,s2⟩" and
                 exec2: "⟨?C2,rev ?C1,s2⟩ -*-> ⟨[],rev(compile(c1;c2)),s3⟩"
        by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
      from exec2 have exec2': "⟨?C2,[],s2⟩ -*-> ⟨[],rev ?C2,s3⟩"
        using exec_star_decomp[of _ "[]" "[]"] by fastsimp
      have "⟨c1,s1⟩ -->c s2" using IH1 exec1 by simp
      moreover have "⟨c2,s2⟩ -->c s3" using IH2 exec2' by fastsimp
      ultimately show "⟨c1;c2,s1⟩ -->c s3" ..
    next
      fix s t b c1 c2
      let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
      let ?C1 = "compile c1" let ?C2 = "compile c2"
      assume IH1: "!!s t. ⟨?C1,[],s⟩ -*-> ⟨[],rev ?C1,t⟩ ==> ⟨c1,s⟩ -->c t"
         and IH2: "!!s t. ⟨?C2,[],s⟩ -*-> ⟨[],rev ?C2,t⟩ ==> ⟨c2,s⟩ -->c t"
         and H: "⟨?C,[],s⟩ -*-> ⟨[],rev ?C,t⟩"
      show "⟨?if,s⟩ -->c t"
      proof cases
        assume b: "b s"
        with H have "⟨?C1,[],s⟩ -*-> ⟨[],rev ?C1,t⟩"
          by (fastsimp dest:exec_star_decomp
                [of _ "[JMPF (λx. False) (size ?C2)]@?C2" "[]",simplified])
        hence "⟨c1,s⟩ -->c t" by(rule IH1)
        with b show ?thesis ..
      next
        assume b: "¬ b s"
        with H have "⟨?C2,[],s⟩ -*-> ⟨[],rev ?C2,t⟩"
          using exec_star_decomp[of _ "[]" "[]"] by simp
        hence "⟨c2,s⟩ -->c t" by(rule IH2)
        with b show ?thesis ..
      qed
    next
      fix b c s t
      let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
      let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
      assume IHc: "!!s t. ⟨?C,[],s⟩ -*-> ⟨[],rev ?C,t⟩ ==> ⟨c,s⟩ -->c t"
         and H: "⟨?W,[],s⟩ -*-> ⟨[],rev ?W,t⟩"
      from H obtain k where ob:"⟨?W,[],s⟩ -k-> ⟨[],rev ?W,t⟩"
        by(simp add:rtrancl_is_UN_rel_pow) blast
      { fix n have "!!s. ⟨?W,[],s⟩ -n-> ⟨[],rev ?W,t⟩ ==> ⟨?w,s⟩ -->c t"
        proof (induct n rule: less_induct)
          fix n
          assume IHm: "!!m s. [|m < n; ⟨?W,[],s⟩ -m-> ⟨[],rev ?W,t⟩ |] ==> ⟨?w,s⟩ -->c t"
          fix s
          assume H: "⟨?W,[],s⟩ -n-> ⟨[],rev ?W,t⟩"
          show "⟨?w,s⟩ -->c t"
          proof cases
            assume b: "b s"
            then obtain m where m: "n = Suc m"
              and "⟨?C @ [?j2],[?j1],s⟩ -m-> ⟨[],rev ?W,t⟩"
              using H by fastsimp
            then obtain r n1 n2 where n1: "⟨?C,[],s⟩ -n1-> ⟨[],rev ?C,r⟩"
              and n2: "⟨[?j2],rev ?C @ [?j1],r⟩ -n2-> ⟨[],rev ?W,t⟩"
              and n12: "m = n1+n2"
              using execn_decomp[of _ "[?j2]"]
              by(simp del: execn_simp) fast
            have n2n: "n2 - 1 < n" using m n12 by arith
            note b
            moreover
            { from n1 have "⟨?C,[],s⟩ -*-> ⟨[],rev ?C,r⟩"
                by (simp add:rtrancl_is_UN_rel_pow) fast
              hence "⟨c,s⟩ -->c r" by(rule IHc)
            }
            moreover
            { have "n2 - 1 < n" using m n12 by arith
              moreover from n2 have "⟨?W,[],r⟩ -n2- 1-> ⟨[],rev ?W,t⟩" by fastsimp
              ultimately have "⟨?w,r⟩ -->c t" by(rule IHm)
            }
            ultimately show ?thesis ..
          next
            assume b: "¬ b s"
            hence "t = s" using H by simp
            with b show ?thesis by simp
          qed
        qed
      }
      with ob show "⟨?w,s⟩ -->c t" by fast
    qed

    (* To Do: connect with Machine 0 using M_equiv *)

    end

### The compiler

### Compiler correctness

theorem

      ⟨c,s⟩ -->c t ==> <compile c @ p,q,s> -*-> <p,rev (compile c) @ q,t>

lemmas

      (([], p, s), next) ∈ stepa1 ==> P

lemma

      (<[],q,s> -n-> <p',q',t>) = (n = 0 ∧ p' = [] ∧ q' = q ∧ t = s)

lemma

      (<[],q,s> -*-> <p',q',t>) = (p' = [] ∧ q' = q ∧ t = s)

lemma

      closed m n (C1.0 @ C2.0) =
      (closed m (n + length C2.0) C1.0 ∧ closed (m + length C1.0) n C2.0)

theorem

      closed m n (compile c)

lemma drop_lem:

      n ≤ length (p1.0 @ p2.0)
      ==> (p1' @ p2.0 = drop n p1.0 @ drop (n - length p1.0) p2.0) =
          (n ≤ length p1.0 ∧ p1' = drop n p1.0)

lemma reduce_exec1:

      <i # p1.0 @ p2.0,q1.0 @ q2.0,s> -1-> <p1' @ p2.0,q1' @ q2.0,s'>
      ==> <i # p1.0,q1.0,s> -1-> <p1',q1',s'>

lemma closed_exec1:

      [| closed 0 0 (rev q1.0 @ instr # p1.0);
         <instr # p1.0 @ p2.0,q1.0 @ q2.0,r> -1-> <p',q',r'> |]
      ==> ∃p1' q1'.
             p' = p1' @ p2.0 ∧
             q' = q1' @ q2.0 ∧ rev q1' @ p1' = rev q1.0 @ instr # p1.0

theorem closed_execn_decomp:

      [| closed 0 0 (rev C1.0 @ C2.0);
         <C2.0 @ p1.0 @ p2.0,C1.0 @ q,r>
         -n-> <p2.0,rev p1.0 @ rev C2.0 @ C1.0 @ q,t> |]
      ==> ∃s n1 n2.
             <C2.0,C1.0,r> -n1-> <[],rev C2.0 @ C1.0,s> ∧
             <p1.0 @ p2.0,rev C2.0 @ C1.0 @ q,s>
             -n2-> <p2.0,rev p1.0 @ rev C2.0 @ C1.0 @ q,t> ∧
             n = n1 + n2

lemma execn_decomp:

      <compile c @ p1.0 @ p2.0,q,r> -n-> <p2.0,rev p1.0 @ rev (compile c) @ q,t>
      ==> ∃s n1 n2.
             <compile c,[],r> -n1-> <[],rev (compile c),s> ∧
             <p1.0 @ p2.0,rev (compile c) @ q,s>
             -n2-> <p2.0,rev p1.0 @ rev (compile c) @ q,t> ∧
             n = n1 + n2

lemma exec_star_decomp:

      <compile c @ p1.0 @ p2.0,q,r> -*-> <p2.0,rev p1.0 @ rev (compile c) @ q,t>
      ==> ∃s. <compile c,[],r> -*-> <[],rev (compile c),s> ∧
              <p1.0 @ p2.0,rev (compile c) @ q,s>
              -*-> <p2.0,rev p1.0 @ rev (compile c) @ q,t>

theorem

      <compile c,[],s> -*-> <[],rev (compile c),t> ==> ⟨c,s⟩ -->c t