src/HOL/UNITY/Detects.thy
 changeset 13805 3786b2fd6808 parent 13798 4c1a53627500 child 13812 91713a1915ee
```--- a/src/HOL/UNITY/Detects.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Detects.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -15,47 +15,47 @@
op_Equality :: "['a set, 'a set] => 'a set"          (infixl "<==>" 60)

defs
-  Detects_def:  "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
-  Equality_def: "A <==> B == (-A Un B) Int (A Un -B)"
+  Detects_def:  "A Detects B == (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
+  Equality_def: "A <==> B == (-A \<union> B) \<inter> (A \<union> -B)"

(* Corollary from Sectiom 3.6.4 *)

-lemma Always_at_FP: "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))"
+lemma Always_at_FP: "F \<in> A LeadsTo B ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
-apply (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))")
-apply (subgoal_tac [2] " (FP F Int A Int - B) = (A Int (FP F Int -B))")
-apply (subgoal_tac "(B Int (FP F Int -B)) = {}")
+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))")
+apply (subgoal_tac "(B \<inter> (FP F \<inter> -B)) = {}")
apply auto
apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
done

lemma Detects_Trans:
-     "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C"
+     "[| F \<in> A Detects B; F \<in> B Detects C |] ==> F \<in> A Detects C"
apply (unfold Detects_def Int_def)
apply (simp (no_asm))
apply safe
apply auto
-apply (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))")
+apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
apply (blast intro: Always_weaken)
done

-lemma Detects_refl: "F : A Detects A"
+lemma Detects_refl: "F \<in> A Detects A"
apply (unfold Detects_def)
done

-lemma Detects_eq_Un: "(A<==>B) = (A Int B) Un (-A Int -B)"
+lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
apply (unfold Equality_def)
apply blast
done

(*Not quite antisymmetry: sets A and B agree in all reachable states *)
lemma Detects_antisym:
-     "[| F : A Detects B;  F : B Detects A|] ==> F : Always (A <==> B)"
+     "[| F \<in> A Detects B;  F \<in> B Detects A|] ==> F \<in> Always (A <==> B)"
apply (unfold Detects_def Equality_def)
done
@@ -64,7 +64,7 @@
(* Theorem from Section 3.8 *)

lemma Detects_Always:
-     "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))"
+     "F \<in> A Detects B ==> 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 (blast dest: Always_at_FP intro: Always_weaken)
@@ -73,11 +73,11 @@
(* Theorem from exercise 11.1 Section 11.3.1 *)