1.1 --- a/src/HOL/IMP/Comp_Rev.thy	Thu Jul 28 11:49:03 2011 +0200
     1.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Thu Jul 28 15:15:26 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  text {* Execution in @{term n} steps for simpler induction *}
     1.5  primrec 
     1.6    exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" 
     1.7 -  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,55,55] 55)
     1.8 +  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55)
     1.9  where 
    1.10    "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" |
    1.11    "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"
    1.12 @@ -41,7 +41,7 @@
    1.13  lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
    1.14  
    1.15  lemma exec_Suc [trans]:
    1.16 -  "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^Suc n c''" 
    1.17 +  "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''" 
    1.18    by (fastsimp simp del: split_paired_Ex)
    1.19  
    1.20  lemma exec_exec_n:

     2.1 --- a/src/HOL/IMP/Compiler.thy	Thu Jul 28 11:49:03 2011 +0200
     2.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Jul 28 15:15:26 2011 +0200
     2.3 @@ -65,22 +65,17 @@
     2.4  
     2.5  declare iexec1.intros
     2.6  
     2.7 -(* FIXME: why does code gen not work with fun? *)
     2.8 -inductive
     2.9 -  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
    2.10 -    ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) where
    2.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'"
    2.12 -
    2.13 -code_pred exec1 .
    2.14 -
    2.15 -declare exec1.intros [intro!]
    2.16 -
    2.17 -inductive_cases exec1_elim [elim!]: "P \<turnstile> c \<rightarrow> c'"
    2.18 -
    2.19 -lemma exec1_simp [simp]:
    2.20 +definition
    2.21 +  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) 
    2.22 +where
    2.23    "P \<turnstile> c \<rightarrow> c' = 
    2.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)"
    2.25 -  by auto
    2.26 +
    2.27 +declare exec1_def [simp] 
    2.28 +
    2.29 +lemma exec1I [intro, code_pred_intro]:
    2.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'"
    2.31 +  by simp
    2.32  
    2.33  inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
    2.34  where
    2.35 @@ -91,7 +86,7 @@
    2.36  
    2.37  lemmas exec_induct = exec.induct[split_format(complete)]
    2.38  
    2.39 -code_pred exec .
    2.40 +code_pred exec by force
    2.41  
    2.42  values
    2.43    "{(i,map t [''x'',''y''],stk) | i t stk.