nipkow@10343
|
1 |
(* Title: HOL/IMP/Compiler.thy
|
nipkow@10343
|
2 |
ID: $Id$
|
nipkow@10343
|
3 |
Author: Tobias Nipkow, TUM
|
nipkow@10343
|
4 |
Copyright 1996 TUM
|
kleing@12429
|
5 |
*)
|
nipkow@10343
|
6 |
|
nipkow@13095
|
7 |
theory Compiler = Machines:
|
nipkow@10342
|
8 |
|
kleing@12429
|
9 |
subsection "The compiler"
|
kleing@12429
|
10 |
|
kleing@12429
|
11 |
consts compile :: "com \<Rightarrow> instr list"
|
nipkow@10342
|
12 |
primrec
|
kleing@12429
|
13 |
"compile \<SKIP> = []"
|
nipkow@13675
|
14 |
"compile (x:==a) = [SET x a]"
|
nipkow@10342
|
15 |
"compile (c1;c2) = compile c1 @ compile c2"
|
kleing@12429
|
16 |
"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
|
nipkow@13095
|
17 |
[JMPF b (length(compile c1) + 1)] @ compile c1 @
|
nipkow@13675
|
18 |
[JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
|
nipkow@13095
|
19 |
"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
|
nipkow@10342
|
20 |
[JMPB (length(compile c)+1)]"
|
nipkow@10342
|
21 |
|
kleing@12429
|
22 |
subsection "Compiler correctness"
|
nipkow@11275
|
23 |
|
nipkow@13095
|
24 |
theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
|
nipkow@13095
|
25 |
shows "\<And>p q. \<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle>"
|
nipkow@13095
|
26 |
(is "\<And>p q. ?P c s t p q")
|
nipkow@12275
|
27 |
proof -
|
nipkow@13095
|
28 |
from A show "\<And>p q. ?thesis p q"
|
nipkow@12275
|
29 |
proof induct
|
nipkow@13095
|
30 |
case Skip thus ?case by simp
|
nipkow@12275
|
31 |
next
|
nipkow@13095
|
32 |
case Assign thus ?case by force
|
nipkow@12275
|
33 |
next
|
nipkow@13095
|
34 |
case Semi thus ?case by simp (blast intro:rtrancl_trans)
|
nipkow@12275
|
35 |
next
|
nipkow@13095
|
36 |
fix b c0 c1 s0 s1 p q
|
nipkow@13095
|
37 |
assume IH: "\<And>p q. ?P c0 s0 s1 p q"
|
nipkow@13095
|
38 |
assume "b s0"
|
nipkow@13095
|
39 |
thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
|
nipkow@13095
|
40 |
by(simp add: IH[THEN rtrancl_trans])
|
nipkow@12275
|
41 |
next
|
nipkow@13095
|
42 |
case IfFalse thus ?case by(simp)
|
nipkow@12275
|
43 |
next
|
nipkow@13095
|
44 |
case WhileFalse thus ?case by simp
|
nipkow@12275
|
45 |
next
|
nipkow@13095
|
46 |
fix b c and s0::state and s1 s2 p q
|
nipkow@13095
|
47 |
assume b: "b s0" and
|
nipkow@13095
|
48 |
IHc: "\<And>p q. ?P c s0 s1 p q" and
|
nipkow@13095
|
49 |
IHw: "\<And>p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
|
nipkow@13095
|
50 |
show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
|
nipkow@13095
|
51 |
using b IHc[THEN rtrancl_trans] IHw by(simp)
|
nipkow@12275
|
52 |
qed
|
nipkow@12275
|
53 |
qed
|
nipkow@11275
|
54 |
|
nipkow@13095
|
55 |
text {* The other direction! *}
|
nipkow@13095
|
56 |
|
nipkow@13095
|
57 |
inductive_cases [elim!]: "(([],p,s),next) : stepa1"
|
nipkow@13095
|
58 |
|
nipkow@13095
|
59 |
lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
|
nipkow@13095
|
60 |
apply(rule iffI)
|
nipkow@13095
|
61 |
apply(erule converse_rel_powE, simp, fast)
|
nipkow@13095
|
62 |
apply simp
|
nipkow@10342
|
63 |
done
|
nipkow@10342
|
64 |
|
nipkow@13095
|
65 |
lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
|
nipkow@13095
|
66 |
by(simp add: rtrancl_is_UN_rel_pow)
|
nipkow@10342
|
67 |
|
nipkow@13095
|
68 |
constdefs
|
nipkow@13095
|
69 |
forws :: "instr \<Rightarrow> nat set"
|
nipkow@13095
|
70 |
"forws instr == case instr of
|
nipkow@13675
|
71 |
SET x a \<Rightarrow> {0} |
|
nipkow@13095
|
72 |
JMPF b n \<Rightarrow> {0,n} |
|
nipkow@13095
|
73 |
JMPB n \<Rightarrow> {}"
|
nipkow@13095
|
74 |
backws :: "instr \<Rightarrow> nat set"
|
nipkow@13095
|
75 |
"backws instr == case instr of
|
nipkow@13675
|
76 |
SET x a \<Rightarrow> {} |
|
nipkow@13095
|
77 |
JMPF b n \<Rightarrow> {} |
|
nipkow@13095
|
78 |
JMPB n \<Rightarrow> {n}"
|
nipkow@13095
|
79 |
|
nipkow@13095
|
80 |
consts closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
|
nipkow@13095
|
81 |
primrec
|
nipkow@13095
|
82 |
"closed m n [] = True"
|
nipkow@13095
|
83 |
"closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
|
nipkow@13095
|
84 |
(\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
|
nipkow@13095
|
85 |
|
nipkow@13095
|
86 |
lemma [simp]:
|
nipkow@13095
|
87 |
"\<And>m n. closed m n (C1@C2) =
|
nipkow@13095
|
88 |
(closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
|
obua@14738
|
89 |
by(induct C1, simp, simp add:add_ac)
|
nipkow@13095
|
90 |
|
nipkow@13095
|
91 |
theorem [simp]: "\<And>m n. closed m n (compile c)"
|
nipkow@13095
|
92 |
by(induct c, simp_all add:backws_def forws_def)
|
nipkow@13095
|
93 |
|
nipkow@13095
|
94 |
lemma drop_lem: "n \<le> size(p1@p2)
|
nipkow@13095
|
95 |
\<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
|
nipkow@13095
|
96 |
(n \<le> size p1 & p1' = drop n p1)"
|
nipkow@13095
|
97 |
apply(rule iffI)
|
nipkow@13095
|
98 |
defer apply simp
|
nipkow@13095
|
99 |
apply(subgoal_tac "n \<le> size p1")
|
nipkow@13095
|
100 |
apply simp
|
nipkow@13095
|
101 |
apply(rule ccontr)
|
nipkow@13095
|
102 |
apply(drule_tac f = length in arg_cong)
|
nipkow@13095
|
103 |
apply simp
|
nipkow@13095
|
104 |
apply arith
|
nipkow@13095
|
105 |
done
|
nipkow@13095
|
106 |
|
nipkow@13095
|
107 |
lemma reduce_exec1:
|
nipkow@13095
|
108 |
"\<langle>i # p1 @ p2,q1 @ q2,s\<rangle> -1\<rightarrow> \<langle>p1' @ p2,q1' @ q2,s'\<rangle> \<Longrightarrow>
|
nipkow@13095
|
109 |
\<langle>i # p1,q1,s\<rangle> -1\<rightarrow> \<langle>p1',q1',s'\<rangle>"
|
nipkow@13095
|
110 |
by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm)
|
nipkow@13095
|
111 |
|
nipkow@13095
|
112 |
|
nipkow@13095
|
113 |
lemma closed_exec1:
|
nipkow@13095
|
114 |
"\<lbrakk> closed 0 0 (rev q1 @ instr # p1);
|
nipkow@13095
|
115 |
\<langle>instr # p1 @ p2, q1 @ q2,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle> \<rbrakk> \<Longrightarrow>
|
nipkow@13095
|
116 |
\<exists>p1' q1'. p' = p1'@p2 \<and> q' = q1'@q2 \<and> rev q1' @ p1' = rev q1 @ instr # p1"
|
nipkow@13095
|
117 |
apply(clarsimp simp add:forws_def backws_def
|
nipkow@13095
|
118 |
split:instr.split_asm split_if_asm)
|
nipkow@13095
|
119 |
done
|
nipkow@13095
|
120 |
|
nipkow@13095
|
121 |
theorem closed_execn_decomp: "\<And>C1 C2 r.
|
nipkow@13095
|
122 |
\<lbrakk> closed 0 0 (rev C1 @ C2);
|
nipkow@13095
|
123 |
\<langle>C2 @ p1 @ p2, C1 @ q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<rbrakk>
|
nipkow@13095
|
124 |
\<Longrightarrow> \<exists>s n1 n2. \<langle>C2,C1,r\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle> \<and>
|
nipkow@13095
|
125 |
\<langle>p1@p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
|
nipkow@13095
|
126 |
n = n1+n2"
|
nipkow@13095
|
127 |
(is "\<And>C1 C2 r. \<lbrakk>?CL C1 C2; ?H C1 C2 r n\<rbrakk> \<Longrightarrow> ?P C1 C2 r n")
|
nipkow@13095
|
128 |
proof(induct n)
|
nipkow@13095
|
129 |
fix C1 C2 r
|
nipkow@13095
|
130 |
assume "?H C1 C2 r 0"
|
nipkow@13095
|
131 |
thus "?P C1 C2 r 0" by simp
|
nipkow@13095
|
132 |
next
|
nipkow@13095
|
133 |
fix C1 C2 r n
|
nipkow@13095
|
134 |
assume IH: "\<And>C1 C2 r. ?CL C1 C2 \<Longrightarrow> ?H C1 C2 r n \<Longrightarrow> ?P C1 C2 r n"
|
nipkow@13095
|
135 |
assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
|
nipkow@13095
|
136 |
show "?P C1 C2 r (Suc n)"
|
nipkow@13095
|
137 |
proof (cases C2)
|
nipkow@13095
|
138 |
assume "C2 = []" with H show ?thesis by simp
|
nipkow@13095
|
139 |
next
|
nipkow@13095
|
140 |
fix instr tlC2
|
nipkow@13095
|
141 |
assume C2: "C2 = instr # tlC2"
|
nipkow@13095
|
142 |
from H C2 obtain p' q' r'
|
nipkow@13095
|
143 |
where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
|
nipkow@13095
|
144 |
and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
|
nipkow@13095
|
145 |
by(fastsimp simp add:R_O_Rn_commute)
|
nipkow@13095
|
146 |
from CL closed_exec1[OF _ 1] C2
|
nipkow@13095
|
147 |
obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
|
nipkow@13095
|
148 |
and same: "rev C1' @ C2' = rev C1 @ C2"
|
nipkow@13095
|
149 |
by fastsimp
|
nipkow@13095
|
150 |
have rev_same: "rev C2' @ C1' = rev C2 @ C1"
|
nipkow@13095
|
151 |
proof -
|
nipkow@13095
|
152 |
have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
|
nipkow@13095
|
153 |
also have "\<dots> = rev(rev C1 @ C2)" by(simp only:same)
|
nipkow@13095
|
154 |
also have "\<dots> = rev C2 @ C1" by simp
|
nipkow@13095
|
155 |
finally show ?thesis .
|
nipkow@13095
|
156 |
qed
|
nipkow@13095
|
157 |
hence rev_same': "\<And>p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
|
nipkow@13095
|
158 |
from n have n': "\<langle>C2' @ p1 @ p2,C1' @ q,r'\<rangle> -n\<rightarrow>
|
nipkow@13095
|
159 |
\<langle>p2,rev p1 @ rev C2' @ C1' @ q,t\<rangle>"
|
nipkow@13095
|
160 |
by(simp add:pq' rev_same')
|
nipkow@13095
|
161 |
from IH[OF _ n'] CL
|
nipkow@13095
|
162 |
obtain s n1 n2 where n1: "\<langle>C2',C1',r'\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>" and
|
nipkow@13095
|
163 |
"\<langle>p1 @ p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
|
nipkow@13095
|
164 |
n = n1 + n2"
|
nipkow@13095
|
165 |
by(fastsimp simp add: same rev_same rev_same')
|
nipkow@13095
|
166 |
moreover
|
nipkow@13095
|
167 |
from 1 n1 pq' C2 have "\<langle>C2,C1,r\<rangle> -Suc n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>"
|
nipkow@13095
|
168 |
by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
|
nipkow@13095
|
169 |
ultimately show ?thesis by (fastsimp simp del:relpow.simps)
|
nipkow@13095
|
170 |
qed
|
nipkow@13095
|
171 |
qed
|
nipkow@13095
|
172 |
|
nipkow@13095
|
173 |
lemma execn_decomp:
|
nipkow@13095
|
174 |
"\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
|
nipkow@13095
|
175 |
\<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
|
nipkow@13095
|
176 |
\<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
|
nipkow@13095
|
177 |
n = n1+n2"
|
nipkow@13095
|
178 |
using closed_execn_decomp[of "[]",simplified] by simp
|
nipkow@13095
|
179 |
|
nipkow@13095
|
180 |
lemma exec_star_decomp:
|
nipkow@13095
|
181 |
"\<langle>compile c @ p1 @ p2,q,r\<rangle> -*\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
|
nipkow@13095
|
182 |
\<Longrightarrow> \<exists>s. \<langle>compile c,[],r\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
|
nipkow@13095
|
183 |
\<langle>p1@p2,rev(compile c) @ q,s\<rangle> -*\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle>"
|
nipkow@13095
|
184 |
by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)
|
nipkow@13095
|
185 |
|
nipkow@13095
|
186 |
|
nipkow@13095
|
187 |
(* Alternative:
|
nipkow@13095
|
188 |
lemma exec_comp_n:
|
nipkow@13095
|
189 |
"\<And>p1 p2 q r t n.
|
nipkow@13095
|
190 |
\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
|
nipkow@13095
|
191 |
\<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
|
nipkow@13095
|
192 |
\<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
|
nipkow@13095
|
193 |
n = n1+n2"
|
nipkow@13095
|
194 |
(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")
|
nipkow@13095
|
195 |
proof (induct c)
|
nipkow@13095
|
196 |
*)
|
nipkow@13095
|
197 |
|
nipkow@13095
|
198 |
text{*Warning:
|
nipkow@13095
|
199 |
@{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"}
|
nipkow@13095
|
200 |
is not true! *}
|
nipkow@13095
|
201 |
|
nipkow@13095
|
202 |
theorem "\<And>s t.
|
nipkow@13095
|
203 |
\<langle>compile c,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
|
nipkow@13095
|
204 |
proof (induct c)
|
nipkow@13095
|
205 |
fix s t
|
nipkow@13095
|
206 |
assume "\<langle>compile SKIP,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile SKIP),t\<rangle>"
|
nipkow@13095
|
207 |
thus "\<langle>SKIP,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
|
nipkow@13095
|
208 |
next
|
nipkow@13095
|
209 |
fix s t v f
|
nipkow@13095
|
210 |
assume "\<langle>compile(v :== f),[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile(v :== f)),t\<rangle>"
|
nipkow@13095
|
211 |
thus "\<langle>v :== f,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
|
nipkow@13095
|
212 |
next
|
nipkow@13095
|
213 |
fix s1 s3 c1 c2
|
nipkow@13095
|
214 |
let ?C1 = "compile c1" let ?C2 = "compile c2"
|
nipkow@13095
|
215 |
assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
|
nipkow@13095
|
216 |
and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
|
nipkow@13095
|
217 |
assume "\<langle>compile(c1;c2),[],s1\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
|
nipkow@13095
|
218 |
then obtain s2 where exec1: "\<langle>?C1,[],s1\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,s2\<rangle>" and
|
nipkow@13095
|
219 |
exec2: "\<langle>?C2,rev ?C1,s2\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
|
nipkow@13095
|
220 |
by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
|
nipkow@13095
|
221 |
from exec2 have exec2': "\<langle>?C2,[],s2\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,s3\<rangle>"
|
nipkow@13095
|
222 |
using exec_star_decomp[of _ "[]" "[]"] by fastsimp
|
nipkow@13095
|
223 |
have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>c s2" using IH1 exec1 by simp
|
nipkow@13095
|
224 |
moreover have "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>c s3" using IH2 exec2' by fastsimp
|
nipkow@13095
|
225 |
ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>c s3" ..
|
nipkow@13095
|
226 |
next
|
nipkow@13095
|
227 |
fix s t b c1 c2
|
nipkow@13095
|
228 |
let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
|
nipkow@13095
|
229 |
let ?C1 = "compile c1" let ?C2 = "compile c2"
|
nipkow@13095
|
230 |
assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
|
nipkow@13095
|
231 |
and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
|
nipkow@13095
|
232 |
and H: "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle>"
|
nipkow@13095
|
233 |
show "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>c t"
|
nipkow@13095
|
234 |
proof cases
|
nipkow@13095
|
235 |
assume b: "b s"
|
nipkow@13095
|
236 |
with H have "\<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle>"
|
nipkow@13095
|
237 |
by (fastsimp dest:exec_star_decomp
|
nipkow@13095
|
238 |
[of _ "[JMPF (\<lambda>x. False) (size ?C2)]@?C2" "[]",simplified])
|
nipkow@13095
|
239 |
hence "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH1)
|
nipkow@13095
|
240 |
with b show ?thesis ..
|
nipkow@13095
|
241 |
next
|
nipkow@13095
|
242 |
assume b: "\<not> b s"
|
nipkow@13095
|
243 |
with H have "\<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle>"
|
nipkow@13095
|
244 |
using exec_star_decomp[of _ "[]" "[]"] by simp
|
nipkow@13095
|
245 |
hence "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH2)
|
nipkow@13095
|
246 |
with b show ?thesis ..
|
nipkow@13095
|
247 |
qed
|
nipkow@13095
|
248 |
next
|
nipkow@13095
|
249 |
fix b c s t
|
nipkow@13095
|
250 |
let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
|
nipkow@13095
|
251 |
let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
|
nipkow@13095
|
252 |
assume IHc: "\<And>s t. \<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
|
nipkow@13095
|
253 |
and H: "\<langle>?W,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
|
nipkow@13095
|
254 |
from H obtain k where ob:"\<langle>?W,[],s\<rangle> -k\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
|
nipkow@13095
|
255 |
by(simp add:rtrancl_is_UN_rel_pow) blast
|
nipkow@13095
|
256 |
{ 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"
|
nipkow@13095
|
257 |
proof (induct n rule: less_induct)
|
nipkow@13095
|
258 |
fix n
|
nipkow@13095
|
259 |
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"
|
nipkow@13095
|
260 |
fix s
|
nipkow@13095
|
261 |
assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
|
nipkow@13095
|
262 |
show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
|
nipkow@13095
|
263 |
proof cases
|
nipkow@13095
|
264 |
assume b: "b s"
|
nipkow@13095
|
265 |
then obtain m where m: "n = Suc m"
|
nipkow@13675
|
266 |
and "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
|
nipkow@13095
|
267 |
using H by fastsimp
|
nipkow@13095
|
268 |
then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
|
nipkow@13095
|
269 |
and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
|
nipkow@13095
|
270 |
and n12: "m = n1+n2"
|
nipkow@13095
|
271 |
using execn_decomp[of _ "[?j2]"]
|
nipkow@13095
|
272 |
by(simp del: execn_simp) fast
|
nipkow@13095
|
273 |
have n2n: "n2 - 1 < n" using m n12 by arith
|
nipkow@13095
|
274 |
note b
|
nipkow@13095
|
275 |
moreover
|
nipkow@13095
|
276 |
{ from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
|
nipkow@13095
|
277 |
by (simp add:rtrancl_is_UN_rel_pow) fast
|
nipkow@13095
|
278 |
hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
|
nipkow@13095
|
279 |
}
|
nipkow@13095
|
280 |
moreover
|
nipkow@13095
|
281 |
{ have "n2 - 1 < n" using m n12 by arith
|
nipkow@13095
|
282 |
moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
|
nipkow@13095
|
283 |
ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
|
nipkow@13095
|
284 |
}
|
nipkow@13095
|
285 |
ultimately show ?thesis ..
|
nipkow@13095
|
286 |
next
|
nipkow@13095
|
287 |
assume b: "\<not> b s"
|
nipkow@13095
|
288 |
hence "t = s" using H by simp
|
nipkow@13095
|
289 |
with b show ?thesis by simp
|
nipkow@13095
|
290 |
qed
|
nipkow@13095
|
291 |
qed
|
nipkow@13095
|
292 |
}
|
nipkow@13095
|
293 |
with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
|
nipkow@13095
|
294 |
qed
|
nipkow@13095
|
295 |
|
nipkow@13095
|
296 |
(* To Do: connect with Machine 0 using M_equiv *)
|
nipkow@13095
|
297 |
|
nipkow@13095
|
298 |
end |