src/HOL/IMP/Compiler2.thy

   "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''" 
   by (fastforce simp del: split_paired_Ex)
 
 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')"
   by (blast intro: exec_exec_n exec_n_exec)
 
 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'"
   by (cases c') simp
 

   (\<exists>c. P \<turnstile> (n,stk,s) \<rightarrow> c \<and> P \<turnstile> c \<rightarrow>^(k - 1) (n',stk',s') \<and> 0 < k)"
   by (cases k) auto
 
 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> 
   P \<turnstile> (n,s,stk) \<rightarrow>^k (n',s',stk') = (n' = n \<and> stk'=stk \<and> s'=s \<and> k =0)"
   by (cases k) (auto simp: exec1_end)

 lemma exec1_split:
   fixes i j :: int
   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
   assumes "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow>^n (j, s')"
           "0 \<le> i" "i < size c" 

       by (fastforce dest!: Suc.IH intro!: exec_Suc)
   } moreover {
     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
     have ?case by fastforce
   }

   then obtain i' :: int where "i = size P1 + i'" ..
   moreover
   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:
   fixes i n :: int
   assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"

   from step `size P \<le> i`
   have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" 
     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..}`     
   have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')"
     by (rule Suc.IH)

     "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (size (acomp a1), s1, stk1)"
     "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (size (acomp a2), s2, stk2)" 
        "[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
   assumes "bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')" 
           "j \<notin> {0..<size (bcomp b c i)}" "0 \<le> i"

           "size (bcomp b c j) \<le> i" "0 \<le> j"
   shows "i = size(bcomp b c j) + (if c = bval b s then j else 0) \<and>
          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
     by (fastforce dest!: Not.IH) 
 next

   with b2 j
   show ?case 
     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!]:
   "ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s"
   by (induct c) auto

   case SKIP
   thus ?case by auto
 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)
 next
   case (If b c1 c2)

   proof (cases "bval b s")
     case True with cs'
     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
       by (auto dest!: exec_n_drop_Cons exec_n_drop_left 
                simp: exits_Cons isuccs_def)

         assume "ccomp c = []"
         with cs k
         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
         assume "ccomp c \<noteq> []"
         with cs

         moreover
         from rest m k stk
         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
         show ?case using b by blast
       qed