1.1 --- a/src/HOL/IMP/Compiler.thy Thu Jul 28 11:49:03 2011 +0200
1.2 +++ b/src/HOL/IMP/Compiler.thy Thu Jul 28 15:15:26 2011 +0200
1.3 @@ -65,22 +65,17 @@
1.4
1.5 declare iexec1.intros
1.6
1.7 -(* FIXME: why does code gen not work with fun? *)
1.8 -inductive
1.9 - exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
1.10 - ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) where
1.11 - "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
1.12 -
1.13 -code_pred exec1 .
1.14 -
1.15 -declare exec1.intros [intro!]
1.16 -
1.17 -inductive_cases exec1_elim [elim!]: "P \<turnstile> c \<rightarrow> c'"
1.18 -
1.19 -lemma exec1_simp [simp]:
1.20 +definition
1.21 + exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50)
1.22 +where
1.23 "P \<turnstile> c \<rightarrow> c' =
1.24 (\<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.25 - by auto
1.26 +
1.27 +declare exec1_def [simp]
1.28 +
1.29 +lemma exec1I [intro, code_pred_intro]:
1.30 + "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
1.31 + by simp
1.32
1.33 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
1.34 where
1.35 @@ -91,7 +86,7 @@
1.36
1.37 lemmas exec_induct = exec.induct[split_format(complete)]
1.38
1.39 -code_pred exec .
1.40 +code_pred exec by force
1.41
1.42 values
1.43 "{(i,map t [''x'',''y''],stk) | i t stk.