1.1 --- a/src/HOL/IMP/Compiler.thy Thu Apr 25 17:36:29 2002 +0200
1.2 +++ b/src/HOL/IMP/Compiler.thy Fri Apr 26 11:47:01 2002 +0200
1.3 @@ -4,46 +4,7 @@
1.4 Copyright 1996 TUM
1.5 *)
1.6
1.7 -header "A Simple Compiler"
1.8 -
1.9 -theory Compiler = Natural:
1.10 -
1.11 -subsection "An abstract, simplistic machine"
1.12 -
1.13 -text {* There are only three instructions: *}
1.14 -datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
1.15 -
1.16 -text {* We describe execution of programs in the machine by
1.17 - an operational (small step) semantics:
1.18 -*}
1.19 -consts stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
1.20 -
1.21 -syntax
1.22 - "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
1.23 - ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
1.24 - "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
1.25 - ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
1.26 -
1.27 -syntax (xsymbols)
1.28 - "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
1.29 - ("_ \<turnstile> \<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
1.30 - "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
1.31 - ("_ \<turnstile>/ \<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
1.32 -
1.33 -translations
1.34 - "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
1.35 - "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
1.36 -
1.37 -inductive "stepa1 P"
1.38 -intros
1.39 -ASIN[simp]:
1.40 - "\<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>"
1.41 -JMPFT[simp,intro]:
1.42 - "\<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>"
1.43 -JMPFF[simp,intro]:
1.44 - "\<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>"
1.45 -JMPB[simp]:
1.46 - "\<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>"
1.47 +theory Compiler = Machines:
1.48
1.49 subsection "The compiler"
1.50
1.51 @@ -53,216 +14,287 @@
1.52 "compile (x:==a) = [ASIN x a]"
1.53 "compile (c1;c2) = compile c1 @ compile c2"
1.54 "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
1.55 - [JMPF b (length(compile c1) + 2)] @ compile c1 @
1.56 - [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
1.57 -"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
1.58 + [JMPF b (length(compile c1) + 1)] @ compile c1 @
1.59 + [JMPF (%x. False) (length(compile c2))] @ compile c2"
1.60 +"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
1.61 [JMPB (length(compile c)+1)]"
1.62
1.63 -declare nth_append[simp]
1.64 -
1.65 -subsection "Context lifting lemmas"
1.66 -
1.67 -text {*
1.68 - Some lemmas for lifting an execution into a prefix and suffix
1.69 - of instructions; only needed for the first proof.
1.70 -*}
1.71 -lemma app_right_1:
1.72 - "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>"
1.73 - (is "?P \<Longrightarrow> _")
1.74 -proof -
1.75 - assume ?P
1.76 - then show ?thesis
1.77 - by induct force+
1.78 -qed
1.79 -
1.80 -lemma app_left_1:
1.81 - "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
1.82 - is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
1.83 - (is "?P \<Longrightarrow> _")
1.84 -proof -
1.85 - assume ?P
1.86 - then show ?thesis
1.87 - by induct force+
1.88 -qed
1.89 -
1.90 -declare rtrancl_induct2 [induct set: rtrancl]
1.91 -
1.92 -lemma app_right:
1.93 - "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow> is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
1.94 - (is "?P \<Longrightarrow> _")
1.95 -proof -
1.96 - assume ?P
1.97 - then show ?thesis
1.98 - proof induct
1.99 - show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
1.100 - next
1.101 - fix s1' i1' s2 i2
1.102 - assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
1.103 - "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
1.104 - thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
1.105 - by(blast intro:app_right_1 rtrancl_trans)
1.106 - qed
1.107 -qed
1.108 -
1.109 -lemma app_left:
1.110 - "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
1.111 - is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
1.112 - (is "?P \<Longrightarrow> _")
1.113 -proof -
1.114 - assume ?P
1.115 - then show ?thesis
1.116 - proof induct
1.117 - show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
1.118 - next
1.119 - fix s1' i1' s2 i2
1.120 - assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
1.121 - "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
1.122 - thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
1.123 - by(blast intro:app_left_1 rtrancl_trans)
1.124 - qed
1.125 -qed
1.126 -
1.127 -lemma app_left2:
1.128 - "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
1.129 - is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
1.130 - by (simp add:app_left)
1.131 -
1.132 -lemma app1_left:
1.133 - "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
1.134 - instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
1.135 - by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
1.136 -
1.137 subsection "Compiler correctness"
1.138
1.139 -declare rtrancl_into_rtrancl[trans]
1.140 - converse_rtrancl_into_rtrancl[trans]
1.141 - rtrancl_trans[trans]
1.142 -
1.143 -text {*
1.144 - The first proof; The statement is very intuitive,
1.145 - but application of induction hypothesis requires the above lifting lemmas
1.146 -*}
1.147 -theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>"
1.148 - (is "?P \<Longrightarrow> ?Q c s t")
1.149 +theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
1.150 +shows "\<And>p q. \<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle>"
1.151 + (is "\<And>p q. ?P c s t p q")
1.152 proof -
1.153 - assume ?P
1.154 - then show ?thesis
1.155 + from A show "\<And>p q. ?thesis p q"
1.156 proof induct
1.157 - show "\<And>s. ?Q \<SKIP> s s" by simp
1.158 + case Skip thus ?case by simp
1.159 next
1.160 - show "\<And>a s x. ?Q (x :== a) s (s[x\<mapsto> a s])" by force
1.161 + case Assign thus ?case by force
1.162 next
1.163 - fix c0 c1 s0 s1 s2
1.164 - assume "?Q c0 s0 s1"
1.165 - hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
1.166 - by(rule app_right)
1.167 - moreover assume "?Q c1 s1 s2"
1.168 - hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
1.169 - \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
1.170 - proof -
1.171 - note app_left[of _ 0]
1.172 - thus
1.173 - "\<And>is1 is2 s1 s2 i2.
1.174 - is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
1.175 - is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
1.176 - by simp
1.177 - qed
1.178 - ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
1.179 - \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
1.180 - by (rule rtrancl_trans)
1.181 - thus "?Q (c0; c1) s0 s2" by simp
1.182 + case Semi thus ?case by simp (blast intro:rtrancl_trans)
1.183 next
1.184 - fix b c0 c1 s0 s1
1.185 - let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
1.186 - assume "b s0" and IH: "?Q c0 s0 s1"
1.187 - hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
1.188 - also from IH
1.189 - have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
1.190 - by(auto intro:app1_left app_right)
1.191 - also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
1.192 - by(auto)
1.193 - finally show "?Q (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
1.194 + fix b c0 c1 s0 s1 p q
1.195 + assume IH: "\<And>p q. ?P c0 s0 s1 p q"
1.196 + assume "b s0"
1.197 + thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
1.198 + by(simp add: IH[THEN rtrancl_trans])
1.199 next
1.200 - fix b c0 c1 s0 s1
1.201 - let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
1.202 - assume "\<not>b s0" and IH: "?Q c1 s0 s1"
1.203 - hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
1.204 - also from IH
1.205 - have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
1.206 - by(force intro!:app_left2 app1_left)
1.207 - finally show "?Q (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
1.208 + case IfFalse thus ?case by(simp)
1.209 next
1.210 - fix b c and s::state
1.211 - assume "\<not>b s"
1.212 - thus "?Q (\<WHILE> b \<DO> c) s s" by force
1.213 + case WhileFalse thus ?case by simp
1.214 next
1.215 - fix b c and s0::state and s1 s2
1.216 - let ?comp = "compile(\<WHILE> b \<DO> c)"
1.217 - assume "b s0" and
1.218 - IHc: "?Q c s0 s1" and IHw: "?Q (\<WHILE> b \<DO> c) s1 s2"
1.219 - hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
1.220 - also from IHc
1.221 - have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
1.222 - by(auto intro:app1_left app_right)
1.223 - also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
1.224 - also note IHw
1.225 - finally show "?Q (\<WHILE> b \<DO> c) s0 s2".
1.226 + fix b c and s0::state and s1 s2 p q
1.227 + assume b: "b s0" and
1.228 + IHc: "\<And>p q. ?P c s0 s1 p q" and
1.229 + IHw: "\<And>p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
1.230 + show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
1.231 + using b IHc[THEN rtrancl_trans] IHw by(simp)
1.232 qed
1.233 qed
1.234
1.235 -text {*
1.236 - Second proof; statement is generalized to cater for prefixes and suffixes;
1.237 - needs none of the lifting lemmas, but instantiations of pre/suffix.
1.238 - *}
1.239 -theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow>
1.240 - !a z. a@compile c@z \<turnstile> \<langle>s,length a\<rangle> -*\<rightarrow> \<langle>t,length a + length(compile c)\<rangle>";
1.241 -apply(erule evalc.induct)
1.242 - apply simp
1.243 - apply(force intro!: ASIN)
1.244 - apply(intro strip)
1.245 - apply(erule_tac x = a in allE)
1.246 - apply(erule_tac x = "a@compile c0" in allE)
1.247 - apply(erule_tac x = "compile c1@z" in allE)
1.248 - apply(erule_tac x = z in allE)
1.249 - apply(simp add:add_assoc[THEN sym])
1.250 - apply(blast intro:rtrancl_trans)
1.251 -(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
1.252 - apply(intro strip)
1.253 - (* instantiate assumption sufficiently for later: *)
1.254 - apply(erule_tac x = "a@[?I]" in allE)
1.255 - apply(simp)
1.256 - (* execute JMPF: *)
1.257 - apply(rule converse_rtrancl_into_rtrancl)
1.258 - apply(force intro!: JMPFT)
1.259 - (* execute compile c0: *)
1.260 - apply(rule rtrancl_trans)
1.261 - apply(erule allE)
1.262 - apply assumption
1.263 - (* execute JMPF: *)
1.264 - apply(rule r_into_rtrancl)
1.265 - apply(force intro!: JMPFF)
1.266 -(* end of case b is true *)
1.267 - apply(intro strip)
1.268 - apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
1.269 - apply(simp add:add_assoc)
1.270 - apply(rule converse_rtrancl_into_rtrancl)
1.271 - apply(force intro!: JMPFF)
1.272 - apply(blast)
1.273 - apply(force intro: JMPFF)
1.274 -apply(intro strip)
1.275 -apply(erule_tac x = "a@[?I]" in allE)
1.276 -apply(erule_tac x = a in allE)
1.277 -apply(simp)
1.278 -apply(rule converse_rtrancl_into_rtrancl)
1.279 - apply(force intro!: JMPFT)
1.280 -apply(rule rtrancl_trans)
1.281 - apply(erule allE)
1.282 - apply assumption
1.283 -apply(rule converse_rtrancl_into_rtrancl)
1.284 - apply(force intro!: JMPB)
1.285 -apply(simp)
1.286 +text {* The other direction! *}
1.287 +
1.288 +inductive_cases [elim!]: "(([],p,s),next) : stepa1"
1.289 +
1.290 +lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
1.291 +apply(rule iffI)
1.292 + apply(erule converse_rel_powE, simp, fast)
1.293 +apply simp
1.294 done
1.295
1.296 -text {* Missing: the other direction! *}
1.297 +lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
1.298 +by(simp add: rtrancl_is_UN_rel_pow)
1.299
1.300 -end
1.301 +constdefs
1.302 + forws :: "instr \<Rightarrow> nat set"
1.303 +"forws instr == case instr of
1.304 + ASIN x a \<Rightarrow> {0} |
1.305 + JMPF b n \<Rightarrow> {0,n} |
1.306 + JMPB n \<Rightarrow> {}"
1.307 + backws :: "instr \<Rightarrow> nat set"
1.308 +"backws instr == case instr of
1.309 + ASIN x a \<Rightarrow> {} |
1.310 + JMPF b n \<Rightarrow> {} |
1.311 + JMPB n \<Rightarrow> {n}"
1.312 +
1.313 +consts closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
1.314 +primrec
1.315 +"closed m n [] = True"
1.316 +"closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
1.317 + (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
1.318 +
1.319 +lemma [simp]:
1.320 + "\<And>m n. closed m n (C1@C2) =
1.321 + (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
1.322 +by(induct C1, simp, simp add:plus_ac0)
1.323 +
1.324 +theorem [simp]: "\<And>m n. closed m n (compile c)"
1.325 +by(induct c, simp_all add:backws_def forws_def)
1.326 +
1.327 +lemma drop_lem: "n \<le> size(p1@p2)
1.328 + \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
1.329 + (n \<le> size p1 & p1' = drop n p1)"
1.330 +apply(rule iffI)
1.331 + defer apply simp
1.332 +apply(subgoal_tac "n \<le> size p1")
1.333 + apply(rotate_tac -1)
1.334 + apply simp
1.335 +apply(rule ccontr)
1.336 +apply(rotate_tac -1)
1.337 +apply(drule_tac f = length in arg_cong)
1.338 +apply simp
1.339 +apply arith
1.340 +done
1.341 +
1.342 +lemma reduce_exec1:
1.343 + "\<langle>i # p1 @ p2,q1 @ q2,s\<rangle> -1\<rightarrow> \<langle>p1' @ p2,q1' @ q2,s'\<rangle> \<Longrightarrow>
1.344 + \<langle>i # p1,q1,s\<rangle> -1\<rightarrow> \<langle>p1',q1',s'\<rangle>"
1.345 +by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm)
1.346 +
1.347 +
1.348 +lemma closed_exec1:
1.349 + "\<lbrakk> closed 0 0 (rev q1 @ instr # p1);
1.350 + \<langle>instr # p1 @ p2, q1 @ q2,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle> \<rbrakk> \<Longrightarrow>
1.351 + \<exists>p1' q1'. p' = p1'@p2 \<and> q' = q1'@q2 \<and> rev q1' @ p1' = rev q1 @ instr # p1"
1.352 +apply(clarsimp simp add:forws_def backws_def
1.353 + split:instr.split_asm split_if_asm)
1.354 +done
1.355 +
1.356 +theorem closed_execn_decomp: "\<And>C1 C2 r.
1.357 + \<lbrakk> closed 0 0 (rev C1 @ C2);
1.358 + \<langle>C2 @ p1 @ p2, C1 @ q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<rbrakk>
1.359 + \<Longrightarrow> \<exists>s n1 n2. \<langle>C2,C1,r\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle> \<and>
1.360 + \<langle>p1@p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
1.361 + n = n1+n2"
1.362 +(is "\<And>C1 C2 r. \<lbrakk>?CL C1 C2; ?H C1 C2 r n\<rbrakk> \<Longrightarrow> ?P C1 C2 r n")
1.363 +proof(induct n)
1.364 + fix C1 C2 r
1.365 + assume "?H C1 C2 r 0"
1.366 + thus "?P C1 C2 r 0" by simp
1.367 +next
1.368 + fix C1 C2 r n
1.369 + assume IH: "\<And>C1 C2 r. ?CL C1 C2 \<Longrightarrow> ?H C1 C2 r n \<Longrightarrow> ?P C1 C2 r n"
1.370 + assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
1.371 + show "?P C1 C2 r (Suc n)"
1.372 + proof (cases C2)
1.373 + assume "C2 = []" with H show ?thesis by simp
1.374 + next
1.375 + fix instr tlC2
1.376 + assume C2: "C2 = instr # tlC2"
1.377 + from H C2 obtain p' q' r'
1.378 + where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
1.379 + and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
1.380 + by(fastsimp simp add:R_O_Rn_commute)
1.381 + from CL closed_exec1[OF _ 1] C2
1.382 + obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
1.383 + and same: "rev C1' @ C2' = rev C1 @ C2"
1.384 + by fastsimp
1.385 + have rev_same: "rev C2' @ C1' = rev C2 @ C1"
1.386 + proof -
1.387 + have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
1.388 + also have "\<dots> = rev(rev C1 @ C2)" by(simp only:same)
1.389 + also have "\<dots> = rev C2 @ C1" by simp
1.390 + finally show ?thesis .
1.391 + qed
1.392 + hence rev_same': "\<And>p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
1.393 + from n have n': "\<langle>C2' @ p1 @ p2,C1' @ q,r'\<rangle> -n\<rightarrow>
1.394 + \<langle>p2,rev p1 @ rev C2' @ C1' @ q,t\<rangle>"
1.395 + by(simp add:pq' rev_same')
1.396 + from IH[OF _ n'] CL
1.397 + obtain s n1 n2 where n1: "\<langle>C2',C1',r'\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>" and
1.398 + "\<langle>p1 @ p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
1.399 + n = n1 + n2"
1.400 + by(fastsimp simp add: same rev_same rev_same')
1.401 + moreover
1.402 + from 1 n1 pq' C2 have "\<langle>C2,C1,r\<rangle> -Suc n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>"
1.403 + by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
1.404 + ultimately show ?thesis by (fastsimp simp del:relpow.simps)
1.405 + qed
1.406 +qed
1.407 +
1.408 +lemma execn_decomp:
1.409 +"\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
1.410 + \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
1.411 + \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
1.412 + n = n1+n2"
1.413 +using closed_execn_decomp[of "[]",simplified] by simp
1.414 +
1.415 +lemma exec_star_decomp:
1.416 +"\<langle>compile c @ p1 @ p2,q,r\<rangle> -*\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
1.417 + \<Longrightarrow> \<exists>s. \<langle>compile c,[],r\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
1.418 + \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -*\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle>"
1.419 +by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)
1.420 +
1.421 +
1.422 +(* Alternative:
1.423 +lemma exec_comp_n:
1.424 +"\<And>p1 p2 q r t n.
1.425 + \<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
1.426 + \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
1.427 + \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
1.428 + n = n1+n2"
1.429 + (is "\<And>p1 p2 q r t n. ?H c p1 p2 q r t n \<Longrightarrow> ?P c p1 p2 q r t n")
1.430 +proof (induct c)
1.431 +*)
1.432 +
1.433 +text{*Warning:
1.434 +@{prop"\<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"}
1.435 +is not true! *}
1.436 +
1.437 +theorem "\<And>s t.
1.438 + \<langle>compile c,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
1.439 +proof (induct c)
1.440 + fix s t
1.441 + assume "\<langle>compile SKIP,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile SKIP),t\<rangle>"
1.442 + thus "\<langle>SKIP,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
1.443 +next
1.444 + fix s t v f
1.445 + assume "\<langle>compile(v :== f),[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile(v :== f)),t\<rangle>"
1.446 + thus "\<langle>v :== f,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
1.447 +next
1.448 + fix s1 s3 c1 c2
1.449 + let ?C1 = "compile c1" let ?C2 = "compile c2"
1.450 + assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
1.451 + and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
1.452 + assume "\<langle>compile(c1;c2),[],s1\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
1.453 + then obtain s2 where exec1: "\<langle>?C1,[],s1\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,s2\<rangle>" and
1.454 + exec2: "\<langle>?C2,rev ?C1,s2\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
1.455 + by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
1.456 + from exec2 have exec2': "\<langle>?C2,[],s2\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,s3\<rangle>"
1.457 + using exec_star_decomp[of _ "[]" "[]"] by fastsimp
1.458 + have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>c s2" using IH1 exec1 by simp
1.459 + moreover have "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>c s3" using IH2 exec2' by fastsimp
1.460 + ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>c s3" ..
1.461 +next
1.462 + fix s t b c1 c2
1.463 + let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
1.464 + let ?C1 = "compile c1" let ?C2 = "compile c2"
1.465 + assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
1.466 + and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
1.467 + and H: "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle>"
1.468 + show "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>c t"
1.469 + proof cases
1.470 + assume b: "b s"
1.471 + with H have "\<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle>"
1.472 + by (fastsimp dest:exec_star_decomp
1.473 + [of _ "[JMPF (\<lambda>x. False) (size ?C2)]@?C2" "[]",simplified])
1.474 + hence "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH1)
1.475 + with b show ?thesis ..
1.476 + next
1.477 + assume b: "\<not> b s"
1.478 + with H have "\<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle>"
1.479 + using exec_star_decomp[of _ "[]" "[]"] by simp
1.480 + hence "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH2)
1.481 + with b show ?thesis ..
1.482 + qed
1.483 +next
1.484 + fix b c s t
1.485 + let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
1.486 + let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
1.487 + assume IHc: "\<And>s t. \<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
1.488 + and H: "\<langle>?W,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
1.489 + from H obtain k where ob:"\<langle>?W,[],s\<rangle> -k\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
1.490 + by(simp add:rtrancl_is_UN_rel_pow) blast
1.491 + { fix n have "\<And>s. \<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle> \<Longrightarrow> \<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
1.492 + proof (induct n rule: less_induct)
1.493 + fix n
1.494 + assume IHm: "\<And>m s. \<lbrakk>m < n; \<langle>?W,[],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle> \<rbrakk> \<Longrightarrow> \<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
1.495 + fix s
1.496 + assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
1.497 + show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
1.498 + proof cases
1.499 + assume b: "b s"
1.500 + then obtain m where m: "n = Suc m"
1.501 + and 1: "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
1.502 + using H by fastsimp
1.503 + then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
1.504 + and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
1.505 + and n12: "m = n1+n2"
1.506 + using execn_decomp[of _ "[?j2]"]
1.507 + by(simp del: execn_simp) fast
1.508 + have n2n: "n2 - 1 < n" using m n12 by arith
1.509 + note b
1.510 + moreover
1.511 + { from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
1.512 + by (simp add:rtrancl_is_UN_rel_pow) fast
1.513 + hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
1.514 + }
1.515 + moreover
1.516 + { have "n2 - 1 < n" using m n12 by arith
1.517 + moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
1.518 + ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
1.519 + }
1.520 + ultimately show ?thesis ..
1.521 + next
1.522 + assume b: "\<not> b s"
1.523 + hence "t = s" using H by simp
1.524 + with b show ?thesis by simp
1.525 + qed
1.526 + qed
1.527 + }
1.528 + with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
1.529 +qed
1.530 +
1.531 +(* To Do: connect with Machine 0 using M_equiv *)
1.532 +
1.533 +end
1.534 \ No newline at end of file