src/HOL/equalities.ML
changeset 1548 afe750876848
parent 1531 e5eb247ad13c
child 1553 4eb4a9c7d736
     1.1 --- a/src/HOL/equalities.ML	Tue Mar 05 17:37:28 1996 +0100
     1.2 +++ b/src/HOL/equalities.ML	Wed Mar 06 10:05:00 1996 +0100
     1.3 @@ -10,6 +10,8 @@
     1.4  
     1.5  val eq_cs = set_cs addSIs [equalityI];
     1.6  
     1.7 +section "{}";
     1.8 +
     1.9  goal Set.thy "{x.False} = {}";
    1.10  by(fast_tac eq_cs 1);
    1.11  qed "Collect_False_empty";
    1.12 @@ -20,7 +22,7 @@
    1.13  qed "subset_empty";
    1.14  Addsimps [subset_empty];
    1.15  
    1.16 -(** The membership relation, : **)
    1.17 +section ":";
    1.18  
    1.19  goal Set.thy "x ~: {}";
    1.20  by(fast_tac set_cs 1);
    1.21 @@ -32,7 +34,7 @@
    1.22  qed "in_insert";
    1.23  Addsimps[in_insert];
    1.24  
    1.25 -(** insert **)
    1.26 +section "insert";
    1.27  
    1.28  (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
    1.29  goal Set.thy "insert a A = {a} Un A";
    1.30 @@ -67,7 +69,7 @@
    1.31  by(fast_tac eq_cs 1);
    1.32  qed "mk_disjoint_insert";
    1.33  
    1.34 -(** Image **)
    1.35 +section "''";
    1.36  
    1.37  goal Set.thy "f``{} = {}";
    1.38  by (fast_tac eq_cs 1);
    1.39 @@ -79,7 +81,7 @@
    1.40  qed "image_insert";
    1.41  Addsimps[image_insert];
    1.42  
    1.43 -(** Binary Intersection **)
    1.44 +section "Int";
    1.45  
    1.46  goal Set.thy "A Int A = A";
    1.47  by (fast_tac eq_cs 1);
    1.48 @@ -127,7 +129,7 @@
    1.49  qed "Int_UNIV";
    1.50  Addsimps[Int_UNIV];
    1.51  
    1.52 -(** Binary Union **)
    1.53 +section "Un";
    1.54  
    1.55  goal Set.thy "A Un A = A";
    1.56  by (fast_tac eq_cs 1);
    1.57 @@ -188,7 +190,7 @@
    1.58  qed "Un_empty";
    1.59  Addsimps[Un_empty];
    1.60  
    1.61 -(** Simple properties of Compl -- complement of a set **)
    1.62 +section "Compl";
    1.63  
    1.64  goal Set.thy "A Int Compl(A) = {}";
    1.65  by (fast_tac eq_cs 1);
    1.66 @@ -227,7 +229,7 @@
    1.67  qed "Un_Int_assoc_eq";
    1.68  
    1.69  
    1.70 -(** Big Union and Intersection **)
    1.71 +section "Union";
    1.72  
    1.73  goal Set.thy "Union({}) = {}";
    1.74  by (fast_tac eq_cs 1);
    1.75 @@ -258,6 +260,8 @@
    1.76  by (fast_tac (eq_cs addSEs [equalityE]) 1);
    1.77  qed "Union_disjoint";
    1.78  
    1.79 +section "Inter";
    1.80 +
    1.81  goal Set.thy "Inter({}) = UNIV";
    1.82  by (fast_tac eq_cs 1);
    1.83  qed "Inter_empty";
    1.84 @@ -284,7 +288,7 @@
    1.85  by (best_tac eq_cs 1);
    1.86  qed "Inter_Un_distrib";
    1.87  
    1.88 -(** Unions and Intersections of Families **)
    1.89 +section "UN and INT";
    1.90  
    1.91  (*Basic identities*)
    1.92  
    1.93 @@ -410,7 +414,7 @@
    1.94  by (fast_tac eq_cs 1);
    1.95  qed "Un_INT_distrib2";
    1.96  
    1.97 -(** Simple properties of Diff -- set difference **)
    1.98 +section "-";
    1.99  
   1.100  goal Set.thy "A-A = {}";
   1.101  by (fast_tac eq_cs 1);
   1.102 @@ -482,20 +486,4 @@
   1.103  by (fast_tac eq_cs 1);
   1.104  qed "Diff_Int";
   1.105  
   1.106 -(* Congruence rule for set comprehension *)
   1.107 -val prems = goal Set.thy
   1.108 -  "[| !!x. P x = Q x; !!x. Q x ==> f x = g x |] ==> \
   1.109 -\  {f x |x. P x} = {g x|x. Q x}";
   1.110 -by(simp_tac (!simpset addsimps prems) 1);
   1.111 -br set_ext 1;
   1.112 -br iffI 1;
   1.113 -by(fast_tac (eq_cs addss (!simpset addsimps prems)) 1);
   1.114 -be CollectE 1;
   1.115 -be exE 1;
   1.116 -by(Asm_simp_tac 1);
   1.117 -be conjE 1;
   1.118 -by(rtac exI 1 THEN rtac conjI 1 THEN atac 2);
   1.119 -by(asm_simp_tac (!simpset addsimps prems) 1);
   1.120 -qed "Collect_cong1";
   1.121 -
   1.122  Addsimps[subset_UNIV, empty_subsetI, subset_refl];