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