# Theory Compiler0

Up to index of Isabelle/HOL/IMP

theory Compiler0
imports Natural
begin

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

    This is an early version of the compiler, where the abstract machine
    has an explicit pc. This turned out to be awkward, and a second
    development was started. See Machines.thy and Compiler.thy.
    *)

    header "A Simple Compiler"

    theory Compiler0 imports Natural begin

    subsection "An abstract, simplistic machine"

    text {* There are only three instructions: *}
    datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat

    text {* We describe execution of programs in the machine by
      an operational (small step) semantics:
    *}
    consts  stepa1 :: "instr list => ((state×nat) × (state×nat))set"

    syntax
      "_stepa1" :: "[instr list,state,nat,state,nat] => bool"
                   ("_ |- (3<_,_>/ -1-> <_,_>)" [50,0,0,0,0] 50)
      "_stepa" :: "[instr list,state,nat,state,nat] => bool"
                   ("_ |-/ (3<_,_>/ -*-> <_,_>)" [50,0,0,0,0] 50)

      "_stepan" :: "[instr list,state,nat,nat,state,nat] => bool"
                   ("_ |-/ (3<_,_>/ -(_)-> <_,_>)" [50,0,0,0,0,0] 50)

    syntax (xsymbols)
      "_stepa1" :: "[instr list,state,nat,state,nat] => bool"
                   ("_ \<turnstile> (3⟨_,_⟩/ -1-> ⟨_,_⟩)" [50,0,0,0,0] 50)
      "_stepa" :: "[instr list,state,nat,state,nat] => bool"
                   ("_ \<turnstile>/ (3⟨_,_⟩/ -*-> ⟨_,_⟩)" [50,0,0,0,0] 50)
      "_stepan" :: "[instr list,state,nat,nat,state,nat] => bool"
                   ("_ \<turnstile>/ (3⟨_,_⟩/ -(_)-> ⟨_,_⟩)" [50,0,0,0,0,0] 50)

    syntax (HTML output)
      "_stepa1" :: "[instr list,state,nat,state,nat] => bool"
                   ("_ |- (3⟨_,_⟩/ -1-> ⟨_,_⟩)" [50,0,0,0,0] 50)
      "_stepa" :: "[instr list,state,nat,state,nat] => bool"
                   ("_ |-/ (3⟨_,_⟩/ -*-> ⟨_,_⟩)" [50,0,0,0,0] 50)
      "_stepan" :: "[instr list,state,nat,nat,state,nat] => bool"
                   ("_ |-/ (3⟨_,_⟩/ -(_)-> ⟨_,_⟩)" [50,0,0,0,0,0] 50)

    translations
      "P \<turnstile> ⟨s,m⟩ -1-> ⟨t,n⟩" == "((s,m),t,n) : stepa1 P"
      "P \<turnstile> ⟨s,m⟩ -*-> ⟨t,n⟩" == "((s,m),t,n) : ((stepa1 P)^*)"
      "P \<turnstile> ⟨s,m⟩ -(i)-> ⟨t,n⟩" == "((s,m),t,n) : ((stepa1 P)^i)"

    inductive "stepa1 P"
    intros
    ASIN[simp]:
      "[| n<size P; P!n = ASIN x a |] ==> P \<turnstile> ⟨s,n⟩ -1-> ⟨s[x\<mapsto> a s],Suc n⟩"
    JMPFT[simp,intro]:
      "[| n<size P; P!n = JMPF b i;  b s |] ==> P \<turnstile> ⟨s,n⟩ -1-> ⟨s,Suc n⟩"
    JMPFF[simp,intro]:
      "[| n<size P; P!n = JMPF b i; ~b s; m=n+i |] ==> P \<turnstile> ⟨s,n⟩ -1-> ⟨s,m⟩"
    JMPB[simp]:
      "[| n<size P; P!n = JMPB i; i <= n; j = n-i |] ==> P \<turnstile> ⟨s,n⟩ -1-> ⟨s,j⟩"

    subsection "The compiler"

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

    declare nth_append[simp]

    subsection "Context lifting lemmas"

    text {*
      Some lemmas for lifting an execution into a prefix and suffix
      of instructions; only needed for the first proof.
    *}
    lemma app_right_1:
      assumes A: "is1 \<turnstile> ⟨s1,i1⟩ -1-> ⟨s2,i2⟩"
      shows "is1 @ is2 \<turnstile> ⟨s1,i1⟩ -1-> ⟨s2,i2⟩"
    proof -
     from A show ?thesis
     by induct force+
    qed

    lemma app_left_1:
      assumes A: "is2 \<turnstile> ⟨s1,i1⟩ -1-> ⟨s2,i2⟩"
      shows "is1 @ is2 \<turnstile> ⟨s1,size is1+i1⟩ -1-> ⟨s2,size is1+i2⟩"
    proof -
     from A show ?thesis
     by induct force+
    qed

    declare rtrancl_induct2 [induct set: rtrancl]

    lemma app_right:
    assumes A: "is1 \<turnstile> ⟨s1,i1⟩ -*-> ⟨s2,i2⟩"
    shows "is1 @ is2 \<turnstile> ⟨s1,i1⟩ -*-> ⟨s2,i2⟩"
    proof -
     from A show ?thesis
     proof induct
       show "is1 @ is2 \<turnstile> ⟨s1,i1⟩ -*-> ⟨s1,i1⟩" by simp
     next
       fix s1' i1' s2 i2
       assume "is1 @ is2 \<turnstile> ⟨s1,i1⟩ -*-> ⟨s1',i1'⟩"
              "is1 \<turnstile> ⟨s1',i1'⟩ -1-> ⟨s2,i2⟩"
       thus "is1 @ is2 \<turnstile> ⟨s1,i1⟩ -*-> ⟨s2,i2⟩"
         by(blast intro:app_right_1 rtrancl_trans)
     qed
    qed

    lemma app_left:
    assumes A: "is2 \<turnstile> ⟨s1,i1⟩ -*-> ⟨s2,i2⟩"
    shows "is1 @ is2 \<turnstile> ⟨s1,size is1+i1⟩ -*-> ⟨s2,size is1+i2⟩"
    proof -
      from A show ?thesis
      proof induct
        show "is1 @ is2 \<turnstile> ⟨s1,length is1 + i1⟩ -*-> ⟨s1,length is1 + i1⟩" by simp
      next
        fix s1' i1' s2 i2
        assume "is1 @ is2 \<turnstile> ⟨s1,length is1 + i1⟩ -*-> ⟨s1',length is1 + i1'⟩"
               "is2 \<turnstile> ⟨s1',i1'⟩ -1-> ⟨s2,i2⟩"
        thus "is1 @ is2 \<turnstile> ⟨s1,length is1 + i1⟩ -*-> ⟨s2,length is1 + i2⟩"
          by(blast intro:app_left_1 rtrancl_trans)
     qed
    qed

    lemma app_left2:
      "[| is2 \<turnstile> ⟨s1,i1⟩ -*-> ⟨s2,i2⟩; j1 = size is1+i1; j2 = size is1+i2 |] ==>
       is1 @ is2 \<turnstile> ⟨s1,j1⟩ -*-> ⟨s2,j2⟩"
      by (simp add:app_left)

    lemma app1_left:
      "is \<turnstile> ⟨s1,i1⟩ -*-> ⟨s2,i2⟩ ==>
       instr # is \<turnstile> ⟨s1,Suc i1⟩ -*-> ⟨s2,Suc i2⟩"
      by(erule app_left[of _ _ _ _ _ "[instr]",simplified])

    subsection "Compiler correctness"

    declare rtrancl_into_rtrancl[trans]
            converse_rtrancl_into_rtrancl[trans]
            rtrancl_trans[trans]

    text {*
      The first proof; The statement is very intuitive,
      but application of induction hypothesis requires the above lifting lemmas
    *}
    theorem assumes A: "⟨c,s⟩ -->c t"
    shows "compile c \<turnstile> ⟨s,0⟩ -*-> ⟨t,length(compile c)⟩" (is "?P c s t")
    proof -
      from A show ?thesis
      proof induct
        show "!!s. ?P \<SKIP> s s" by simp
      next
        show "!!a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
      next
        fix c0 c1 s0 s1 s2
        assume "?P c0 s0 s1"
        hence "compile c0 @ compile c1 \<turnstile> ⟨s0,0⟩ -*-> ⟨s1,length(compile c0)⟩"
          by(rule app_right)
        moreover assume "?P c1 s1 s2"
        hence "compile c0 @ compile c1 \<turnstile> ⟨s1,length(compile c0)⟩ -*->
               ⟨s2,length(compile c0)+length(compile c1)⟩"
        proof -
          show "!!is1 is2 s1 s2 i2.
                  is2 \<turnstile> ⟨s1,0⟩ -*-> ⟨s2,i2⟩ ==>
                  is1 @ is2 \<turnstile> ⟨s1,size is1⟩ -*-> ⟨s2,size is1+i2⟩"
            using app_left[of _ 0] by simp
        qed
        ultimately have "compile c0 @ compile c1 \<turnstile> ⟨s0,0⟩ -*->
                           ⟨s2,length(compile c0)+length(compile c1)⟩"
          by (rule rtrancl_trans)
        thus "?P (c0; c1) s0 s2" by simp
      next
        fix b c0 c1 s0 s1
        let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
        assume "b s0" and IH: "?P c0 s0 s1"
        hence "?comp \<turnstile> ⟨s0,0⟩ -1-> ⟨s0,1⟩" by auto
        also from IH
        have "?comp \<turnstile> ⟨s0,1⟩ -*-> ⟨s1,length(compile c0)+1⟩"
          by(auto intro:app1_left app_right)
        also have "?comp \<turnstile> ⟨s1,length(compile c0)+1⟩ -1-> ⟨s1,length ?comp⟩"
          by(auto)
        finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
      next
        fix b c0 c1 s0 s1
        let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
        assume "¬b s0" and IH: "?P c1 s0 s1"
        hence "?comp \<turnstile> ⟨s0,0⟩ -1-> ⟨s0,length(compile c0) + 2⟩" by auto
        also from IH
        have "?comp \<turnstile> ⟨s0,length(compile c0)+2⟩ -*-> ⟨s1,length ?comp⟩"
          by(force intro!:app_left2 app1_left)
        finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
      next
        fix b c and s::state
        assume "¬b s"
        thus "?P (\<WHILE> b \<DO> c) s s" by force
      next
        fix b c and s0::state and s1 s2
        let ?comp = "compile(\<WHILE> b \<DO> c)"
        assume "b s0" and
          IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
        hence "?comp \<turnstile> ⟨s0,0⟩ -1-> ⟨s0,1⟩" by auto
        also from IHc
        have "?comp \<turnstile> ⟨s0,1⟩ -*-> ⟨s1,length(compile c)+1⟩"
          by(auto intro:app1_left app_right)
        also have "?comp \<turnstile> ⟨s1,length(compile c)+1⟩ -1-> ⟨s1,0⟩" by simp
        also note IHw
        finally show "?P (\<WHILE> b \<DO> c) s0 s2".
      qed
    qed

    text {*
      Second proof; statement is generalized to cater for prefixes and suffixes;
      needs none of the lifting lemmas, but instantiations of pre/suffix.
      *}
    (*
    theorem assumes A: "⟨c,s⟩ -->c t"
    shows "!!a z. a@compile c@z \<turnstile> ⟨s,size a⟩ -*-> ⟨t,size a + size(compile c)⟩"
          (is "!!a z. ?P c s t a z")
    proof -
      from A show "!!a z. ?thesis a z"
      proof induct
        case Skip thus ?case by simp
      next
        case Assign thus ?case by (force intro!: ASIN)
      next
        fix c1 c2 s s' s'' a z
        assume IH1: "!!a z. ?P c1 s s' a z" and IH2: "!!a z. ?P c2 s' s'' a z"
        from IH1 IH2[of "a@compile c1"]
        show "?P (c1;c2) s s'' a z"
          by(simp add:add_assoc[THEN sym])(blast intro:rtrancl_trans)
      next
    (* at this point I gave up converting to structured proofs *)
    (* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
       apply(intro strip)
       (* instantiate assumption sufficiently for later: *)
       apply(erule_tac x = "a@[?I]" in allE)
       apply(simp)
       (* execute JMPF: *)
       apply(rule converse_rtrancl_into_rtrancl)
        apply(force intro!: JMPFT)
       (* execute compile c0: *)
       apply(rule rtrancl_trans)
        apply(erule allE)
        apply assumption
       (* execute JMPF: *)
       apply(rule r_into_rtrancl)
       apply(force intro!: JMPFF)
    (* end of case b is true *)
      apply(intro strip)
      apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
      apply(simp add:add_assoc)
      apply(rule converse_rtrancl_into_rtrancl)
       apply(force intro!: JMPFF)
      apply(blast)
     apply(force intro: JMPFF)
    apply(intro strip)
    apply(erule_tac x = "a@[?I]" in allE)
    apply(erule_tac x = a in allE)
    apply(simp)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(force intro!: JMPFT)
    apply(rule rtrancl_trans)
     apply(erule allE)
     apply assumption
    apply(rule converse_rtrancl_into_rtrancl)
     apply(force intro!: JMPB)
    apply(simp)
    done
    *)
    text {* Missing: the other direction! I did much of it, and although
    the main lemma is very similar to the one in the new development, the
    lemmas surrounding it seemed much more complicated. In the end I gave
    up. *}

    end

### An abstract, simplistic machine

### The compiler

### Context lifting lemmas

lemma app_right_1:

      is1.0 |- ⟨s1.0,i1.0⟩ -1-> ⟨s2.0,i2.0⟩
      ==> is1.0 @ is2.0 |- ⟨s1.0,i1.0⟩ -1-> ⟨s2.0,i2.0⟩

lemma app_left_1:

      is2.0 |- ⟨s1.0,i1.0⟩ -1-> ⟨s2.0,i2.0⟩
      ==> is1.0 @ is2.0 |- ⟨s1.0,length is1.0 + i1.0⟩ -1-> ⟨s2.0,length is1.0 + i2.0⟩

lemma app_right:

      is1.0 |- ⟨s1.0,i1.0⟩ -*-> ⟨s2.0,i2.0⟩
      ==> is1.0 @ is2.0 |- ⟨s1.0,i1.0⟩ -*-> ⟨s2.0,i2.0⟩

lemma app_left:

      is2.0 |- ⟨s1.0,i1.0⟩ -*-> ⟨s2.0,i2.0⟩
      ==> is1.0 @ is2.0 |- ⟨s1.0,length is1.0 + i1.0⟩ -*-> ⟨s2.0,length is1.0 + i2.0⟩

lemma app_left2:

      [| is2.0 |- ⟨s1.0,i1.0⟩ -*-> ⟨s2.0,i2.0⟩; j1.0 = length is1.0 + i1.0;
         j2.0 = length is1.0 + i2.0 |]
      ==> is1.0 @ is2.0 |- ⟨s1.0,j1.0⟩ -*-> ⟨s2.0,j2.0⟩

lemma app1_left:

      is |- ⟨s1.0,i1.0⟩ -*-> ⟨s2.0,i2.0⟩
      ==> instr # is |- ⟨s1.0,Suc i1.0⟩ -*-> ⟨s2.0,Suc i2.0⟩

### Compiler correctness

theorem

      ⟨c,s⟩ -->c t ==> compile c |- ⟨s,0⟩ -*-> ⟨t,length (compile c)⟩