1.1 --- a/src/HOL/IMP/Compiler.thy Tue Nov 13 12:12:14 2012 +0100
1.2 +++ b/src/HOL/IMP/Compiler.thy Wed Nov 14 14:11:47 2012 +0100
1.3 @@ -26,7 +26,7 @@
1.4 lemma inth_append [simp]:
1.5 "0 \<le> n \<Longrightarrow>
1.6 (xs @ ys) !! n = (if n < isize xs then xs !! n else ys !! (n - isize xs))"
1.7 - by (induction xs arbitrary: n) (auto simp: algebra_simps)
1.8 +by (induction xs arbitrary: n) (auto simp: algebra_simps)
1.9
1.10 subsection "Instructions and Stack Machine"
1.11
1.12 @@ -45,35 +45,32 @@
1.13 abbreviation "hd2 xs == hd(tl xs)"
1.14 abbreviation "tl2 xs == tl(tl xs)"
1.15
1.16 -inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
1.17 - ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [59,0,59] 60)
1.18 -where
1.19 -"LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
1.20 -"LOAD x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
1.21 -"ADD \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
1.22 -"STORE x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(x := hd stk),tl stk)" |
1.23 -"JMP n \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
1.24 -"JMPLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
1.25 -"JMPGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
1.26 -
1.27 -code_pred iexec1 .
1.28 -
1.29 -declare iexec1.intros
1.30 +fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where
1.31 +"iexec instr (i,s,stk) = (case instr of
1.32 + LOADI n \<Rightarrow> (i+1,s, n#stk) |
1.33 + LOAD x \<Rightarrow> (i+1,s, s x # stk) |
1.34 + ADD \<Rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk) |
1.35 + STORE x \<Rightarrow> (i+1,s(x := hd stk),tl stk) |
1.36 + JMP n \<Rightarrow> (i+1+n,s,stk) |
1.37 + JMPLESS n \<Rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk) |
1.38 + JMPGE n \<Rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk))"
1.39
1.40 definition
1.41 - exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60)
1.42 + exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
1.43 + ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60)
1.44 where
1.45 "P \<turnstile> c \<rightarrow> c' =
1.46 - (\<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)"
1.47 + (\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < isize P)"
1.48
1.49 -declare exec1_def [simp]
1.50 +declare exec1_def [simp]
1.51
1.52 lemma exec1I [intro, code_pred_intro]:
1.53 - assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P"
1.54 - shows "P \<turnstile> (i,s,stk) \<rightarrow> c'"
1.55 - using assms by simp
1.56 + "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < isize P
1.57 + \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
1.58 +by simp
1.59
1.60 -inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
1.61 +inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
1.62 + ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
1.63 where
1.64 refl: "P \<turnstile> c \<rightarrow>* c" |
1.65 step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
1.66 @@ -93,68 +90,31 @@
1.67 subsection{* Verification infrastructure *}
1.68
1.69 lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
1.70 - by (induction rule: exec.induct) fastforce+
1.71 -
1.72 -inductive_cases iexec1_cases [elim!]:
1.73 - "LOADI n \<turnstile>i c \<rightarrow> c'"
1.74 - "LOAD x \<turnstile>i c \<rightarrow> c'"
1.75 - "ADD \<turnstile>i c \<rightarrow> c'"
1.76 - "STORE n \<turnstile>i c \<rightarrow> c'"
1.77 - "JMP n \<turnstile>i c \<rightarrow> c'"
1.78 - "JMPLESS n \<turnstile>i c \<rightarrow> c'"
1.79 - "JMPGE n \<turnstile>i c \<rightarrow> c'"
1.80 -
1.81 -text {* Simplification rules for @{const iexec1}. *}
1.82 -lemma iexec1_simps [simp]:
1.83 - "LOADI n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, n # stk))"
1.84 - "LOAD x \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, s x # stk))"
1.85 - "ADD \<turnstile>i c \<rightarrow> c' =
1.86 - (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))"
1.87 - "STORE x \<turnstile>i c \<rightarrow> c' =
1.88 - (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x := hd stk), tl stk))"
1.89 - "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
1.90 - "JMPLESS n \<turnstile>i c \<rightarrow> c' =
1.91 - (\<exists>i s stk. c = (i, s, stk) \<and>
1.92 - c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))"
1.93 - "JMPGE n \<turnstile>i c \<rightarrow> c' =
1.94 - (\<exists>i s stk. c = (i, s, stk) \<and>
1.95 - c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))"
1.96 - by (auto split del: split_if intro!: iexec1.intros)
1.97 -
1.98 +by (induction rule: exec.induct) fastforce+
1.99
1.100 text{* Below we need to argue about the execution of code that is embedded in
1.101 larger programs. For this purpose we show that execution is preserved by
1.102 appending code to the left or right of a program. *}
1.103
1.104 +lemma iexec_shift [simp]:
1.105 + "((n+i',s',stk') = iexec x (n+i,s,stk)) = ((i',s',stk') = iexec x (i,s,stk))"
1.106 +by(auto split:instr.split)
1.107 +
1.108 lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
1.109 - by auto
1.110 +by auto
1.111
1.112 lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
1.113 - by (induction rule: exec.induct) (fastforce intro: exec1_appendR)+
1.114 +by (induction rule: exec.induct) (fastforce intro: exec1_appendR)+
1.115
1.116 -lemma iexec1_shiftI:
1.117 - assumes "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
1.118 - shows "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
1.119 - using assms by cases auto
1.120 -
1.121 -lemma iexec1_shiftD:
1.122 - assumes "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
1.123 - shows "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
1.124 - using assms by cases auto
1.125 -
1.126 -lemma iexec_shift [simp]:
1.127 - "(X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')) = (X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk'))"
1.128 - by (blast intro: iexec1_shiftI dest: iexec1_shiftD)
1.129 -
1.130 lemma exec1_appendL:
1.131 "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
1.132 P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')"
1.133 - by simp
1.134 +by (auto split: instr.split)
1.135
1.136 lemma exec_appendL:
1.137 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
1.138 P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')"
1.139 - by (induction rule: exec_induct) (blast intro!: exec1_appendL)+
1.140 +by (induction rule: exec_induct) (blast intro!: exec1_appendL)+
1.141
1.142 text{* Now we specialise the above lemmas to enable automatic proofs of
1.143 @{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
1.144 @@ -167,13 +127,13 @@
1.145 lemma exec_Cons_1 [intro]:
1.146 "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
1.147 instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
1.148 - by (drule exec_appendL[where P'="[instr]"]) simp
1.149 +by (drule exec_appendL[where P'="[instr]"]) simp
1.150
1.151 lemma exec_appendL_if[intro]:
1.152 "isize P' <= i
1.153 \<Longrightarrow> P \<turnstile> (i - isize P',s,stk) \<rightarrow>* (i',s',stk')
1.154 \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')"
1.155 - by (drule exec_appendL[where P'=P']) simp
1.156 +by (drule exec_appendL[where P'=P']) simp
1.157
1.158 text{* Split the execution of a compound program up into the excution of its
1.159 parts: *}
1.160 @@ -185,10 +145,10 @@
1.161 j'' = isize P + i''
1.162 \<Longrightarrow>
1.163 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
1.164 - by(metis exec_trans[OF exec_appendR exec_appendL_if])
1.165 +by(metis exec_trans[OF exec_appendR exec_appendL_if])
1.166
1.167
1.168 -declare Let_def[simp]
1.169 +declare Let_def[simp]
1.170
1.171
1.172 subsection "Compilation"
1.173 @@ -200,7 +160,7 @@
1.174
1.175 lemma acomp_correct[intro]:
1.176 "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)"
1.177 - by (induction a arbitrary: stk) fastforce+
1.178 +by (induction a arbitrary: stk) fastforce+
1.179
1.180 fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
1.181 "bcomp (Bc v) c n = (if v=c then [JMP n] else [])" |
1.182 @@ -226,7 +186,7 @@
1.183 from Not(1)[where c="~c"] Not(2) show ?case by fastforce
1.184 next
1.185 case (And b1 b2)
1.186 - from And(1)[of "if c then isize (bcomp b2 c n) else isize (bcomp b2 c n) + n"
1.187 + from And(1)[of "if c then isize(bcomp b2 c n) else isize(bcomp b2 c n) + n"
1.188 "False"]
1.189 And(2)[of n "c"] And(3)
1.190 show ?case by fastforce