1.1 --- a/src/HOL/IMP/Compiler.thy Wed Jun 01 15:53:47 2011 +0200
1.2 +++ b/src/HOL/IMP/Compiler.thy Wed Jun 01 21:35:34 2011 +0200
1.3 @@ -1,298 +1,237 @@
1.4 -(* Title: HOL/IMP/Compiler.thy
1.5 - Author: Tobias Nipkow, TUM
1.6 - Copyright 1996 TUM
1.7 -*)
1.8 +(* Author: Tobias Nipkow *)
1.9
1.10 -theory Compiler imports Machines begin
1.11 +header "A Compiler for IMP"
1.12
1.13 -subsection "The compiler"
1.14 +theory Compiler imports Big_Step
1.15 +begin
1.16
1.17 -primrec compile :: "com \<Rightarrow> instr list"
1.18 +subsection "Instructions and Stack Machine"
1.19 +
1.20 +datatype instr =
1.21 + LOADI int | LOAD string | ADD |
1.22 + STORE string |
1.23 + JMPF nat |
1.24 + JMPB nat |
1.25 + JMPFLESS nat |
1.26 + JMPFGE nat
1.27 +
1.28 +type_synonym stack = "int list"
1.29 +type_synonym config = "nat\<times>state\<times>stack"
1.30 +
1.31 +abbreviation "hd2 xs == hd(tl xs)"
1.32 +abbreviation "tl2 xs == tl(tl xs)"
1.33 +
1.34 +inductive exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
1.35 + ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50)
1.36 + for P :: "instr list"
1.37 where
1.38 - "compile \<SKIP> = []"
1.39 -| "compile (x:==a) = [SET x a]"
1.40 -| "compile (c1;c2) = compile c1 @ compile c2"
1.41 -| "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
1.42 - [JMPF b (length(compile c1) + 1)] @ compile c1 @
1.43 - [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
1.44 -| "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
1.45 - [JMPB (length(compile c)+1)]"
1.46 +"\<lbrakk> i < size P; P!i = LOADI n \<rbrakk> \<Longrightarrow>
1.47 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
1.48 +"\<lbrakk> i < size P; P!i = LOAD x \<rbrakk> \<Longrightarrow>
1.49 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
1.50 +"\<lbrakk> i < size P; P!i = ADD \<rbrakk> \<Longrightarrow>
1.51 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
1.52 +"\<lbrakk> i < size P; P!i = STORE n \<rbrakk> \<Longrightarrow>
1.53 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
1.54 +"\<lbrakk> i < size P; P!i = JMPF n \<rbrakk> \<Longrightarrow>
1.55 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
1.56 +"\<lbrakk> i < size P; P!i = JMPB n; n \<le> i+1 \<rbrakk> \<Longrightarrow>
1.57 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1-n,s,stk)" |
1.58 +"\<lbrakk> i < size P; P!i = JMPFLESS n \<rbrakk> \<Longrightarrow>
1.59 + P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
1.60 +"\<lbrakk> i < size P; P!i = JMPFGE n \<rbrakk> \<Longrightarrow>
1.61 + P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
1.62
1.63 -subsection "Compiler correctness"
1.64 +code_pred exec1 .
1.65
1.66 -theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
1.67 -shows "\<And>p q. \<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle>"
1.68 - (is "\<And>p q. ?P c s t p q")
1.69 -proof -
1.70 - from A show "\<And>p q. ?thesis p q"
1.71 - proof induct
1.72 - case Skip thus ?case by simp
1.73 - next
1.74 - case Assign thus ?case by force
1.75 - next
1.76 - case Semi thus ?case by simp (blast intro:rtrancl_trans)
1.77 - next
1.78 - fix b c0 c1 s0 s1 p q
1.79 - assume IH: "\<And>p q. ?P c0 s0 s1 p q"
1.80 - assume "b s0"
1.81 - thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
1.82 - by(simp add: IH[THEN rtrancl_trans])
1.83 - next
1.84 - case IfFalse thus ?case by(simp)
1.85 - next
1.86 - case WhileFalse thus ?case by simp
1.87 - next
1.88 - fix b c and s0::state and s1 s2 p q
1.89 - assume b: "b s0" and
1.90 - IHc: "\<And>p q. ?P c s0 s1 p q" and
1.91 - IHw: "\<And>p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
1.92 - show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
1.93 - using b IHc[THEN rtrancl_trans] IHw by(simp)
1.94 - qed
1.95 +declare exec1.intros[intro]
1.96 +
1.97 +inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
1.98 +where
1.99 +refl: "P \<turnstile> c \<rightarrow>* c" |
1.100 +step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
1.101 +
1.102 +declare exec.intros[intro]
1.103 +
1.104 +lemmas exec_induct = exec.induct[split_format(complete)]
1.105 +
1.106 +code_pred exec .
1.107 +
1.108 +values
1.109 + "{(i,map t [''x'',''y''],stk) | i t stk.
1.110 + [LOAD ''y'', STORE ''x''] \<turnstile>
1.111 + (0,lookup[(''x'',3),(''y'',4)],[]) \<rightarrow>* (i,t,stk)}"
1.112 +
1.113 +
1.114 +subsection{* Verification infrastructure *}
1.115 +
1.116 +lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
1.117 +apply(induct rule: exec.induct)
1.118 + apply blast
1.119 +by (metis exec.step)
1.120 +
1.121 +lemma exec1_subst: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> c' = c'' \<Longrightarrow> P \<turnstile> c \<rightarrow> c''"
1.122 +by auto
1.123 +
1.124 +lemmas exec1_simps = exec1.intros[THEN exec1_subst]
1.125 +
1.126 +text{* Below we need to argue about the execution of code that is embedded in
1.127 +larger programs. For this purpose we show that execution is preserved by
1.128 +appending code to the left or right of a program. *}
1.129 +
1.130 +lemma exec1_appendR: assumes "P \<turnstile> c \<rightarrow> c'" shows "P@P' \<turnstile> c \<rightarrow> c'"
1.131 +proof-
1.132 + from assms show ?thesis
1.133 + by cases (simp_all add: exec1_simps nth_append)
1.134 + -- "All cases proved with the final simp-all"
1.135 qed
1.136
1.137 -text {* The other direction! *}
1.138 +lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
1.139 +apply(induct rule: exec.induct)
1.140 + apply blast
1.141 +by (metis exec1_appendR exec.step)
1.142
1.143 -inductive_cases [elim!]: "(([],p,s),(is',p',s')) : stepa1"
1.144 +lemma exec1_appendL:
1.145 +assumes "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk')"
1.146 +shows "P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
1.147 +proof-
1.148 + from assms show ?thesis
1.149 + by cases (simp_all add: exec1_simps)
1.150 +qed
1.151
1.152 -lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
1.153 -apply(rule iffI)
1.154 - apply(erule rel_pow_E2, simp, fast)
1.155 +lemma exec_appendL:
1.156 + "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
1.157 + P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
1.158 +apply(induct rule: exec_induct)
1.159 + apply blast
1.160 +by (blast intro: exec1_appendL exec.step)
1.161 +
1.162 +text{* Now we specialise the above lemmas to enable automatic proofs of
1.163 +@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
1.164 +pieces of code that we already know how they execute (by induction), combined
1.165 +by @{text "@"} and @{text "#"}. Backward jumps are not supported.
1.166 +The details should be skipped on a first reading.
1.167 +
1.168 +If the pc points beyond the first instruction or part of the program, drop it: *}
1.169 +
1.170 +lemma exec_Cons_Suc[intro]:
1.171 + "P \<turnstile> (i,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
1.172 + instr#P \<turnstile> (Suc i,s,stk) \<rightarrow>* (Suc j,t,stk')"
1.173 +apply(drule exec_appendL[where P'="[instr]"])
1.174 apply simp
1.175 done
1.176
1.177 -lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
1.178 -by(simp add: rtrancl_is_UN_rel_pow)
1.179 -
1.180 -definition
1.181 - forws :: "instr \<Rightarrow> nat set" where
1.182 - "forws instr = (case instr of
1.183 - SET x a \<Rightarrow> {0} |
1.184 - JMPF b n \<Rightarrow> {0,n} |
1.185 - JMPB n \<Rightarrow> {})"
1.186 -
1.187 -definition
1.188 - backws :: "instr \<Rightarrow> nat set" where
1.189 - "backws instr = (case instr of
1.190 - SET x a \<Rightarrow> {} |
1.191 - JMPF b n \<Rightarrow> {} |
1.192 - JMPB n \<Rightarrow> {n})"
1.193 -
1.194 -primrec closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
1.195 -where
1.196 - "closed m n [] = True"
1.197 -| "closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
1.198 - (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
1.199 -
1.200 -lemma [simp]:
1.201 - "\<And>m n. closed m n (C1@C2) =
1.202 - (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
1.203 -by(induct C1) (simp, simp add:add_ac)
1.204 -
1.205 -theorem [simp]: "\<And>m n. closed m n (compile c)"
1.206 -by(induct c) (simp_all add:backws_def forws_def)
1.207 -
1.208 -lemma drop_lem: "n \<le> size(p1@p2)
1.209 - \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
1.210 - (n \<le> size p1 & p1' = drop n p1)"
1.211 -apply(rule iffI)
1.212 - defer apply simp
1.213 -apply(subgoal_tac "n \<le> size p1")
1.214 - apply simp
1.215 -apply(rule ccontr)
1.216 -apply(drule_tac f = length in arg_cong)
1.217 +lemma exec_appendL_if[intro]:
1.218 + "size P' <= i
1.219 + \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (i',s',stk')
1.220 + \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (size P' + i',s',stk')"
1.221 +apply(drule exec_appendL[where P'=P'])
1.222 apply simp
1.223 done
1.224
1.225 -lemma reduce_exec1:
1.226 - "\<langle>i # p1 @ p2,q1 @ q2,s\<rangle> -1\<rightarrow> \<langle>p1' @ p2,q1' @ q2,s'\<rangle> \<Longrightarrow>
1.227 - \<langle>i # p1,q1,s\<rangle> -1\<rightarrow> \<langle>p1',q1',s'\<rangle>"
1.228 -by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm)
1.229 +text{* Split the execution of a compound program up into the excution of its
1.230 +parts: *}
1.231
1.232 +lemma exec_append_trans[intro]:
1.233 +"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
1.234 + size P \<le> i' \<Longrightarrow>
1.235 + P' \<turnstile> (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
1.236 + j'' = size P + i''
1.237 + \<Longrightarrow>
1.238 + P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
1.239 +by(metis exec_trans[OF exec_appendR exec_appendL_if])
1.240
1.241 -lemma closed_exec1:
1.242 - "\<lbrakk> closed 0 0 (rev q1 @ instr # p1);
1.243 - \<langle>instr # p1 @ p2, q1 @ q2,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle> \<rbrakk> \<Longrightarrow>
1.244 - \<exists>p1' q1'. p' = p1'@p2 \<and> q' = q1'@q2 \<and> rev q1' @ p1' = rev q1 @ instr # p1"
1.245 -apply(clarsimp simp add:forws_def backws_def
1.246 - split:instr.split_asm split_if_asm)
1.247 +
1.248 +declare Let_def[simp] eval_nat_numeral[simp]
1.249 +
1.250 +
1.251 +subsection "Compilation"
1.252 +
1.253 +fun acomp :: "aexp \<Rightarrow> instr list" where
1.254 +"acomp (N n) = [LOADI n]" |
1.255 +"acomp (V x) = [LOAD x]" |
1.256 +"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
1.257 +
1.258 +lemma acomp_correct[intro]:
1.259 + "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
1.260 +apply(induct a arbitrary: stk)
1.261 +apply(fastsimp)+
1.262 done
1.263
1.264 -theorem closed_execn_decomp: "\<And>C1 C2 r.
1.265 - \<lbrakk> closed 0 0 (rev C1 @ C2);
1.266 - \<langle>C2 @ p1 @ p2, C1 @ q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<rbrakk>
1.267 - \<Longrightarrow> \<exists>s n1 n2. \<langle>C2,C1,r\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle> \<and>
1.268 - \<langle>p1@p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
1.269 - n = n1+n2"
1.270 -(is "\<And>C1 C2 r. \<lbrakk>?CL C1 C2; ?H C1 C2 r n\<rbrakk> \<Longrightarrow> ?P C1 C2 r n")
1.271 -proof(induct n)
1.272 - fix C1 C2 r
1.273 - assume "?H C1 C2 r 0"
1.274 - thus "?P C1 C2 r 0" by simp
1.275 +fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> instr list" where
1.276 +"bcomp (B bv) c n = (if bv=c then [JMPF n] else [])" |
1.277 +"bcomp (Not b) c n = bcomp b (\<not>c) n" |
1.278 +"bcomp (And b1 b2) c n =
1.279 + (let cb2 = bcomp b2 c n;
1.280 + m = (if c then size cb2 else size cb2+n);
1.281 + cb1 = bcomp b1 False m
1.282 + in cb1 @ cb2)" |
1.283 +"bcomp (Less a1 a2) c n =
1.284 + acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
1.285 +
1.286 +value
1.287 + "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
1.288 + False 3"
1.289 +
1.290 +lemma bcomp_correct[intro]:
1.291 + "bcomp b c n \<turnstile>
1.292 + (0,s,stk) \<rightarrow>* (size(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
1.293 +proof(induct b arbitrary: c n m)
1.294 + case Not
1.295 + from Not[of "~c"] show ?case by fastsimp
1.296 next
1.297 - fix C1 C2 r n
1.298 - assume IH: "\<And>C1 C2 r. ?CL C1 C2 \<Longrightarrow> ?H C1 C2 r n \<Longrightarrow> ?P C1 C2 r n"
1.299 - assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
1.300 - show "?P C1 C2 r (Suc n)"
1.301 - proof (cases C2)
1.302 - assume "C2 = []" with H show ?thesis by simp
1.303 - next
1.304 - fix instr tlC2
1.305 - assume C2: "C2 = instr # tlC2"
1.306 - from H C2 obtain p' q' r'
1.307 - where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
1.308 - and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
1.309 - by(fastsimp simp add:rel_pow_commute)
1.310 - from CL closed_exec1[OF _ 1] C2
1.311 - obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
1.312 - and same: "rev C1' @ C2' = rev C1 @ C2"
1.313 - by fastsimp
1.314 - have rev_same: "rev C2' @ C1' = rev C2 @ C1"
1.315 - proof -
1.316 - have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
1.317 - also have "\<dots> = rev(rev C1 @ C2)" by(simp only:same)
1.318 - also have "\<dots> = rev C2 @ C1" by simp
1.319 - finally show ?thesis .
1.320 - qed
1.321 - hence rev_same': "\<And>p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
1.322 - from n have n': "\<langle>C2' @ p1 @ p2,C1' @ q,r'\<rangle> -n\<rightarrow>
1.323 - \<langle>p2,rev p1 @ rev C2' @ C1' @ q,t\<rangle>"
1.324 - by(simp add:pq' rev_same')
1.325 - from IH[OF _ n'] CL
1.326 - obtain s n1 n2 where n1: "\<langle>C2',C1',r'\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>" and
1.327 - "\<langle>p1 @ p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
1.328 - n = n1 + n2"
1.329 - by(fastsimp simp add: same rev_same rev_same')
1.330 - moreover
1.331 - from 1 n1 pq' C2 have "\<langle>C2,C1,r\<rangle> -Suc n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>"
1.332 - by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
1.333 - ultimately show ?thesis by (fastsimp simp del:relpow.simps)
1.334 - qed
1.335 -qed
1.336 + case (And b1 b2)
1.337 + from And(1)[of "False"] And(2)[of "c"] show ?case by fastsimp
1.338 +qed fastsimp+
1.339
1.340 -lemma execn_decomp:
1.341 -"\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
1.342 - \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
1.343 - \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
1.344 - n = n1+n2"
1.345 -using closed_execn_decomp[of "[]",simplified] by simp
1.346
1.347 -lemma exec_star_decomp:
1.348 -"\<langle>compile c @ p1 @ p2,q,r\<rangle> -*\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
1.349 - \<Longrightarrow> \<exists>s. \<langle>compile c,[],r\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
1.350 - \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -*\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle>"
1.351 -by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)
1.352 +fun ccomp :: "com \<Rightarrow> instr list" where
1.353 +"ccomp SKIP = []" |
1.354 +"ccomp (x ::= a) = acomp a @ [STORE x]" |
1.355 +"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
1.356 +"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
1.357 + (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1)
1.358 + in cb @ cc\<^isub>1 @ JMPF(size cc\<^isub>2) # cc\<^isub>2)" |
1.359 +"ccomp (WHILE b DO c) =
1.360 + (let cc = ccomp c; cb = bcomp b False (size cc + 1)
1.361 + in cb @ cc @ [JMPB (size cb + size cc + 1)])"
1.362
1.363 +value "ccomp
1.364 + (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
1.365 + ELSE ''v'' ::= V ''u'')"
1.366
1.367 -(* Alternative:
1.368 -lemma exec_comp_n:
1.369 -"\<And>p1 p2 q r t n.
1.370 - \<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
1.371 - \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
1.372 - \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
1.373 - n = n1+n2"
1.374 - (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.375 -proof (induct c)
1.376 -*)
1.377 +value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
1.378
1.379 -text{*Warning:
1.380 -@{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.381 -is not true! *}
1.382
1.383 -theorem "\<And>s t.
1.384 - \<langle>compile c,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
1.385 -proof (induct c)
1.386 - fix s t
1.387 - assume "\<langle>compile SKIP,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile SKIP),t\<rangle>"
1.388 - thus "\<langle>SKIP,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
1.389 +subsection "Preservation of sematics"
1.390 +
1.391 +lemma ccomp_correct:
1.392 + "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
1.393 +proof(induct arbitrary: stk rule: big_step_induct)
1.394 + case (Assign x a s)
1.395 + show ?case by (fastsimp simp:fun_upd_def)
1.396 next
1.397 - fix s t v f
1.398 - assume "\<langle>compile(v :== f),[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile(v :== f)),t\<rangle>"
1.399 - thus "\<langle>v :== f,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
1.400 + case (Semi c1 s1 s2 c2 s3)
1.401 + let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
1.402 + have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
1.403 + using Semi.hyps(2) by (fastsimp)
1.404 + moreover
1.405 + have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
1.406 + using Semi.hyps(4) by (fastsimp)
1.407 + ultimately show ?case by simp (blast intro: exec_trans)
1.408 next
1.409 - fix s1 s3 c1 c2
1.410 - let ?C1 = "compile c1" let ?C2 = "compile c2"
1.411 - 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.412 - 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.413 - assume "\<langle>compile(c1;c2),[],s1\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
1.414 - then obtain s2 where exec1: "\<langle>?C1,[],s1\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,s2\<rangle>" and
1.415 - exec2: "\<langle>?C2,rev ?C1,s2\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
1.416 - by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
1.417 - from exec2 have exec2': "\<langle>?C2,[],s2\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,s3\<rangle>"
1.418 - using exec_star_decomp[of _ "[]" "[]"] by fastsimp
1.419 - have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>c s2" using IH1 exec1 by simp
1.420 - moreover have "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>c s3" using IH2 exec2' by fastsimp
1.421 - ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>c s3" ..
1.422 -next
1.423 - fix s t b c1 c2
1.424 - let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
1.425 - let ?C1 = "compile c1" let ?C2 = "compile c2"
1.426 - 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.427 - 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.428 - and H: "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle>"
1.429 - show "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>c t"
1.430 - proof cases
1.431 - assume b: "b s"
1.432 - with H have "\<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle>"
1.433 - by (fastsimp dest:exec_star_decomp
1.434 - [of _ "[JMPF (\<lambda>x. False) (size ?C2)]@?C2" "[]",simplified])
1.435 - hence "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH1)
1.436 - with b show ?thesis ..
1.437 - next
1.438 - assume b: "\<not> b s"
1.439 - with H have "\<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle>"
1.440 - using exec_star_decomp[of _ "[]" "[]"] by simp
1.441 - hence "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH2)
1.442 - with b show ?thesis ..
1.443 - qed
1.444 -next
1.445 - fix b c s t
1.446 - let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
1.447 - let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
1.448 - 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.449 - and H: "\<langle>?W,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
1.450 - from H obtain k where ob:"\<langle>?W,[],s\<rangle> -k\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
1.451 - by(simp add:rtrancl_is_UN_rel_pow) blast
1.452 - { 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.453 - proof (induct n rule: less_induct)
1.454 - fix n
1.455 - 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.456 - fix s
1.457 - assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
1.458 - show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
1.459 - proof cases
1.460 - assume b: "b s"
1.461 - then obtain m where m: "n = Suc m"
1.462 - and "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
1.463 - using H by fastsimp
1.464 - then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
1.465 - and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
1.466 - and n12: "m = n1+n2"
1.467 - using execn_decomp[of _ "[?j2]"]
1.468 - by(simp del: execn_simp) fast
1.469 - have n2n: "n2 - 1 < n" using m n12 by arith
1.470 - note b
1.471 - moreover
1.472 - { from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
1.473 - by (simp add:rtrancl_is_UN_rel_pow) fast
1.474 - hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
1.475 - }
1.476 - moreover
1.477 - { have "n2 - 1 < n" using m n12 by arith
1.478 - moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
1.479 - ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
1.480 - }
1.481 - ultimately show ?thesis ..
1.482 - next
1.483 - assume b: "\<not> b s"
1.484 - hence "t = s" using H by simp
1.485 - with b show ?thesis by simp
1.486 - qed
1.487 - qed
1.488 - }
1.489 - with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
1.490 -qed
1.491 -
1.492 -(* TODO: connect with Machine 0 using M_equiv *)
1.493 + case (WhileTrue b s1 c s2 s3)
1.494 + let ?cc = "ccomp c"
1.495 + let ?cb = "bcomp b False (size ?cc + 1)"
1.496 + let ?cw = "ccomp(WHILE b DO c)"
1.497 + have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)"
1.498 + using WhileTrue(1,3) by fastsimp
1.499 + moreover
1.500 + have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
1.501 + by (fastsimp)
1.502 + moreover
1.503 + have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue(5))
1.504 + ultimately show ?case by(blast intro: exec_trans)
1.505 +qed fastsimp+
1.506
1.507 end