# HG changeset patch
# User kleing
# Date 1311858926 -7200
# Node ID ab4d8499815c3c9d55bb73be5c37e5cdc1bcc35b
# Parent  04fd92795458f1f8101a83f897e9991f6c5e2564
resolved code_pred FIXME in IMP; clearer notation for exec_n

diff -r 04fd92795458 -r ab4d8499815c src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Thu Jul 28 11:49:03 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy	Thu Jul 28 15:15:26 2011 +0200
@@ -9,7 +9,7 @@
 text {* Execution in @{term n} steps for simpler induction *}
 primrec 
   exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" 
-  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,55,55] 55)
+  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55)
 where 
   "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" |
   "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"
@@ -41,7 +41,7 @@
 lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
 
 lemma exec_Suc [trans]:
-  "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^Suc n c''" 
+  "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''" 
   by (fastsimp simp del: split_paired_Ex)
 
 lemma exec_exec_n:
diff -r 04fd92795458 -r ab4d8499815c src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Jul 28 11:49:03 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy	Thu Jul 28 15:15:26 2011 +0200
@@ -65,22 +65,17 @@
 
 declare iexec1.intros
 
-(* FIXME: why does code gen not work with fun? *)
-inductive
-  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
-    ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) where
- "\<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'"
-
-code_pred exec1 .
-
-declare exec1.intros [intro!]
-
-inductive_cases exec1_elim [elim!]: "P \<turnstile> c \<rightarrow> c'"
-
-lemma exec1_simp [simp]:
+definition
+  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) 
+where
   "P \<turnstile> c \<rightarrow> c' = 
    (\<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)"
-  by auto
+
+declare exec1_def [simp] 
+
+lemma exec1I [intro, code_pred_intro]:
+  "\<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'"
+  by simp
 
 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
 where
@@ -91,7 +86,7 @@
 
 lemmas exec_induct = exec.induct[split_format(complete)]
 
-code_pred exec .
+code_pred exec by force
 
 values
   "{(i,map t [''x'',''y''],stk) | i t stk.