diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Constrains.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -18,65 +18,65 @@
 inductive "traces init acts"  
   intros 
          (*Initial trace is empty*)
-    Init:  "s: init ==> (s,[]) : traces init acts"
+    Init:  "s \<in> init ==> (s,[]) \<in> traces init acts"
 
-    Acts:  "[| act: acts;  (s,evs) : traces init acts;  (s,s'): act |]
-	    ==> (s', s#evs) : traces init acts"
+    Acts:  "[| act: acts;  (s,evs) \<in> traces init acts;  (s,s'): act |]
+	    ==> (s', s#evs) \<in> traces init acts"
 
 
 consts reachable :: "'a program => 'a set"
 
 inductive "reachable F"
   intros 
-    Init:  "s: Init F ==> s : reachable F"
+    Init:  "s \<in> Init F ==> s \<in> reachable F"
 
-    Acts:  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
-	    ==> s' : reachable F"
+    Acts:  "[| act: Acts F;  s \<in> reachable F;  (s,s'): act |]
+	    ==> s' \<in> reachable F"
 
 constdefs
   Constrains :: "['a set, 'a set] => 'a program set"  (infixl "Co" 60)
-    "A Co B == {F. F : (reachable F Int A)  co  B}"
+    "A Co B == {F. F \<in> (reachable F \<inter> A)  co  B}"
 
   Unless  :: "['a set, 'a set] => 'a program set"     (infixl "Unless" 60)
-    "A Unless B == (A-B) Co (A Un B)"
+    "A Unless B == (A-B) Co (A \<union> B)"
 
   Stable     :: "'a set => 'a program set"
     "Stable A == A Co A"
 
   (*Always is the weak form of "invariant"*)
   Always :: "'a set => 'a program set"
-    "Always A == {F. Init F <= A} Int Stable A"
+    "Always A == {F. Init F \<subseteq> A} \<inter> Stable A"
 
-  (*Polymorphic in both states and the meaning of <= *)
+  (*Polymorphic in both states and the meaning of \<le> *)
   Increasing :: "['a => 'b::{order}] => 'a program set"
-    "Increasing f == INT z. Stable {s. z <= f s}"
+    "Increasing f == \<Inter>z. Stable {s. z \<le> f s}"
 
 
 subsection{*traces and reachable*}
 
 lemma reachable_equiv_traces:
-     "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"
+     "reachable F = {s. \<exists>evs. (s,evs): traces (Init F) (Acts F)}"
 apply safe
 apply (erule_tac [2] traces.induct)
 apply (erule reachable.induct)
 apply (blast intro: reachable.intros traces.intros)+
 done
 
-lemma Init_subset_reachable: "Init F <= reachable F"
+lemma Init_subset_reachable: "Init F \<subseteq> reachable F"
 by (blast intro: reachable.intros)
 
 lemma stable_reachable [intro!,simp]:
-     "Acts G <= Acts F ==> G : stable (reachable F)"
+     "Acts G \<subseteq> Acts F ==> G \<in> stable (reachable F)"
 by (blast intro: stableI constrainsI reachable.intros)
 
 (*The set of all reachable states is an invariant...*)
-lemma invariant_reachable: "F : invariant (reachable F)"
+lemma invariant_reachable: "F \<in> invariant (reachable F)"
 apply (simp add: invariant_def)
 apply (blast intro: reachable.intros)
 done
 
 (*...in fact the strongest invariant!*)
-lemma invariant_includes_reachable: "F : invariant A ==> reachable F <= A"
+lemma invariant_includes_reachable: "F \<in> invariant A ==> reachable F \<subseteq> A"
 apply (simp add: stable_def constrains_def invariant_def)
 apply (rule subsetI)
 apply (erule reachable.induct)
@@ -86,55 +86,55 @@
 
 subsection{*Co*}
 
-(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
+(*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
 lemmas constrains_reachable_Int =  
     subset_refl [THEN stable_reachable [unfolded stable_def], 
                  THEN constrains_Int, standard]
 
 (*Resembles the previous definition of Constrains*)
 lemma Constrains_eq_constrains: 
-     "A Co B = {F. F : (reachable F  Int  A) co (reachable F  Int  B)}"
+     "A Co B = {F. F \<in> (reachable F  \<inter>  A) co (reachable F  \<inter>  B)}"
 apply (unfold Constrains_def)
 apply (blast dest: constrains_reachable_Int intro: constrains_weaken)
 done
 
-lemma constrains_imp_Constrains: "F : A co A' ==> F : A Co A'"
+lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_weaken_L)
 done
 
-lemma stable_imp_Stable: "F : stable A ==> F : Stable A"
+lemma stable_imp_Stable: "F \<in> stable A ==> F \<in> Stable A"
 apply (unfold stable_def Stable_def)
 apply (erule constrains_imp_Constrains)
 done
 
 lemma ConstrainsI: 
-    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A')  
-     ==> F : A Co A'"
+    "(!!act s s'. [| act: Acts F;  (s,s') \<in> act;  s \<in> A |] ==> s': A')  
+     ==> F \<in> A Co A'"
 apply (rule constrains_imp_Constrains)
 apply (blast intro: constrainsI)
 done
 
-lemma Constrains_empty [iff]: "F : {} Co B"
+lemma Constrains_empty [iff]: "F \<in> {} Co B"
 by (unfold Constrains_def constrains_def, blast)
 
-lemma Constrains_UNIV [iff]: "F : A Co UNIV"
+lemma Constrains_UNIV [iff]: "F \<in> A Co UNIV"
 by (blast intro: ConstrainsI)
 
 lemma Constrains_weaken_R: 
-    "[| F : A Co A'; A'<=B' |] ==> F : A Co B'"
+    "[| F \<in> A Co A'; A'<=B' |] ==> F \<in> A Co B'"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_weaken_R)
 done
 
 lemma Constrains_weaken_L: 
-    "[| F : A Co A'; B<=A |] ==> F : B Co A'"
+    "[| F \<in> A Co A'; B \<subseteq> A |] ==> F \<in> B Co A'"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_weaken_L)
 done
 
 lemma Constrains_weaken: 
-   "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'"
+   "[| F \<in> A Co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B Co B'"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_weaken)
 done
