src/HOL/Bali/DefiniteAssignmentCorrect.thy

   qed
 next
   case False
   with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Body D c-\<succ>v\<rightarrow>s1"
                                  "s0 = (Some abr, s0')"
-    by (cases s0) fastsimp
+    by (cases s0) fastforce
   with this jump
   show ?thesis
     by (cases) (simp)
 qed
 

     by (rule Body_no_jump)
 next
   case False
   with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Methd D sig-\<succ>v\<rightarrow>s1"
                                  "s0 = (Some abr, s0')"
-    by (cases s0) fastsimp
+    by (cases s0) fastforce
   with this jump
   show ?thesis
     by (cases) (simp)
 qed
 

     by simp
   ultimately show ?thesis
     apply (rule jumpNestingOk_evalE)
     apply assumption
     apply simp
-    apply fastsimp
+    apply fastforce
     done
 qed
 
 lemmas jumpNestingOk_eval_no_jumpE 
        = jumpNestingOk_eval_no_jump [THEN conjE,rule_format]

       from nrm_c2' nrm_c2 A
       have "?NormalAssigned s2 A" 
         by blast
       moreover from brk_c2' brk_c2 A
       have "?BreakAssigned s1 s2 A" 
-        by fastsimp
+        by fastforce
       with True 
       have "?BreakAssigned (Norm s0) s2 A" by simp
       moreover from res_c2 True
       have "?ResAssigned (Norm s0) s2"
         by simp

         from nrm_c1' nrm_c1 A
         have "?NormalAssigned s2 A" 
           by blast
         moreover from brk_c1' brk_c1 A
         have "?BreakAssigned s1 s2 A" 
-          by fastsimp
+          by fastforce
         with normal_s1
         have "?BreakAssigned (Norm s0) s2 A" by simp
         moreover from res_c1 normal_s1 have "?ResAssigned (Norm s0) s2"
           by simp
         ultimately show ?thesis by (intro conjI)

         from nrm_c2' nrm_c2 A
         have "?NormalAssigned s2 A" 
           by blast
         moreover from brk_c2' brk_c2 A
         have "?BreakAssigned s1 s2 A" 
-          by fastsimp
+          by fastforce
         with normal_s1
         have "?BreakAssigned (Norm s0) s2 A" by simp
         moreover from res_c2 normal_s1 have "?ResAssigned (Norm s0) s2"
           by simp
         ultimately show ?thesis by (intro conjI)

           moreover 
           have "?BreakAssigned (Norm s0) s3 A" 
           proof -
             from brk_A_A' brk_A' 
             have "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A" 
-              by fastsimp
+              by fastforce
             moreover
             from True have "normal (abupd (absorb (Cont l)) s2)"
               by (cases s2) auto
             ultimately show ?thesis
               by simp

           with eval_while 
           have eq_s3_s2: "s3=s2"
             by auto
           with nrm_C_C' nrm_C' A
           have "?NormalAssigned s3 A"
-            by fastsimp
+            by fastforce
           moreover
           from eq_s3_s2 brk_C_C' brk_C' normal_s1 A
           have "?BreakAssigned (Norm s0) s3 A"
-            by fastsimp
+            by fastforce
           moreover 
           from eq_s3_s2 res_s2 normal_s1 have "?ResAssigned (Norm s0) s3"
             by simp
           ultimately show ?thesis by (intro conjI)
         qed

           have "?BreakAssigned (Norm s0) s3 A"
           proof -
             from brkAss_C2 have "?BreakAssigned (Norm s0) s3 C2'"
               by (cases s2) (auto simp add: new_xcpt_var_def)
             with brk_C2' A show ?thesis 
-              by fastsimp
+              by fastforce
           qed
           moreover
           from resAss_s3 have "?ResAssigned (Norm s0) s3"
             by (cases s2) ( simp add: new_xcpt_var_def)
           ultimately show ?thesis by (intro conjI)

         by simp
       from nrmAss_C2' nrm_C2' have "?NormalAssigned s2 C2"
         by blast
       moreover
       from brkAss_C2' brk_C2' have "?BreakAssigned (Norm s1) s2 C2"
-        by fastsimp
+        by fastforce
       ultimately
       show ?thesis
         using that resAss_s2' by simp
     qed
     note s3 = `s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)

           from normal_s3 s3
           have "normal (x1,s1)"
             by (cases s2) (simp add: abrupt_if_def)
           with normal_s3 nrmAss_C1 s3 s1_s2
           show ?thesis
-            by fastsimp
+            by fastforce
         qed
         moreover 
         have "nrm C2 \<subseteq> dom (locals (snd s3))"
         proof -
           from normal_s3 s3
           have "normal s2"
             by (cases s2) (simp add: abrupt_if_def)
           with normal_s3 nrmAss_C2 s3 s1_s2
           show ?thesis
-            by fastsimp
+            by fastforce
         qed
         ultimately have "nrm C1 \<union> nrm C2 \<subseteq> \<dots>"
           by (rule Un_least)
         with nrm_A show ?thesis
           by simp