src/HOL/equalities.ML

 
 writeln"File HOL/equalities";
 
 val eq_cs = set_cs addSIs [equalityI];
 
+section "{}";
+
 goal Set.thy "{x.False} = {}";
 by(fast_tac eq_cs 1);
 qed "Collect_False_empty";
 Addsimps [Collect_False_empty];
 
 goal Set.thy "(A <= {}) = (A = {})";
 by(fast_tac eq_cs 1);
 qed "subset_empty";
 Addsimps [subset_empty];
 
-(** The membership relation, : **)
+section ":";
 
 goal Set.thy "x ~: {}";
 by(fast_tac set_cs 1);
 qed "in_empty";
 Addsimps[in_empty];

 goal Set.thy "x : insert y A = (x=y | x:A)";
 by(fast_tac set_cs 1);
 qed "in_insert";
 Addsimps[in_insert];
 
-(** insert **)
+section "insert";
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
 goal Set.thy "insert a A = {a} Un A";
 by(fast_tac eq_cs 1);
 qed "insert_is_Un";

 goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
 by(res_inst_tac [("x","A-{a}")] exI 1);
 by(fast_tac eq_cs 1);
 qed "mk_disjoint_insert";
 
-(** Image **)
+section "''";
 
 goal Set.thy "f``{} = {}";
 by (fast_tac eq_cs 1);
 qed "image_empty";
 Addsimps[image_empty];

 goal Set.thy "f``insert a B = insert (f a) (f``B)";
 by (fast_tac eq_cs 1);
 qed "image_insert";
 Addsimps[image_insert];
 
-(** Binary Intersection **)
+section "Int";
 
 goal Set.thy "A Int A = A";
 by (fast_tac eq_cs 1);
 qed "Int_absorb";
 Addsimps[Int_absorb];

 goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
 by (fast_tac (eq_cs addEs [equalityCE]) 1);
 qed "Int_UNIV";
 Addsimps[Int_UNIV];
 
-(** Binary Union **)
+section "Un";
 
 goal Set.thy "A Un A = A";
 by (fast_tac eq_cs 1);
 qed "Un_absorb";
 Addsimps[Un_absorb];

 goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
 by (fast_tac (eq_cs addEs [equalityCE]) 1);
 qed "Un_empty";
 Addsimps[Un_empty];
 
-(** Simple properties of Compl -- complement of a set **)
+section "Compl";
 
 goal Set.thy "A Int Compl(A) = {}";
 by (fast_tac eq_cs 1);
 qed "Compl_disjoint";
 Addsimps[Compl_disjoint];

 goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 qed "Un_Int_assoc_eq";
 
 
-(** Big Union and Intersection **)
+section "Union";
 
 goal Set.thy "Union({}) = {}";
 by (fast_tac eq_cs 1);
 qed "Union_empty";
 Addsimps[Union_empty];

 val prems = goal Set.thy
    "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
+section "Inter";
+
 goal Set.thy "Inter({}) = UNIV";
 by (fast_tac eq_cs 1);
 qed "Inter_empty";
 Addsimps[Inter_empty];
 

 
 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
 by (best_tac eq_cs 1);
 qed "Inter_Un_distrib";
 
-(** Unions and Intersections of Families **)
+section "UN and INT";
 
 (*Basic identities*)
 
 goal Set.thy "(UN x:{}. B x) = {}";
 by (fast_tac eq_cs 1);

 goal Set.thy
     "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
 by (fast_tac eq_cs 1);
 qed "Un_INT_distrib2";
 
-(** Simple properties of Diff -- set difference **)
+section "-";
 
 goal Set.thy "A-A = {}";
 by (fast_tac eq_cs 1);
 qed "Diff_cancel";
 Addsimps[Diff_cancel];

 
 goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
 by (fast_tac eq_cs 1);
 qed "Diff_Int";
 
-(* Congruence rule for set comprehension *)
-val prems = goal Set.thy
-  "[| !!x. P x = Q x; !!x. Q x ==> f x = g x |] ==> \
-\  {f x |x. P x} = {g x|x. Q x}";
-by(simp_tac (!simpset addsimps prems) 1);
-br set_ext 1;
-br iffI 1;
-by(fast_tac (eq_cs addss (!simpset addsimps prems)) 1);
-be CollectE 1;
-be exE 1;
-by(Asm_simp_tac 1);
-be conjE 1;
-by(rtac exI 1 THEN rtac conjI 1 THEN atac 2);
-by(asm_simp_tac (!simpset addsimps prems) 1);
-qed "Collect_cong1";
-
 Addsimps[subset_UNIV, empty_subsetI, subset_refl];