--- a/src/HOL/UNITY/Detects.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Detects.thy Sat Feb 08 16:05:33 2003 +0100
@@ -21,7 +21,8 @@
(* Corollary from Sectiom 3.6.4 *)
-lemma Always_at_FP: "F \<in> A LeadsTo B ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
+lemma Always_at_FP:
+ "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
apply (rule LeadsTo_empty)
apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
@@ -36,8 +37,7 @@
apply (unfold Detects_def Int_def)
apply (simp (no_asm))
apply safe
-apply (rule_tac [2] LeadsTo_Trans)
-apply auto
+apply (rule_tac [2] LeadsTo_Trans, auto)
apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
apply (blast intro: Always_weaken)
apply (simp add: Always_Int_distrib)
@@ -49,9 +49,7 @@
done
lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
-apply (unfold Equality_def)
-apply blast
-done
+by (unfold Equality_def, blast)
(*Not quite antisymmetry: sets A and B agree in all reachable states *)
lemma Detects_antisym:
@@ -64,9 +62,9 @@
(* Theorem from Section 3.8 *)
lemma Detects_Always:
- "F \<in> A Detects B ==> F \<in> Always ((-(FP F)) \<union> (A <==> B))"
+ "[|F \<in> A Detects B; all_total F|] ==> F \<in> Always (-(FP F) \<union> (A <==> B))"
apply (unfold Detects_def Equality_def)
-apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib)
+apply (simp add: Un_Int_distrib Always_Int_distrib)
apply (blast dest: Always_at_FP intro: Always_weaken)
done
@@ -75,7 +73,7 @@
lemma Detects_Imp_LeadstoEQ:
"F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
apply (unfold Detects_def Equality_def)
-apply (rule_tac B = "B" in LeadsTo_Diff)
+apply (rule_tac B = B in LeadsTo_Diff)
apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
apply (blast intro: Always_LeadsTo_weaken)
done