--- a/src/HOL/IMP/Compiler.thy Thu Aug 08 16:38:50 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy Thu Aug 08 18:13:12 2013 +0200
@@ -2,7 +2,7 @@
header "Compiler for IMP"
-theory Compiler imports Big_Step
+theory Compiler imports Big_Step Star
begin
subsection "List setup"
@@ -63,24 +63,25 @@
"P \<turnstile> c \<rightarrow> c' =
(\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < size P)"
+(*
declare exec1_def [simp]
+*)
lemma exec1I [intro, code_pred_intro]:
"c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
\<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
-by simp
+by (simp add: exec1_def)
-inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
- ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
+abbreviation
+ exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
where
-refl: "P \<turnstile> c \<rightarrow>* c" |
-step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
+ "exec P \<equiv> star (exec1 P)"
+
+declare star.step[intro]
-declare refl[intro] step[intro]
+lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]
-lemmas exec_induct = exec.induct[split_format(complete)]
-
-code_pred exec by fastforce
+code_pred exec1 by (metis exec1_def)
values
"{(i,map t [''x'',''y''],stk) | i t stk.
@@ -90,9 +91,6 @@
subsection{* Verification infrastructure *}
-lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
-by (induction rule: exec.induct) fastforce+
-
text{* Below we need to argue about the execution of code that is embedded in
larger programs. For this purpose we show that execution is preserved by
appending code to the left or right of a program. *}
@@ -102,16 +100,17 @@
by(auto split:instr.split)
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
-by auto
+by (auto simp: exec1_def)
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
-by (induction rule: exec.induct) (fastforce intro: exec1_appendR)+
+by (induction rule: star.induct) (fastforce intro: exec1_appendR)+
lemma exec1_appendL:
fixes i i' :: int
shows
"P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
+ unfolding exec1_def
by (auto split: instr.split)
lemma exec_appendL:
@@ -154,7 +153,7 @@
j'' = size P + i''
\<Longrightarrow>
P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
-by(metis exec_trans[OF exec_appendR exec_appendL_if])
+by(metis star_trans[OF exec_appendR exec_appendL_if])
declare Let_def[simp]
@@ -237,7 +236,7 @@
moreover
have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
using Seq.IH(2) by fastforce
- ultimately show ?case by simp (blast intro: exec_trans)
+ ultimately show ?case by simp (blast intro: star_trans)
next
case (WhileTrue b s1 c s2 s3)
let ?cc = "ccomp c"
@@ -253,7 +252,7 @@
by fastforce
moreover
have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2))
- ultimately show ?case by(blast intro: exec_trans)
+ ultimately show ?case by(blast intro: star_trans)
qed fastforce+
end
--- a/src/HOL/IMP/Compiler2.thy Thu Aug 08 16:38:50 2013 +0200
+++ b/src/HOL/IMP/Compiler2.thy Thu Aug 08 18:13:12 2013 +0200
@@ -50,7 +50,7 @@
lemma exec_exec_n:
"P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'"
- by (induct rule: exec.induct) (auto simp del: exec1_def intro: exec_Suc)
+ by (induct rule: star.induct) (auto intro: exec_Suc)
lemma exec_eq_exec_n:
"(P \<turnstile> c \<rightarrow>* c') = (\<exists>n. P \<turnstile> c \<rightarrow>^n c')"
@@ -58,7 +58,7 @@
lemma exec_n_Nil [simp]:
"[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)"
- by (induct k) auto
+ by (induct k) (auto simp: exec1_def)
lemma exec1_exec_n [intro!]:
"P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'"
@@ -75,7 +75,7 @@
lemma exec1_end:
"size P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'"
- by auto
+ by (auto simp: exec1_def)
lemma exec_n_end:
"size P <= (n::int) \<Longrightarrow>
@@ -262,7 +262,7 @@
shows
"P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size c \<Longrightarrow>
c \<turnstile> (i,s) \<rightarrow> (j - size P, s')"
- by (auto split: instr.splits)
+ by (auto split: instr.splits simp: exec1_def)
lemma exec_n_split:
fixes i j :: int
@@ -304,7 +304,7 @@
assume "j0 \<notin> {0 ..< size c}"
moreover
from c j0 have "j0 \<in> succs c 0"
- by (auto dest: succs_iexec1 simp del: iexec.simps)
+ by (auto dest: succs_iexec1 simp: exec1_def simp del: iexec.simps)
ultimately
have "j0 \<in> exits c" by (simp add: exits_def)
with c j0 rest
@@ -343,7 +343,8 @@
have "n = size P1 + (n - size P1)" by simp
then obtain n' :: int where "n = size P1 + n'" ..
ultimately
- show ?thesis using assms by (clarsimp simp del: iexec.simps)
+ show ?thesis using assms
+ by (clarsimp simp: exec1_def simp del: iexec.simps)
qed
lemma exec_n_drop_left:
@@ -365,7 +366,7 @@
by (rule exec1_drop_left)
moreover
then have "i' - size P \<in> succs P' 0"
- by (fastforce dest!: succs_iexec1 simp del: iexec.simps)
+ by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps)
with `exits P' \<subseteq> {0..}`
have "size P \<le> i'" by (auto simp: exits_def)
from rest this `exits P' \<subseteq> {0..}`
@@ -438,8 +439,8 @@
"[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
by (auto dest!: exec_n_split_full)
- thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps)
-qed (auto simp: exec_n_simps)
+ thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps exec1_def)
+qed (auto simp: exec_n_simps exec1_def)
lemma bcomp_split:
fixes i j :: int
@@ -460,7 +461,7 @@
s' = s \<and> stk' = stk"
using assms proof (induction b arbitrary: c j i n s' stk')
case Bc thus ?case
- by (simp split: split_if_asm add: exec_n_simps)
+ by (simp split: split_if_asm add: exec_n_simps exec1_def)
next
case (Not b)
from Not.prems show ?case
@@ -488,7 +489,7 @@
by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm)
next
case Less
- thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *)
+ thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps exec1_def) (* takes time *)
qed
lemma ccomp_empty [elim!]:
@@ -506,7 +507,7 @@
next
case (Assign x a)
thus ?case
- by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps)
+ by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps exec1_def)
next
case (Seq c1 c2)
thus ?case by (fastforce dest!: exec_n_split_full)
@@ -542,7 +543,8 @@
show ?thesis
by simp
(fastforce dest: exec_n_drop_right
- split: split_if_asm simp: exec_n_simps)
+ split: split_if_asm
+ simp: exec_n_simps exec1_def)
next
case False with cs'
show ?thesis
@@ -583,7 +585,7 @@
obtain m where
"?cs \<turnstile> (0,s,stk) \<rightarrow>^m (size (ccomp ?c0), t, stk')"
"m < n"
- by (auto simp: exec_n_step [where k=k])
+ by (auto simp: exec_n_step [where k=k] exec1_def)
with "1.IH"
show ?case by blast
next
@@ -603,7 +605,7 @@
obtain k' where
"?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (size ?cs, t, stk')"
"k' < n"
- by (auto simp: exec_n_step [where k=m])
+ by (auto simp: exec_n_step [where k=m] exec1_def)
with "1.IH"
have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast
ultimately