@@ -142,14 +142,14 @@
 (** Union **)
 
 lemma Constrains_Un: 
-    "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')"
+    "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<union> B) Co (A' \<union> B')"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_Un [THEN constrains_weaken])
 done
 
 lemma Constrains_UN: 
-  assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
-  shows "F : (UN i:I. A i) Co (UN i:I. A' i)"
+  assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)"
+  shows "F \<in> (\<Union>i \<in> I. A i) Co (\<Union>i \<in> I. A' i)"
 apply (unfold Constrains_def)
 apply (rule CollectI)
 apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, 
@@ -159,83 +159,83 @@
 (** Intersection **)
 
 lemma Constrains_Int: 
-    "[| F : A Co A'; F : B Co B' |] ==> F : (A Int B) Co (A' Int B')"
+    "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<inter> B) Co (A' \<inter> B')"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_Int [THEN constrains_weaken])
 done
 
 lemma Constrains_INT: 
-  assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
-  shows "F : (INT i:I. A i) Co (INT i:I. A' i)"
+  assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)"
+  shows "F \<in> (\<Inter>i \<in> I. A i) Co (\<Inter>i \<in> I. A' i)"
 apply (unfold Constrains_def)
 apply (rule CollectI)
 apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, 
                 THEN constrains_weaken],   auto)
 done
 
-lemma Constrains_imp_subset: "F : A Co A' ==> reachable F Int A <= A'"
+lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable F \<inter> A \<subseteq> A'"
 by (simp add: constrains_imp_subset Constrains_def)
 
