(*  Title:      HOL/IMP/Compiler.thy

     ID:         $Id$

     Author:     Tobias Nipkow, TUM

     Copyright   1996 TUM

 *)

 header "A Simple Compiler"

 theory Compiler = Natural:

 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 \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"

 syntax

   "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"

                ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)

   "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"

                ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)

 syntax (xsymbols)

   "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"

                ("_ \<turnstile> \<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)

   "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"

                ("_ \<turnstile>/ \<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)

 translations  

   "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"

   "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"

 inductive "stepa1 P"

 intros

 ASIN[simp]:

   "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s[x\<mapsto> a s],Suc n\<rangle>"

 JMPFT[simp,intro]:

   "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,Suc n\<rangle>"

 JMPFF[simp,intro]:

   "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,m\<rangle>"

 JMPB[simp]:

   "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,j\<rangle>"

 subsection "The compiler"

 consts compile :: "com \<Rightarrow> 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:

   "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow> is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"

   (is "?P \<Longrightarrow> _")

 proof -

  assume ?P

  then show ?thesis

  by induct force+

 qed

 lemma app_left_1:

   "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>

    is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"

   (is "?P \<Longrightarrow> _")

 proof -

  assume ?P

  then show ?thesis

  by induct force+

 qed

 declare rtrancl_induct2 [induct set: rtrancl]

 lemma app_right:

   "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow> is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"

   (is "?P \<Longrightarrow> _")

 proof -

  assume ?P

  then show ?thesis

  proof induct

    show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp

  next

    fix s1' i1' s2 i2

    assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"

           "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"

    thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"

      by(blast intro:app_right_1 rtrancl_trans)

  qed

 qed

 lemma app_left:

   "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>

    is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"

   (is "?P \<Longrightarrow> _")

 proof -

  assume ?P

  then show ?thesis

  proof induct

    show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp

  next

    fix s1' i1' s2 i2

    assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"

           "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"

    thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"

      by(blast intro:app_left_1 rtrancl_trans)

  qed

 qed

 lemma app_left2:

   "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>

    is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"

   by (simp add:app_left)

 lemma app1_left:

   "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>

    instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"

   by(erule app_left[of _ _ _ _ _ "[instr]",simplified])

 subsection "Compiler correctness"

 declare rtrancl_into_rtrancl[trans]

         rtrancl_into_rtrancl2[trans]

         rtrancl_trans[trans]

 text {*

   The first proof; The statement is very intuitive,

   but application of induction hypothesis requires the above lifting lemmas

 *}

 theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>"

         (is "?P \<Longrightarrow> ?Q c s t")

 proof -

   assume ?P

   then show ?thesis

   proof induct

     show "\<And>s. ?Q \<SKIP> s s" by simp

   next

     show "\<And>a s x. ?Q (x :== a) s (s[x\<mapsto> a s])" by force

   next

     fix c0 c1 s0 s1 s2

     assume "?Q c0 s0 s1"

     hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"

       by(rule app_right)

     moreover assume "?Q c1 s1 s2"

     hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>

            \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"

     proof -

       note app_left[of _ 0]

       thus

 	      "\<And>is1 is2 s1 s2 i2.

 	      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>

 	      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"

 	      by simp

     qed

     ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>

                        \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"

       by (rule rtrancl_trans)

     thus "?Q (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: "?Q c0 s0 s1"

     hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto

     also from IH

     have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"

       by(auto intro:app1_left app_right)

     also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"

       by(auto)

     finally show "?Q (\<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 "\<not>b s0" and IH: "?Q c1 s0 s1"

     hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto

     also from IH

     have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"

       by(force intro!:app_left2 app1_left)

     finally show "?Q (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .

   next

     fix b c and s::state

     assume "\<not>b s"

     thus "?Q (\<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: "?Q c s0 s1" and IHw: "?Q (\<WHILE> b \<DO> c) s1 s2"

     hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto

     also from IHc

     have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"

       by(auto intro:app1_left app_right)

     also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp

     also note IHw

     finally show "?Q (\<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 "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> 

   !a z. a@compile c@z \<turnstile> \<langle>s,length a\<rangle> -*\<rightarrow> \<langle>t,length a + length(compile c)\<rangle>";

 apply(erule evalc.induct)

       apply simp

      apply(force intro!: ASIN)

     apply(intro strip)

     apply(erule_tac x = a in allE)

     apply(erule_tac x = "a@compile c0" in allE)

     apply(erule_tac x = "compile c1@z" in allE)

     apply(erule_tac x = z in allE)

     apply(simp add:add_assoc[THEN sym])

     apply(blast intro:rtrancl_trans)

 (* \<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 rtrancl_into_rtrancl2)

     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 rtrancl_into_rtrancl2)

    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 rtrancl_into_rtrancl2)

  apply(force intro!: JMPFT)

 apply(rule rtrancl_trans)

  apply(erule allE)

  apply assumption

 apply(rule rtrancl_into_rtrancl2)

  apply(force intro!: JMPB)

 apply(simp)

 done

 text {* Missing: the other direction! *}

 end