src/HOL/Finite.ML
changeset 4304 af2a2cd9fa51
parent 4153 e534c4c32d54
child 4386 b3cff8adc213
     1.1 --- a/src/HOL/Finite.ML	Wed Nov 26 17:26:12 1997 +0100
     1.2 +++ b/src/HOL/Finite.ML	Wed Nov 26 17:27:34 1997 +0100
     1.3 @@ -63,20 +63,23 @@
     1.4  qed "finite_UnI";
     1.5  
     1.6  (*Every subset of a finite set is finite*)
     1.7 -val [subs,fin] = goal Finite.thy "[| A<=B;  finite B |] ==> finite A";
     1.8 -by (EVERY1 [subgoal_tac "ALL C. C<=B --> finite C",
     1.9 -            rtac mp, etac spec,
    1.10 -            rtac subs]);
    1.11 -by (rtac (fin RS finite_induct) 1);
    1.12 -by (simp_tac (simpset() addsimps [subset_Un_eq]) 1);
    1.13 +goal Finite.thy "!!B. finite B ==> ALL A. A<=B --> finite A";
    1.14 +by (etac finite_induct 1);
    1.15 +by (Simp_tac 1);
    1.16  by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1]));
    1.17 -by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
    1.18 +by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 2);
    1.19  by (ALLGOALS Asm_simp_tac);
    1.20 +val lemma = result();
    1.21 +
    1.22 +goal Finite.thy "!!A. [| A<=B;  finite B |] ==> finite A";
    1.23 +bd lemma 1;
    1.24 +by (Blast_tac 1);
    1.25  qed "finite_subset";
    1.26  
    1.27  goal Finite.thy "finite(F Un G) = (finite F & finite G)";
    1.28 -by (blast_tac (claset() addIs [finite_UnI] addDs
    1.29 -                [Un_upper1 RS finite_subset, Un_upper2 RS finite_subset]) 1);
    1.30 +by (blast_tac (claset() 
    1.31 +	         addIs [read_instantiate [("B", "?AA Un ?BB")] finite_subset, 
    1.32 +			finite_UnI]) 1);
    1.33  qed "finite_Un";
    1.34  AddIffs[finite_Un];
    1.35  
    1.36 @@ -207,7 +210,7 @@
    1.37  
    1.38  section "Finite cardinality -- 'card'";
    1.39  
    1.40 -goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
    1.41 +goal Set.thy "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
    1.42  by (Blast_tac 1);
    1.43  val Collect_conv_insert = result();
    1.44