(*  Title:      HOL/IMP/Compiler.thy

    ID:         $Id$

    Author:     Tobias Nipkow, TUM

    Copyright   1996 TUM

A simple compiler for a simplistic machine.

*)

theory Compiler = Natural:

datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat

consts  stepa1 :: "instr list => ((state*nat) * (state*nat))set"

syntax

        "@stepa1" :: "[instr list,state,nat,state,nat] => bool"

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

        "@stepa" :: "[instr list,state,nat,state,nat] => bool"

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

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

              "P \<turnstile> <s,m> -*\<rightarrow> <t,n>" == "((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> <s,n> -1\<rightarrow> <s[x::= a s],Suc n>"

JMPFT[simp,intro]:

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

JMPFF[simp,intro]:

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

JMPB[simp]:

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

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];

(* Lemmas for lifting an execution into a prefix and suffix

   of instructions; only needed for the first proof *)

lemma app_right_1:

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

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

proof -

 assume ?P

 then show ?thesis

 by induct force+

qed

lemma app_left_1:

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

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

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

proof -

 assume ?P

 then show ?thesis

 by induct force+

qed

declare rtrancl_induct2 [induct set: rtrancl]

lemma app_right:

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

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

proof -

 assume ?P

 then show ?thesis

 proof induct

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

 next

   fix s1' i1' s2 i2

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

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

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

     by(blast intro:app_right_1 rtrancl_trans)

 qed

qed

lemma app_left:

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

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

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

proof -

 assume ?P

 then show ?thesis

 proof induct

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

 next

   fix s1' i1' s2 i2

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

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

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

     by(blast intro:app_left_1 rtrancl_trans)

 qed

qed

lemma app_left2:

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

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

by (simp add:app_left)

lemma app1_left:

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

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

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

declare rtrancl_into_rtrancl[trans]

        rtrancl_into_rtrancl2[trans]

        rtrancl_trans[trans]

(* The first proof; statement very intuitive,

   but application of induction hypothesis requires the above lifting lemmas

*)

theorem "<c,s> -c-> t \<Longrightarrow> compile c \<turnstile> <s,0> -*\<rightarrow> <t,length(compile c)>"

        (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::= a s])" by force

  next

    fix c0 c1 s0 s1 s2

    assume "?Q c0 s0 s1"

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

      by(rule app_right)

    moreover assume "?Q c1 s1 s2"

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

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

    proof -

      note app_left[of _ 0]

      thus

	"\<And>is1 is2 s1 s2 i2.

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

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

	by simp

    qed

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

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

      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> <s0,0> -1\<rightarrow> <s0,1>" by auto

    also from IH

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

      by(auto intro:app1_left app_right)

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

      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> <s0,0> -1\<rightarrow> <s0,length(compile c0) + 2>" by auto

    also from IH

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

      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> <s0,0> -1\<rightarrow> <s0,1>" by auto

    also from IHc

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

      by(auto intro:app1_left app_right)

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

    also note IHw

    finally show "?Q (WHILE b DO c) s0 s2".

  qed

qed

(* Second proof; statement is generalized to cater for prefixes and suffixes;

   needs none of the lifting lemmas, but instantiations of pre/suffix.

*)

theorem "<c,s> -c-> t ==> 

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

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

(* Missing: the other direction! *)

end