src/HOL/IMP/AbsInt0_fun.thy

 and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "pfp_above f x0 \<sqsubseteq> p"
 proof-
   let ?F = "lift f x0"
   obtain k where "pfp_above f x0 = (?F^^k) x0"
     using pfp_funpow `pfp_above f x0 \<noteq> Top`
-    by(fastsimp simp add: pfp_above_def)
+    by(fastforce simp add: pfp_above_def)
   moreover
   { fix n have "(?F^^n) x0 \<sqsubseteq> p"
     proof(induct n)
       case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
     next

 shows "pfp_above f x0 \<sqsubseteq> x0 \<squnion> f(pfp_above f x0)"
 proof-
   let ?p = "pfp_above f x0"
   obtain k where 1: "?p = ((f\<up>x0)^^k) x0"
     using pfp_funpow `?p \<noteq> Top`
-    by(fastsimp simp add: pfp_above_def)
+    by(fastforce simp add: pfp_above_def)
   thus ?thesis using chain mono by simp
 qed
 
 end
 

 "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
 "AI (WHILE b DO c) S = pfp_above (AI c) S"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
 proof(induct c arbitrary: s t S0)
-  case SKIP thus ?case by fastsimp
+  case SKIP thus ?case by fastforce
 next
   case Assign thus ?case by (auto simp: aval'_sound)
 next
   case Semi thus ?case by auto
 next