1 (* Title: HOL/IMP/Compiler.thy
3 Author: Tobias Nipkow, TUM
7 header "A Simple Compiler"
9 theory Compiler = Natural:
11 subsection "An abstract, simplistic machine"
13 text {* There are only three instructions: *}
14 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
16 text {* We describe execution of programs in the machine by
17 an operational (small step) semantics:
19 consts stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
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)
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)
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)^*)"
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>"
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>"
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>"
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>"
48 subsection "The compiler"
50 consts compile :: "com \<Rightarrow> instr list"
52 "compile \<SKIP> = []"
53 "compile (x:==a) = [ASIN x a]"
54 "compile (c1;c2) = compile c1 @ compile c2"
55 "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
56 [JMPF b (length(compile c1) + 2)] @ compile c1 @
57 [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
58 "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
59 [JMPB (length(compile c)+1)]"
61 declare nth_append[simp]
63 subsection "Context lifting lemmas"
66 Some lemmas for lifting an execution into a prefix and suffix
67 of instructions; only needed for the first proof.
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> _")
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> _")
88 declare rtrancl_induct2 [induct set: rtrancl]
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> _")
97 show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
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)
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> _")
115 show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
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)
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)
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])
135 subsection "Compiler correctness"
137 declare rtrancl_into_rtrancl[trans]
138 converse_rtrancl_into_rtrancl[trans]
142 The first proof; The statement is very intuitive,
143 but application of induction hypothesis requires the above lifting lemmas
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")
151 show "\<And>s. ?Q \<SKIP> s s" by simp
153 show "\<And>a s x. ?Q (x :== a) s (s[x\<mapsto> a s])" by force
157 hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
159 moreover assume "?Q c1 s1 s2"
160 hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
161 \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
163 note app_left[of _ 0]
165 "\<And>is1 is2 s1 s2 i2.
166 is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
167 is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
170 ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
171 \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
172 by (rule rtrancl_trans)
173 thus "?Q (c0; c1) s0 s2" by simp
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
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>"
184 finally show "?Q (\<IF> b \<THEN> c0 \<ELSE> 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
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" .
197 thus "?Q (\<WHILE> b \<DO> c) s s" by force
199 fix b c and s0::state and s1 s2
200 let ?comp = "compile(\<WHILE> b \<DO> c)"
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
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
209 finally show "?Q (\<WHILE> b \<DO> c) s0 s2".
214 Second proof; statement is generalized to cater for prefixes and suffixes;
215 needs none of the lifting lemmas, but instantiations of pre/suffix.
217 theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow>
218 !a z. a@compile c@z \<turnstile> \<langle>s,length a\<rangle> -*\<rightarrow> \<langle>t,length a + length(compile c)\<rangle>";
219 apply(erule evalc.induct)
221 apply(force intro!: ASIN)
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 *)
231 (* instantiate assumption sufficiently for later: *)
232 apply(erule_tac x = "a@[?I]" in allE)
235 apply(rule converse_rtrancl_into_rtrancl)
236 apply(force intro!: JMPFT)
237 (* execute compile c0: *)
238 apply(rule rtrancl_trans)
242 apply(rule r_into_rtrancl)
243 apply(force intro!: JMPFF)
244 (* end of case b is true *)
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)
251 apply(force intro: JMPFF)
253 apply(erule_tac x = "a@[?I]" in allE)
254 apply(erule_tac x = a in allE)
256 apply(rule converse_rtrancl_into_rtrancl)
257 apply(force intro!: JMPFT)
258 apply(rule rtrancl_trans)
261 apply(rule converse_rtrancl_into_rtrancl)
262 apply(force intro!: JMPB)
266 text {* Missing: the other direction! *}