--- a/src/HOL/Finite.ML Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/Finite.ML Thu Jun 05 14:39:22 1997 +0200
@@ -8,8 +8,9 @@
open Finite;
-section "The finite powerset operator -- Fin";
+section "finite";
+(*
goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
@@ -21,124 +22,99 @@
(* A : Fin(B) ==> A <= B *)
val FinD = Fin_subset_Pow RS subsetD RS PowD;
+*)
(*Discharging ~ x:y entails extra work*)
val major::prems = goal Finite.thy
- "[| F:Fin(A); P({}); \
-\ !!F x. [| x:A; F:Fin(A); x~:F; P(F) |] ==> P(insert x F) \
+ "[| finite F; P({}); \
+\ !!F x. [| finite F; x ~: F; P(F) |] ==> P(insert x F) \
\ |] ==> P(F)";
-by (rtac (major RS Fin.induct) 1);
-by (excluded_middle_tac "a:b" 2);
+by (rtac (major RS Finites.induct) 1);
+by (excluded_middle_tac "a:A" 2);
by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*)
by (REPEAT (ares_tac prems 1));
-qed "Fin_induct";
+qed "finite_induct";
+
+val major::prems = goal Finite.thy
+ "[| finite F; \
+\ P({}); \
+\ !!F a. [| finite F; a:A; a ~: F; P(F) |] ==> P(insert a F) \
+\ |] ==> F <= A --> P(F)";
+by (rtac (major RS finite_induct) 1);
+by(ALLGOALS (blast_tac (!claset addIs prems)));
+val lemma = result();
-Addsimps Fin.intrs;
+val prems = goal Finite.thy
+ "[| finite F; F <= A; \
+\ P({}); \
+\ !!F a. [| finite F; a:A; a ~: F; P(F) |] ==> P(insert a F) \
+\ |] ==> P(F)";
+by(blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
+qed "finite_subset_induct";
+
+Addsimps Finites.intrs;
+AddSIs Finites.intrs;
(*The union of two finite sets is finite*)
val major::prems = goal Finite.thy
- "[| F: Fin(A); G: Fin(A) |] ==> F Un G : Fin(A)";
-by (rtac (major RS Fin_induct) 1);
+ "[| finite F; finite G |] ==> finite(F Un G)";
+by (rtac (major RS finite_induct) 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
-qed "Fin_UnI";
+qed "finite_UnI";
(*Every subset of a finite set is finite*)
-val [subs,fin] = goal Finite.thy "[| A<=B; B: Fin(M) |] ==> A: Fin(M)";
-by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)",
+val [subs,fin] = goal Finite.thy "[| A<=B; finite B |] ==> finite A";
+by (EVERY1 [subgoal_tac "ALL C. C<=B --> finite C",
rtac mp, etac spec,
rtac subs]);
-by (rtac (fin RS Fin_induct) 1);
+by (rtac (fin RS finite_induct) 1);
by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1]));
by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
by (ALLGOALS Asm_simp_tac);
-qed "Fin_subset";
+qed "finite_subset";
-goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
-by (blast_tac (!claset addIs [Fin_UnI] addDs
- [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
-qed "subset_Fin";
-Addsimps[subset_Fin];
+goal Finite.thy "finite(F Un G) = (finite F & finite G)";
+by (blast_tac (!claset addIs [finite_UnI] addDs
+ [Un_upper1 RS finite_subset, Un_upper2 RS finite_subset]) 1);
+qed "finite_Un";
+AddIffs[finite_Un];
-goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
+goal Finite.thy "finite(insert a A) = finite A";
by (stac insert_is_Un 1);
-by (simp_tac (HOL_ss addsimps [subset_Fin]) 1);
-by (blast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
-qed "insert_Fin";
-Addsimps[insert_Fin];
+by (simp_tac (HOL_ss addsimps [finite_Un]) 1);
+by (blast_tac (!claset addSIs Finites.intrs) 1);
+qed "finite_insert";
+Addsimps[finite_insert];
-(*The image of a finite set is finite*)
-val major::_ = goal Finite.thy
- "F: Fin(A) ==> h``F : Fin(h``A)";
-by (rtac (major RS Fin_induct) 1);
+(*The image of a finite set is finite *)
+goal Finite.thy "!!F. finite F ==> finite(h``F)";
+by (etac finite_induct 1);
by (Simp_tac 1);
-by (asm_simp_tac
- (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]
- delsimps [insert_Fin]) 1);
-qed "Fin_imageI";
+by (Asm_simp_tac 1);
+qed "finite_imageI";
val major::prems = goal Finite.thy
- "[| c: Fin(A); b: Fin(A); \
+ "[| finite c; finite b; \
\ P(b); \
-\ !!(x::'a) y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
+\ !!x y. [| finite y; x:y; P(y) |] ==> P(y-{x}) \
\ |] ==> c<=b --> P(b-c)";
-by (rtac (major RS Fin_induct) 1);
+by (rtac (major RS finite_induct) 1);
by (stac Diff_insert 2);
by (ALLGOALS (asm_simp_tac
- (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
+ (!simpset addsimps (prems@[Diff_subset RS finite_subset]))));
val lemma = result();
val prems = goal Finite.thy
- "[| b: Fin(A); \
-\ P(b); \
-\ !!x y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
+ "[| finite A; \
+\ P(A); \
+\ !!a A. [| finite A; a:A; P(A) |] ==> P(A-{a}) \
\ |] ==> P({})";
by (rtac (Diff_cancel RS subst) 1);
by (rtac (lemma RS mp) 1);
by (REPEAT (ares_tac (subset_refl::prems) 1));
-qed "Fin_empty_induct";
-
-
-section "The predicate 'finite'";
-
-val major::prems = goalw Finite.thy [finite_def]
- "[| finite F; P({}); \
-\ !!F x. [| finite F; x~:F; P(F) |] ==> P(insert x F) \
-\ |] ==> P(F)";
-by (rtac (major RS Fin_induct) 1);
-by (REPEAT (ares_tac prems 1));
-qed "finite_induct";
-
-
-goalw Finite.thy [finite_def] "finite {}";
-by (Simp_tac 1);
-qed "finite_emptyI";
-Addsimps [finite_emptyI];
+qed "finite_empty_induct";
-goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)";
-by (Asm_simp_tac 1);
-qed "finite_insertI";
-
-(*The union of two finite sets is finite*)
-goalw Finite.thy [finite_def]
- "!!F. [| finite F; finite G |] ==> finite(F Un G)";
-by (Asm_simp_tac 1);
-qed "finite_UnI";
-
-goalw Finite.thy [finite_def] "!!A. [| A<=B; finite B |] ==> finite A";
-by (etac Fin_subset 1);
-by (assume_tac 1);
-qed "finite_subset";
-
-goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
-by (Simp_tac 1);
-qed "finite_Un_eq";
-Addsimps[finite_Un_eq];
-
-goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
-by (Simp_tac 1);
-qed "finite_insert";
-Addsimps[finite_insert];
(* finite B ==> finite (B - Ba) *)
bind_thm ("finite_Diff", Diff_subset RS finite_subset);
@@ -152,25 +128,22 @@
qed "finite_Diff_singleton";
AddIffs [finite_Diff_singleton];
-(*The image of a finite set is finite*)
-goal Finite.thy "!!F. finite F ==> finite(h``F)";
+(*** FIXME -> equalities.ML ***)
+goal Set.thy "(f``A = {}) = (A = {})";
+by (blast_tac (!claset addSEs [equalityE]) 1);
+qed "image_is_empty";
+Addsimps [image_is_empty];
+
+goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
by (etac finite_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "finite_imageI";
-
-goal Finite.thy "!!A. finite B ==> !A. B = f``A --> inj_onto f A --> finite A";
-by (etac finite_induct 1);
-by (ALLGOALS Asm_simp_tac);
+ by (ALLGOALS Asm_simp_tac);
by (Step_tac 1);
-by (subgoal_tac "A={}" 1);
-by (blast_tac (!claset addSEs [equalityE]) 2);
-by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 2);
-by (Step_tac 1);
-bw inj_onto_def;
-by (Blast_tac 2);
-by (ALLGOALS Asm_simp_tac);
+by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
+ by (Step_tac 1);
+ bw inj_onto_def;
+ by (Blast_tac 1);
by (thin_tac "ALL A. ?PP(A)" 1);
-by (forward_tac [[equalityD1, insertI1] MRS subsetD] 1);
+by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
by (Step_tac 1);
by (res_inst_tac [("x","xa")] bexI 1);
by (ALLGOALS Asm_simp_tac);
@@ -207,15 +180,6 @@
qed "finite_Pow_iff";
AddIffs [finite_Pow_iff];
-val major::prems = goalw Finite.thy [finite_def]
- "[| finite A; \
-\ P(A); \
-\ !!a A. [| finite A; a:A; P(A) |] ==> P(A-{a}) \
-\ |] ==> P({})";
-by (rtac (major RS Fin_empty_induct) 1);
-by (REPEAT (ares_tac (subset_refl::prems) 1));
-qed "finite_empty_induct";
-
section "Finite cardinality -- 'card'";
@@ -346,7 +310,7 @@
by (Simp_tac 1);
by (strip_tac 1);
by (case_tac "x:B" 1);
- by (dtac mk_disjoint_insert 1);
+ by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
by (SELECT_GOAL(safe_tac (!claset))1);
by (rotate_tac ~1 1);
by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
@@ -439,7 +403,7 @@
by (etac conjE 1);
by (case_tac "x:A" 1);
(*1*)
-by (dtac mk_disjoint_insert 1);
+by (dres_inst_tac [("A","A")]mk_disjoint_insert 1);
by (etac exE 1);
by (etac conjE 1);
by (hyp_subst_tac 1);