author  blanchet 
Mon, 22 Jun 2015 16:56:03 +0200  
changeset 60542  c5953e3a1e4f 
parent 58889  5b7a9633cfa8 
child 61147  263a354329e9 
permissions  rwrr 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

1 
(* Author: Tobias Nipkow and Gerwin Klein *) 
43141  2 

58889  3 
section "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 
53869  24 
"(x # xs) !! i = (if i = 0 then x else xs !! (i  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]: 
53869  31 
"0 \<le> i \<Longrightarrow> 
32 
(xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i  size xs))" 

33 
by (induction xs arbitrary: i) (auto simp: algebra_simps) 

43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

34 

53958  35 
text{* We hide coercion @{const int} applied to @{const length}: *} 
36 

37 
abbreviation (output) 

38 
"isize xs == int (length xs)" 

39 

40 
notation isize ("size") 

41 

42 

43141  43 
subsection "Instructions and Stack Machine" 
10342  44 

52906  45 
text_raw{*\snip{instrdef}{0}{1}{% *} 
58310  46 
datatype instr = 
52906  47 
LOADI int  LOAD vname  ADD  STORE vname  
48 
JMP int  JMPLESS int  JMPGE int 

49 
text_raw{*}%endsnip*} 

10342  50 

43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

51 
type_synonym stack = "val list" 
45637  52 
type_synonym config = "int \<times> state \<times> stack" 
43141  53 

54 
abbreviation "hd2 xs == hd(tl xs)" 

55 
abbreviation "tl2 xs == tl(tl xs)" 

11275  56 

50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

57 
fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where 
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

58 
"iexec instr (i,s,stk) = (case instr of 
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

59 
LOADI n \<Rightarrow> (i+1,s, n#stk)  
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

60 
LOAD x \<Rightarrow> (i+1,s, s x # stk)  
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

61 
ADD \<Rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)  
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

62 
STORE x \<Rightarrow> (i+1,s(x := hd stk),tl stk)  
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

63 
JMP n \<Rightarrow> (i+1+n,s,stk)  
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

64 
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

65 
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

66 

44000
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset

67 
definition 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

68 
exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" 
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

69 
("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
44000
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset

70 
where 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

71 
"P \<turnstile> c \<rightarrow> c' = 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

72 
(\<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

73 

ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset

74 
lemma exec1I [intro, code_pred_intro]: 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

75 
"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

76 
\<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'" 
52915  77 
by (simp add: exec1_def) 
43141  78 

52915  79 
abbreviation 
80 
exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50) 

43141  81 
where 
52915  82 
"exec P \<equiv> star (exec1 P)" 
83 

84 
declare star.step[intro] 

43141  85 

52915  86 
lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)] 
43141  87 

52915  88 
code_pred exec1 by (metis exec1_def) 
43141  89 

90 
values 

91 
"{(i,map t [''x'',''y''],stk)  i t stk. 

92 
[LOAD ''y'', STORE ''x''] \<turnstile> 

44036  93 
(0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}" 
43141  94 

95 

96 
subsection{* Verification infrastructure *} 

97 

98 
text{* Below we need to argue about the execution of code that is embedded in 

99 
larger programs. For this purpose we show that execution is preserved by 

100 
appending code to the left or right of a program. *} 

101 

50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

102 
lemma iexec_shift [simp]: 
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

103 
"((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

104 
by(auto split:instr.split) 
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

105 

43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

106 
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'" 
52915  107 
by (auto simp: exec1_def) 
11275  108 

43141  109 
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'" 
52915  110 
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

111 

43141  112 
lemma exec1_appendL: 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

113 
fixes i i' :: int 
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

114 
shows 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

115 
"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

116 
P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')" 
52915  117 
unfolding exec1_def 
52952  118 
by (auto simp del: iexec.simps) 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

119 

43141  120 
lemma exec_appendL: 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

121 
fixes i i' :: int 
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

122 
shows 
43141  123 
"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

124 
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

125 
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

126 

43141  127 
text{* Now we specialise the above lemmas to enable automatic proofs of 
128 
@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and 

129 
pieces of code that we already know how they execute (by induction), combined 

130 
by @{text "@"} and @{text "#"}. Backward jumps are not supported. 

131 
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

132 

43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

133 
If we have just executed the first instruction of the program, drop it: *} 
43141  134 

43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

135 
lemma exec_Cons_1 [intro]: 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

136 
"P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow> 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

137 
instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')" 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

