author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45637  5f85efcb50c1 
child 47818  151d137f1095 
permissions  rwrr 
43141  1 
(* Author: Tobias Nipkow *) 
2 

3 
header "A 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))" 
45616  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 

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

48 
inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" 
44004  49 
("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [59,0,59] 60) 
43141  50 
where 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

51 
"LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)"  
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

52 
"LOAD x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)"  
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

53 
"ADD \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)"  
45616  54 
"STORE x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(x := hd stk),tl stk)"  
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

55 
"JMP n \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)"  
45322
654cc47f6115
JMPF(LESSGE) > JMP(LESSGE) because jumps are int now.
kleing
parents:
45200
diff
changeset

56 
"JMPLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)"  
654cc47f6115
JMPF(LESSGE) > JMP(LESSGE) because jumps are int now.
kleing
parents:
45200
diff
changeset

57 
"JMPGE n \<turnstile>i (i,s,stk) \<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 

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

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

60 

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

61 
declare iexec1.intros 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

62 

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

63 
definition 
44004  64 
exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
44000
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset

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

66 
"P \<turnstile> c \<rightarrow> c' = 
44004  67 
(\<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)" 
44000
ab4d8499815c
resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents:
43438
diff
changeset

68 

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

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

70 

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

71 
lemma exec1I [intro, code_pred_intro]: 
44004  72 
assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P" 
73 
shows "P \<turnstile> (i,s,stk) \<rightarrow> c'" 

74 
using assms by simp 

43141  75 

76 
inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50) 

77 
where 

78 
refl: "P \<turnstile> c \<rightarrow>* c"  

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

80 

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

81 
declare refl[intro] step[intro] 
43141  82 

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

84 

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

85 
code_pred exec by force 
43141  86 

87 
values 

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

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

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

92 

93 
subsection{* Verification infrastructure *} 

94 

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

45616  96 
by (induction rule: exec.induct) fastforce+ 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

97 

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

98 
inductive_cases iexec1_cases [elim!]: 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

99 
"LOADI n \<turnstile>i c \<rightarrow> c'" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

100 
"LOAD x \<turnstile>i c \<rightarrow> c'" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

101 
"ADD \<turnstile>i c \<rightarrow> c'" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

102 
"STORE n \<turnstile>i c \<rightarrow> c'" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

103 
"JMP n \<turnstile>i c \<rightarrow> c'" 
45322
654cc47f6115
JMPF(LESSGE) > JMP(LESSGE) because jumps are int now.
kleing
parents:
45200
diff
changeset

104 
"JMPLESS n \<turnstile>i c \<rightarrow> c'" 
654cc47f6115
JMPF(LESSGE) > JMP(LESSGE) because jumps are int now.
kleing
parents:
45200
diff
changeset

105 
"JMPGE n \<turnstile>i c \<rightarrow> c'" 
43141  106 

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

107 
text {* Simplification rules for @{const iexec1}. *} 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

108 
lemma iexec1_simps [simp]: 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

109 
"LOADI n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, n # stk))" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

110 
"LOAD x \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, s x # stk))" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

111 
"ADD \<turnstile>i c \<rightarrow> c' = 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

112 
(\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

113 
"STORE x \<turnstile>i c \<rightarrow> c' = 
44036  114 
(\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x := hd stk), tl stk))" 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

115 
"JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))" 
45322
654cc47f6115
JMPF(LESSGE) > JMP(LESSGE) because jumps are int now.
kleing
parents:
45200
diff
changeset

116 
"JMPLESS n \<turnstile>i c \<rightarrow> c' = 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

117 
(\<exists>i s stk. c = (i, s, stk) \<and> 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

118 
c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))" 
45322
654cc47f6115
JMPF(LESSGE) > JMP(LESSGE) because jumps are int now.
kleing
parents:
45200
diff
changeset

119 
"JMPGE n \<turnstile>i c \<rightarrow> c' = 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

120 
(\<exists>i s stk. c = (i, s, stk) \<and> 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

121 
c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

122 
by (auto split del: split_if intro!: iexec1.intros) 
43141  123 

124 

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

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

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

128 

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

129 
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

130 
by auto 
11275  131 

43141  132 
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'" 
45616  133 
by (induction rule: exec.induct) (fastforce intro: exec1_appendR)+ 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

134 

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

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

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

137 
shows "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

138 
using assms by cases auto 
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset

139 

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

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

141 
assumes "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

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

143 
using assms by cases auto 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

144 

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

145 
lemma iexec_shift [simp]: 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

146 
"(X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')) = (X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk'))" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

147 
by (blast intro: iexec1_shiftI dest: iexec1_shiftD) 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

148 

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

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

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

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

153 

43141  154 
lemma exec_appendL: 
155 
"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

156 
P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')" 
45616  157 
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

158 

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

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

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

163 
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

164 

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

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

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

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

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

169 
instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')" 
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

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

171 

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

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

174 
\<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

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

176 
by (drule exec_appendL[where P'=P']) simp 
10342  177 

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

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

180 

43141  181 
lemma exec_append_trans[intro]: 
182 
"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

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

184 
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

185 
j'' = isize P + i'' 
43141  186 
\<Longrightarrow> 
187 
P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')" 

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

188 
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

189 

43141  190 

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

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

192 

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

193 

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

195 

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

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

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

200 

201 
lemma acomp_correct[intro]: 

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

202 
"acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)" 
45616  203 
by (induction a arbitrary: stk) fastforce+ 
10342  204 

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

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

209 
(let cb2 = bcomp b2 c n; 

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

210 
m = (if c then isize cb2 else isize cb2+n); 
43141  211 
cb1 = bcomp b1 False m 
212 
in cb1 @ cb2)"  

213 
"bcomp (Less a1 a2) c n = 

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

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

216 
value 

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

218 
False 3" 

219 

220 
lemma bcomp_correct[intro]: 

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

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

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

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

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

226 
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

227 
next 
43141  228 
case (And b1 b2) 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

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

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

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

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

233 
qed fastforce+ 
43141  234 

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

236 
"ccomp SKIP = []"  

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

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

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

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

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

243 
(let cc = ccomp c; cb = bcomp b False (isize cc + 1) 
44004  244 
in cb @ cc @ [JMP ((isize cb + isize cc + 1))])" 
245 

43141  246 

247 
value "ccomp 

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

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

250 

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

252 

253 

45114  254 
subsection "Preservation of semantics" 
43141  255 

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

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

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

260 
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

261 
next 
43141  262 
case (Semi c1 s1 s2 c2 s3) 
263 
let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2" 

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

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

267 
have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)" 
45015  268 
using Semi.IH(2) by fastforce 
43141  269 
ultimately show ?case by simp (blast intro: exec_trans) 
270 
next 

271 
case (WhileTrue b s1 c s2 s3) 

272 
let ?cc = "ccomp c" 

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

273 
let ?cb = "bcomp b False (isize ?cc + 1)" 
43141  274 
let ?cw = "ccomp(WHILE b DO c)" 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

275 
have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)" 
45015  276 
using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce 
43141  277 
moreover 
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset

278 
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

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

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

284 

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

285 
end 