src/HOL/UNITY/PPROD.thy
changeset 61943 7fba644ed827
parent 60773 d09c66a0ea10
child 63146 f1ecba0272f9
     1.1 --- a/src/HOL/UNITY/PPROD.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/UNITY/PPROD.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -48,9 +48,9 @@
     1.4  
     1.5  lemma PLam_constrains:
     1.6       "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
     1.7 -      ==> (PLam I F \<in> (lift_set i (A <*> UNIV)) co
     1.8 -                      (lift_set i (B <*> UNIV)))  =
     1.9 -          (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
    1.10 +      ==> (PLam I F \<in> (lift_set i (A \<times> UNIV)) co
    1.11 +                      (lift_set i (B \<times> UNIV)))  =
    1.12 +          (F i \<in> (A \<times> UNIV) co (B \<times> UNIV))"
    1.13  apply (simp add: PLam_def JN_constrains)
    1.14  apply (subst insert_Diff [symmetric], assumption)
    1.15  apply (simp add: lift_constrains)
    1.16 @@ -59,8 +59,8 @@
    1.17  
    1.18  lemma PLam_stable:
    1.19       "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
    1.20 -      ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =
    1.21 -          (F i \<in> stable (A <*> UNIV))"
    1.22 +      ==> (PLam I F \<in> stable (lift_set i (A \<times> UNIV))) =
    1.23 +          (F i \<in> stable (A \<times> UNIV))"
    1.24  by (simp add: stable_def PLam_constrains)
    1.25  
    1.26  lemma PLam_transient:
    1.27 @@ -70,9 +70,9 @@
    1.28  
    1.29  text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
    1.30  lemma PLam_ensures:
    1.31 -     "[| i \<in> I;  F i \<in> (A <*> UNIV) ensures (B <*> UNIV);
    1.32 +     "[| i \<in> I;  F i \<in> (A \<times> UNIV) ensures (B \<times> UNIV);
    1.33           \<forall>j. F j \<in> preserves snd |]
    1.34 -      ==> PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
    1.35 +      ==> PLam I F \<in> lift_set i (A \<times> UNIV) ensures lift_set i (B \<times> UNIV)"
    1.36  apply (simp add: ensures_def PLam_constrains PLam_transient
    1.37                lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric]
    1.38                Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
    1.39 @@ -82,11 +82,11 @@
    1.40  
    1.41  lemma PLam_leadsTo_Basis:
    1.42       "[| i \<in> I;
    1.43 -         F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co
    1.44 -               ((A <*> UNIV) \<union> (B <*> UNIV));
    1.45 -         F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));
    1.46 +         F i \<in> ((A \<times> UNIV) - (B \<times> UNIV)) co
    1.47 +               ((A \<times> UNIV) \<union> (B \<times> UNIV));
    1.48 +         F i \<in> transient ((A \<times> UNIV) - (B \<times> UNIV));
    1.49           \<forall>j. F j \<in> preserves snd |]
    1.50 -      ==> PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
    1.51 +      ==> PLam I F \<in> lift_set i (A \<times> UNIV) leadsTo lift_set i (B \<times> UNIV)"
    1.52  by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
    1.53  
    1.54  
    1.55 @@ -94,9 +94,9 @@
    1.56  (** invariant **)
    1.57  
    1.58  lemma invariant_imp_PLam_invariant:
    1.59 -     "[| F i \<in> invariant (A <*> UNIV);  i \<in> I;
    1.60 +     "[| F i \<in> invariant (A \<times> UNIV);  i \<in> I;
    1.61           \<forall>j. F j \<in> preserves snd |]
    1.62 -      ==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
    1.63 +      ==> PLam I F \<in> invariant (lift_set i (A \<times> UNIV))"
    1.64  by (auto simp add: PLam_stable invariant_def)
    1.65  
    1.66