# HG changeset patch
# User nipkow
# Date 826103100 -3600
# Node ID afe750876848a4bcce707b03ee7a9fffeeab5746
# Parent  9ee49b349bb4a8d81f06a1f7b27a3ab828c6a6fd
Added 'section' commands

diff -r 9ee49b349bb4 -r afe750876848 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Tue Mar 05 17:37:28 1996 +0100
+++ b/src/HOL/Finite.ML	Wed Mar 06 10:05:00 1996 +0100
@@ -8,7 +8,7 @@
 
 open Finite;
 
-(*** Fin ***)
+section "The finite powerset operator -- Fin";
 
 goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
 by (rtac lfp_mono 1);
@@ -98,7 +98,7 @@
 qed "Fin_empty_induct";
 
 
-(*** finite ***)
+section "The predicate 'finite'";
 
 val major::prems = goalw Finite.thy [finite_def]
     "[| finite F;  P({}); \
@@ -163,7 +163,7 @@
 qed "finite_empty_induct";
 
 
-(*** Cardinality ***)
+section "Finite cardinality -- 'card'";
 
 goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
 by(fast_tac eq_cs 1);
@@ -175,8 +175,6 @@
 qed "card_empty";
 Addsimps [card_empty];
 
-(*Addsimps [Collect_conv_insert];*)
-
 val [major] = goal Finite.thy
   "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
 br (major RS finite_induct) 1;
@@ -188,7 +186,7 @@
 by(res_inst_tac [("x","Suc n")] exI 1);
 by(res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
 by(asm_simp_tac (!simpset addsimps [Collect_conv_insert]
-                          addcongs [Collect_cong1]) 1);
+                          addcongs [rev_conj_cong]) 1);
 qed "finite_has_card";
 
 goal Finite.thy
@@ -265,7 +263,7 @@
  by(res_inst_tac
    [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
  by(simp_tac
-    (!simpset addsimps [Collect_conv_insert] addcongs [Collect_cong1]) 1);
+    (!simpset addsimps [Collect_conv_insert] addcongs [rev_conj_cong]) 1);
  be subst 1;
  br refl 1;
 br notI 1;
diff -r 9ee49b349bb4 -r afe750876848 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Mar 05 17:37:28 1996 +0100
+++ b/src/HOL/Set.ML	Wed Mar 06 10:05:00 1996 +0100
@@ -8,7 +8,9 @@
 
 open Set;
 
-val [prem] = goal Set.thy "[| P(a) |] ==> a : {x.P(x)}";
+section "Relating predicates and sets";
+
+val [prem] = goal Set.thy "P(a) ==> a : {x.P(x)}";
 by (rtac (mem_Collect_eq RS ssubst) 1);
 by (rtac prem 1);
 qed "CollectI";
@@ -29,7 +31,7 @@
 
 val CollectE = make_elim CollectD;
 
-(*** Bounded quantifiers ***)
+section "Bounded quantifiers";
 
 val prems = goalw Set.thy [Ball_def]
     "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
@@ -91,7 +93,7 @@
      ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1));
 qed "bex_cong";
 
-(*** Subsets ***)
+section "Subsets";
 
 val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B";
 by (REPEAT (ares_tac (prems @ [ballI]) 1));
@@ -126,7 +128,7 @@
 qed "subset_trans";
 
 
-(*** Equality ***)
+section "Equality";
 
 (*Anti-symmetry of the subset relation*)
 val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = (B::'a set)";
@@ -168,7 +170,7 @@
 qed "setup_induction";
 
 
-(*** Set complement -- Compl ***)
+section "Set complement -- Compl";
 
 val prems = goalw Set.thy [Compl_def]
     "[| c:A ==> False |] ==> c : Compl(A)";
@@ -186,7 +188,7 @@
 val ComplE = make_elim ComplD;
 
 
-(*** Binary union -- Un ***)
+section "Binary union -- Un";
 
 val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B";
 by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1));
@@ -210,7 +212,7 @@
 qed "UnE";
 
 
-(*** Binary intersection -- Int ***)
+section "Binary intersection -- Int";
 
 val prems = goalw Set.thy [Int_def]
     "[| c:A;  c:B |] ==> c : A Int B";
@@ -233,7 +235,7 @@
 qed "IntE";
 
 
-(*** Set difference ***)
+section "Set difference";
 
 qed_goalw "DiffI" Set.thy [set_diff_def]
     "[| c : A;  c ~: B |] ==> c : A - B"