-lemma Constrains_trans: "[| F : A Co B; F : B Co C |] ==> F : A Co C"
+lemma Constrains_trans: "[| F \<in> A Co B; F \<in> B Co C |] ==> F \<in> A Co C"
 apply (simp add: Constrains_eq_constrains)
 apply (blast intro: constrains_trans constrains_weaken)
 done
 
 lemma Constrains_cancel:
-     "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"
+     "[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')"
 by (simp add: Constrains_eq_constrains constrains_def, blast)
 
 
 subsection{*Stable*}
 
 (*Useful because there's no Stable_weaken.  [Tanja Vos]*)
-lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B"
+lemma Stable_eq: "[| F \<in> Stable A; A = B |] ==> F \<in> Stable B"
 by blast
 
-lemma Stable_eq_stable: "(F : Stable A) = (F : stable (reachable F Int A))"
+lemma Stable_eq_stable: "(F \<in> Stable A) = (F \<in> stable (reachable F \<inter> A))"
 by (simp add: Stable_def Constrains_eq_constrains stable_def)
 
-lemma StableI: "F : A Co A ==> F : Stable A"
+lemma StableI: "F \<in> A Co A ==> F \<in> Stable A"
 by (unfold Stable_def, assumption)
 
-lemma StableD: "F : Stable A ==> F : A Co A"
+lemma StableD: "F \<in> Stable A ==> F \<in> A Co A"
 by (unfold Stable_def, assumption)
 
 lemma Stable_Un: 
-    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')"
+    "[| F \<in> Stable A; F \<in> Stable A' |] ==> F \<in> Stable (A \<union> A')"
 apply (unfold Stable_def)
 apply (blast intro: Constrains_Un)
 done
 
 lemma Stable_Int: 
-    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')"
+    "[| F \<in> Stable A; F \<in> Stable A' |] ==> F \<in> Stable (A \<inter> A')"
 apply (unfold Stable_def)
 apply (blast intro: Constrains_Int)
 done
 
 lemma Stable_Constrains_Un: 
-    "[| F : Stable C; F : A Co (C Un A') |]    
-     ==> F : (C Un A) Co (C Un A')"
+    "[| F \<in> Stable C; F \<in> A Co (C \<union> A') |]    
+     ==> F \<in> (C \<union> A) Co (C \<union> A')"
 apply (unfold Stable_def)
 apply (blast intro: Constrains_Un [THEN Constrains_weaken])
 done
 
 lemma Stable_Constrains_Int: 
-    "[| F : Stable C; F : (C Int A) Co A' |]    
-     ==> F : (C Int A) Co (C Int A')"
+    "[| F \<in> Stable C; F \<in> (C \<inter> A) Co A' |]    
+     ==> F \<in> (C \<inter> A) Co (C \<inter> A')"
 apply (unfold Stable_def)
 apply (blast intro: Constrains_Int [THEN Constrains_weaken])
 done
 
 lemma Stable_UN: 
-    "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)"
+    "(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Union>i \<in> I. A i)"
 by (simp add: Stable_def Constrains_UN) 
 
 lemma Stable_INT: 
-    "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)"
+    "(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Inter>i \<in> I. A i)"
 by (simp add: Stable_def Constrains_INT) 
 
-lemma Stable_reachable: "F : Stable (reachable F)"
+lemma Stable_reachable: "F \<in> Stable (reachable F)"
 by (simp add: Stable_eq_stable)
 
 
@@ -243,22 +243,22 @@
 subsection{*Increasing*}
 
 lemma IncreasingD: 
-     "F : Increasing f ==> F : Stable {s. x <= f s}"
+     "F \<in> Increasing f ==> F \<in> Stable {s. x \<le> f s}"
 by (unfold Increasing_def, blast)
 
 lemma mono_Increasing_o: 
-     "mono g ==> Increasing f <= Increasing (g o f)"
+     "mono g ==> Increasing f \<subseteq> Increasing (g o f)"
 apply (simp add: Increasing_def Stable_def Constrains_def stable_def 
                  constrains_def)
 apply (blast intro: monoD order_trans)
 done
 
 lemma strict_IncreasingD: 
-     "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}"
+     "!!z::nat. F \<in> Increasing f ==> F \<in> Stable {s. z < f s}"
 by (simp add: Increasing_def Suc_le_eq [symmetric])
 
 lemma increasing_imp_Increasing: 
-     "F : increasing f ==> F : Increasing f"
+     "F \<in> increasing f ==> F \<in> Increasing f"
 apply (unfold increasing_def Increasing_def)
 apply (blast intro: stable_imp_Stable)
 done
@@ -270,17 +270,17 @@
 subsection{*The Elimination Theorem*}
 
 (*The "free" m has become universally quantified! Should the premise be !!m
-instead of ALL m ?  Would make it harder to use in forward proof.*)
+instead of \<forall>m ?  Would make it harder to use in forward proof.*)
 
 lemma Elimination: 
-    "[| ALL m. F : {s. s x = m} Co (B m) |]  
-     ==> F : {s. s x : M} Co (UN m:M. B m)"
+    "[| \<forall>m. F \<in> {s. s x = m} Co (B m) |]  
+     ==> F \<in> {s. s x \<in> M} Co (\<Union>m \<in> M. B m)"
 by (unfold Constrains_def constrains_def, blast)
 
 (*As above, but for the trivial case of a one-variable state, in which the
   state is identified with its one variable.*)
 lemma Elimination_sing: 
-    "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)"
+    "(\<forall>m. F \<in> {m} Co (B m)) ==> F \<in> M Co (\<Union>m \<in> M. B m)"
 by (unfold Constrains_def constrains_def, blast)
 
 
@@ -288,10 +288,10 @@
 
 (** Natural deduction rules for "Always A" **)
 
-lemma AlwaysI: "[| Init F<=A;  F : Stable A |] ==> F : Always A"
+lemma AlwaysI: "[| Init F \<subseteq> A;  F \<in> Stable A |] ==> F \<in> Always A"
 by (simp add: Always_def)
 
-lemma AlwaysD: "F : Always A ==> Init F<=A & F : Stable A"
+lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A"
 by (simp add: Always_def)
 
 lemmas AlwaysE = AlwaysD [THEN conjE, standard]
@@ -299,7 +299,7 @@
 
 
 (*The set of all reachable states is Always*)
-lemma Always_includes_reachable: "F : Always A ==> reachable F <= A"
+lemma Always_includes_reachable: "F \<in> Always A ==> reachable F \<subseteq> A"
 apply (simp add: Stable_def Constrains_def constrains_def Always_def)
 apply (rule subsetI)
 apply (erule reachable.induct)
@@ -307,7 +307,7 @@
 done
 
 lemma invariant_imp_Always: 
-     "F : invariant A ==> F : Always A"
+     "F \<in> invariant A ==> F \<in> Always A"
 apply (unfold Always_def invariant_def Stable_def stable_def)
 apply (blast intro: constrains_imp_Constrains)
 done
@@ -316,55 +316,55 @@
     invariant_reachable [THEN invariant_imp_Always, standard]
 
 lemma Always_eq_invariant_reachable:
-     "Always A = {F. F : invariant (reachable F Int A)}"
+     "Always A = {F. F \<in> invariant (reachable F \<inter> A)}"
 apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains
                  stable_def)
 apply (blast intro: reachable.intros)
 done
 
 (*the RHS is the traditional definition of the "always" operator*)
-lemma Always_eq_includes_reachable: "Always A = {F. reachable F <= A}"
+lemma Always_eq_includes_reachable: "Always A = {F. reachable F \<subseteq> A}"
 by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable)
 
 lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV"
 by (auto simp add: Always_eq_includes_reachable)
 
-lemma UNIV_AlwaysI: "UNIV <= A ==> F : Always A"
+lemma UNIV_AlwaysI: "UNIV \<subseteq> A ==> F \<in> Always A"
 by (auto simp add: Always_eq_includes_reachable)
 
-lemma Always_eq_UN_invariant: "Always A = (UN I: Pow A. invariant I)"
+lemma Always_eq_UN_invariant: "Always A = (\<Union>I \<in> Pow A. invariant I)"
 apply (simp add: Always_eq_includes_reachable)
 apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] 
                     invariant_includes_reachable [THEN subsetD])
 done
 
-lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B"
+lemma Always_weaken: "[| F \<in> Always A; A \<subseteq> B |] ==> F \<in> Always B"
 by (auto simp add: Always_eq_includes_reachable)
 
 
 subsection{*"Co" rules involving Always*}
 
 lemma Always_Constrains_pre:
-     "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')"
+     "F \<in> Always INV ==> (F \<in> (INV \<inter> A) Co A') = (F \<in> A Co A')"
 by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def 
               Int_assoc [symmetric])
 
 lemma Always_Constrains_post:
-     "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')"
+     "F \<in> Always INV ==> (F \<in> A Co (INV \<inter> A')) = (F \<in> A Co A')"
 by (simp add: Always_includes_reachable [THEN Int_absorb2] 
               Constrains_eq_constrains Int_assoc [symmetric])
 
-(* [| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A' *)
+(* [| F \<in> Always INV;  F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *)
 lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard]
 
-(* [| F : Always INV;  F : A Co A' |] ==> F : A Co (INV Int A') *)
+(* [| F \<in> Always INV;  F \<in> A Co A' |] ==> F \<in> A Co (INV \<inter> A') *)
 lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
 
 (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
 lemma Always_Constrains_weaken:
-     "[| F : Always C;  F : A Co A';    
-         C Int B <= A;   C Int A' <= B' |]  
-      ==> F : B Co B'"
+     "[| F \<in> Always C;  F \<in> A Co A';    
+         C \<inter> B \<subseteq> A;   C \<inter> A' \<subseteq> B' |]  
+      ==> F \<in> B Co B'"
 apply (rule Always_ConstrainsI, assumption)
 apply (drule Always_ConstrainsD, assumption)
 apply (blast intro: Constrains_weaken)
@@ -373,23 +373,23 @@
 
 (** Conjoining Always properties **)
 
-lemma Always_Int_distrib: "Always (A Int B) = Always A Int Always B"
+lemma Always_Int_distrib: "Always (A \<inter> B) = Always A \<inter> Always B"
 by (auto simp add: Always_eq_includes_reachable)
 
-lemma Always_INT_distrib: "Always (INTER I A) = (INT i:I. Always (A i))"
+lemma Always_INT_distrib: "Always (INTER I A) = (\<Inter>i \<in> I. Always (A i))"
 by (auto simp add: Always_eq_includes_reachable)
 
 lemma Always_Int_I:
-     "[| F : Always A;  F : Always B |] ==> F : Always (A Int B)"
+     "[| F \<in> Always A;  F \<in> Always B |] ==> F \<in> Always (A \<inter> B)"
 by (simp add: Always_Int_distrib)
 
 (*Allows a kind of "implication introduction"*)
 lemma Always_Compl_Un_eq:
-     "F : Always A ==> (F : Always (-A Un B)) = (F : Always B)"
+     "F \<in> Always A ==> (F \<in> Always (-A \<union> B)) = (F \<in> Always B)"
 by (auto simp add: Always_eq_includes_reachable)
 
 (*Delete the nearest invariance assumption (which will be the second one
   used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F : Always A", standard]
+lemmas Always_thin = thin_rl [of "F \<in> Always A", standard]
 
 end