(* 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
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〉
theorem
〈c,s〉 -->c t ==> compile c |- 〈s,0〉 -*-> 〈t,length (compile c)〉