src/HOL/IMP/Comp_Rev.thy

 
 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''" 
-  by (fastsimp simp del: split_paired_Ex)
+  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 intro: exec_Suc)
     

   thus "succs (x#xs) n \<subseteq> ?x \<union> ?xs" ..
   
   { fix p assume "p \<in> ?x \<or> p \<in> ?xs"
     hence "p \<in> succs (x#xs) n"
     proof
-      assume "p \<in> ?x" thus ?thesis by (fastsimp simp: succs_def)
+      assume "p \<in> ?x" thus ?thesis by (fastforce simp: succs_def)
     next
       assume "p \<in> ?xs"
       then obtain i where "?isuccs p xs (1+n) i"
         unfolding succs_def by auto
       hence "?isuccs p (x#xs) n (1+i)"

   shows "fst c' \<in> succs P 0"
   using assms by (auto elim!: iexec1.cases simp: succs_def isuccs_def)
 
 lemma succs_shift:
   "(p - n \<in> succs P 0) = (p \<in> succs P n)" 
-  by (fastsimp simp: succs_def isuccs_def split: instr.split)
+  by (fastforce simp: succs_def isuccs_def split: instr.split)
   
 lemma inj_op_plus [simp]:
   "inj (op + (i::int))"
   by (metis add_minus_cancel inj_on_inverseI)
 

   case Assign thus ?case by simp
 next
   case (Semi c1 c2)
   from Semi.prems
   show ?case 
-    by (fastsimp dest: Semi.hyps [THEN subsetD])
+    by (fastforce dest: Semi.hyps [THEN subsetD])
 next
   case (If b c1 c2)
   from If.prems
   show ?case
     by (auto dest!: If.hyps [THEN subsetD] simp: isuccs_def succs_Cons)

   note split_paired_Ex [simp del]
 
   { assume "j0 \<in> {0 ..< isize c}"
     with j0 j rest c
     have ?case
-      by (fastsimp dest!: Suc.hyps intro!: exec_Suc)
+      by (fastforce dest!: Suc.hyps intro!: exec_Suc)
   } moreover {
     assume "j0 \<notin> {0 ..< isize c}"
     moreover
     from c j0 have "j0 \<in> succs c 0"
       by (auto dest: succs_iexec1)
     ultimately
     have "j0 \<in> exits c" by (simp add: exits_def)
     with c j0 rest
-    have ?case by fastsimp
+    have ?case by fastforce
   }
   ultimately
   show ?case by cases
 qed
 

   from step `isize P \<le> i`
   have "P' \<turnstile> (i - isize P, s, stk) \<rightarrow> (i' - isize P, s'', stk'')" 
     by (rule exec1_drop_left)
   also
   then have "i' - isize P \<in> succs P' 0"
-    by (fastsimp dest!: succs_iexec1)
+    by (fastforce dest!: succs_iexec1)
   with `exits P' \<subseteq> {0..}`
   have "isize P \<le> i'" by (auto simp: exits_def)
   from rest this `exits P' \<subseteq> {0..}`     
   have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')"
     by (rule Suc.hyps)

   assumes exits: "exits P' \<subseteq> {0..}"
   shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (isize P, s'', stk'') \<and> 
                            P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - isize P, s', stk')"
 proof (cases "P")
   case Nil with exec
-  show ?thesis by fastsimp
+  show ?thesis by fastforce
 next
   case Cons
   hence "0 < isize P" by simp
   with exec P closed
   obtain k1 k2 s'' stk'' where

   moreover
   have "j = isize P + (j - isize P)" by simp
   then obtain j0 where "j = isize P + j0" ..
   ultimately
   show ?thesis using exits
-    by (fastsimp dest: exec_n_drop_left)
+    by (fastforce dest: exec_n_drop_left)
 qed
 
 
 subsection {* Correctness theorem *}
 

     "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (isize (acomp a1), s1, stk1)"
     "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (isize (acomp a2), s2, stk2)" 
        "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
     by (auto dest!: exec_n_split_full)
 
