diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -116,23 +116,23 @@
 lemma lift_set_empty [simp]: "lift_set i {} = {}"
 by (unfold lift_set_def, auto)
 
-lemma lift_set_iff: "(lift_map i x : lift_set i A) = (x : A)"
+lemma lift_set_iff: "(lift_map i x \<in> lift_set i A) = (x \<in> A)"
 apply (unfold lift_set_def)
 apply (rule inj_lift_map [THEN inj_image_mem_iff])
 done
 
 (*Do we really need both this one and its predecessor?*)
 lemma lift_set_iff2 [iff]:
-     "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)"
+     "((f,uu) \<in> lift_set i A) = ((f i, (delete_map i f, uu)) \<in> A)"
 by (simp add: lift_set_def mem_rename_set_iff drop_map_def)
 
 
-lemma lift_set_mono: "A<=B ==> lift_set i A <= lift_set i B"
+lemma lift_set_mono: "A \<subseteq> B ==> lift_set i A \<subseteq> lift_set i B"
 apply (unfold lift_set_def)
 apply (erule image_mono)
 done
 
-lemma lift_set_Un_distrib: "lift_set i (A Un B) = lift_set i A Un lift_set i B"
+lemma lift_set_Un_distrib: "lift_set i (A \<union> B) = lift_set i A \<union> lift_set i B"
 apply (unfold lift_set_def)
 apply (simp add: image_Un)
 done
@@ -154,39 +154,39 @@
 lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
 by (simp add: lift_def)
 
-lemma lift_JN [simp]: "lift j (JOIN I F) = (JN i:I. lift j (F i))"
+lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
 by (simp add: lift_def)
 
 (*** Safety: co, stable, invariant ***)
 
 lemma lift_constrains: 
-     "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)"
+     "(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)"
 by (simp add: lift_def lift_set_def rename_constrains)
 
 lemma lift_stable: 
-     "(lift i F : stable (lift_set i A)) = (F : stable A)"
+     "(lift i F \<in> stable (lift_set i A)) = (F \<in> stable A)"
 by (simp add: lift_def lift_set_def rename_stable)
 
 lemma lift_invariant: 
-     "(lift i F : invariant (lift_set i A)) = (F : invariant A)"
+     "(lift i F \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
 apply (unfold lift_def lift_set_def)
 apply (simp add: rename_invariant)
 done
 
 lemma lift_Constrains: 
-     "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)"
+     "(lift i F \<in> (lift_set i A) Co (lift_set i B)) = (F \<in> A Co B)"
 apply (unfold lift_def lift_set_def)
 apply (simp add: rename_Constrains)
 done
 
 lemma lift_Stable: 
-     "(lift i F : Stable (lift_set i A)) = (F : Stable A)"
+     "(lift i F \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
 apply (unfold lift_def lift_set_def)
 apply (simp add: rename_Stable)
 done
 
 lemma lift_Always: 
-     "(lift i F : Always (lift_set i A)) = (F : Always A)"
+     "(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)"
 apply (unfold lift_def lift_set_def)
 apply (simp add: rename_Always)
 done
@@ -194,37 +194,37 @@
 (*** Progress: transient, ensures ***)
 
 lemma lift_transient: 
-     "(lift i F : transient (lift_set i A)) = (F : transient A)"
+     "(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)"
 by (simp add: lift_def lift_set_def rename_transient)
 
 lemma lift_ensures: 
-     "(lift i F : (lift_set i A) ensures (lift_set i B)) =  
-      (F : A ensures B)"
+     "(lift i F \<in> (lift_set i A) ensures (lift_set i B)) =  
+      (F \<in> A ensures B)"
 by (simp add: lift_def lift_set_def rename_ensures)
 
 lemma lift_leadsTo: 
-     "(lift i F : (lift_set i A) leadsTo (lift_set i B)) =  
-      (F : A leadsTo B)"
+     "(lift i F \<in> (lift_set i A) leadsTo (lift_set i B)) =  
+      (F \<in> A leadsTo B)"
 by (simp add: lift_def lift_set_def rename_leadsTo)
 
 lemma lift_LeadsTo: 
-     "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) =   
-      (F : A LeadsTo B)"
+     "(lift i F \<in> (lift_set i A) LeadsTo (lift_set i B)) =   
+      (F \<in> A LeadsTo B)"
 by (simp add: lift_def lift_set_def rename_LeadsTo)
 
 
 (** guarantees **)
 
 lemma lift_lift_guarantees_eq: 
