src/HOL/UNITY/Guar.thy
changeset 69313 b021008c5397
parent 67613 ce654b0e6d69
     1.1 --- a/src/HOL/UNITY/Guar.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/UNITY/Guar.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -215,7 +215,7 @@
     1.4  by (simp add: guarantees_Int_right)
     1.5  
     1.6  lemma guarantees_INT_right_iff:
     1.7 -     "(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
     1.8 +     "(F \<in> X guarantees (\<Inter>(Y ` I))) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
     1.9  by (simp add: guarantees_INT_right)
    1.10  
    1.11  lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
    1.12 @@ -276,7 +276,7 @@
    1.13  
    1.14  lemma guarantees_JN_INT: 
    1.15       "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
    1.16 -      ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)"
    1.17 +      ==> (JOIN I F) \<in> (\<Inter>(X ` I)) guarantees (\<Inter>(Y ` I))"
    1.18  apply (unfold guar_def, auto)
    1.19  apply (drule bspec, assumption)
    1.20  apply (rename_tac "i")
    1.21 @@ -287,7 +287,7 @@
    1.22  
    1.23  lemma guarantees_JN_UN: 
    1.24      "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
    1.25 -     ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
    1.26 +     ==> (JOIN I F) \<in> (\<Union>(X ` I)) guarantees (\<Union>(Y ` I))"
    1.27  apply (unfold guar_def, auto)
    1.28  apply (drule bspec, assumption)
    1.29  apply (rename_tac "i")