New machine architecture and other direction of compiler proof.
authornipkow
Fri Apr 26 11:47:01 2002 +0200 (2002-04-26)
changeset 130958ed413a57bdc
parent 13094 643fce75f6cd
child 13096 04f8cbd1b500
New machine architecture and other direction of compiler proof.
src/HOL/IMP/Compiler.thy
src/HOL/IMP/Compiler0.thy
src/HOL/IMP/Machines.thy
src/HOL/IMP/ROOT.ML
     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 +    case Semi thus ?case by simp (blast intro:rtrancl_trans)
   1.164    next
   1.165 -    fix c0 c1 s0 s1 s2
   1.166 -    assume "?Q c0 s0 s1"
   1.167 -    hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
   1.168 -      by(rule app_right)
   1.169 -    moreover assume "?Q c1 s1 s2"
   1.170 -    hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
   1.171 -           \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
   1.172 -    proof -
   1.173 -      note app_left[of _ 0]
   1.174 -      thus
   1.175 -	      "\<And>is1 is2 s1 s2 i2.
   1.176 -	      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
   1.177 -	      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
   1.178 -	      by simp
   1.179 -    qed
   1.180 -    ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
   1.181 -                       \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
   1.182 -      by (rule rtrancl_trans)
   1.183 -    thus "?Q (c0; c1) s0 s2" by simp
   1.184 +    fix b c0 c1 s0 s1 p q
   1.185 +    assume IH: "\<And>p q. ?P c0 s0 s1 p q"
   1.186 +    assume "b s0"
   1.187 +    thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
   1.188 +      by(simp add: IH[THEN rtrancl_trans])
   1.189 +  next
   1.190 +    case IfFalse thus ?case by(simp)
   1.191    next
   1.192 -    fix b c0 c1 s0 s1
   1.193 -    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
   1.194 -    assume "b s0" and IH: "?Q c0 s0 s1"
   1.195 -    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
   1.196 -    also from IH
   1.197 -    have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
   1.198 -      by(auto intro:app1_left app_right)
   1.199 -    also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
   1.200 -      by(auto)
   1.201 -    finally show "?Q (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
   1.202 +    case WhileFalse thus ?case by simp
   1.203    next
   1.204 -    fix b c0 c1 s0 s1
   1.205 -    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
   1.206 -    assume "\<not>b s0" and IH: "?Q c1 s0 s1"
   1.207 -    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
   1.208 -    also from IH
   1.209 -    have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
   1.210 -      by(force intro!:app_left2 app1_left)
   1.211 -    finally show "?Q (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
   1.212 -  next
   1.213 -    fix b c and s::state
   1.214 -    assume "\<not>b s"
   1.215 -    thus "?Q (\<WHILE> b \<DO> c) s s" by force
   1.216 -  next
   1.217 -    fix b c and s0::state and s1 s2
   1.218 -    let ?comp = "compile(\<WHILE> b \<DO> c)"
   1.219 -    assume "b s0" and
   1.220 -      IHc: "?Q c s0 s1" and IHw: "?Q (\<WHILE> b \<DO> c) s1 s2"
   1.221 -    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
   1.222 -    also from IHc
   1.223 -    have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
   1.224 -      by(auto intro:app1_left app_right)
   1.225 -    also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
   1.226 -    also note IHw
   1.227 -    finally show "?Q (\<WHILE> b \<DO> c) s0 s2".
   1.228 +    fix b c and s0::state and s1 s2 p q
   1.229 +    assume b: "b s0" and
   1.230 +      IHc: "\<And>p q. ?P c s0 s1 p q" and
   1.231 +      IHw: "\<And>p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
   1.232 +    show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
   1.233 +      using b  IHc[THEN rtrancl_trans] IHw by(simp)
   1.234    qed
   1.235  qed
   1.236  
   1.237 -text {*
   1.238 -  Second proof; statement is generalized to cater for prefixes and suffixes;
   1.239 -  needs none of the lifting lemmas, but instantiations of pre/suffix.
   1.240 -  *}
   1.241 -theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> 
   1.242 -  !a z. a@compile c@z \<turnstile> \<langle>s,length a\<rangle> -*\<rightarrow> \<langle>t,length a + length(compile c)\<rangle>";
   1.243 -apply(erule evalc.induct)
   1.244 -      apply simp
   1.245 -     apply(force intro!: ASIN)
   1.246 -    apply(intro strip)
   1.247 -    apply(erule_tac x = a in allE)
   1.248 -    apply(erule_tac x = "a@compile c0" in allE)
   1.249 -    apply(erule_tac x = "compile c1@z" in allE)
   1.250 -    apply(erule_tac x = z in allE)
   1.251 -    apply(simp add:add_assoc[THEN sym])
   1.252 -    apply(blast intro:rtrancl_trans)
   1.253 -(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
   1.254 -   apply(intro strip)
   1.255 -   (* instantiate assumption sufficiently for later: *)
   1.256 -   apply(erule_tac x = "a@[?I]" in allE)
   1.257 -   apply(simp)
   1.258 -   (* execute JMPF: *)
   1.259 -   apply(rule converse_rtrancl_into_rtrancl)
   1.260 -    apply(force intro!: JMPFT)
   1.261 -   (* execute compile c0: *)
   1.262 -   apply(rule rtrancl_trans)
   1.263 -    apply(erule allE)
   1.264 -    apply assumption
   1.265 -   (* execute JMPF: *)
   1.266 -   apply(rule r_into_rtrancl)
   1.267 -   apply(force intro!: JMPFF)
   1.268 -(* end of case b is true *)
   1.269 -  apply(intro strip)
   1.270 -  apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
   1.271 -  apply(simp add:add_assoc)
   1.272 -  apply(rule converse_rtrancl_into_rtrancl)
   1.273 -   apply(force intro!: JMPFF)
   1.274 -  apply(blast)
   1.275 - apply(force intro: JMPFF)
   1.276 -apply(intro strip)
   1.277 -apply(erule_tac x = "a@[?I]" in allE)
   1.278 -apply(erule_tac x = a in allE)
   1.279 -apply(simp)
   1.280 -apply(rule converse_rtrancl_into_rtrancl)
   1.281 - apply(force intro!: JMPFT)
   1.282 -apply(rule rtrancl_trans)
   1.283 - apply(erule allE)
   1.284 - apply assumption
   1.285 -apply(rule converse_rtrancl_into_rtrancl)
   1.286 - apply(force intro!: JMPB)
   1.287 -apply(simp)
   1.288 +text {* The other direction! *}
   1.289 +
   1.290 +inductive_cases [elim!]: "(([],p,s),next) : stepa1"
   1.291 +
   1.292 +lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
   1.293 +apply(rule iffI)
   1.294 + apply(erule converse_rel_powE, simp, fast)
   1.295 +apply simp
   1.296 +done
   1.297 +
   1.298 +lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
   1.299 +by(simp add: rtrancl_is_UN_rel_pow)
   1.300 +
   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 -text {* Missing: the other direction! *}
   1.357 +theorem closed_execn_decomp: "\<And>C1 C2 r.
   1.358 + \<lbrakk> closed 0 0 (rev C1 @ C2);
   1.359 +   \<langle>C2 @ p1 @ p2, C1 @ q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<rbrakk>
   1.360 + \<Longrightarrow> \<exists>s n1 n2. \<langle>C2,C1,r\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle> \<and>
   1.361 +     \<langle>p1@p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
   1.362 +         n = n1+n2"
   1.363 +(is "\<And>C1 C2 r. \<lbrakk>?CL C1 C2; ?H C1 C2 r n\<rbrakk> \<Longrightarrow> ?P C1 C2 r n")
   1.364 +proof(induct n)
   1.365 +  fix C1 C2 r
   1.366 +  assume "?H C1 C2 r 0"
   1.367 +  thus "?P C1 C2 r 0" by simp
   1.368 +next
   1.369 +  fix C1 C2 r n
   1.370 +  assume IH: "\<And>C1 C2 r. ?CL C1 C2 \<Longrightarrow> ?H C1 C2 r n \<Longrightarrow> ?P C1 C2 r n"
   1.371 +  assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
   1.372 +  show "?P C1 C2 r (Suc n)"
   1.373 +  proof (cases C2)
   1.374 +    assume "C2 = []" with H show ?thesis by simp
   1.375 +  next
   1.376 +    fix instr tlC2
   1.377 +    assume C2: "C2 = instr # tlC2"
   1.378 +    from H C2 obtain p' q' r'
   1.379 +      where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
   1.380 +      and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
   1.381 +      by(fastsimp simp add:R_O_Rn_commute)
   1.382 +    from CL closed_exec1[OF _ 1] C2
   1.383 +    obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
   1.384 +      and same: "rev C1' @ C2' = rev C1 @ C2"
   1.385 +      by fastsimp
   1.386 +    have rev_same: "rev C2' @ C1' = rev C2 @ C1"
   1.387 +    proof -
   1.388 +      have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
   1.389 +      also have "\<dots> = rev(rev C1 @ C2)" by(simp only:same)
   1.390 +      also have "\<dots> =  rev C2 @ C1" by simp
   1.391 +      finally show ?thesis .
   1.392 +    qed
   1.393 +    hence rev_same': "\<And>p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
   1.394 +    from n have n': "\<langle>C2' @ p1 @ p2,C1' @ q,r'\<rangle> -n\<rightarrow>
   1.395 +                     \<langle>p2,rev p1 @ rev C2' @ C1' @ q,t\<rangle>"
   1.396 +      by(simp add:pq' rev_same')
   1.397 +    from IH[OF _ n'] CL
   1.398 +    obtain s n1 n2 where n1: "\<langle>C2',C1',r'\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>" and
   1.399 +      "\<langle>p1 @ p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
   1.400 +       n = n1 + n2"
   1.401 +      by(fastsimp simp add: same rev_same rev_same')
   1.402 +    moreover
   1.403 +    from 1 n1 pq' C2 have "\<langle>C2,C1,r\<rangle> -Suc n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>"
   1.404 +      by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
   1.405 +    ultimately show ?thesis by (fastsimp simp del:relpow.simps)
   1.406 +  qed
   1.407 +qed
   1.408 +
   1.409 +lemma execn_decomp:
   1.410 +"\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
   1.411 + \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
   1.412 +     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
   1.413 +         n = n1+n2"
   1.414 +using closed_execn_decomp[of "[]",simplified] by simp
   1.415 +
   1.416 +lemma exec_star_decomp:
   1.417 +"\<langle>compile c @ p1 @ p2,q,r\<rangle> -*\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
   1.418 + \<Longrightarrow> \<exists>s. \<langle>compile c,[],r\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
   1.419 +     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -*\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle>"
   1.420 +by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)
   1.421 +
   1.422 +
   1.423 +(* Alternative:
   1.424 +lemma exec_comp_n:
   1.425 +"\<And>p1 p2 q r t n.
   1.426 + \<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
   1.427 + \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
   1.428 +     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
   1.429 +         n = n1+n2"
   1.430 + (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.431 +proof (induct c)
   1.432 +*)
   1.433 +
   1.434 +text{*Warning: 
   1.435 +@{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.436 +is not true! *}
   1.437  
   1.438 -end
   1.439 +theorem "\<And>s t.
   1.440 + \<langle>compile c,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   1.441 +proof (induct c)
   1.442 +  fix s t
   1.443 +  assume "\<langle>compile SKIP,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile SKIP),t\<rangle>"
   1.444 +  thus "\<langle>SKIP,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
   1.445 +next
   1.446 +  fix s t v f
   1.447 +  assume "\<langle>compile(v :== f),[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile(v :== f)),t\<rangle>"
   1.448 +  thus "\<langle>v :== f,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
   1.449 +next
   1.450 +  fix s1 s3 c1 c2
   1.451 +  let ?C1 = "compile c1" let ?C2 = "compile c2"
   1.452 +  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.453 +     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.454 +  assume "\<langle>compile(c1;c2),[],s1\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
   1.455 +  then obtain s2 where exec1: "\<langle>?C1,[],s1\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,s2\<rangle>" and
   1.456 +             exec2: "\<langle>?C2,rev ?C1,s2\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
   1.457 +    by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
   1.458 +  from exec2 have exec2': "\<langle>?C2,[],s2\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,s3\<rangle>"
   1.459 +    using exec_star_decomp[of _ "[]" "[]"] by fastsimp
   1.460 +  have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>c s2" using IH1 exec1 by simp
   1.461 +  moreover have "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>c s3" using IH2 exec2' by fastsimp
   1.462 +  ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>c s3" ..
   1.463 +next
   1.464 +  fix s t b c1 c2
   1.465 +  let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
   1.466 +  let ?C1 = "compile c1" let ?C2 = "compile c2"
   1.467 +  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.468 +     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.469 +     and H: "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle>"
   1.470 +  show "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>c t"
   1.471 +  proof cases
   1.472 +    assume b: "b s"
   1.473 +    with H have "\<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle>"
   1.474 +      by (fastsimp dest:exec_star_decomp
   1.475 +            [of _ "[JMPF (\<lambda>x. False) (size ?C2)]@?C2" "[]",simplified])
   1.476 +    hence "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH1)
   1.477 +    with b show ?thesis ..
   1.478 +  next
   1.479 +    assume b: "\<not> b s"
   1.480 +    with H have "\<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle>"
   1.481 +      using exec_star_decomp[of _ "[]" "[]"] by simp
   1.482 +    hence "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH2)
   1.483 +    with b show ?thesis ..
   1.484 +  qed
   1.485 +next
   1.486 +  fix b c s t
   1.487 +  let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
   1.488 +  let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
   1.489 +  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.490 +     and H: "\<langle>?W,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
   1.491 +  from H obtain k where ob:"\<langle>?W,[],s\<rangle> -k\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
   1.492 +    by(simp add:rtrancl_is_UN_rel_pow) blast
   1.493 +  { 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.494 +    proof (induct n rule: less_induct)
   1.495 +      fix n
   1.496 +      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.497 +      fix s
   1.498 +      assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
   1.499 +      show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
   1.500 +      proof cases
   1.501 +	assume b: "b s"
   1.502 +	then obtain m where m: "n = Suc m"
   1.503 +          and 1: "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
   1.504 +	  using H by fastsimp
   1.505 +	then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
   1.506 +          and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
   1.507 +          and n12: "m = n1+n2"
   1.508 +	  using execn_decomp[of _ "[?j2]"]
   1.509 +	  by(simp del: execn_simp) fast
   1.510 +	have n2n: "n2 - 1 < n" using m n12 by arith
   1.511 +	note b
   1.512 +	moreover
   1.513 +	{ from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
   1.514 +	    by (simp add:rtrancl_is_UN_rel_pow) fast
   1.515 +	  hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
   1.516 +	}
   1.517 +	moreover
   1.518 +	{ have "n2 - 1 < n" using m n12 by arith
   1.519 +	  moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
   1.520 +	  ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
   1.521 +	}
   1.522 +	ultimately show ?thesis ..
   1.523 +      next
   1.524 +	assume b: "\<not> b s"
   1.525 +	hence "t = s" using H by simp
   1.526 +	with b show ?thesis by simp
   1.527 +      qed
   1.528 +    qed
   1.529 +  }
   1.530 +  with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
   1.531 +qed
   1.532 +
   1.533 +(* To Do: connect with Machine 0 using M_equiv *)
   1.534 +
   1.535 +end
   1.536 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMP/Compiler0.thy	Fri Apr 26 11:47:01 2002 +0200
     2.3 @@ -0,0 +1,272 @@
     2.4 +(*  Title:      HOL/IMP/Compiler.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow, TUM
     2.7 +    Copyright   1996 TUM
     2.8 +
     2.9 +This is an early version of the compiler, where the abstract machine
    2.10 +has an explicit pc. This turned out to be awkward, and a second
    2.11 +development was started. See Machines.thy and Compiler.thy.
    2.12 +*)
    2.13 +
    2.14 +header "A Simple Compiler"
    2.15 +
    2.16 +theory Compiler0 = Natural:
    2.17 +
    2.18 +subsection "An abstract, simplistic machine"
    2.19 +
    2.20 +text {* There are only three instructions: *}
    2.21 +datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
    2.22 +
    2.23 +text {* We describe execution of programs in the machine by
    2.24 +  an operational (small step) semantics:
    2.25 +*}
    2.26 +consts  stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
    2.27 +
    2.28 +syntax
    2.29 +  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    2.30 +               ("_ |- (3<_,_>/ -1-> <_,_>)" [50,0,0,0,0] 50)
    2.31 +  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    2.32 +               ("_ |-/ (3<_,_>/ -*-> <_,_>)" [50,0,0,0,0] 50)
    2.33 +
    2.34 +  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
    2.35 +               ("_ |-/ (3<_,_>/ -(_)-> <_,_>)" [50,0,0,0,0,0] 50)
    2.36 +
    2.37 +syntax (xsymbols)
    2.38 +  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    2.39 +               ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
    2.40 +  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    2.41 +               ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
    2.42 +  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
    2.43 +               ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
    2.44 +
    2.45 +translations  
    2.46 +  "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
    2.47 +  "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
    2.48 +  "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^i)"
    2.49 +
    2.50 +inductive "stepa1 P"
    2.51 +intros
    2.52 +ASIN[simp]:
    2.53 +  "\<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>"
    2.54 +JMPFT[simp,intro]:
    2.55 +  "\<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>"
    2.56 +JMPFF[simp,intro]:
    2.57 +  "\<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>"
    2.58 +JMPB[simp]:
    2.59 +  "\<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>"
    2.60 +
    2.61 +subsection "The compiler"
    2.62 +
    2.63 +consts compile :: "com \<Rightarrow> instr list"
    2.64 +primrec
    2.65 +"compile \<SKIP> = []"
    2.66 +"compile (x:==a) = [ASIN x a]"
    2.67 +"compile (c1;c2) = compile c1 @ compile c2"
    2.68 +"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
    2.69 + [JMPF b (length(compile c1) + 2)] @ compile c1 @
    2.70 + [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
    2.71 +"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
    2.72 + [JMPB (length(compile c)+1)]"
    2.73 +
    2.74 +declare nth_append[simp]
    2.75 +
    2.76 +subsection "Context lifting lemmas"
    2.77 +
    2.78 +text {* 
    2.79 +  Some lemmas for lifting an execution into a prefix and suffix
    2.80 +  of instructions; only needed for the first proof.
    2.81 +*}
    2.82 +lemma app_right_1:
    2.83 +  assumes A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    2.84 +  shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    2.85 +proof -
    2.86 + from A show ?thesis
    2.87 + by induct force+
    2.88 +qed
    2.89 +
    2.90 +lemma app_left_1:
    2.91 +  assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    2.92 +  shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
    2.93 +proof -
    2.94 + from A show ?thesis
    2.95 + by induct force+
    2.96 +qed
    2.97 +
    2.98 +declare rtrancl_induct2 [induct set: rtrancl]
    2.99 +
   2.100 +lemma app_right:
   2.101 +assumes A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
   2.102 +shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
   2.103 +proof -
   2.104 + from A show ?thesis
   2.105 + proof induct
   2.106 +   show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
   2.107 + next
   2.108 +   fix s1' i1' s2 i2
   2.109 +   assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
   2.110 +          "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
   2.111 +   thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
   2.112 +     by(blast intro:app_right_1 rtrancl_trans)
   2.113 + qed
   2.114 +qed
   2.115 +
   2.116 +lemma app_left:
   2.117 +assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
   2.118 +shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
   2.119 +proof -
   2.120 +  from A show ?thesis
   2.121 +  proof induct
   2.122 +    show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
   2.123 +  next
   2.124 +    fix s1' i1' s2 i2
   2.125 +    assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
   2.126 +           "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
   2.127 +    thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
   2.128 +      by(blast intro:app_left_1 rtrancl_trans)
   2.129 + qed
   2.130 +qed
   2.131 +
   2.132 +lemma app_left2:
   2.133 +  "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
   2.134 +   is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
   2.135 +  by (simp add:app_left)
   2.136 +
   2.137 +lemma app1_left:
   2.138 +  "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
   2.139 +   instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
   2.140 +  by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
   2.141 +
   2.142 +subsection "Compiler correctness"
   2.143 +
   2.144 +declare rtrancl_into_rtrancl[trans]
   2.145 +        converse_rtrancl_into_rtrancl[trans]
   2.146 +        rtrancl_trans[trans]
   2.147 +
   2.148 +text {*
   2.149 +  The first proof; The statement is very intuitive,
   2.150 +  but application of induction hypothesis requires the above lifting lemmas
   2.151 +*}
   2.152 +theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   2.153 +shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
   2.154 +proof -
   2.155 +  from A show ?thesis
   2.156 +  proof induct
   2.157 +    show "\<And>s. ?P \<SKIP> s s" by simp
   2.158 +  next
   2.159 +    show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
   2.160 +  next
   2.161 +    fix c0 c1 s0 s1 s2
   2.162 +    assume "?P c0 s0 s1"
   2.163 +    hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
   2.164 +      by(rule app_right)
   2.165 +    moreover assume "?P c1 s1 s2"
   2.166 +    hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
   2.167 +           \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
   2.168 +    proof -
   2.169 +      show "\<And>is1 is2 s1 s2 i2.
   2.170 +	      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
   2.171 +	      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
   2.172 +	using app_left[of _ 0] by simp
   2.173 +    qed
   2.174 +    ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
   2.175 +                       \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
   2.176 +      by (rule rtrancl_trans)
   2.177 +    thus "?P (c0; c1) s0 s2" by simp
   2.178 +  next
   2.179 +    fix b c0 c1 s0 s1
   2.180 +    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
   2.181 +    assume "b s0" and IH: "?P c0 s0 s1"
   2.182 +    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
   2.183 +    also from IH
   2.184 +    have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
   2.185 +      by(auto intro:app1_left app_right)
   2.186 +    also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
   2.187 +      by(auto)
   2.188 +    finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
   2.189 +  next
   2.190 +    fix b c0 c1 s0 s1
   2.191 +    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
   2.192 +    assume "\<not>b s0" and IH: "?P c1 s0 s1"
   2.193 +    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
   2.194 +    also from IH
   2.195 +    have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
   2.196 +      by(force intro!:app_left2 app1_left)
   2.197 +    finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
   2.198 +  next
   2.199 +    fix b c and s::state
   2.200 +    assume "\<not>b s"
   2.201 +    thus "?P (\<WHILE> b \<DO> c) s s" by force
   2.202 +  next
   2.203 +    fix b c and s0::state and s1 s2
   2.204 +    let ?comp = "compile(\<WHILE> b \<DO> c)"
   2.205 +    assume "b s0" and
   2.206 +      IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
   2.207 +    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
   2.208 +    also from IHc
   2.209 +    have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
   2.210 +      by(auto intro:app1_left app_right)
   2.211 +    also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
   2.212 +    also note IHw
   2.213 +    finally show "?P (\<WHILE> b \<DO> c) s0 s2".
   2.214 +  qed
   2.215 +qed
   2.216 +
   2.217 +text {*
   2.218 +  Second proof; statement is generalized to cater for prefixes and suffixes;
   2.219 +  needs none of the lifting lemmas, but instantiations of pre/suffix.
   2.220 +  *}
   2.221 +theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> 
   2.222 +  !a z. a@compile c@z \<turnstile> \<langle>s,length a\<rangle> -*\<rightarrow> \<langle>t,length a + length(compile c)\<rangle>";
   2.223 +apply(erule evalc.induct)
   2.224 +      apply simp
   2.225 +     apply(force intro!: ASIN)
   2.226 +    apply(intro strip)
   2.227 +    apply(erule_tac x = a in allE)
   2.228 +    apply(erule_tac x = "a@compile c0" in allE)
   2.229 +    apply(erule_tac x = "compile c1@z" in allE)
   2.230 +    apply(erule_tac x = z in allE)
   2.231 +    apply(simp add:add_assoc[THEN sym])
   2.232 +    apply(blast intro:rtrancl_trans)
   2.233 +(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
   2.234 +   apply(intro strip)
   2.235 +   (* instantiate assumption sufficiently for later: *)
   2.236 +   apply(erule_tac x = "a@[?I]" in allE)
   2.237 +   apply(simp)
   2.238 +   (* execute JMPF: *)
   2.239 +   apply(rule converse_rtrancl_into_rtrancl)
   2.240 +    apply(force intro!: JMPFT)
   2.241 +   (* execute compile c0: *)
   2.242 +   apply(rule rtrancl_trans)
   2.243 +    apply(erule allE)
   2.244 +    apply assumption
   2.245 +   (* execute JMPF: *)
   2.246 +   apply(rule r_into_rtrancl)
   2.247 +   apply(force intro!: JMPFF)
   2.248 +(* end of case b is true *)
   2.249 +  apply(intro strip)
   2.250 +  apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
   2.251 +  apply(simp add:add_assoc)
   2.252 +  apply(rule converse_rtrancl_into_rtrancl)
   2.253 +   apply(force intro!: JMPFF)
   2.254 +  apply(blast)
   2.255 + apply(force intro: JMPFF)
   2.256 +apply(intro strip)
   2.257 +apply(erule_tac x = "a@[?I]" in allE)
   2.258 +apply(erule_tac x = a in allE)
   2.259 +apply(simp)
   2.260 +apply(rule converse_rtrancl_into_rtrancl)
   2.261 + apply(force intro!: JMPFT)
   2.262 +apply(rule rtrancl_trans)
   2.263 + apply(erule allE)
   2.264 + apply assumption
   2.265 +apply(rule converse_rtrancl_into_rtrancl)
   2.266 + apply(force intro!: JMPB)
   2.267 +apply(simp)
   2.268 +done
   2.269 +
   2.270 +text {* Missing: the other direction! I did much of it, and although
   2.271 +the main lemma is very similar to the one in the new development, the
   2.272 +lemmas surrounding it seemed much more complicated. In the end I gave
   2.273 +up. *}
   2.274 +
   2.275 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/IMP/Machines.thy	Fri Apr 26 11:47:01 2002 +0200
     3.3 @@ -0,0 +1,242 @@
     3.4 +theory Machines = Natural:
     3.5 +
     3.6 +lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
     3.7 +by(fast intro:rtrancl.intros elim:rtranclE)
     3.8 +
     3.9 +lemma converse_rtrancl_eq: "R^* = Id \<union> (R^* O R)"
    3.10 +by(subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
    3.11 +
    3.12 +lemmas converse_rel_powE = rel_pow_E2
    3.13 +
    3.14 +lemma R_O_Rn_commute: "R O R^n = R^n O R"
    3.15 +by(induct_tac n, simp, simp add: O_assoc[symmetric])
    3.16 +
    3.17 +lemma converse_in_rel_pow_eq:
    3.18 +"((x,z) \<in> R^n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R^m))"
    3.19 +apply(rule iffI)
    3.20 + apply(blast elim:converse_rel_powE)
    3.21 +apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
    3.22 +done
    3.23 +
    3.24 +lemma rel_pow_plus: "R^(m+n) = R^n O R^m"
    3.25 +by(induct n, simp, simp add:O_assoc)
    3.26 +
    3.27 +lemma rel_pow_plusI: "\<lbrakk> (x,y) \<in> R^m; (y,z) \<in> R^n \<rbrakk> \<Longrightarrow> (x,z) \<in> R^(m+n)"
    3.28 +by(simp add:rel_pow_plus rel_compI)
    3.29 +
    3.30 +subsection "Instructions"
    3.31 +
    3.32 +text {* There are only three instructions: *}
    3.33 +datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
    3.34 +
    3.35 +types instrs = "instr list"
    3.36 +
    3.37 +subsection "M0 with PC"
    3.38 +
    3.39 +consts  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
    3.40 +
    3.41 +syntax
    3.42 +  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    3.43 +               ("(_/ |- (1<_,/_>)/ -1-> (1<_,/_>))" [50,0,0,0,0] 50)
    3.44 +  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    3.45 +               ("(_/ |- (1<_,/_>)/ -*-> (1<_,/_>))" [50,0,0,0,0] 50)
    3.46 +  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
    3.47 +               ("(_/ |- (1<_,/_>)/ -_-> (1<_,/_>))" [50,0,0,0,0] 50)
    3.48 +
    3.49 +syntax (xsymbols)
    3.50 +  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    3.51 +               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    3.52 +  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    3.53 +               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    3.54 +  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
    3.55 +               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    3.56 +
    3.57 +translations  
    3.58 +  "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
    3.59 +  "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
    3.60 +  "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^n"
    3.61 +
    3.62 +inductive "exec01 P"
    3.63 +intros
    3.64 +ASIN: "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s[x\<mapsto> a s]\<rangle>"
    3.65 +JMPFT: "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s\<rangle>"
    3.66 +JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk>
    3.67 +        \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>"
    3.68 +JMPB:  "\<lbrakk> n<size P; P!n = JMPB i; i \<le> n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>j,s\<rangle>"
    3.69 +
    3.70 +subsection "M0 with lists"
    3.71 +
    3.72 +text {* We describe execution of programs in the machine by
    3.73 +  an operational (small step) semantics:
    3.74 +*}
    3.75 +
    3.76 +types config = "instrs \<times> instrs \<times> state"
    3.77 +
    3.78 +consts  stepa1 :: "(config \<times> config)set"
    3.79 +
    3.80 +syntax
    3.81 +  "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
    3.82 +               ("((1<_,/_,/_>)/ -1-> (1<_,/_,/_>))" 50)
    3.83 +  "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
    3.84 +               ("((1<_,/_,/_>)/ -*-> (1<_,/_,/_>))" 50)
    3.85 +  "_stepan" :: "[state,instrs,instrs, nat, instrs,instrs,state] \<Rightarrow> bool"
    3.86 +               ("((1<_,/_,/_>)/ -_-> (1<_,/_,/_>))" 50)
    3.87 +
    3.88 +syntax (xsymbols)
    3.89 +  "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
    3.90 +               ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
    3.91 +  "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
    3.92 +               ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
    3.93 +  "_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
    3.94 +               ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
    3.95 +
    3.96 +translations  
    3.97 +  "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : stepa1"
    3.98 +  "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^*)"
    3.99 +  "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^i)"
   3.100 +
   3.101 +
   3.102 +inductive "stepa1"
   3.103 +intros
   3.104 +  "\<langle>ASIN x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,ASIN x a#q,s[x\<mapsto> a s]\<rangle>"
   3.105 +  "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>"
   3.106 +  "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk>
   3.107 +   \<Longrightarrow> \<langle>JMPF b i # p, q, s\<rangle> -1\<rightarrow> \<langle>drop i p, rev(take i p) @ JMPF b i # q, s\<rangle>"
   3.108 +  "i \<le> size q
   3.109 +   \<Longrightarrow> \<langle>JMPB i # p, q, s\<rangle> -1\<rightarrow> \<langle>rev(take i q) @ JMPB i # p, drop i q, s\<rangle>"
   3.110 +
   3.111 +inductive_cases execE: "((i#is,p,s),next) : stepa1"
   3.112 +
   3.113 +lemma exec_simp[simp]:
   3.114 + "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of
   3.115 + ASIN x a \<Rightarrow> t = s[x\<mapsto> a s] \<and> p' = p \<and> q' = i#q |
   3.116 + JMPF b n \<Rightarrow> t=s \<and> (if b s then p' = p \<and> q' = i#q
   3.117 +            else n \<le> size p \<and> p' = drop n p \<and> q' = rev(take n p) @ i # q) |
   3.118 + JMPB n \<Rightarrow> n \<le> size q \<and> t=s \<and> p' = rev(take n q) @ i # p \<and> q' = drop n q)"
   3.119 +apply(rule iffI)
   3.120 +defer
   3.121 +apply(clarsimp simp add: stepa1.intros split: instr.split_asm split_if_asm)
   3.122 +apply(erule execE)
   3.123 +apply(simp_all)
   3.124 +done
   3.125 +
   3.126 +lemma execn_simp[simp]:
   3.127 +"(\<langle>i#p,q,s\<rangle> -n\<rightarrow> \<langle>p'',q'',u\<rangle>) =
   3.128 + (n=0 \<and> p'' = i#p \<and> q'' = q \<and> u = s \<or>
   3.129 +  ((\<exists>m p' q' t. n = Suc m \<and>
   3.130 +                \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -m\<rightarrow> \<langle>p'',q'',u\<rangle>)))"
   3.131 +by(subst converse_in_rel_pow_eq, simp)
   3.132 +
   3.133 +
   3.134 +lemma exec_star_simp[simp]: "(\<langle>i#p,q,s\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>) =
   3.135 + (p'' = i#p & q''=q & u=s |
   3.136 + (\<exists>p' q' t. \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>))"
   3.137 +apply(simp add: rtrancl_is_UN_rel_pow del:exec_simp)
   3.138 +apply(blast)
   3.139 +done
   3.140 +
   3.141 +declare nth_append[simp]
   3.142 +
   3.143 +lemma rev_revD: "rev xs = rev ys \<Longrightarrow> xs = ys"
   3.144 +by simp
   3.145 +
   3.146 +lemma [simp]: "(rev xs @ rev ys = rev zs) = (ys @ xs = zs)"
   3.147 +apply(rule iffI)
   3.148 + apply(rule rev_revD, simp)
   3.149 +apply fastsimp
   3.150 +done
   3.151 +
   3.152 +lemma direction1:
   3.153 + "\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle> \<Longrightarrow>
   3.154 +  rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>"
   3.155 +apply(erule stepa1.induct)
   3.156 +   apply(simp add:exec01.ASIN)
   3.157 +  apply(fastsimp intro:exec01.JMPFT)
   3.158 + apply simp
   3.159 + apply(rule exec01.JMPFF)
   3.160 +     apply simp
   3.161 +    apply fastsimp
   3.162 +   apply simp
   3.163 +  apply simp
   3.164 +  apply arith
   3.165 + apply simp
   3.166 + apply arith
   3.167 +apply(fastsimp simp add:exec01.JMPB)
   3.168 +done
   3.169 +
   3.170 +lemma drop_take_rev: "\<And>i. drop (length xs - i) (rev xs) = rev (take i xs)"
   3.171 +apply(induct xs)
   3.172 + apply simp_all
   3.173 +apply(case_tac i)
   3.174 +apply simp_all
   3.175 +done
   3.176 +
   3.177 +lemma take_drop_rev: "\<And>i. take (length xs - i) (rev xs) = rev (drop i xs)"
   3.178 +apply(induct xs)
   3.179 + apply simp_all
   3.180 +apply(case_tac i)
   3.181 +apply simp_all
   3.182 +done
   3.183 +
   3.184 +lemma direction2:
   3.185 + "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
   3.186 + \<forall>p q p' q'. rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
   3.187 +          rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
   3.188 +apply(erule exec01.induct)
   3.189 +   apply(clarsimp simp add: neq_Nil_conv)
   3.190 +   apply(rule conjI)
   3.191 +    apply(drule_tac f = "drop (size p')" in arg_cong)
   3.192 +    apply simp
   3.193 +    apply(drule sym)
   3.194 +    apply simp
   3.195 +   apply(drule_tac f = "take (size p')" in arg_cong)
   3.196 +   apply simp
   3.197 +   apply(drule sym)
   3.198 +   apply simp
   3.199 +   apply(rule rev_revD)
   3.200 +   apply simp
   3.201 +  apply(clarsimp simp add: neq_Nil_conv)
   3.202 +  apply(rule conjI)
   3.203 +   apply(drule_tac f = "drop (size p')" in arg_cong)
   3.204 +   apply simp
   3.205 +   apply(drule sym)
   3.206 +   apply simp
   3.207 +  apply(drule_tac f = "take (size p')" in arg_cong)
   3.208 +  apply simp
   3.209 +  apply(drule sym)
   3.210 +  apply simp
   3.211 +  apply(rule rev_revD)
   3.212 +  apply simp
   3.213 + apply(clarsimp simp add: neq_Nil_conv)
   3.214 + apply(rule conjI)
   3.215 +  apply(drule_tac f = "drop (size p')" in arg_cong)
   3.216 +  apply simp
   3.217 +  apply(drule sym)
   3.218 +  apply simp
   3.219 + apply(drule_tac f = "take (size p')" in arg_cong)
   3.220 + apply simp
   3.221 + apply(drule sym)
   3.222 + apply simp
   3.223 + apply(rule rev_revD)
   3.224 + apply simp
   3.225 +apply(clarsimp simp add: neq_Nil_conv)
   3.226 +apply(rule conjI)
   3.227 + apply(drule_tac f = "drop (size p')" in arg_cong)
   3.228 + apply simp
   3.229 + apply(drule sym)
   3.230 + apply(simp add:drop_take_rev)
   3.231 +apply(drule_tac f = "take (size p')" in arg_cong)
   3.232 +apply simp
   3.233 +apply(drule sym)
   3.234 +apply simp
   3.235 +apply(rule rev_revD)
   3.236 +apply(simp add:take_drop_rev)
   3.237 +done
   3.238 +
   3.239 +
   3.240 +theorem M_eqiv:
   3.241 +"(\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>) =
   3.242 + (rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>)"
   3.243 +by(fast dest:direction1 direction2)
   3.244 +
   3.245 +end
     4.1 --- a/src/HOL/IMP/ROOT.ML	Thu Apr 25 17:36:29 2002 +0200
     4.2 +++ b/src/HOL/IMP/ROOT.ML	Fri Apr 26 11:47:01 2002 +0200
     4.3 @@ -10,4 +10,5 @@
     4.4  time_use_thy "Transition";
     4.5  time_use_thy "VC";
     4.6  time_use_thy "Examples";
     4.7 +time_use_thy "Compiler0";
     4.8  time_use_thy "Compiler";