author  nipkow 
Tue, 20 Nov 2012 17:49:26 +0100  
changeset 50133  5b43abaf8415 
parent 50061  7110422d4cb3 
child 51259  1491459df114 
permissions  rwrr 
43141  1 
(* Author: Tobias Nipkow *) 
2 

50061  3 
header "Compiler for IMP" 
10343  4 

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

5 
theory Compiler imports Big_Step 
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 

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

10 
text {* 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

11 
We are going to define a small machine language where programs are 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

12 
lists of instructions. For nicer algebraic properties in our lemmas 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

13 
later, we prefer @{typ int} to @{term nat} as program counter. 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

14 

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

15 
Therefore, we define notation for size and indexing for lists 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

16 
on @{typ int}: 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

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

18 
abbreviation "isize xs == int (length xs)" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

19 

45637  20 
fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where 
21 
"(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

22 

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

23 
text {* 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

24 
The only additional lemma we need is indexing over append: 
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 
lemma inth_append [simp]: 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

27 
"0 \<le> n \<Longrightarrow> 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

28 
(xs @ ys) !! n = (if n < isize xs then xs !! n else ys !! (n  isize xs))" 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

29 
by (induction xs arbitrary: n) (auto simp: algebra_simps) 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

30 

43141  31 
subsection "Instructions and Stack Machine" 
10342  32 

43141  33 
datatype instr = 
45323  34 
LOADI int  
35 
LOAD vname  

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

36 
ADD  
45323  37 
STORE vname  
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

38 
JMP int  
45322
654cc47f6115
JMPF(LESSGE) > JMP(LESSGE) because jumps are int now.
kleing
parents:
45200
diff
changeset

39 
JMPLESS int  
654cc47f6115
JMPF(LESSGE) > JMP(LESSGE) because jumps are int now.
kleing
parents:
45200
diff
changeset

40 
JMPGE int 
10342  41 

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

42 
type_synonym stack = "val list" 
45637  43 
type_synonym config = "int \<times> state \<times> stack" 
43141  44 

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

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

11275  47 

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

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

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

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

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

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

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

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

55 
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

56 
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

57 

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

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

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

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

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

62 
"P \<turnstile> c \<rightarrow> c' = 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

63 
(\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < isize P)" 
44000
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset

64 

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

65 
declare exec1_def [simp] 
44000
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset

66 

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

67 
lemma exec1I [intro, code_pred_intro]: 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

68 
"c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < isize P 
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

69 
\<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'" 
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

70 
by simp 
43141  71 

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

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

73 
("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50) 
43141  74 
where 
75 
refl: "P \<turnstile> c \<rightarrow>* c"  

76 
step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" 

77 

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

78 
declare refl[intro] step[intro] 
43141  79 

80 
lemmas exec_induct = exec.induct[split_format(complete)] 

81 

50133  82 
code_pred exec by fastforce 
43141  83 

84 
values 

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

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

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

89 

90 
subsection{* Verification infrastructure *} 

91 

92 
lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" 

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

93 
by (induction rule: exec.induct) fastforce+ 
43141  94 

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

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

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

98 

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

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

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

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

102 

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

103 
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'" 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

104 
by auto 
11275  105 

43141  106 
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'" 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

107 
by (induction rule: exec.induct) (fastforce intro: exec1_appendR)+ 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

108 

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

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

111 
P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')" 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

112 
by (auto split: instr.split) 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

113 

43141  114 
lemma exec_appendL: 
115 
"P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow> 

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

116 
P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')" 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

117 
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

118 

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

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

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

123 
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

124 

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

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

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

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

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

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

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

131 

43141  132 
lemma exec_appendL_if[intro]: 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

133 
"isize P' <= i 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

134 
\<Longrightarrow> P \<turnstile> (i  isize P',s,stk) \<rightarrow>* (i',s',stk') 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

135 
\<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')" 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

136 
by (drule exec_appendL[where P'=P']) simp 
10342  137 

43141  138 
text{* Split the execution of a compound program up into the excution of its 
139 
parts: *} 

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

140 

43141  141 
lemma exec_append_trans[intro]: 
142 
"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow> 

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

143 
isize P \<le> i' \<Longrightarrow> 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

144 
P' \<turnstile> (i'  isize P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow> 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

145 
j'' = isize P + i'' 
43141  146 
\<Longrightarrow> 
147 
P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')" 

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

148 
by(metis exec_trans[OF exec_appendR exec_appendL_if]) 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

149 

43141  150 

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

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

152 

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

153 

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

155 

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

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

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

160 

161 
lemma acomp_correct[intro]: 

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

162 
"acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)" 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

163 
by (induction a arbitrary: stk) fastforce+ 
10342  164 

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

165 
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where 
45200  166 
"bcomp (Bc v) c n = (if v=c then [JMP n] else [])"  
43141  167 
"bcomp (Not b) c n = bcomp b (\<not>c) n"  
168 
"bcomp (And b1 b2) c n = 

169 
(let cb2 = bcomp b2 c n; 

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

170 
m = (if c then isize cb2 else isize cb2+n); 
43141  171 
cb1 = bcomp b1 False m 
172 
in cb1 @ cb2)"  

173 
"bcomp (Less a1 a2) c n = 

45322
654cc47f6115
JMPF(LESSGE) > JMP(LESSGE) because jumps are int now.
kleing
parents:
45200
diff
changeset

174 
acomp a1 @ acomp a2 @ (if c then [JMPLESS n] else [JMPGE n])" 
43141  175 

176 
value 

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

178 
False 3" 

179 

180 
lemma bcomp_correct[intro]: 

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

181 
"0 \<le> n \<Longrightarrow> 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

182 
bcomp b c n \<turnstile> 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

183 
(0,s,stk) \<rightarrow>* (isize(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

184 
proof(induction b arbitrary: c n) 
43141  185 
case Not 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44036
diff
changeset

186 
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

187 
next 
43141  188 
case (And b1 b2) 
50060
43753eca324a
replaced relation by function  simplifies development
nipkow
parents:
47818
diff
changeset

189 
from And(1)[of "if c then isize(bcomp b2 c n) else isize(bcomp b2 c n) + n" 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

190 
"False"] 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

191 
And(2)[of n "c"] And(3) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44036
diff
changeset

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

193 
qed fastforce+ 
43141  194 

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

196 
"ccomp SKIP = []"  

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

198 
"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2"  

199 
"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = 

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

200 
(let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (isize cc\<^isub>1 + 1) 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

201 
in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)"  
43141  202 
"ccomp (WHILE b DO c) = 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

203 
(let cc = ccomp c; cb = bcomp b False (isize cc + 1) 
44004  204 
in cb @ cc @ [JMP ((isize cb + isize cc + 1))])" 
205 

43141  206 

207 
value "ccomp 

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

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

210 

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

212 

213 

45114  214 
subsection "Preservation of semantics" 
43141  215 

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

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

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

220 
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

221 
next 
47818  222 
case (Seq c1 s1 s2 c2 s3) 
43141  223 
let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2" 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

224 
have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)" 
47818  225 
using Seq.IH(1) by fastforce 
43141  226 
moreover 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

227 
have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)" 
47818  228 
using Seq.IH(2) by fastforce 
43141  229 
ultimately show ?case by simp (blast intro: exec_trans) 
230 
next 

231 
case (WhileTrue b s1 c s2 s3) 

232 
let ?cc = "ccomp c" 

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

233 
let ?cb = "bcomp b False (isize ?cc + 1)" 
43141  234 
let ?cw = "ccomp(WHILE b DO c)" 
50133  235 
have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb,s1,stk)" 
236 
using `bval b s1` by fastforce 

237 
moreover 

238 
have "?cw \<turnstile> (isize ?cb,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)" 

239 
using WhileTrue.IH(1) by fastforce 

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

241 
have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44036
diff
changeset

242 
by fastforce 
43141  243 
moreover 
45015  244 
have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2)) 
43141  245 
ultimately show ?case by(blast intro: exec_trans) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44036
diff
changeset

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

247 

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

248 
end 