diff -r 7a1537b54f16 -r c10bd1f49ff5 src/HOL/IMP/Compiler.thy
--- 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