@@ -257,7 +259,7 @@
 qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)"
  (fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
 
-(*** The empty set -- {} ***)
+section "The empty set -- {}";
 
 qed_goalw "emptyE" Set.thy [empty_def] "a:{} ==> P"
  (fn [prem] => [rtac (prem RS CollectD RS FalseE) 1]);
@@ -275,7 +277,7 @@
   [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
 
 
-(*** Augmenting a set -- insert ***)
+section "Augmenting a set -- insert";
 
 qed_goalw "insertI1" Set.thy [insert_def] "a : insert a B"
  (fn _ => [rtac (CollectI RS UnI1) 1, rtac refl 1]);
@@ -298,7 +300,7 @@
   [ (rtac (disjCI RS (insert_iff RS iffD2)) 1),
     (etac prem 1) ]);
 
-(*** Singletons, using insert ***)
+section "Singletons, using insert";
 
 qed_goal "singletonI" Set.thy "a : {a}"
  (fn _=> [ (rtac insertI1 1) ]);
@@ -320,13 +322,13 @@
 qed "singleton_inject";
 
 
-(*** UNIV - The universal set ***)
+section "The universal set -- UNIV";
 
 qed_goal "subset_UNIV" Set.thy "A <= UNIV"
   (fn _ => [rtac subsetI 1, rtac ComplI 1, etac emptyE 1]);
 
 
-(*** Unions of families -- UNION x:A. B(x) is Union(B``A)  ***)
+section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
 
 (*The order of the premises presupposes that A is rigid; b may be flexible*)
 val prems = goalw Set.thy [UNION_def]
@@ -349,7 +351,7 @@
 qed "UN_cong";
 
 
-(*** Intersections of families -- INTER x:A. B(x) is Inter(B``A) *)
+section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
 
 val prems = goalw Set.thy [INTER_def]
     "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
@@ -378,7 +380,7 @@
 qed "INT_cong";
 
 
-(*** Unions over a type; UNION1(B) = Union(range(B)) ***)
+section "Unions over a type; UNION1(B) = Union(range(B))";
 
 (*The order of the premises presupposes that A is rigid; b may be flexible*)
 val prems = goalw Set.thy [UNION1_def]
@@ -393,7 +395,7 @@
 qed "UN1_E";
 
 
-(*** Intersections over a type; INTER1(B) = Inter(range(B)) *)
+section "Intersections over a type; INTER1(B) = Inter(range(B))";
 
 val prems = goalw Set.thy [INTER1_def]
     "(!!x. b: B(x)) ==> b : (INT x. B(x))";
@@ -405,7 +407,7 @@
 by (rtac (TrueI RS (CollectI RS (major RS INT_D))) 1);
 qed "INT1_D";
 
-(*** Unions ***)
+section "Union";
 
 (*The order of the premises presupposes that C is rigid; A may be flexible*)
 val prems = goalw Set.thy [Union_def]
@@ -419,7 +421,7 @@
 by (REPEAT (ares_tac prems 1));
 qed "UnionE";
 
-(*** Inter ***)
+section "Inter";
 
 val prems = goalw Set.thy [Inter_def]
     "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
@@ -441,7 +443,7 @@
 by (REPEAT (eresolve_tac prems 1));
 qed "InterE";
 
-(*** Powerset ***)
+section "The Powerset operator -- Pow";
 
 qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)"
  (fn _ => [ (etac CollectI 1) ]);
diff -r 9ee49b349bb4 -r afe750876848 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Mar 05 17:37:28 1996 +0100
+++ b/src/HOL/equalities.ML	Wed Mar 06 10:05:00 1996 +0100
@@ -10,6 +10,8 @@
 
 val eq_cs = set_cs addSIs [equalityI];
 
+section "{}";
+
 goal Set.thy "{x.False} = {}";
 by(fast_tac eq_cs 1);
 qed "Collect_False_empty";
@@ -20,7 +22,7 @@
 qed "subset_empty";
 Addsimps [subset_empty];
 
-(** The membership relation, : **)
+section ":";
 
 goal Set.thy "x ~: {}";
 by(fast_tac set_cs 1);
@@ -32,7 +34,7 @@
 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";
@@ -67,7 +69,7 @@
 by(fast_tac eq_cs 1);
 qed "mk_disjoint_insert";
 
-(** Image **)
+section "''";
 
 goal Set.thy "f``{} = {}";
 by (fast_tac eq_cs 1);
@@ -79,7 +81,7 @@
 qed "image_insert";
 Addsimps[image_insert];
 
-(** Binary Intersection **)
+section "Int";
 
 goal Set.thy "A Int A = A";
 by (fast_tac eq_cs 1);
@@ -127,7 +129,7 @@
 qed "Int_UNIV";
 Addsimps[Int_UNIV];
 
-(** Binary Union **)
+section "Un";
 
 goal Set.thy "A Un A = A";
 by (fast_tac eq_cs 1);
@@ -188,7 +190,7 @@
 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);
@@ -227,7 +229,7 @@
 qed "Un_Int_assoc_eq";
 
 
-(** Big Union and Intersection **)
+section "Union";
 
 goal Set.thy "Union({}) = {}";
 by (fast_tac eq_cs 1);
@@ -258,6 +260,8 @@
 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";
@@ -284,7 +288,7 @@
 by (best_tac eq_cs 1);
 qed "Inter_Un_distrib";
 
-(** Unions and Intersections of Families **)
+section "UN and INT";
 
 (*Basic identities*)
 
@@ -410,7 +414,7 @@
 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);
@@ -482,20 +486,4 @@
 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];
diff -r 9ee49b349bb4 -r afe750876848 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Mar 05 17:37:28 1996 +0100
+++ b/src/HOL/simpdata.ML	Wed Mar 06 10:05:00 1996 +0100
@@ -143,6 +143,10 @@
     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
         (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
 
+val rev_conj_cong = impI RSN
+    (2, prove_goal HOL.thy "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
+        (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
+
 (** 'if' congruence rules: neither included by default! *)
 
 (*Simplifies x assuming c and y assuming ~c*)