-  thus ?case by (fastsimp dest: Plus.hyps simp: exec_n_simps)
+  thus ?case by (fastforce dest: Plus.hyps simp: exec_n_simps)
 qed (auto simp: exec_n_simps)
 
 lemma bcomp_split:
   assumes "bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')" 
           "j \<notin> {0..<isize (bcomp b c i)}" "0 \<le> i"
   shows "\<exists>s'' stk'' i' k m. 
            bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and>
            (i' = isize (bcomp b c i) \<or> i' = i + isize (bcomp b c i)) \<and>
            bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and>
            n = k + m"
-  using assms by (cases "bcomp b c i = []") (fastsimp dest!: exec_n_drop_right)+
+  using assms by (cases "bcomp b c i = []") (fastforce dest!: exec_n_drop_right)+
 
 lemma bcomp_exec_n [dest]:
   assumes "bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')"
           "isize (bcomp b c j) \<le> i" "0 \<le> j"
   shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>

   case B thus ?case 
     by (simp split: split_if_asm add: exec_n_simps)
 next
   case (Not b) 
   from Not.prems show ?case
-    by (fastsimp dest!: Not.hyps) 
+    by (fastforce dest!: Not.hyps) 
 next
   case (And b1 b2)
   
   let ?b2 = "bcomp b2 c j" 
   let ?m  = "if c then isize ?b2 else isize ?b2 + j"

   from b1 j
   have "i' = isize ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
     by (auto dest!: And.hyps)
   with b2 j
   show ?case 
-    by (fastsimp dest!: And.hyps simp: exec_n_end split: split_if_asm)
+    by (fastforce dest!: And.hyps 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 *) 
 qed
 

   case SKIP
   thus ?case by auto
 next
   case (Assign x a)
   thus ?case
-    by simp (fastsimp dest!: exec_n_split_full simp: exec_n_simps)
+    by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps)
 next
   case (Semi c1 c2)
-  thus ?case by (fastsimp dest!: exec_n_split_full)
+  thus ?case by (fastforce dest!: exec_n_split_full)
 next
   case (If b c1 c2)
   note If.hyps [dest!]
 
   let ?if = "IF b THEN c1 ELSE c2"

   
   with cs have cs':
     "ccomp c1@JMP (isize (ccomp c2))#ccomp c2 \<turnstile> 
        (if bval b s then 0 else isize (ccomp c1)+1, s, stk) \<rightarrow>^m
        (1 + isize (ccomp c1) + isize (ccomp c2), t, stk')"
-    by (fastsimp dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)
+    by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)
      
   show ?case
   proof (cases "bval b s")
     case True with cs'
     show ?thesis
       by simp
-         (fastsimp dest: exec_n_drop_right 
+         (fastforce dest: exec_n_drop_right 
                    split: split_if_asm simp: exec_n_simps)
   next
     case False with cs'
     show ?thesis
       by (auto dest!: exec_n_drop_Cons exec_n_drop_left 

     
     { assume "\<not> bval b s"
       with "1.prems"
       have ?case
         by simp
-           (fastsimp dest!: bcomp_exec_n bcomp_split 
+           (fastforce dest!: bcomp_exec_n bcomp_split 
                      simp: exec_n_simps)
     } moreover {
       assume b: "bval b s"
       let ?c0 = "WHILE b DO c"
       let ?cs = "ccomp ?c0"

       
       from "1.prems" b
       obtain k where
         cs: "?cs \<turnstile> (isize ?bs, s, stk) \<rightarrow>^k (isize ?cs, t, stk')" and
         k:  "k \<le> n"
-        by (fastsimp dest!: bcomp_split)
+        by (fastforce dest!: bcomp_split)
       
       have ?case
       proof cases
         assume "ccomp c = []"
         with cs k