138 
by (drule exec_appendL[where P'="[instr]"]) simp 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

139 

43141  140 
lemma exec_appendL_if[intro]: 
54428  141 
fixes i i' j :: int 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

142 
shows 
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

143 
"size P' <= i 
54428  144 
\<Longrightarrow> P \<turnstile> (i  size P',s,stk) \<rightarrow>* (j,s',stk') 
145 
\<Longrightarrow> i' = size P' + j 

146 
\<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')" 

50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

147 
by (drule exec_appendL[where P'=P']) simp 
10342  148 

60542  149 
text{* Split the execution of a compound program up into the execution of its 
43141  150 
parts: *} 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

151 

43141  152 
lemma exec_append_trans[intro]: 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

153 
fixes i' i'' j'' :: int 
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

154 
shows 
43141  155 
"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

156 
size P \<le> i' \<Longrightarrow> 
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

157 
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

158 
j'' = size P + i'' 
43141  159 
\<Longrightarrow> 
160 
P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')" 

52915  161 
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

162 

43141  163 

50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

164 
declare Let_def[simp] 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

165 

8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

166 

43141  167 
subsection "Compilation" 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

168 

43141  169 
fun acomp :: "aexp \<Rightarrow> instr list" where 
170 
"acomp (N n) = [LOADI n]"  

171 
"acomp (V x) = [LOAD x]"  

172 
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]" 

173 

174 
lemma acomp_correct[intro]: 

51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

175 
"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

176 
by (induction a arbitrary: stk) fastforce+ 
10342  177 

43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

178 
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where 
53880  179 
"bcomp (Bc v) f n = (if v=f then [JMP n] else [])"  
180 
"bcomp (Not b) f n = bcomp b (\<not>f) n"  

181 
"bcomp (And b1 b2) f n = 

182 
(let cb2 = bcomp b2 f n; 

55582  183 
m = if f then size cb2 else (size cb2::int)+n; 
43141  184 
cb1 = bcomp b1 False m 
185 
in cb1 @ cb2)"  

53880  186 
"bcomp (Less a1 a2) f n = 
187 
acomp a1 @ acomp a2 @ (if f then [JMPLESS n] else [JMPGE n])" 

43141  188 

189 
value 

190 
"bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v'')))) 

191 
False 3" 

192 

193 
lemma bcomp_correct[intro]: 

51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

194 
fixes n :: int 
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

195 
shows 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

196 
"0 \<le> n \<Longrightarrow> 
53880  197 
bcomp b f n \<turnstile> 
198 
(0,s,stk) \<rightarrow>* (size(bcomp b f n) + (if f = bval b s then n else 0),s,stk)" 

199 
proof(induction b arbitrary: f n) 

43141  200 
case Not 
53880  201 
from Not(1)[where f="~f"] Not(2) show ?case by fastforce 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

202 
next 
43141  203 
case (And b1 b2) 
53880  204 
from And(1)[of "if f then size(bcomp b2 f n) else size(bcomp b2 f n) + n" 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

205 
"False"] 
53880  206 
And(2)[of n f] And(3) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44036
diff
changeset

207 
show ?case by fastforce 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44036
diff
changeset

208 
qed fastforce+ 
43141  209 

210 
fun ccomp :: "com \<Rightarrow> instr list" where 

211 
"ccomp SKIP = []"  

212 
"ccomp (x ::= a) = acomp a @ [STORE x]"  

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52952
diff
changeset

213 
"ccomp (c\<^sub>1;;c\<^sub>2) = ccomp c\<^sub>1 @ ccomp c\<^sub>2"  
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52952
diff
changeset

214 
"ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52952
diff
changeset

215 
(let cc\<^sub>1 = ccomp c\<^sub>1; cc\<^sub>2 = ccomp c\<^sub>2; cb = bcomp b False (size cc\<^sub>1 + 1) 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52952
diff
changeset

216 
in cb @ cc\<^sub>1 @ JMP (size cc\<^sub>2) # cc\<^sub>2)"  
43141  217 
"ccomp (WHILE b DO c) = 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

218 
(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

219 
in cb @ cc @ [JMP ((size cb + size cc + 1))])" 
44004  220 

43141  221 

222 
value "ccomp 

223 
(IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1) 

224 
ELSE ''v'' ::= V ''u'')" 

225 

226 
value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))" 

227 

228 

45114  229 
subsection "Preservation of semantics" 
43141  230 

43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

231 
lemma ccomp_bigstep: 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

232 
"(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)" 
45015  233 
proof(induction arbitrary: stk rule: big_step_induct) 
43141  234 
case (Assign x a s) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44036
diff
changeset

235 
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

236 
next 
47818  237 
case (Seq c1 s1 s2 c2 s3) 
43141  238 
let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2" 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

239 
have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)" 
47818  240 
using Seq.IH(1) by fastforce 
43141  241 
moreover 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

242 
have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)" 
47818  243 
using Seq.IH(2) by fastforce 
52915  244 
ultimately show ?case by simp (blast intro: star_trans) 
43141  245 
next 
246 
case (WhileTrue b s1 c s2 s3) 

247 
let ?cc = "ccomp c" 

51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

248 
let ?cb = "bcomp b False (size ?cc + 1)" 
43141  249 
let ?cw = "ccomp(WHILE b DO c)" 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

250 
have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb,s1,stk)" 
50133  251 
using `bval b s1` by fastforce 
252 
moreover 

51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

253 
have "?cw \<turnstile> (size ?cb,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)" 
50133  254 
using WhileTrue.IH(1) by fastforce 
43141  255 
moreover 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

256 
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

257 
by fastforce 
43141  258 
moreover 
51259
1491459df114
eliminated isize in favour of size + type coercion
kleing
parents:
50133
diff
changeset

259 
have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2)) 
52915  260 
ultimately show ?case by(blast intro: star_trans) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44036
diff
changeset

261 
qed fastforce+ 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

262 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
16417
diff
changeset

263 
end 