src/HOL/UNITY/PPROD.thy
changeset 13805 3786b2fd6808
parent 13798 4c1a53627500
child 13812 91713a1915ee
     1.1 --- a/src/HOL/UNITY/PPROD.thy	Mon Feb 03 11:45:05 2003 +0100
     1.2 +++ b/src/HOL/UNITY/PPROD.thy	Tue Feb 04 18:12:40 2003 +0100
     1.3 @@ -15,19 +15,19 @@
     1.4  
     1.5    PLam  :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
     1.6              => ((nat=>'b) * 'c) program"
     1.7 -    "PLam I F == JN i:I. lift i (F i)"
     1.8 +    "PLam I F == \<Squnion>i \<in> I. lift i (F i)"
     1.9  
    1.10  syntax
    1.11    "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
    1.12                ("(3plam _:_./ _)" 10)
    1.13  
    1.14  translations
    1.15 -  "plam x:A. B"   == "PLam A (%x. B)"
    1.16 +  "plam x : A. B"   == "PLam A (%x. B)"
    1.17  
    1.18  
    1.19  (*** Basic properties ***)
    1.20  
    1.21 -lemma Init_PLam: "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))"
    1.22 +lemma Init_PLam: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))"
    1.23  apply (simp (no_asm) add: PLam_def lift_def lift_set_def)
    1.24  done
    1.25  
    1.26 @@ -37,7 +37,7 @@
    1.27  apply (simp (no_asm) add: PLam_def)
    1.28  done
    1.29  
    1.30 -lemma PLam_SKIP: "(plam i: I. SKIP) = SKIP"
    1.31 +lemma PLam_SKIP: "(plam i : I. SKIP) = SKIP"
    1.32  apply (simp (no_asm) add: PLam_def lift_SKIP JN_constant)
    1.33  done
    1.34  
    1.35 @@ -46,11 +46,11 @@
    1.36  lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
    1.37  by (unfold PLam_def, auto)
    1.38  
    1.39 -lemma PLam_component_iff: "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)"
    1.40 +lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
    1.41  apply (simp (no_asm) add: PLam_def JN_component_iff)
    1.42  done
    1.43  
    1.44 -lemma component_PLam: "i : I ==> lift i (F i) <= (PLam I F)"
    1.45 +lemma component_PLam: "i \<in> I ==> lift i (F i) \<le> (PLam I F)"
    1.46  apply (unfold PLam_def)
    1.47  (*blast_tac doesn't use HO unification*)
    1.48  apply (fast intro: component_JN)
    1.49 @@ -60,10 +60,10 @@
    1.50  (** Safety & Progress: but are they used anywhere? **)
    1.51  
    1.52  lemma PLam_constrains: 
    1.53 -     "[| i : I;  ALL j. F j : preserves snd |] ==>   
    1.54 -      (PLam I F : (lift_set i (A <*> UNIV)) co  
    1.55 +     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |] ==>   
    1.56 +      (PLam I F \<in> (lift_set i (A <*> UNIV)) co  
    1.57                    (lift_set i (B <*> UNIV)))  =   
    1.58 -      (F i : (A <*> UNIV) co (B <*> UNIV))"
    1.59 +      (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
    1.60  apply (simp (no_asm_simp) add: PLam_def JN_constrains)
    1.61  apply (subst insert_Diff [symmetric], assumption)
    1.62  apply (simp (no_asm_simp) add: lift_constrains)
    1.63 @@ -71,33 +71,33 @@
    1.64  done
    1.65  
    1.66  lemma PLam_stable: 
    1.67 -     "[| i : I;  ALL j. F j : preserves snd |]   
    1.68 -      ==> (PLam I F : stable (lift_set i (A <*> UNIV))) =  
    1.69 -          (F i : stable (A <*> UNIV))"
    1.70 +     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]   
    1.71 +      ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =  
    1.72 +          (F i \<in> stable (A <*> UNIV))"
    1.73  apply (simp (no_asm_simp) add: stable_def PLam_constrains)
    1.74  done
    1.75  
    1.76  lemma PLam_transient: 
    1.77 -     "i : I ==>  
    1.78 -    PLam I F : transient A = (EX i:I. lift i (F i) : transient A)"
    1.79 +     "i \<in> I ==>  
    1.80 +    PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
    1.81  apply (simp (no_asm_simp) add: JN_transient PLam_def)
    1.82  done
    1.83  
    1.84  (*This holds because the F j cannot change (lift_set i)*)
    1.85  lemma PLam_ensures: 
    1.86 -     "[| i : I;  F i : (A <*> UNIV) ensures (B <*> UNIV);   
    1.87 -         ALL j. F j : preserves snd |] ==>   
    1.88 -      PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
    1.89 +     "[| i \<in> I;  F i \<in> (A <*> UNIV) ensures (B <*> UNIV);   
    1.90 +         \<forall>j. F j \<in> preserves snd |] ==>   
    1.91 +      PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
    1.92  apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
    1.93  done
    1.94  
    1.95  lemma PLam_leadsTo_Basis: 
    1.96 -     "[| i : I;   
    1.97 -         F i : ((A <*> UNIV) - (B <*> UNIV)) co  
    1.98 -               ((A <*> UNIV) Un (B <*> UNIV));   
    1.99 -         F i : transient ((A <*> UNIV) - (B <*> UNIV));   
   1.100 -         ALL j. F j : preserves snd |] ==>   
   1.101 -      PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
   1.102 +     "[| i \<in> I;   
   1.103 +         F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co  
   1.104 +               ((A <*> UNIV) \<union> (B <*> UNIV));   
   1.105 +         F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));   
   1.106 +         \<forall>j. F j \<in> preserves snd |] ==>   
   1.107 +      PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
   1.108  by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
   1.109  
   1.110  
   1.111 @@ -105,20 +105,20 @@
   1.112  (** invariant **)
   1.113  
   1.114  lemma invariant_imp_PLam_invariant: 
   1.115 -     "[| F i : invariant (A <*> UNIV);  i : I;   
   1.116 -         ALL j. F j : preserves snd |]  
   1.117 -      ==> PLam I F : invariant (lift_set i (A <*> UNIV))"
   1.118 +     "[| F i \<in> invariant (A <*> UNIV);  i \<in> I;   
   1.119 +         \<forall>j. F j \<in> preserves snd |]  
   1.120 +      ==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
   1.121  by (auto simp add: PLam_stable invariant_def)
   1.122  
   1.123  
   1.124  lemma PLam_preserves_fst [simp]:
   1.125 -     "ALL j. F j : preserves snd  
   1.126 -      ==> (PLam I F : preserves (v o sub j o fst)) =  
   1.127 -          (if j: I then F j : preserves (v o fst) else True)"
   1.128 +     "\<forall>j. F j \<in> preserves snd  
   1.129 +      ==> (PLam I F \<in> preserves (v o sub j o fst)) =  
   1.130 +          (if j \<in> I then F j \<in> preserves (v o fst) else True)"
   1.131  by (simp (no_asm_simp) add: PLam_def lift_preserves_sub)
   1.132  
   1.133  lemma PLam_preserves_snd [simp,intro]:
   1.134 -     "ALL j. F j : preserves snd ==> PLam I F : preserves snd"
   1.135 +     "\<forall>j. F j \<in> preserves snd ==> PLam I F \<in> preserves snd"
   1.136  by (simp (no_asm_simp) add: PLam_def lift_preserves_snd_I)
   1.137  
   1.138  
   1.139 @@ -130,44 +130,44 @@
   1.140    something like lift_preserves_sub to rewrite the third.  However there's
   1.141    no obvious way to alternative for the third premise.*)
   1.142  lemma guarantees_PLam_I: 
   1.143 -    "[| lift i (F i): X guarantees Y;  i : I;   
   1.144 +    "[| lift i (F i): X guarantees Y;  i \<in> I;   
   1.145          OK I (%i. lift i (F i)) |]   
   1.146 -     ==> (PLam I F) : X guarantees Y"
   1.147 +     ==> (PLam I F) \<in> X guarantees Y"
   1.148  apply (unfold PLam_def)
   1.149  apply (simp (no_asm_simp) add: guarantees_JN_I)
   1.150  done
   1.151  
   1.152  lemma Allowed_PLam [simp]:
   1.153 -     "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))"
   1.154 +     "Allowed (PLam I F) = (\<Inter>i \<in> I. lift i ` Allowed(F i))"
   1.155  by (simp (no_asm) add: PLam_def)
   1.156  
   1.157  
   1.158  lemma PLam_preserves [simp]:
   1.159 -     "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))"
   1.160 -by (simp (no_asm) add: PLam_def lift_def rename_preserves)
   1.161 +     "(PLam I F) \<in> preserves v = (\<forall>i \<in> I. F i \<in> preserves (v o lift_map i))"
   1.162 +by (simp add: PLam_def lift_def rename_preserves)
   1.163  
   1.164  
   1.165  (**UNUSED
   1.166      (*The f0 premise ensures that the product is well-defined.*)
   1.167      lemma PLam_invariant_imp_invariant: 
   1.168 -     "[| PLam I F : invariant (lift_set i A);  i : I;   
   1.169 -             f0: Init (PLam I F) |] ==> F i : invariant A"
   1.170 +     "[| PLam I F \<in> invariant (lift_set i A);  i \<in> I;   
   1.171 +             f0: Init (PLam I F) |] ==> F i \<in> invariant A"
   1.172      apply (auto simp add: invariant_def)
   1.173      apply (drule_tac c = "f0 (i:=x) " in subsetD)
   1.174      apply auto
   1.175      done
   1.176  
   1.177      lemma PLam_invariant: 
   1.178 -     "[| i : I;  f0: Init (PLam I F) |]  
   1.179 -          ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)"
   1.180 +     "[| i \<in> I;  f0: Init (PLam I F) |]  
   1.181 +          ==> (PLam I F \<in> invariant (lift_set i A)) = (F i \<in> invariant A)"
   1.182      apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
   1.183      done
   1.184  
   1.185      (*The f0 premise isn't needed if F is a constant program because then
   1.186        we get an initial state by replicating that of F*)
   1.187      lemma reachable_PLam: 
   1.188 -     "i : I  
   1.189 -          ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)"
   1.190 +     "i \<in> I  
   1.191 +          ==> ((plam x \<in> I. F) \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
   1.192      apply (auto simp add: invariant_def)
   1.193      done
   1.194  **)
   1.195 @@ -176,25 +176,25 @@
   1.196  (**UNUSED
   1.197      (** Reachability **)
   1.198  
   1.199 -    Goal "[| f : reachable (PLam I F);  i : I |] ==> f i : reachable (F i)"
   1.200 +    Goal "[| f \<in> reachable (PLam I F);  i \<in> I |] ==> f i \<in> reachable (F i)"
   1.201      apply (erule reachable.induct)
   1.202      apply (auto intro: reachable.intrs)
   1.203      done
   1.204  
   1.205      (*Result to justify a re-organization of this file*)
   1.206 -    lemma "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"
   1.207 +    lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))"
   1.208      by auto
   1.209  
   1.210      lemma reachable_PLam_subset1: 
   1.211 -     "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"
   1.212 +     "reachable (PLam I F) \<subseteq> (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
   1.213      apply (force dest!: reachable_PLam)
   1.214      done
   1.215  
   1.216      (*simplify using reachable_lift??*)
   1.217      lemma reachable_lift_Join_PLam [rule_format]:
   1.218 -      "[| i ~: I;  A : reachable (F i) |]      
   1.219 -       ==> ALL f. f : reachable (PLam I F)       
   1.220 -                  --> f(i:=A) : reachable (lift i (F i) Join PLam I F)"
   1.221 +      "[| i \<notin> I;  A \<in> reachable (F i) |]      
   1.222 +       ==> \<forall>f. f \<in> reachable (PLam I F)       
   1.223 +                  --> f(i:=A) \<in> reachable (lift i (F i) Join PLam I F)"
   1.224      apply (erule reachable.induct)
   1.225      apply (ALLGOALS Clarify_tac)
   1.226      apply (erule reachable.induct)
   1.227 @@ -224,7 +224,7 @@
   1.228        perform actions, and PLam can never catch up in finite time.*)
   1.229      lemma reachable_PLam_subset2: 
   1.230       "finite I  
   1.231 -          ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)"
   1.232 +          ==> (\<Inter>i \<in> I. lift_set i (reachable (F i))) \<subseteq> reachable (PLam I F)"
   1.233      apply (erule finite_induct)
   1.234      apply (simp (no_asm))
   1.235      apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
   1.236 @@ -232,7 +232,7 @@
   1.237  
   1.238      lemma reachable_PLam_eq: 
   1.239       "finite I ==>  
   1.240 -          reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))"
   1.241 +          reachable (PLam I F) = (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
   1.242      apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
   1.243      done
   1.244  
   1.245 @@ -240,8 +240,8 @@
   1.246      (** Co **)
   1.247  
   1.248      lemma Constrains_imp_PLam_Constrains: 
   1.249 -     "[| F i : A Co B;  i: I;  finite I |]   
   1.250 -          ==> PLam I F : (lift_set i A) Co (lift_set i B)"
   1.251 +     "[| F i \<in> A Co B;  i \<in> I;  finite I |]   
   1.252 +          ==> PLam I F \<in> (lift_set i A) Co (lift_set i B)"
   1.253      apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
   1.254      apply (auto simp add: constrains_def PLam_def)
   1.255      apply (REPEAT (blast intro: reachable.intrs))
   1.256 @@ -250,15 +250,15 @@
   1.257  
   1.258  
   1.259      lemma PLam_Constrains: 
   1.260 -     "[| i: I;  finite I;  f0: Init (PLam I F) |]   
   1.261 -          ==> (PLam I F : (lift_set i A) Co (lift_set i B)) =   
   1.262 -              (F i : A Co B)"
   1.263 +     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]   
   1.264 +          ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =   
   1.265 +              (F i \<in> A Co B)"
   1.266      apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
   1.267      done
   1.268  
   1.269      lemma PLam_Stable: 
   1.270 -     "[| i: I;  finite I;  f0: Init (PLam I F) |]   
   1.271 -          ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)"
   1.272 +     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]   
   1.273 +          ==> (PLam I F \<in> Stable (lift_set i A)) = (F i \<in> Stable A)"
   1.274      apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains)
   1.275      done
   1.276  
   1.277 @@ -266,23 +266,23 @@
   1.278      (** const_PLam (no dependence on i) doesn't require the f0 premise **)
   1.279  
   1.280      lemma const_PLam_Constrains: 
   1.281 -     "[| i: I;  finite I |]   
   1.282 -          ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =   
   1.283 -              (F : A Co B)"
   1.284 +     "[| i \<in> I;  finite I |]   
   1.285 +          ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =   
   1.286 +              (F \<in> A Co B)"
   1.287      apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
   1.288      done
   1.289  
   1.290      lemma const_PLam_Stable: 
   1.291 -     "[| i: I;  finite I |]   
   1.292 -          ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)"
   1.293 +     "[| i \<in> I;  finite I |]   
   1.294 +          ==> ((plam x \<in> I. F) \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
   1.295      apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains)
   1.296      done
   1.297  
   1.298      lemma const_PLam_Increasing: 
   1.299 -	 "[| i: I;  finite I |]   
   1.300 -          ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)"
   1.301 +	 "[| i \<in> I;  finite I |]   
   1.302 +          ==> ((plam x \<in> I. F) \<in> Increasing (f o sub i)) = (F \<in> Increasing f)"
   1.303      apply (unfold Increasing_def)
   1.304 -    apply (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}")
   1.305 +    apply (subgoal_tac "\<forall>z. {s. z \<subseteq> (f o sub i) s} = lift_set i {s. z \<subseteq> f s}")
   1.306      apply (asm_simp_tac (simpset () add: lift_set_sub) 2)
   1.307      apply (simp add: finite_lessThan const_PLam_Stable)
   1.308      done