author | kleing |
Thu, 08 Aug 2013 18:13:12 +0200 | |
changeset 52915 | c10bd1f49ff5 |
parent 52906 | ba514b5aa809 |
child 52924 | 9587134ec780 |
permissions | -rw-r--r-- |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
1 |
(* Author: Tobias Nipkow and Gerwin Klein *) |
43141 | 2 |
|
50061 | 3 |
header "Compiler for IMP" |
10343 | 4 |
|
52915 | 5 |
theory Compiler imports Big_Step Star |
43141 | 6 |
begin |
12429 | 7 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
8 |
subsection "List setup" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
9 |
|
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
10 |
text {* |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
11 |
In the following, we use the length of lists as integers |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
12 |
instead of natural numbers. Instead of converting @{typ nat} |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
13 |
to @{typ int} explicitly, we tell Isabelle to coerce @{typ nat} |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
14 |
automatically when necessary. |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
15 |
*} |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
16 |
declare [[coercion_enabled]] |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
17 |
declare [[coercion "int :: nat \<Rightarrow> int"]] |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
18 |
|
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
19 |
text {* |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
20 |
Similarly, we will want to access the ith element of a list, |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
21 |
where @{term i} is an @{typ int}. |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
22 |
*} |
45637 | 23 |
fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where |
24 |
"(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))" |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
25 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
26 |
text {* |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
27 |
The only additional lemma we need about this function |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
28 |
is indexing over append: |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
29 |
*} |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
30 |
lemma inth_append [simp]: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
31 |
"0 \<le> n \<Longrightarrow> |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
32 |
(xs @ ys) !! n = (if n < size xs then xs !! n else ys !! (n - size xs))" |
50060
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
33 |
by (induction xs arbitrary: n) (auto simp: algebra_simps) |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
34 |
|
43141 | 35 |
subsection "Instructions and Stack Machine" |
10342 | 36 |
|
52906 | 37 |
text_raw{*\snip{instrdef}{0}{1}{% *} |
43141 | 38 |
datatype instr = |
52906 | 39 |
LOADI int | LOAD vname | ADD | STORE vname | |
40 |
JMP int | JMPLESS int | JMPGE int |
|
41 |
text_raw{*}%endsnip*} |
|
10342 | 42 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
43 |
type_synonym stack = "val list" |
45637 | 44 |
type_synonym config = "int \<times> state \<times> stack" |
43141 | 45 |
|
46 |
abbreviation "hd2 xs == hd(tl xs)" |
|
47 |
abbreviation "tl2 xs == tl(tl xs)" |
|
11275 | 48 |
|
50060
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
49 |
fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
50 |
"iexec instr (i,s,stk) = (case instr of |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
51 |
LOADI n \<Rightarrow> (i+1,s, n#stk) | |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
52 |
LOAD x \<Rightarrow> (i+1,s, s x # stk) | |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
53 |
ADD \<Rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk) | |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
54 |
STORE x \<Rightarrow> (i+1,s(x := hd stk),tl stk) | |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
55 |
JMP n \<Rightarrow> (i+1+n,s,stk) | |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
56 |
JMPLESS n \<Rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk) | |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
57 |
JMPGE n \<Rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk))" |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
58 |
|
44000
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset
|
59 |
definition |
50060
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
60 |
exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
61 |
("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) |
44000
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset
|
62 |
where |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
63 |
"P \<turnstile> c \<rightarrow> c' = |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
64 |
(\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < size P)" |
44000
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset
|
65 |
|
52915 | 66 |
(* |
50060
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
67 |
declare exec1_def [simp] |
52915 | 68 |
*) |
44000
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset
|
69 |
|
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset
|
70 |
lemma exec1I [intro, code_pred_intro]: |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
71 |
"c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P |
50060
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
72 |
\<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'" |
52915 | 73 |
by (simp add: exec1_def) |
43141 | 74 |
|
52915 | 75 |
abbreviation |
76 |
exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50) |
|
43141 | 77 |
where |
52915 | 78 |
"exec P \<equiv> star (exec1 P)" |
79 |
||
80 |
declare star.step[intro] |
|
43141 | 81 |
|
52915 | 82 |
lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)] |
43141 | 83 |
|
52915 | 84 |
code_pred exec1 by (metis exec1_def) |
43141 | 85 |
|
86 |
values |
|
87 |
"{(i,map t [''x'',''y''],stk) | i t stk. |
|
88 |
[LOAD ''y'', STORE ''x''] \<turnstile> |
|
44036 | 89 |
(0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}" |
43141 | 90 |
|
91 |
||
92 |
subsection{* Verification infrastructure *} |
|
93 |
||
94 |
text{* Below we need to argue about the execution of code that is embedded in |
|
95 |
larger programs. For this purpose we show that execution is preserved by |
|
96 |
appending code to the left or right of a program. *} |
|
97 |
||
50060
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
98 |
lemma iexec_shift [simp]: |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
99 |
"((n+i',s',stk') = iexec x (n+i,s,stk)) = ((i',s',stk') = iexec x (i,s,stk))" |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
100 |
by(auto split:instr.split) |
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
101 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
102 |
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'" |
52915 | 103 |
by (auto simp: exec1_def) |
11275 | 104 |
|
43141 | 105 |
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'" |
52915 | 106 |
by (induction rule: star.induct) (fastforce intro: exec1_appendR)+ |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
107 |
|
43141 | 108 |
lemma exec1_appendL: |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
109 |
fixes i i' :: int |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
110 |
shows |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
111 |
"P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow> |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
112 |
P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')" |
52915 | 113 |
unfolding exec1_def |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
114 |
by (auto split: instr.split) |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
115 |
|
43141 | 116 |
lemma exec_appendL: |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
117 |
fixes i i' :: int |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
118 |
shows |
43141 | 119 |
"P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow> |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
120 |
P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')" |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
121 |
by (induction rule: exec_induct) (blast intro!: exec1_appendL)+ |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
122 |
|
43141 | 123 |
text{* Now we specialise the above lemmas to enable automatic proofs of |
124 |
@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and |
|
125 |
pieces of code that we already know how they execute (by induction), combined |
|
126 |
by @{text "@"} and @{text "#"}. Backward jumps are not supported. |
|
127 |
The details should be skipped on a first reading. |
|
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
128 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
129 |
If we have just executed the first instruction of the program, drop it: *} |
43141 | 130 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
131 |
lemma exec_Cons_1 [intro]: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
132 |
"P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
133 |
instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')" |
50060
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
134 |
by (drule exec_appendL[where P'="[instr]"]) simp |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
135 |
|
43141 | 136 |
lemma exec_appendL_if[intro]: |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
137 |
fixes i i' :: int |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
138 |
shows |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
139 |
"size P' <= i |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
140 |
\<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (i',s',stk') |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
141 |
\<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (size P' + i',s',stk')" |
50060
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
142 |
by (drule exec_appendL[where P'=P']) simp |
10342 | 143 |
|
43141 | 144 |
text{* Split the execution of a compound program up into the excution of its |
145 |
parts: *} |
|
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
146 |
|
43141 | 147 |
lemma exec_append_trans[intro]: |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
148 |
fixes i' i'' j'' :: int |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
149 |
shows |
43141 | 150 |
"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow> |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
151 |
size P \<le> i' \<Longrightarrow> |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
152 |
P' \<turnstile> (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow> |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
153 |
j'' = size P + i'' |
43141 | 154 |
\<Longrightarrow> |
155 |
P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')" |
|
52915 | 156 |
by(metis star_trans[OF exec_appendR exec_appendL_if]) |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
157 |
|
43141 | 158 |
|
50060
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
159 |
declare Let_def[simp] |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
160 |
|
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
161 |
|
43141 | 162 |
subsection "Compilation" |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
163 |
|
43141 | 164 |
fun acomp :: "aexp \<Rightarrow> instr list" where |
165 |
"acomp (N n) = [LOADI n]" | |
|
166 |
"acomp (V x) = [LOAD x]" | |
|
167 |
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]" |
|
168 |
||
169 |
lemma acomp_correct[intro]: |
|
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
170 |
"acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)" |
50060
43753eca324a
replaced relation by function - simplifies development
nipkow
parents:
47818
diff
changeset
|
171 |
by (induction a arbitrary: stk) fastforce+ |
10342 | 172 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
173 |
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where |
45200 | 174 |
"bcomp (Bc v) c n = (if v=c then [JMP n] else [])" | |
43141 | 175 |
"bcomp (Not b) c n = bcomp b (\<not>c) n" | |
176 |
"bcomp (And b1 b2) c n = |
|
177 |
(let cb2 = bcomp b2 c n; |
|
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
178 |
m = (if c then size cb2 else (size cb2::int)+n); |
43141 | 179 |
cb1 = bcomp b1 False m |
180 |
in cb1 @ cb2)" | |
|
181 |
"bcomp (Less a1 a2) c n = |
|
45322
654cc47f6115
JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents:
45200
diff
changeset
|
182 |
acomp a1 @ acomp a2 @ (if c then [JMPLESS n] else [JMPGE n])" |
43141 | 183 |
|
184 |
value |
|
185 |
"bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v'')))) |
|
186 |
False 3" |
|
187 |
||
188 |
lemma bcomp_correct[intro]: |
|
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
189 |
fixes n :: int |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
190 |
shows |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
191 |
"0 \<le> n \<Longrightarrow> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
192 |
bcomp b c n \<turnstile> |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
193 |
(0,s,stk) \<rightarrow>* (size(bcomp b c n) + (if c = bval b s then n else 0),s,stk)" |
45129
1fce03e3e8ad
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
wenzelm
parents:
45114
diff
changeset
|
194 |
proof(induction b arbitrary: c n) |
43141 | 195 |
case Not |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44036
diff
changeset
|
196 |
from Not(1)[where c="~c"] Not(2) show ?case by fastforce |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
197 |
next |
43141 | 198 |
case (And b1 b2) |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
199 |
from And(1)[of "if c then size(bcomp b2 c n) else size(bcomp b2 c n) + n" |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
200 |
"False"] |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
201 |
And(2)[of n "c"] And(3) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44036
diff
changeset
|
202 |
show ?case by fastforce |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44036
diff
changeset
|
203 |
qed fastforce+ |
43141 | 204 |
|
205 |
fun ccomp :: "com \<Rightarrow> instr list" where |
|
206 |
"ccomp SKIP = []" | |
|
207 |
"ccomp (x ::= a) = acomp a @ [STORE x]" | |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51259
diff
changeset
|
208 |
"ccomp (c\<^isub>1;;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" | |
43141 | 209 |
"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
210 |
(let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1) |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
211 |
in cb @ cc\<^isub>1 @ JMP (size cc\<^isub>2) # cc\<^isub>2)" | |
43141 | 212 |
"ccomp (WHILE b DO c) = |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
213 |
(let cc = ccomp c; cb = bcomp b False (size cc + 1) |
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
214 |
in cb @ cc @ [JMP (-(size cb + size cc + 1))])" |
44004 | 215 |
|
43141 | 216 |
|
217 |
value "ccomp |
|
218 |
(IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1) |
|
219 |
ELSE ''v'' ::= V ''u'')" |
|
220 |
||
221 |
value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))" |
|
222 |
||
223 |
||
45114 | 224 |
subsection "Preservation of semantics" |
43141 | 225 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
226 |
lemma ccomp_bigstep: |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
227 |
"(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)" |
45015 | 228 |
proof(induction arbitrary: stk rule: big_step_induct) |
43141 | 229 |
case (Assign x a s) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44036
diff
changeset
|
230 |
show ?case by (fastforce simp:fun_upd_def cong: if_cong) |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
231 |
next |
47818 | 232 |
case (Seq c1 s1 s2 c2 s3) |
43141 | 233 |
let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2" |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
234 |
have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)" |
47818 | 235 |
using Seq.IH(1) by fastforce |
43141 | 236 |
moreover |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
237 |
have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)" |
47818 | 238 |
using Seq.IH(2) by fastforce |
52915 | 239 |
ultimately show ?case by simp (blast intro: star_trans) |
43141 | 240 |
next |
241 |
case (WhileTrue b s1 c s2 s3) |
|
242 |
let ?cc = "ccomp c" |
|
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
243 |
let ?cb = "bcomp b False (size ?cc + 1)" |
43141 | 244 |
let ?cw = "ccomp(WHILE b DO c)" |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
245 |
have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb,s1,stk)" |
50133 | 246 |
using `bval b s1` by fastforce |
247 |
moreover |
|
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
248 |
have "?cw \<turnstile> (size ?cb,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)" |
50133 | 249 |
using WhileTrue.IH(1) by fastforce |
43141 | 250 |
moreover |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
251 |
have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44036
diff
changeset
|
252 |
by fastforce |
43141 | 253 |
moreover |
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset
|
254 |
have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2)) |
52915 | 255 |
ultimately show ?case by(blast intro: star_trans) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44036
diff
changeset
|
256 |
qed fastforce+ |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
257 |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
16417
diff
changeset
|
258 |
end |