1.1 --- a/src/HOL/IMP/Compiler.thy Sun Dec 09 14:34:18 2001 +0100
1.2 +++ b/src/HOL/IMP/Compiler.thy Sun Dec 09 14:34:56 2001 +0100
1.3 @@ -2,55 +2,72 @@
1.4 ID: $Id$
1.5 Author: Tobias Nipkow, TUM
1.6 Copyright 1996 TUM
1.7 +*)
1.8
1.9 -A simple compiler for a simplistic machine.
1.10 -*)
1.11 +header "A Simple Compiler"
1.12
1.13 theory Compiler = Natural:
1.14
1.15 +subsection "An abstract, simplistic machine"
1.16 +
1.17 +text {* There are only three instructions: *}
1.18 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
1.19
1.20 -consts stepa1 :: "instr list => ((state*nat) * (state*nat))set"
1.21 +text {* We describe execution of programs in the machine by
1.22 + an operational (small step) semantics:
1.23 +*}
1.24 +consts stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
1.25
1.26 syntax
1.27 - "@stepa1" :: "[instr list,state,nat,state,nat] => bool"
1.28 - ("_ \<turnstile> <_,_>/ -1\<rightarrow> <_,_>" [50,0,0,0,0] 50)
1.29 - "@stepa" :: "[instr list,state,nat,state,nat] => bool"
1.30 - ("_ \<turnstile>/ <_,_>/ -*\<rightarrow> <_,_>" [50,0,0,0,0] 50)
1.31 + "@stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
1.32 + ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
1.33 + "@stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
1.34 + ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
1.35
1.36 -translations "P \<turnstile> <s,m> -1\<rightarrow> <t,n>" == "((s,m),t,n) : stepa1 P"
1.37 - "P \<turnstile> <s,m> -*\<rightarrow> <t,n>" == "((s,m),t,n) : ((stepa1 P)^*)"
1.38 +syntax (xsymbols)
1.39 + "@stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
1.40 + ("_ \<turnstile> \<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
1.41 + "@stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
1.42 + ("_ \<turnstile>/ \<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
1.43
1.44 +translations
1.45 + "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
1.46 + "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
1.47
1.48 inductive "stepa1 P"
1.49 intros
1.50 ASIN[simp]:
1.51 - "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s[x::= a s],Suc n>"
1.52 + "\<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.53 JMPFT[simp,intro]:
1.54 - "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s,Suc n>"
1.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>"
1.56 JMPFF[simp,intro]:
1.57 - "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s,m>"
1.58 + "\<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.59 JMPB[simp]:
1.60 - "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s,j>"
1.61 + "\<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.62
1.63 -consts compile :: "com => instr list"
1.64 +subsection "The compiler"
1.65 +
1.66 +consts compile :: "com \<Rightarrow> instr list"
1.67 primrec
1.68 -"compile SKIP = []"
1.69 +"compile \<SKIP> = []"
1.70 "compile (x:==a) = [ASIN x a]"
1.71 "compile (c1;c2) = compile c1 @ compile c2"
1.72 -"compile (IF b THEN c1 ELSE c2) =
1.73 +"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
1.74 [JMPF b (length(compile c1) + 2)] @ compile c1 @
1.75 [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
1.76 -"compile (WHILE b DO c) = [JMPF b (length(compile c) + 2)] @ compile c @
1.77 +"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
1.78 [JMPB (length(compile c)+1)]"
1.79
1.80 -declare nth_append[simp];
1.81 +declare nth_append[simp]
1.82
1.83 -(* Lemmas for lifting an execution into a prefix and suffix
1.84 - of instructions; only needed for the first proof *)
1.85 +subsection "Context lifting lemmas"
1.86
1.87 +text {*
1.88 + Some lemmas for lifting an execution into a prefix and suffix
1.89 + of instructions; only needed for the first proof.
1.90 +*}
1.91 lemma app_right_1:
1.92 - "is1 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2> \<Longrightarrow> is1 @ is2 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2>"
1.93 + "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.94 (is "?P \<Longrightarrow> _")
1.95 proof -
1.96 assume ?P
1.97 @@ -59,8 +76,8 @@
1.98 qed
1.99
1.100 lemma app_left_1:
1.101 - "is2 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2> \<Longrightarrow>
1.102 - is1 @ is2 \<turnstile> <s1,size is1+i1> -1\<rightarrow> <s2,size is1+i2>"
1.103 + "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
1.104 + is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
1.105 (is "?P \<Longrightarrow> _")
1.106 proof -
1.107 assume ?P
1.108 @@ -71,176 +88,181 @@
1.109 declare rtrancl_induct2 [induct set: rtrancl]
1.110
1.111 lemma app_right:
1.112 - "is1 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow> is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2>"
1.113 + "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.114 (is "?P \<Longrightarrow> _")
1.115 proof -
1.116 assume ?P
1.117 then show ?thesis
1.118 proof induct
1.119 - show "is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s1,i1>" by simp
1.120 + show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
1.121 next
1.122 fix s1' i1' s2 i2
1.123 - assume "is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s1',i1'>"
1.124 - "is1 \<turnstile> <s1',i1'> -1\<rightarrow> <s2,i2>"
1.125 - thus "is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2>"
1.126 + assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
1.127 + "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
1.128 + thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
1.129 by(blast intro:app_right_1 rtrancl_trans)
1.130 qed
1.131 qed
1.132
1.133 lemma app_left:
1.134 - "is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow>
1.135 - is1 @ is2 \<turnstile> <s1,size is1+i1> -*\<rightarrow> <s2,size is1+i2>"
1.136 + "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
1.137 + is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
1.138 (is "?P \<Longrightarrow> _")
1.139 proof -
1.140 assume ?P
1.141 then show ?thesis
1.142 proof induct
1.143 - show "is1 @ is2 \<turnstile> <s1,length is1 + i1> -*\<rightarrow> <s1,length is1 + i1>" by simp
1.144 + show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
1.145 next
1.146 fix s1' i1' s2 i2
1.147 - assume "is1 @ is2 \<turnstile> <s1,length is1 + i1> -*\<rightarrow> <s1',length is1 + i1'>"
1.148 - "is2 \<turnstile> <s1',i1'> -1\<rightarrow> <s2,i2>"
1.149 - thus "is1 @ is2 \<turnstile> <s1,length is1 + i1> -*\<rightarrow> <s2,length is1 + i2>"
1.150 + assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
1.151 + "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
1.152 + thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
1.153 by(blast intro:app_left_1 rtrancl_trans)
1.154 qed
1.155 qed
1.156
1.157 lemma app_left2:
1.158 - "\<lbrakk> is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
1.159 - is1 @ is2 \<turnstile> <s1,j1> -*\<rightarrow> <s2,j2>"
1.160 -by (simp add:app_left)
1.161 + "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
1.162 + is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
1.163 + by (simp add:app_left)
1.164
1.165 lemma app1_left:
1.166 - "is \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow>
1.167 - instr # is \<turnstile> <s1,Suc i1> -*\<rightarrow> <s2,Suc i2>"
1.168 -by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
1.169 + "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
1.170 + instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
1.171 + by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
1.172 +
1.173 +subsection "Compiler correctness"
1.174
1.175 declare rtrancl_into_rtrancl[trans]
1.176 rtrancl_into_rtrancl2[trans]
1.177 rtrancl_trans[trans]
1.178 -(* The first proof; statement very intuitive,
1.179 - but application of induction hypothesis requires the above lifting lemmas
1.180 -*)
1.181 -theorem "<c,s> -c-> t \<Longrightarrow> compile c \<turnstile> <s,0> -*\<rightarrow> <t,length(compile c)>"
1.182 +
1.183 +text {*
1.184 + The first proof; The statement is very intuitive,
1.185 + but application of induction hypothesis requires the above lifting lemmas
1.186 +*}
1.187 +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.188 (is "?P \<Longrightarrow> ?Q c s t")
1.189 proof -
1.190 assume ?P
1.191 then show ?thesis
1.192 proof induct
1.193 - show "\<And>s. ?Q SKIP s s" by simp
1.194 + show "\<And>s. ?Q \<SKIP> s s" by simp
1.195 next
1.196 - show "\<And>a s x. ?Q (x :== a) s (s[x::= a s])" by force
1.197 + show "\<And>a s x. ?Q (x :== a) s (s[x\<mapsto> a s])" by force
1.198 next
1.199 fix c0 c1 s0 s1 s2
1.200 assume "?Q c0 s0 s1"
1.201 - hence "compile c0 @ compile c1 \<turnstile> <s0,0> -*\<rightarrow> <s1,length(compile c0)>"
1.202 + hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
1.203 by(rule app_right)
1.204 moreover assume "?Q c1 s1 s2"
1.205 - hence "compile c0 @ compile c1 \<turnstile> <s1,length(compile c0)> -*\<rightarrow>
1.206 - <s2,length(compile c0)+length(compile c1)>"
1.207 + hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
1.208 + \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
1.209 proof -
1.210 note app_left[of _ 0]
1.211 thus
1.212 - "\<And>is1 is2 s1 s2 i2.
1.213 - is2 \<turnstile> <s1,0> -*\<rightarrow> <s2,i2> \<Longrightarrow>
1.214 - is1 @ is2 \<turnstile> <s1,size is1> -*\<rightarrow> <s2,size is1+i2>"
1.215 - by simp
1.216 + "\<And>is1 is2 s1 s2 i2.
1.217 + is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
1.218 + is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
1.219 + by simp
1.220 qed
1.221 - ultimately have "compile c0 @ compile c1 \<turnstile> <s0,0> -*\<rightarrow>
1.222 - <s2,length(compile c0)+length(compile c1)>"
1.223 + ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
1.224 + \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
1.225 by (rule rtrancl_trans)
1.226 thus "?Q (c0; c1) s0 s2" by simp
1.227 next
1.228 fix b c0 c1 s0 s1
1.229 - let ?comp = "compile(IF b THEN c0 ELSE c1)"
1.230 + let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
1.231 assume "b s0" and IH: "?Q c0 s0 s1"
1.232 - hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,1>" by auto
1.233 + hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
1.234 also from IH
1.235 - have "?comp \<turnstile> <s0,1> -*\<rightarrow> <s1,length(compile c0)+1>"
1.236 + have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
1.237 by(auto intro:app1_left app_right)
1.238 - also have "?comp \<turnstile> <s1,length(compile c0)+1> -1\<rightarrow> <s1,length ?comp>"
1.239 + also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
1.240 by(auto)
1.241 - finally show "?Q (IF b THEN c0 ELSE c1) s0 s1" .
1.242 + finally show "?Q (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
1.243 next
1.244 fix b c0 c1 s0 s1
1.245 - let ?comp = "compile(IF b THEN c0 ELSE c1)"
1.246 + let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
1.247 assume "\<not>b s0" and IH: "?Q c1 s0 s1"
1.248 - hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,length(compile c0) + 2>" by auto
1.249 + hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
1.250 also from IH
1.251 - have "?comp \<turnstile> <s0,length(compile c0)+2> -*\<rightarrow> <s1,length ?comp>"
1.252 + have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
1.253 by(force intro!:app_left2 app1_left)
1.254 - finally show "?Q (IF b THEN c0 ELSE c1) s0 s1" .
1.255 + finally show "?Q (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
1.256 next
1.257 fix b c and s::state
1.258 assume "\<not>b s"
1.259 - thus "?Q (WHILE b DO c) s s" by force
1.260 + thus "?Q (\<WHILE> b \<DO> c) s s" by force
1.261 next
1.262 fix b c and s0::state and s1 s2
1.263 - let ?comp = "compile(WHILE b DO c)"
1.264 + let ?comp = "compile(\<WHILE> b \<DO> c)"
1.265 assume "b s0" and
1.266 - IHc: "?Q c s0 s1" and IHw: "?Q (WHILE b DO c) s1 s2"
1.267 - hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,1>" by auto
1.268 + IHc: "?Q c s0 s1" and IHw: "?Q (\<WHILE> b \<DO> c) s1 s2"
1.269 + hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
1.270 also from IHc
1.271 - have "?comp \<turnstile> <s0,1> -*\<rightarrow> <s1,length(compile c)+1>"
1.272 + have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
1.273 by(auto intro:app1_left app_right)
1.274 - also have "?comp \<turnstile> <s1,length(compile c)+1> -1\<rightarrow> <s1,0>" by simp
1.275 + also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
1.276 also note IHw
1.277 - finally show "?Q (WHILE b DO c) s0 s2".
1.278 + finally show "?Q (\<WHILE> b \<DO> c) s0 s2".
1.279 qed
1.280 qed
1.281
1.282 -(* Second proof; statement is generalized to cater for prefixes and suffixes;
1.283 - needs none of the lifting lemmas, but instantiations of pre/suffix.
1.284 -*)
1.285 -theorem "<c,s> -c-> t ==>
1.286 - !a z. a@compile c@z \<turnstile> <s,length a> -*\<rightarrow> <t,length a + length(compile c)>";
1.287 -apply(erule evalc.induct);
1.288 - apply simp;
1.289 - apply(force intro!: ASIN);
1.290 - apply(intro strip);
1.291 - apply(erule_tac x = a in allE);
1.292 - apply(erule_tac x = "a@compile c0" in allE);
1.293 - apply(erule_tac x = "compile c1@z" in allE);
1.294 - apply(erule_tac x = z in allE);
1.295 - apply(simp add:add_assoc[THEN sym]);
1.296 - apply(blast intro:rtrancl_trans);
1.297 -(* IF b THEN c0 ELSE c1; case b is true *)
1.298 - apply(intro strip);
1.299 +text {*
1.300 + Second proof; statement is generalized to cater for prefixes and suffixes;
1.301 + needs none of the lifting lemmas, but instantiations of pre/suffix.
1.302 + *}
1.303 +theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow>
1.304 + !a z. a@compile c@z \<turnstile> \<langle>s,length a\<rangle> -*\<rightarrow> \<langle>t,length a + length(compile c)\<rangle>";
1.305 +apply(erule evalc.induct)
1.306 + apply simp
1.307 + apply(force intro!: ASIN)
1.308 + apply(intro strip)
1.309 + apply(erule_tac x = a in allE)
1.310 + apply(erule_tac x = "a@compile c0" in allE)
1.311 + apply(erule_tac x = "compile c1@z" in allE)
1.312 + apply(erule_tac x = z in allE)
1.313 + apply(simp add:add_assoc[THEN sym])
1.314 + apply(blast intro:rtrancl_trans)
1.315 +(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
1.316 + apply(intro strip)
1.317 (* instantiate assumption sufficiently for later: *)
1.318 - apply(erule_tac x = "a@[?I]" in allE);
1.319 - apply(simp);
1.320 + apply(erule_tac x = "a@[?I]" in allE)
1.321 + apply(simp)
1.322 (* execute JMPF: *)
1.323 - apply(rule rtrancl_into_rtrancl2);
1.324 - apply(force intro!: JMPFT);
1.325 + apply(rule rtrancl_into_rtrancl2)
1.326 + apply(force intro!: JMPFT)
1.327 (* execute compile c0: *)
1.328 - apply(rule rtrancl_trans);
1.329 - apply(erule allE);
1.330 - apply assumption;
1.331 + apply(rule rtrancl_trans)
1.332 + apply(erule allE)
1.333 + apply assumption
1.334 (* execute JMPF: *)
1.335 - apply(rule r_into_rtrancl);
1.336 - apply(force intro!: JMPFF);
1.337 + apply(rule r_into_rtrancl)
1.338 + apply(force intro!: JMPFF)
1.339 (* end of case b is true *)
1.340 - apply(intro strip);
1.341 - apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE);
1.342 - apply(simp add:add_assoc);
1.343 - apply(rule rtrancl_into_rtrancl2);
1.344 - apply(force intro!: JMPFF);
1.345 - apply(blast);
1.346 - apply(force intro: JMPFF);
1.347 -apply(intro strip);
1.348 -apply(erule_tac x = "a@[?I]" in allE);
1.349 -apply(erule_tac x = a in allE);
1.350 -apply(simp);
1.351 -apply(rule rtrancl_into_rtrancl2);
1.352 - apply(force intro!: JMPFT);
1.353 -apply(rule rtrancl_trans);
1.354 - apply(erule allE);
1.355 - apply assumption;
1.356 -apply(rule rtrancl_into_rtrancl2);
1.357 - apply(force intro!: JMPB);
1.358 -apply(simp);
1.359 + apply(intro strip)
1.360 + apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
1.361 + apply(simp add:add_assoc)
1.362 + apply(rule rtrancl_into_rtrancl2)
1.363 + apply(force intro!: JMPFF)
1.364 + apply(blast)
1.365 + apply(force intro: JMPFF)
1.366 +apply(intro strip)
1.367 +apply(erule_tac x = "a@[?I]" in allE)
1.368 +apply(erule_tac x = a in allE)
1.369 +apply(simp)
1.370 +apply(rule rtrancl_into_rtrancl2)
1.371 + apply(force intro!: JMPFT)
1.372 +apply(rule rtrancl_trans)
1.373 + apply(erule allE)
1.374 + apply assumption
1.375 +apply(rule rtrancl_into_rtrancl2)
1.376 + apply(force intro!: JMPB)
1.377 +apply(simp)
1.378 done
1.379
1.380 -(* Missing: the other direction! *)
1.381 +text {* Missing: the other direction! *}
1.382
1.383 end