src/HOL/UNITY/UNITY.ML
changeset 7826 c6a8b73b6c2a
parent 7630 d0e4a6f1f05c
child 7915 c7fd7eb3b0ef
     1.1 --- a/src/HOL/UNITY/UNITY.ML	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY.ML	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -133,10 +133,20 @@
     1.4  by (Blast_tac 1);
     1.5  qed "constrains_empty";
     1.6  
     1.7 +Goalw [constrains_def] "(F : A co {}) = (A={})";
     1.8 +by (Blast_tac 1);
     1.9 +qed "constrains_empty2";
    1.10 +
    1.11 +Goalw [constrains_def] "(F : UNIV co B) = (B = UNIV)";
    1.12 +by (Blast_tac 1);
    1.13 +qed "constrains_UNIV";
    1.14 +
    1.15  Goalw [constrains_def] "F : A co UNIV";
    1.16  by (Blast_tac 1);
    1.17 -qed "constrains_UNIV";
    1.18 -AddIffs [constrains_empty, constrains_UNIV];
    1.19 +qed "constrains_UNIV2";
    1.20 +
    1.21 +AddIffs [constrains_empty, constrains_empty2, 
    1.22 +	 constrains_UNIV, constrains_UNIV2];
    1.23  
    1.24  (*monotonic in 2nd argument*)
    1.25  Goalw [constrains_def]
    1.26 @@ -167,6 +177,22 @@
    1.27  by (Blast_tac 1);
    1.28  qed "ball_constrains_UN";
    1.29  
    1.30 +Goalw [constrains_def] "(A Un B) co C = (A co C) Int (B co C)";
    1.31 +by (Blast_tac 1);
    1.32 +qed "constrains_Un_distrib";
    1.33 +
    1.34 +Goalw [constrains_def] "(UN i:I. A i) co B = (INT i:I. A i co B)";
    1.35 +by (Blast_tac 1);
    1.36 +qed "constrains_UN_distrib";
    1.37 +
    1.38 +Goalw [constrains_def] "C co (A Int B) = (C co A) Int (C co B)";
    1.39 +by (Blast_tac 1);
    1.40 +qed "constrains_Int_distrib";
    1.41 +
    1.42 +Goalw [constrains_def] "A co (INT i:I. B i) = (INT i:I. A co B i)";
    1.43 +by (Blast_tac 1);
    1.44 +qed "constrains_INT_distrib";
    1.45 +
    1.46  (** Intersection **)
    1.47  
    1.48  Goalw [constrains_def]