|
1 (* Title: HOL/IMP/Compiler.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, TUM |
|
4 Copyright 1996 TUM |
|
5 |
|
6 This is an early version of the compiler, where the abstract machine |
|
7 has an explicit pc. This turned out to be awkward, and a second |
|
8 development was started. See Machines.thy and Compiler.thy. |
|
9 *) |
|
10 |
|
11 header "A Simple Compiler" |
|
12 |
|
13 theory Compiler0 = Natural: |
|
14 |
|
15 subsection "An abstract, simplistic machine" |
|
16 |
|
17 text {* There are only three instructions: *} |
|
18 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat |
|
19 |
|
20 text {* We describe execution of programs in the machine by |
|
21 an operational (small step) semantics: |
|
22 *} |
|
23 consts stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set" |
|
24 |
|
25 syntax |
|
26 "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
|
27 ("_ |- (3<_,_>/ -1-> <_,_>)" [50,0,0,0,0] 50) |
|
28 "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
|
29 ("_ |-/ (3<_,_>/ -*-> <_,_>)" [50,0,0,0,0] 50) |
|
30 |
|
31 "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool" |
|
32 ("_ |-/ (3<_,_>/ -(_)-> <_,_>)" [50,0,0,0,0,0] 50) |
|
33 |
|
34 syntax (xsymbols) |
|
35 "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
|
36 ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50) |
|
37 "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
|
38 ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50) |
|
39 "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool" |
|
40 ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50) |
|
41 |
|
42 translations |
|
43 "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P" |
|
44 "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)" |
|
45 "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^i)" |
|
46 |
|
47 inductive "stepa1 P" |
|
48 intros |
|
49 ASIN[simp]: |
|
50 "\<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>" |
|
51 JMPFT[simp,intro]: |
|
52 "\<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>" |
|
53 JMPFF[simp,intro]: |
|
54 "\<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>" |
|
55 JMPB[simp]: |
|
56 "\<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>" |
|
57 |
|
58 subsection "The compiler" |
|
59 |
|
60 consts compile :: "com \<Rightarrow> instr list" |
|
61 primrec |
|
62 "compile \<SKIP> = []" |
|
63 "compile (x:==a) = [ASIN x a]" |
|
64 "compile (c1;c2) = compile c1 @ compile c2" |
|
65 "compile (\<IF> b \<THEN> c1 \<ELSE> c2) = |
|
66 [JMPF b (length(compile c1) + 2)] @ compile c1 @ |
|
67 [JMPF (%x. False) (length(compile c2)+1)] @ compile c2" |
|
68 "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @ |
|
69 [JMPB (length(compile c)+1)]" |
|
70 |
|
71 declare nth_append[simp] |
|
72 |
|
73 subsection "Context lifting lemmas" |
|
74 |
|
75 text {* |
|
76 Some lemmas for lifting an execution into a prefix and suffix |
|
77 of instructions; only needed for the first proof. |
|
78 *} |
|
79 lemma app_right_1: |
|
80 assumes A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>" |
|
81 shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>" |
|
82 proof - |
|
83 from A show ?thesis |
|
84 by induct force+ |
|
85 qed |
|
86 |
|
87 lemma app_left_1: |
|
88 assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>" |
|
89 shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>" |
|
90 proof - |
|
91 from A show ?thesis |
|
92 by induct force+ |
|
93 qed |
|
94 |
|
95 declare rtrancl_induct2 [induct set: rtrancl] |
|
96 |
|
97 lemma app_right: |
|
98 assumes A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>" |
|
99 shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>" |
|
100 proof - |
|
101 from A show ?thesis |
|
102 proof induct |
|
103 show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp |
|
104 next |
|
105 fix s1' i1' s2 i2 |
|
106 assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>" |
|
107 "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>" |
|
108 thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>" |
|
109 by(blast intro:app_right_1 rtrancl_trans) |
|
110 qed |
|
111 qed |
|
112 |
|
113 lemma app_left: |
|
114 assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>" |
|
115 shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>" |
|
116 proof - |
|
117 from A show ?thesis |
|
118 proof induct |
|
119 show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp |
|
120 next |
|
121 fix s1' i1' s2 i2 |
|
122 assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>" |
|
123 "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>" |
|
124 thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>" |
|
125 by(blast intro:app_left_1 rtrancl_trans) |
|
126 qed |
|
127 qed |
|
128 |
|
129 lemma app_left2: |
|
130 "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow> |
|
131 is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>" |
|
132 by (simp add:app_left) |
|
133 |
|
134 lemma app1_left: |
|
135 "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow> |
|
136 instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>" |
|
137 by(erule app_left[of _ _ _ _ _ "[instr]",simplified]) |
|
138 |
|
139 subsection "Compiler correctness" |
|
140 |
|
141 declare rtrancl_into_rtrancl[trans] |
|
142 converse_rtrancl_into_rtrancl[trans] |
|
143 rtrancl_trans[trans] |
|
144 |
|
145 text {* |
|
146 The first proof; The statement is very intuitive, |
|
147 but application of induction hypothesis requires the above lifting lemmas |
|
148 *} |
|
149 theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" |
|
150 shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t") |
|
151 proof - |
|
152 from A show ?thesis |
|
153 proof induct |
|
154 show "\<And>s. ?P \<SKIP> s s" by simp |
|
155 next |
|
156 show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force |
|
157 next |
|
158 fix c0 c1 s0 s1 s2 |
|
159 assume "?P c0 s0 s1" |
|
160 hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>" |
|
161 by(rule app_right) |
|
162 moreover assume "?P c1 s1 s2" |
|
163 hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow> |
|
164 \<langle>s2,length(compile c0)+length(compile c1)\<rangle>" |
|
165 proof - |
|
166 show "\<And>is1 is2 s1 s2 i2. |
|
167 is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow> |
|
168 is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>" |
|
169 using app_left[of _ 0] by simp |
|
170 qed |
|
171 ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> |
|
172 \<langle>s2,length(compile c0)+length(compile c1)\<rangle>" |
|
173 by (rule rtrancl_trans) |
|
174 thus "?P (c0; c1) s0 s2" by simp |
|
175 next |
|
176 fix b c0 c1 s0 s1 |
|
177 let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)" |
|
178 assume "b s0" and IH: "?P c0 s0 s1" |
|
179 hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto |
|
180 also from IH |
|
181 have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>" |
|
182 by(auto intro:app1_left app_right) |
|
183 also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>" |
|
184 by(auto) |
|
185 finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" . |
|
186 next |
|
187 fix b c0 c1 s0 s1 |
|
188 let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)" |
|
189 assume "\<not>b s0" and IH: "?P c1 s0 s1" |
|
190 hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto |
|
191 also from IH |
|
192 have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>" |
|
193 by(force intro!:app_left2 app1_left) |
|
194 finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" . |
|
195 next |
|
196 fix b c and s::state |
|
197 assume "\<not>b s" |
|
198 thus "?P (\<WHILE> b \<DO> c) s s" by force |
|
199 next |
|
200 fix b c and s0::state and s1 s2 |
|
201 let ?comp = "compile(\<WHILE> b \<DO> c)" |
|
202 assume "b s0" and |
|
203 IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2" |
|
204 hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto |
|
205 also from IHc |
|
206 have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>" |
|
207 by(auto intro:app1_left app_right) |
|
208 also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp |
|
209 also note IHw |
|
210 finally show "?P (\<WHILE> b \<DO> c) s0 s2". |
|
211 qed |
|
212 qed |
|
213 |
|
214 text {* |
|
215 Second proof; statement is generalized to cater for prefixes and suffixes; |
|
216 needs none of the lifting lemmas, but instantiations of pre/suffix. |
|
217 *} |
|
218 theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> |
|
219 !a z. a@compile c@z \<turnstile> \<langle>s,length a\<rangle> -*\<rightarrow> \<langle>t,length a + length(compile c)\<rangle>"; |
|
220 apply(erule evalc.induct) |
|
221 apply simp |
|
222 apply(force intro!: ASIN) |
|
223 apply(intro strip) |
|
224 apply(erule_tac x = a in allE) |
|
225 apply(erule_tac x = "a@compile c0" in allE) |
|
226 apply(erule_tac x = "compile c1@z" in allE) |
|
227 apply(erule_tac x = z in allE) |
|
228 apply(simp add:add_assoc[THEN sym]) |
|
229 apply(blast intro:rtrancl_trans) |
|
230 (* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *) |
|
231 apply(intro strip) |
|
232 (* instantiate assumption sufficiently for later: *) |
|
233 apply(erule_tac x = "a@[?I]" in allE) |
|
234 apply(simp) |
|
235 (* execute JMPF: *) |
|
236 apply(rule converse_rtrancl_into_rtrancl) |
|
237 apply(force intro!: JMPFT) |
|
238 (* execute compile c0: *) |
|
239 apply(rule rtrancl_trans) |
|
240 apply(erule allE) |
|
241 apply assumption |
|
242 (* execute JMPF: *) |
|
243 apply(rule r_into_rtrancl) |
|
244 apply(force intro!: JMPFF) |
|
245 (* end of case b is true *) |
|
246 apply(intro strip) |
|
247 apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE) |
|
248 apply(simp add:add_assoc) |
|
249 apply(rule converse_rtrancl_into_rtrancl) |
|
250 apply(force intro!: JMPFF) |
|
251 apply(blast) |
|
252 apply(force intro: JMPFF) |
|
253 apply(intro strip) |
|
254 apply(erule_tac x = "a@[?I]" in allE) |
|
255 apply(erule_tac x = a in allE) |
|
256 apply(simp) |
|
257 apply(rule converse_rtrancl_into_rtrancl) |
|
258 apply(force intro!: JMPFT) |
|
259 apply(rule rtrancl_trans) |
|
260 apply(erule allE) |
|
261 apply assumption |
|
262 apply(rule converse_rtrancl_into_rtrancl) |
|
263 apply(force intro!: JMPB) |
|
264 apply(simp) |
|
265 done |
|
266 |
|
267 text {* Missing: the other direction! I did much of it, and although |
|
268 the main lemma is very similar to the one in the new development, the |
|
269 lemmas surrounding it seemed much more complicated. In the end I gave |
|
270 up. *} |
|
271 |
|
272 end |