src/HOL/Finite.ML
changeset 1548 afe750876848
parent 1531 e5eb247ad13c
child 1553 4eb4a9c7d736
     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;