1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 header "A Compiler for IMP" |
3 header "A Compiler for IMP" |
4 |
4 |
5 theory Compiler imports Big_Step |
5 theory Compiler imports Big_Step |
6 begin |
6 begin |
7 |
7 |
|
8 subsection "List setup" |
|
9 |
|
10 text {* |
|
11 We are going to define a small machine language where programs are |
|
12 lists of instructions. For nicer algebraic properties in our lemmas |
|
13 later, we prefer @{typ int} to @{term nat} as program counter. |
|
14 |
|
15 Therefore, we define notation for size and indexing for lists |
|
16 on @{typ int}: |
|
17 *} |
|
18 abbreviation "isize xs == int (length xs)" |
|
19 |
|
20 primrec |
|
21 inth :: "'a list => int => 'a" (infixl "!!" 100) where |
|
22 inth_Cons: "(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))" |
|
23 |
|
24 text {* |
|
25 The only additional lemma we need is indexing over append: |
|
26 *} |
|
27 lemma inth_append [simp]: |
|
28 "0 \<le> n \<Longrightarrow> |
|
29 (xs @ ys) !! n = (if n < isize xs then xs !! n else ys !! (n - isize xs))" |
|
30 by (induct xs arbitrary: n) (auto simp: algebra_simps) |
|
31 |
8 subsection "Instructions and Stack Machine" |
32 subsection "Instructions and Stack Machine" |
9 |
33 |
10 datatype instr = |
34 datatype instr = |
11 LOADI int | LOAD string | ADD | |
35 LOADI int | |
|
36 LOAD string | |
|
37 ADD | |
12 STORE string | |
38 STORE string | |
13 JMPF nat | |
39 JMP int | |
14 JMPB nat | |
40 JMPFLESS int | |
15 JMPFLESS nat | |
41 JMPFGE int |
16 JMPFGE nat |
42 |
17 |
43 (* reads slightly nicer *) |
18 type_synonym stack = "int list" |
44 abbreviation |
19 type_synonym config = "nat\<times>state\<times>stack" |
45 "JMPB i == JMP (-i)" |
|
46 |
|
47 type_synonym stack = "val list" |
|
48 type_synonym config = "int\<times>state\<times>stack" |
20 |
49 |
21 abbreviation "hd2 xs == hd(tl xs)" |
50 abbreviation "hd2 xs == hd(tl xs)" |
22 abbreviation "tl2 xs == tl(tl xs)" |
51 abbreviation "tl2 xs == tl(tl xs)" |
23 |
52 |
24 inductive exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" |
53 inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" |
25 ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) |
54 ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [50,0,0] 50) |
26 for P :: "instr list" |
|
27 where |
55 where |
28 "\<lbrakk> i < size P; P!i = LOADI n \<rbrakk> \<Longrightarrow> |
56 "LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" | |
29 P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, n#stk)" | |
57 "LOAD x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" | |
30 "\<lbrakk> i < size P; P!i = LOAD x \<rbrakk> \<Longrightarrow> |
58 "ADD \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" | |
31 P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" | |
59 "STORE n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" | |
32 "\<lbrakk> i < size P; P!i = ADD \<rbrakk> \<Longrightarrow> |
60 "JMP n \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)" | |
33 P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" | |
61 "JMPFLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" | |
34 "\<lbrakk> i < size P; P!i = STORE n \<rbrakk> \<Longrightarrow> |
62 "JMPFGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)" |
35 P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" | |
63 |
36 "\<lbrakk> i < size P; P!i = JMPF n \<rbrakk> \<Longrightarrow> |
64 code_pred iexec1 . |
37 P \<turnstile> (i,s,stk) \<rightarrow> (i+1+n,s,stk)" | |
65 |
38 "\<lbrakk> i < size P; P!i = JMPB n; n \<le> i+1 \<rbrakk> \<Longrightarrow> |
66 declare iexec1.intros |
39 P \<turnstile> (i,s,stk) \<rightarrow> (i+1-n,s,stk)" | |
67 |
40 "\<lbrakk> i < size P; P!i = JMPFLESS n \<rbrakk> \<Longrightarrow> |
68 (* FIXME: why does code gen not work with fun? *) |
41 P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" | |
69 inductive |
42 "\<lbrakk> i < size P; P!i = JMPFGE n \<rbrakk> \<Longrightarrow> |
70 exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" |
43 P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)" |
71 ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) where |
|
72 "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'" |
44 |
73 |
45 code_pred exec1 . |
74 code_pred exec1 . |
46 |
75 |
47 declare exec1.intros[intro] |
76 declare exec1.intros [intro!] |
|
77 |
|
78 inductive_cases exec1_elim [elim!]: "P \<turnstile> c \<rightarrow> c'" |
|
79 |
|
80 lemma exec1_simp [simp]: |
|
81 "P \<turnstile> c \<rightarrow> c' = |
|
82 (\<exists>i s stk. c = (i,s,stk) \<and> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c' \<and> 0 \<le> i \<and> i < isize P)" |
|
83 by auto |
48 |
84 |
49 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50) |
85 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50) |
50 where |
86 where |
51 refl: "P \<turnstile> c \<rightarrow>* c" | |
87 refl: "P \<turnstile> c \<rightarrow>* c" | |
52 step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" |
88 step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" |
53 |
89 |
54 declare exec.intros[intro] |
90 declare refl[intro] step[intro] |
55 |
91 |
56 lemmas exec_induct = exec.induct[split_format(complete)] |
92 lemmas exec_induct = exec.induct[split_format(complete)] |
57 |
93 |
58 code_pred exec . |
94 code_pred exec . |
59 |
95 |
64 |
100 |
65 |
101 |
66 subsection{* Verification infrastructure *} |
102 subsection{* Verification infrastructure *} |
67 |
103 |
68 lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" |
104 lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" |
69 apply(induct rule: exec.induct) |
105 by (induct rule: exec.induct) fastsimp+ |
70 apply blast |
106 |
71 by (metis exec.step) |
107 inductive_cases iexec1_cases [elim!]: |
72 |
108 "LOADI n \<turnstile>i c \<rightarrow> c'" |
73 lemma exec1_subst: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> c' = c'' \<Longrightarrow> P \<turnstile> c \<rightarrow> c''" |
109 "LOAD x \<turnstile>i c \<rightarrow> c'" |
74 by auto |
110 "ADD \<turnstile>i c \<rightarrow> c'" |
75 |
111 "STORE n \<turnstile>i c \<rightarrow> c'" |
76 lemmas exec1_simps = exec1.intros[THEN exec1_subst] |
112 "JMP n \<turnstile>i c \<rightarrow> c'" |
|
113 "JMPFLESS n \<turnstile>i c \<rightarrow> c'" |
|
114 "JMPFGE n \<turnstile>i c \<rightarrow> c'" |
|
115 |
|
116 text {* Simplification rules for @{const iexec1}. *} |
|
117 lemma iexec1_simps [simp]: |
|
118 "LOADI n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, n # stk))" |
|
119 "LOAD x \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, s x # stk))" |
|
120 "ADD \<turnstile>i c \<rightarrow> c' = |
|
121 (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))" |
|
122 "STORE x \<turnstile>i c \<rightarrow> c' = |
|
123 (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x \<rightarrow> hd stk), tl stk))" |
|
124 "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))" |
|
125 "JMPFLESS n \<turnstile>i c \<rightarrow> c' = |
|
126 (\<exists>i s stk. c = (i, s, stk) \<and> |
|
127 c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))" |
|
128 "JMPFGE n \<turnstile>i c \<rightarrow> c' = |
|
129 (\<exists>i s stk. c = (i, s, stk) \<and> |
|
130 c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))" |
|
131 by (auto split del: split_if intro!: iexec1.intros) |
|
132 |
77 |
133 |
78 text{* Below we need to argue about the execution of code that is embedded in |
134 text{* Below we need to argue about the execution of code that is embedded in |
79 larger programs. For this purpose we show that execution is preserved by |
135 larger programs. For this purpose we show that execution is preserved by |
80 appending code to the left or right of a program. *} |
136 appending code to the left or right of a program. *} |
81 |
137 |
82 lemma exec1_appendR: assumes "P \<turnstile> c \<rightarrow> c'" shows "P@P' \<turnstile> c \<rightarrow> c'" |
138 lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'" |
83 proof- |
139 by auto |
84 from assms show ?thesis |
|
85 by cases (simp_all add: exec1_simps nth_append) |
|
86 -- "All cases proved with the final simp-all" |
|
87 qed |
|
88 |
140 |
89 lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'" |
141 lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'" |
90 apply(induct rule: exec.induct) |
142 by (induct rule: exec.induct) (fastsimp intro: exec1_appendR)+ |
91 apply blast |
143 |
92 by (metis exec1_appendR exec.step) |
144 lemma iexec1_shiftI: |
93 |
145 assumes "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')" |
|
146 shows "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')" |
|
147 using assms by cases auto |
|
148 |
|
149 lemma iexec1_shiftD: |
|
150 assumes "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')" |
|
151 shows "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')" |
|
152 using assms by cases auto |
|
153 |
|
154 lemma iexec_shift [simp]: |
|
155 "(X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')) = (X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk'))" |
|
156 by (blast intro: iexec1_shiftI dest: iexec1_shiftD) |
|
157 |
94 lemma exec1_appendL: |
158 lemma exec1_appendL: |
95 assumes "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk')" |
159 "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow> |
96 shows "P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')" |
160 P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')" |
97 proof- |
161 by simp |
98 from assms show ?thesis |
|
99 by cases (simp_all add: exec1_simps) |
|
100 qed |
|
101 |
162 |
102 lemma exec_appendL: |
163 lemma exec_appendL: |
103 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow> |
164 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow> |
104 P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')" |
165 P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')" |
105 apply(induct rule: exec_induct) |
166 by (induct rule: exec_induct) (blast intro!: exec1_appendL)+ |
106 apply blast |
|
107 by (blast intro: exec1_appendL exec.step) |
|
108 |
167 |
109 text{* Now we specialise the above lemmas to enable automatic proofs of |
168 text{* Now we specialise the above lemmas to enable automatic proofs of |
110 @{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and |
169 @{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and |
111 pieces of code that we already know how they execute (by induction), combined |
170 pieces of code that we already know how they execute (by induction), combined |
112 by @{text "@"} and @{text "#"}. Backward jumps are not supported. |
171 by @{text "@"} and @{text "#"}. Backward jumps are not supported. |
113 The details should be skipped on a first reading. |
172 The details should be skipped on a first reading. |
114 |
173 |
115 If the pc points beyond the first instruction or part of the program, drop it: *} |
174 If we have just executed the first instruction of the program, drop it: *} |
116 |
175 |
117 lemma exec_Cons_Suc[intro]: |
176 lemma exec_Cons_1 [intro]: |
118 "P \<turnstile> (i,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow> |
177 "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow> |
119 instr#P \<turnstile> (Suc i,s,stk) \<rightarrow>* (Suc j,t,stk')" |
178 instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')" |
120 apply(drule exec_appendL[where P'="[instr]"]) |
179 by (drule exec_appendL[where P'="[instr]"]) simp |
121 apply simp |
|
122 done |
|
123 |
180 |
124 lemma exec_appendL_if[intro]: |
181 lemma exec_appendL_if[intro]: |
125 "size P' <= i |
182 "isize P' <= i |
126 \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (i',s',stk') |
183 \<Longrightarrow> P \<turnstile> (i - isize P',s,stk) \<rightarrow>* (i',s',stk') |
127 \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (size P' + i',s',stk')" |
184 \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')" |
128 apply(drule exec_appendL[where P'=P']) |
185 by (drule exec_appendL[where P'=P']) simp |
129 apply simp |
|
130 done |
|
131 |
186 |
132 text{* Split the execution of a compound program up into the excution of its |
187 text{* Split the execution of a compound program up into the excution of its |
133 parts: *} |
188 parts: *} |
134 |
189 |
135 lemma exec_append_trans[intro]: |
190 lemma exec_append_trans[intro]: |
136 "P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow> |
191 "P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow> |
137 size P \<le> i' \<Longrightarrow> |
192 isize P \<le> i' \<Longrightarrow> |
138 P' \<turnstile> (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow> |
193 P' \<turnstile> (i' - isize P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow> |
139 j'' = size P + i'' |
194 j'' = isize P + i'' |
140 \<Longrightarrow> |
195 \<Longrightarrow> |
141 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')" |
196 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')" |
142 by(metis exec_trans[OF exec_appendR exec_appendL_if]) |
197 by(metis exec_trans[OF exec_appendR exec_appendL_if]) |
143 |
198 |
144 |
199 |
145 declare Let_def[simp] eval_nat_numeral[simp] |
200 declare Let_def[simp] |
146 |
201 |
147 |
202 |
148 subsection "Compilation" |
203 subsection "Compilation" |
149 |
204 |
150 fun acomp :: "aexp \<Rightarrow> instr list" where |
205 fun acomp :: "aexp \<Rightarrow> instr list" where |
151 "acomp (N n) = [LOADI n]" | |
206 "acomp (N n) = [LOADI n]" | |
152 "acomp (V x) = [LOAD x]" | |
207 "acomp (V x) = [LOAD x]" | |
153 "acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]" |
208 "acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]" |
154 |
209 |
155 lemma acomp_correct[intro]: |
210 lemma acomp_correct[intro]: |
156 "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)" |
211 "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)" |
157 apply(induct a arbitrary: stk) |
212 by (induct a arbitrary: stk) fastsimp+ |
158 apply(fastsimp)+ |
213 |
159 done |
214 fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where |
160 |
215 "bcomp (B bv) c n = (if bv=c then [JMP n] else [])" | |
161 fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> instr list" where |
|
162 "bcomp (B bv) c n = (if bv=c then [JMPF n] else [])" | |
|
163 "bcomp (Not b) c n = bcomp b (\<not>c) n" | |
216 "bcomp (Not b) c n = bcomp b (\<not>c) n" | |
164 "bcomp (And b1 b2) c n = |
217 "bcomp (And b1 b2) c n = |
165 (let cb2 = bcomp b2 c n; |
218 (let cb2 = bcomp b2 c n; |
166 m = (if c then size cb2 else size cb2+n); |
219 m = (if c then isize cb2 else isize cb2+n); |
167 cb1 = bcomp b1 False m |
220 cb1 = bcomp b1 False m |
168 in cb1 @ cb2)" | |
221 in cb1 @ cb2)" | |
169 "bcomp (Less a1 a2) c n = |
222 "bcomp (Less a1 a2) c n = |
170 acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])" |
223 acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])" |
171 |
224 |
172 value |
225 value |
173 "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v'')))) |
226 "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v'')))) |
174 False 3" |
227 False 3" |
175 |
228 |
176 lemma bcomp_correct[intro]: |
229 lemma bcomp_correct[intro]: |
177 "bcomp b c n \<turnstile> |
230 "0 \<le> n \<Longrightarrow> |
178 (0,s,stk) \<rightarrow>* (size(bcomp b c n) + (if c = bval b s then n else 0),s,stk)" |
231 bcomp b c n \<turnstile> |
|
232 (0,s,stk) \<rightarrow>* (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)" |
179 proof(induct b arbitrary: c n m) |
233 proof(induct b arbitrary: c n m) |
180 case Not |
234 case Not |
181 from Not[of "~c"] show ?case by fastsimp |
235 from Not(1)[where c="~c"] Not(2) show ?case by fastsimp |
182 next |
236 next |
183 case (And b1 b2) |
237 case (And b1 b2) |
184 from And(1)[of "False"] And(2)[of "c"] show ?case by fastsimp |
238 from And(1)[of "if c then isize (bcomp b2 c n) else isize (bcomp b2 c n) + n" |
|
239 "False"] |
|
240 And(2)[of n "c"] And(3) |
|
241 show ?case by fastsimp |
185 qed fastsimp+ |
242 qed fastsimp+ |
186 |
|
187 |
243 |
188 fun ccomp :: "com \<Rightarrow> instr list" where |
244 fun ccomp :: "com \<Rightarrow> instr list" where |
189 "ccomp SKIP = []" | |
245 "ccomp SKIP = []" | |
190 "ccomp (x ::= a) = acomp a @ [STORE x]" | |
246 "ccomp (x ::= a) = acomp a @ [STORE x]" | |
191 "ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" | |
247 "ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" | |
192 "ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = |
248 "ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = |
193 (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1) |
249 (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (isize cc\<^isub>1 + 1) |
194 in cb @ cc\<^isub>1 @ JMPF(size cc\<^isub>2) # cc\<^isub>2)" | |
250 in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" | |
195 "ccomp (WHILE b DO c) = |
251 "ccomp (WHILE b DO c) = |
196 (let cc = ccomp c; cb = bcomp b False (size cc + 1) |
252 (let cc = ccomp c; cb = bcomp b False (isize cc + 1) |
197 in cb @ cc @ [JMPB (size cb + size cc + 1)])" |
253 in cb @ cc @ [JMPB (isize cb + isize cc + 1)])" |
198 |
254 |
199 value "ccomp |
255 value "ccomp |
200 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1) |
256 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1) |
201 ELSE ''v'' ::= V ''u'')" |
257 ELSE ''v'' ::= V ''u'')" |
202 |
258 |
203 value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))" |
259 value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))" |
204 |
260 |
205 |
261 |
206 subsection "Preservation of sematics" |
262 subsection "Preservation of sematics" |
207 |
263 |
208 lemma ccomp_correct: |
264 lemma ccomp_bigstep: |
209 "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)" |
265 "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)" |
210 proof(induct arbitrary: stk rule: big_step_induct) |
266 proof(induct arbitrary: stk rule: big_step_induct) |
211 case (Assign x a s) |
267 case (Assign x a s) |
212 show ?case by (fastsimp simp:fun_upd_def) |
268 show ?case by (fastsimp simp:fun_upd_def cong: if_cong) |
213 next |
269 next |
214 case (Semi c1 s1 s2 c2 s3) |
270 case (Semi c1 s1 s2 c2 s3) |
215 let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2" |
271 let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2" |
216 have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)" |
272 have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)" |
217 using Semi.hyps(2) by (fastsimp) |
273 using Semi.hyps(2) by fastsimp |
218 moreover |
274 moreover |
219 have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)" |
275 have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)" |
220 using Semi.hyps(4) by (fastsimp) |
276 using Semi.hyps(4) by fastsimp |
221 ultimately show ?case by simp (blast intro: exec_trans) |
277 ultimately show ?case by simp (blast intro: exec_trans) |
222 next |
278 next |
223 case (WhileTrue b s1 c s2 s3) |
279 case (WhileTrue b s1 c s2 s3) |
224 let ?cc = "ccomp c" |
280 let ?cc = "ccomp c" |
225 let ?cb = "bcomp b False (size ?cc + 1)" |
281 let ?cb = "bcomp b False (isize ?cc + 1)" |
226 let ?cw = "ccomp(WHILE b DO c)" |
282 let ?cw = "ccomp(WHILE b DO c)" |
227 have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)" |
283 have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)" |
228 using WhileTrue(1,3) by fastsimp |
284 using WhileTrue(1,3) by fastsimp |
229 moreover |
285 moreover |
230 have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)" |
286 have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)" |
231 by (fastsimp) |
287 by fastsimp |
232 moreover |
288 moreover |
233 have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue(5)) |
289 have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue(5)) |
234 ultimately show ?case by(blast intro: exec_trans) |
290 ultimately show ?case by(blast intro: exec_trans) |
235 qed fastsimp+ |
291 qed fastsimp+ |
236 |
292 |
237 end |
293 end |