-     "(lift i F : (lift i ` X) guarantees (lift i ` Y)) =  
-      (F : X guarantees Y)"
+     "(lift i F \<in> (lift i ` X) guarantees (lift i ` Y)) =  
+      (F \<in> X guarantees Y)"
 apply (unfold lift_def)
 apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric])
 apply (simp add: o_def)
 done
 
-lemma lift_guarantees_eq_lift_inv: "(lift i F : X guarantees Y) =  
-      (F : (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
+lemma lift_guarantees_eq_lift_inv: "(lift i F \<in> X guarantees Y) =  
+      (F \<in> (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
 by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def)
 
 
@@ -236,14 +236,14 @@
 (*To preserve snd means that the second component is there just to allow
   guarantees properties to be stated.  Converse fails, for lift i F can 
   change function components other than i*)
-lemma lift_preserves_snd_I: "F : preserves snd ==> lift i F : preserves snd"
+lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd"
 apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
 apply (simp add: lift_def rename_preserves)
 apply (simp add: lift_map_def o_def split_def)
 done
 
 lemma delete_map_eqE':
-     "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)"
+     "(delete_map i g) = (delete_map i g') ==> \<exists>x. g = g'(i:=x)"
 apply (drule_tac f = "insert_map i (g i) " in arg_cong)
 apply (simp add: insert_map_delete_map_eq)
 apply (erule exI)
@@ -252,7 +252,7 @@
 lemmas delete_map_eqE = delete_map_eqE' [THEN exE, elim!]
 
 lemma delete_map_neq_apply:
-     "[| delete_map j g = delete_map j g';  i~=j |] ==> g i = g' i"
+     "[| delete_map j g = delete_map j g';  i\<noteq>j |] ==> g i = g' i"
 by force
 
 (*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
@@ -265,27 +265,27 @@
 by auto
 
 lemma mem_lift_act_iff [iff]: 
-     "((s,s') : extend_act (%(x,u::unit). lift_map i x) act) =  
-      ((drop_map i s, drop_map i s') : act)"
+     "((s,s') \<in> extend_act (%(x,u::unit). lift_map i x) act) =  
+      ((drop_map i s, drop_map i s') \<in> act)"
 apply (unfold extend_act_def, auto)
 apply (rule bexI, auto)
 done
 
 lemma preserves_snd_lift_stable:
-     "[| F : preserves snd;  i~=j |]  
-      ==> lift j F : stable (lift_set i (A <*> UNIV))"
+     "[| F \<in> preserves snd;  i\<noteq>j |]  
+      ==> lift j F \<in> stable (lift_set i (A <*> UNIV))"
 apply (auto simp add: lift_def lift_set_def stable_def constrains_def 
                       rename_def extend_def mem_rename_set_iff)
 apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
 apply (drule_tac x = i in fun_cong, auto)
 done
 
-(*If i~=j then lift j F  does nothing to lift_set i, and the 
-  premise ensures A<=B.*)
+(*If i\<noteq>j then lift j F  does nothing to lift_set i, and the 
+  premise ensures A \<subseteq> B.*)
 lemma constrains_imp_lift_constrains:
-    "[| F i : (A <*> UNIV) co (B <*> UNIV);   
-        F j : preserves snd |]   
-     ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
+    "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);   
+        F j \<in> preserves snd |]   
+     ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
 apply (case_tac "i=j")
 apply (simp add: lift_def lift_set_def rename_constrains)
 apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
@@ -309,24 +309,24 @@
 done
 
 lemma insert_map_eq_diff:
-     "[| insert_map i s f = insert_map j t g;  i~=j |]  
-      ==> EX g'. insert_map i s' f = insert_map j t g'"
+     "[| insert_map i s f = insert_map j t g;  i\<noteq>j |]  
+      ==> \<exists>g'. insert_map i s' f = insert_map j t g'"
 apply (subst insert_map_upd_same [symmetric])
 apply (erule ssubst)
 apply (simp only: insert_map_upd if_False split: split_if, blast)
 done
 
 lemma lift_map_eq_diff: 
-     "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv));  i~=j |]  
-      ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
+     "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv));  i\<noteq>j |]  
+      ==> \<exists>g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
 apply (unfold lift_map_def, auto)
 apply (blast dest: insert_map_eq_diff)
 done
 
 lemma lift_transient_eq_disj:
-     "F : preserves snd  
-      ==> (lift i F : transient (lift_set j (A <*> UNIV))) =  
-          (i=j & F : transient (A <*> UNIV) | A={})"
+     "F \<in> preserves snd  
+      ==> (lift i F \<in> transient (lift_set j (A <*> UNIV))) =  
+          (i=j & F \<in> transient (A <*> UNIV) | A={})"
 apply (case_tac "i=j")
 apply (auto simp add: lift_transient)
 apply (auto simp add: lift_set_def lift_def transient_def rename_def 
@@ -346,21 +346,21 @@
 
 (*USELESS??*)
 lemma lift_map_image_Times: "lift_map i ` (A <*> UNIV) =  
-      (UN s:A. UN f. {insert_map i s f}) <*> UNIV"
+      (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
 apply (auto intro!: bexI image_eqI simp add: lift_map_def)
 apply (rule split_conv [symmetric])
 done
 
 lemma lift_preserves_eq:
-     "(lift i F : preserves v) = (F : preserves (v o lift_map i))"
+     "(lift i F \<in> preserves v) = (F \<in> preserves (v o lift_map i))"
 by (simp add: lift_def rename_preserves)
 
 (*A useful rewrite.  If o, sub have been rewritten out already then can also
   use it as   rewrite_rule [sub_def, o_def] lift_preserves_sub*)
 lemma lift_preserves_sub:
-     "F : preserves snd  
-      ==> lift i F : preserves (v o sub j o fst) =  
-          (if i=j then F : preserves (v o fst) else True)"
+     "F \<in> preserves snd  
+      ==> lift i F \<in> preserves (v o sub j o fst) =  
+          (if i=j then F \<in> preserves (v o fst) else True)"
 apply (drule subset_preserves_o [THEN subsetD])
 apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
 apply (auto cong del: if_weak_cong 
@@ -374,7 +374,7 @@
 lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
 by (simp add: expand_fun_eq o_def)
 
-lemma o_equiv_apply: "f o g = h ==> ALL x. f(g x) = h x"
+lemma o_equiv_apply: "f o g = h ==> \<forall>x. f(g x) = h x"
 by (simp add: expand_fun_eq o_def)
 
 lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
@@ -402,7 +402,7 @@
 
 lemma project_act_extend_act:
      "project_act h (extend_act h' act) =  
-        {(x,x'). EX s s' y y' z. (s,s') : act &  
+        {(x,x'). \<exists>s s' y y' z. (s,s') \<in> act &  
                  h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}"
 by (simp add: extend_act_def project_act_def, blast)
 
@@ -410,24 +410,24 @@
 (*** OK and "lift" ***)
 
 lemma act_in_UNION_preserves_fst:
-     "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts"
+     "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
 apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I)
 apply (auto simp add: preserves_def stable_def constrains_def)
 done
 
 lemma UNION_OK_lift_I:
-     "[| ALL i:I. F i : preserves snd;   
-         ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |]  
+     "[| \<forall>i \<in> I. F i \<in> preserves snd;   
+         \<forall>i \<in> I. UNION (preserves fst) Acts \<subseteq> AllowedActs (F i) |]  
       ==> OK I (%i. lift i (F i))"
 apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
 apply (simp add: Extend.AllowedActs_extend project_act_extend_act)
 apply (rename_tac "act")
 apply (subgoal_tac
        "{(x, x'). \<exists>s f u s' f' u'. 
-                    ((s, f, u), s', f', u') : act & 
+                    ((s, f, u), s', f', u') \<in> act & 
                     lift_map j x = lift_map i (s, f, u) & 
                     lift_map j x' = lift_map i (s', f', u') } 
-                <= { (x,x') . fst x = fst x'}")
+                \<subseteq> { (x,x') . fst x = fst x'}")
 apply (blast intro: act_in_UNION_preserves_fst, clarify)
 apply (drule_tac x = j in fun_cong)+
 apply (drule_tac x = i in bspec, assumption)
@@ -435,8 +435,8 @@
 done
 
 lemma OK_lift_I:
-     "[| ALL i:I. F i : preserves snd;   
-         ALL i:I. preserves fst <= Allowed (F i) |]  
+     "[| \<forall>i \<in> I. F i \<in> preserves snd;   
+         \<forall>i \<in> I. preserves fst \<subseteq> Allowed (F i) |]  
       ==> OK I (%i. lift i (F i))"
 by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)