Added 'section' commands
authornipkow
Wed Mar 06 10:05:00 1996 +0100 (1996-03-06 ago)
changeset 1548afe750876848
parent 1547 9ee49b349bb4
child 1549 ac9b58304d62
Added 'section' commands
src/HOL/Finite.ML
src/HOL/Set.ML
src/HOL/equalities.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Finite.ML	Tue Mar 05 17:37:28 1996 +0100
     1.2 +++ b/src/HOL/Finite.ML	Wed Mar 06 10:05:00 1996 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  open Finite;
     1.6  
     1.7 -(*** Fin ***)
     1.8 +section "The finite powerset operator -- Fin";
     1.9  
    1.10  goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
    1.11  by (rtac lfp_mono 1);
    1.12 @@ -98,7 +98,7 @@
    1.13  qed "Fin_empty_induct";
    1.14  
    1.15  
    1.16 -(*** finite ***)
    1.17 +section "The predicate 'finite'";
    1.18  
    1.19  val major::prems = goalw Finite.thy [finite_def]
    1.20      "[| finite F;  P({}); \
    1.21 @@ -163,7 +163,7 @@
    1.22  qed "finite_empty_induct";
    1.23  
    1.24  
    1.25 -(*** Cardinality ***)
    1.26 +section "Finite cardinality -- 'card'";
    1.27  
    1.28  goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
    1.29  by(fast_tac eq_cs 1);
    1.30 @@ -175,8 +175,6 @@
    1.31  qed "card_empty";
    1.32  Addsimps [card_empty];
    1.33  
    1.34 -(*Addsimps [Collect_conv_insert];*)
    1.35 -
    1.36  val [major] = goal Finite.thy
    1.37    "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
    1.38  br (major RS finite_induct) 1;
    1.39 @@ -188,7 +186,7 @@
    1.40  by(res_inst_tac [("x","Suc n")] exI 1);
    1.41  by(res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
    1.42  by(asm_simp_tac (!simpset addsimps [Collect_conv_insert]
    1.43 -                          addcongs [Collect_cong1]) 1);
    1.44 +                          addcongs [rev_conj_cong]) 1);
    1.45  qed "finite_has_card";
    1.46  
    1.47  goal Finite.thy
    1.48 @@ -265,7 +263,7 @@
    1.49   by(res_inst_tac
    1.50     [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
    1.51   by(simp_tac
    1.52 -    (!simpset addsimps [Collect_conv_insert] addcongs [Collect_cong1]) 1);
    1.53 +    (!simpset addsimps [Collect_conv_insert] addcongs [rev_conj_cong]) 1);
    1.54   be subst 1;
    1.55   br refl 1;
    1.56  br notI 1;
     2.1 --- a/src/HOL/Set.ML	Tue Mar 05 17:37:28 1996 +0100
     2.2 +++ b/src/HOL/Set.ML	Wed Mar 06 10:05:00 1996 +0100
     2.3 @@ -8,7 +8,9 @@
     2.4  
     2.5  open Set;
     2.6  
     2.7 -val [prem] = goal Set.thy "[| P(a) |] ==> a : {x.P(x)}";
     2.8 +section "Relating predicates and sets";
     2.9 +
    2.10 +val [prem] = goal Set.thy "P(a) ==> a : {x.P(x)}";
    2.11  by (rtac (mem_Collect_eq RS ssubst) 1);
    2.12  by (rtac prem 1);
    2.13  qed "CollectI";
    2.14 @@ -29,7 +31,7 @@
    2.15  
    2.16  val CollectE = make_elim CollectD;
    2.17  
    2.18 -(*** Bounded quantifiers ***)
    2.19 +section "Bounded quantifiers";
    2.20  
    2.21  val prems = goalw Set.thy [Ball_def]
    2.22      "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
    2.23 @@ -91,7 +93,7 @@
    2.24       ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1));
    2.25  qed "bex_cong";
    2.26  
    2.27 -(*** Subsets ***)
    2.28 +section "Subsets";
    2.29  
    2.30  val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B";
    2.31  by (REPEAT (ares_tac (prems @ [ballI]) 1));
    2.32 @@ -126,7 +128,7 @@
    2.33  qed "subset_trans";
    2.34  
    2.35  
    2.36 -(*** Equality ***)
    2.37 +section "Equality";
    2.38  
    2.39  (*Anti-symmetry of the subset relation*)
    2.40  val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = (B::'a set)";
    2.41 @@ -168,7 +170,7 @@
    2.42  qed "setup_induction";
    2.43  
    2.44  
    2.45 -(*** Set complement -- Compl ***)
    2.46 +section "Set complement -- Compl";
    2.47  
    2.48  val prems = goalw Set.thy [Compl_def]
    2.49      "[| c:A ==> False |] ==> c : Compl(A)";
    2.50 @@ -186,7 +188,7 @@
    2.51  val ComplE = make_elim ComplD;
    2.52  
    2.53  
    2.54 -(*** Binary union -- Un ***)
    2.55 +section "Binary union -- Un";
    2.56  
    2.57  val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B";
    2.58  by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1));
    2.59 @@ -210,7 +212,7 @@
    2.60  qed "UnE";
    2.61  
    2.62  
    2.63 -(*** Binary intersection -- Int ***)
    2.64 +section "Binary intersection -- Int";
    2.65  
    2.66  val prems = goalw Set.thy [Int_def]
    2.67      "[| c:A;  c:B |] ==> c : A Int B";
    2.68 @@ -233,7 +235,7 @@
    2.69  qed "IntE";
    2.70  
    2.71  
    2.72 -(*** Set difference ***)
    2.73 +section "Set difference";
    2.74  
    2.75  qed_goalw "DiffI" Set.thy [set_diff_def]
    2.76      "[| c : A;  c ~: B |] ==> c : A - B"
    2.77 @@ -257,7 +259,7 @@
    2.78  qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)"
    2.79   (fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
    2.80  
    2.81 -(*** The empty set -- {} ***)
    2.82 +section "The empty set -- {}";
    2.83  
    2.84  qed_goalw "emptyE" Set.thy [empty_def] "a:{} ==> P"
    2.85   (fn [prem] => [rtac (prem RS CollectD RS FalseE) 1]);
    2.86 @@ -275,7 +277,7 @@
    2.87    [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
    2.88  
    2.89  
    2.90 -(*** Augmenting a set -- insert ***)
    2.91 +section "Augmenting a set -- insert";
    2.92  
    2.93  qed_goalw "insertI1" Set.thy [insert_def] "a : insert a B"
    2.94   (fn _ => [rtac (CollectI RS UnI1) 1, rtac refl 1]);
    2.95 @@ -298,7 +300,7 @@
    2.96    [ (rtac (disjCI RS (insert_iff RS iffD2)) 1),
    2.97      (etac prem 1) ]);
    2.98  
    2.99 -(*** Singletons, using insert ***)
   2.100 +section "Singletons, using insert";
   2.101  
   2.102  qed_goal "singletonI" Set.thy "a : {a}"
   2.103   (fn _=> [ (rtac insertI1 1) ]);
   2.104 @@ -320,13 +322,13 @@
   2.105  qed "singleton_inject";
   2.106  
   2.107  
   2.108 -(*** UNIV - The universal set ***)
   2.109 +section "The universal set -- UNIV";
   2.110  
   2.111  qed_goal "subset_UNIV" Set.thy "A <= UNIV"
   2.112    (fn _ => [rtac subsetI 1, rtac ComplI 1, etac emptyE 1]);
   2.113  
   2.114  
   2.115 -(*** Unions of families -- UNION x:A. B(x) is Union(B``A)  ***)
   2.116 +section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
   2.117  
   2.118  (*The order of the premises presupposes that A is rigid; b may be flexible*)
   2.119  val prems = goalw Set.thy [UNION_def]
   2.120 @@ -349,7 +351,7 @@
   2.121  qed "UN_cong";
   2.122  
   2.123  
   2.124 -(*** Intersections of families -- INTER x:A. B(x) is Inter(B``A) *)
   2.125 +section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
   2.126  
   2.127  val prems = goalw Set.thy [INTER_def]
   2.128      "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
   2.129 @@ -378,7 +380,7 @@
   2.130  qed "INT_cong";
   2.131  
   2.132  
   2.133 -(*** Unions over a type; UNION1(B) = Union(range(B)) ***)
   2.134 +section "Unions over a type; UNION1(B) = Union(range(B))";
   2.135  
   2.136  (*The order of the premises presupposes that A is rigid; b may be flexible*)
   2.137  val prems = goalw Set.thy [UNION1_def]
   2.138 @@ -393,7 +395,7 @@
   2.139  qed "UN1_E";
   2.140  
   2.141  
   2.142 -(*** Intersections over a type; INTER1(B) = Inter(range(B)) *)
   2.143 +section "Intersections over a type; INTER1(B) = Inter(range(B))";
   2.144  
   2.145  val prems = goalw Set.thy [INTER1_def]
   2.146      "(!!x. b: B(x)) ==> b : (INT x. B(x))";
   2.147 @@ -405,7 +407,7 @@
   2.148  by (rtac (TrueI RS (CollectI RS (major RS INT_D))) 1);
   2.149  qed "INT1_D";
   2.150  
   2.151 -(*** Unions ***)
   2.152 +section "Union";
   2.153  
   2.154  (*The order of the premises presupposes that C is rigid; A may be flexible*)
   2.155  val prems = goalw Set.thy [Union_def]
   2.156 @@ -419,7 +421,7 @@
   2.157  by (REPEAT (ares_tac prems 1));
   2.158  qed "UnionE";
   2.159  
   2.160 -(*** Inter ***)
   2.161 +section "Inter";
   2.162  
   2.163  val prems = goalw Set.thy [Inter_def]
   2.164      "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
   2.165 @@ -441,7 +443,7 @@
   2.166  by (REPEAT (eresolve_tac prems 1));
   2.167  qed "InterE";
   2.168  
   2.169 -(*** Powerset ***)
   2.170 +section "The Powerset operator -- Pow";
   2.171  
   2.172  qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)"
   2.173   (fn _ => [ (etac CollectI 1) ]);
     3.1 --- a/src/HOL/equalities.ML	Tue Mar 05 17:37:28 1996 +0100
     3.2 +++ b/src/HOL/equalities.ML	Wed Mar 06 10:05:00 1996 +0100
     3.3 @@ -10,6 +10,8 @@
     3.4  
     3.5  val eq_cs = set_cs addSIs [equalityI];
     3.6  
     3.7 +section "{}";
     3.8 +
     3.9  goal Set.thy "{x.False} = {}";
    3.10  by(fast_tac eq_cs 1);
    3.11  qed "Collect_False_empty";
    3.12 @@ -20,7 +22,7 @@
    3.13  qed "subset_empty";
    3.14  Addsimps [subset_empty];
    3.15  
    3.16 -(** The membership relation, : **)
    3.17 +section ":";
    3.18  
    3.19  goal Set.thy "x ~: {}";
    3.20  by(fast_tac set_cs 1);
    3.21 @@ -32,7 +34,7 @@
    3.22  qed "in_insert";
    3.23  Addsimps[in_insert];
    3.24  
    3.25 -(** insert **)
    3.26 +section "insert";
    3.27  
    3.28  (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
    3.29  goal Set.thy "insert a A = {a} Un A";
    3.30 @@ -67,7 +69,7 @@
    3.31  by(fast_tac eq_cs 1);
    3.32  qed "mk_disjoint_insert";
    3.33  
    3.34 -(** Image **)
    3.35 +section "''";
    3.36  
    3.37  goal Set.thy "f``{} = {}";
    3.38  by (fast_tac eq_cs 1);
    3.39 @@ -79,7 +81,7 @@
    3.40  qed "image_insert";
    3.41  Addsimps[image_insert];
    3.42  
    3.43 -(** Binary Intersection **)
    3.44 +section "Int";
    3.45  
    3.46  goal Set.thy "A Int A = A";
    3.47  by (fast_tac eq_cs 1);
    3.48 @@ -127,7 +129,7 @@
    3.49  qed "Int_UNIV";
    3.50  Addsimps[Int_UNIV];
    3.51  
    3.52 -(** Binary Union **)
    3.53 +section "Un";
    3.54  
    3.55  goal Set.thy "A Un A = A";
    3.56  by (fast_tac eq_cs 1);
    3.57 @@ -188,7 +190,7 @@
    3.58  qed "Un_empty";
    3.59  Addsimps[Un_empty];
    3.60  
    3.61 -(** Simple properties of Compl -- complement of a set **)
    3.62 +section "Compl";
    3.63  
    3.64  goal Set.thy "A Int Compl(A) = {}";
    3.65  by (fast_tac eq_cs 1);
    3.66 @@ -227,7 +229,7 @@
    3.67  qed "Un_Int_assoc_eq";
    3.68  
    3.69  
    3.70 -(** Big Union and Intersection **)
    3.71 +section "Union";
    3.72  
    3.73  goal Set.thy "Union({}) = {}";
    3.74  by (fast_tac eq_cs 1);
    3.75 @@ -258,6 +260,8 @@
    3.76  by (fast_tac (eq_cs addSEs [equalityE]) 1);
    3.77  qed "Union_disjoint";
    3.78  
    3.79 +section "Inter";
    3.80 +
    3.81  goal Set.thy "Inter({}) = UNIV";
    3.82  by (fast_tac eq_cs 1);
    3.83  qed "Inter_empty";
    3.84 @@ -284,7 +288,7 @@
    3.85  by (best_tac eq_cs 1);
    3.86  qed "Inter_Un_distrib";
    3.87  
    3.88 -(** Unions and Intersections of Families **)
    3.89 +section "UN and INT";
    3.90  
    3.91  (*Basic identities*)
    3.92  
    3.93 @@ -410,7 +414,7 @@
    3.94  by (fast_tac eq_cs 1);
    3.95  qed "Un_INT_distrib2";
    3.96  
    3.97 -(** Simple properties of Diff -- set difference **)
    3.98 +section "-";
    3.99  
   3.100  goal Set.thy "A-A = {}";
   3.101  by (fast_tac eq_cs 1);
   3.102 @@ -482,20 +486,4 @@
   3.103  by (fast_tac eq_cs 1);
   3.104  qed "Diff_Int";
   3.105  
   3.106 -(* Congruence rule for set comprehension *)
   3.107 -val prems = goal Set.thy
   3.108 -  "[| !!x. P x = Q x; !!x. Q x ==> f x = g x |] ==> \
   3.109 -\  {f x |x. P x} = {g x|x. Q x}";
   3.110 -by(simp_tac (!simpset addsimps prems) 1);
   3.111 -br set_ext 1;
   3.112 -br iffI 1;
   3.113 -by(fast_tac (eq_cs addss (!simpset addsimps prems)) 1);
   3.114 -be CollectE 1;
   3.115 -be exE 1;
   3.116 -by(Asm_simp_tac 1);
   3.117 -be conjE 1;
   3.118 -by(rtac exI 1 THEN rtac conjI 1 THEN atac 2);
   3.119 -by(asm_simp_tac (!simpset addsimps prems) 1);
   3.120 -qed "Collect_cong1";
   3.121 -
   3.122  Addsimps[subset_UNIV, empty_subsetI, subset_refl];
     4.1 --- a/src/HOL/simpdata.ML	Tue Mar 05 17:37:28 1996 +0100
     4.2 +++ b/src/HOL/simpdata.ML	Wed Mar 06 10:05:00 1996 +0100
     4.3 @@ -143,6 +143,10 @@
     4.4      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
     4.5          (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
     4.6  
     4.7 +val rev_conj_cong = impI RSN
     4.8 +    (2, prove_goal HOL.thy "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
     4.9 +        (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
    4.10 +
    4.11  (** 'if' congruence rules: neither included by default! *)
    4.12  
    4.13  (*Simplifies x assuming c and y assuming ~c*)