--- a/src/ZF/CardinalArith.ML Fri May 31 12:27:24 2002 +0200
+++ b/src/ZF/CardinalArith.ML Fri May 31 15:06:06 2002 +0200
@@ -707,7 +707,7 @@
Goal "n: nat ==> ALL A. A eqpoll n --> A : Fin(A)";
by (induct_tac "n" 1);
-by (simp_tac (simpset() addsimps eqpoll_0_iff::Fin.intrs) 1);
+by (simp_tac (simpset() addsimps [eqpoll_0_iff]) 1);
by (Clarify_tac 1);
by (subgoal_tac "EX u. u:A" 1);
by (etac exE 1);
@@ -716,7 +716,7 @@
by (assume_tac 1);
by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1);
by (assume_tac 1);
-by (resolve_tac [Fin.consI] 1);
+by (resolve_tac [thm "Fin.consI"] 1);
by (Blast_tac 1);
by (blast_tac (claset() addIs [subset_consI RS Fin_mono RS subsetD]) 1);
(*Now for the lemma assumed above*)
@@ -729,7 +729,7 @@
qed "Finite_into_Fin";
Goal "A : Fin(U) ==> Finite(A)";
-by (fast_tac (claset() addSIs [Finite_0, Finite_cons] addEs [Fin.induct]) 1);
+by (fast_tac (claset() addSIs [Finite_0, Finite_cons] addEs [Fin_induct]) 1);
qed "Fin_into_Finite";
Goal "Finite(A) <-> A : Fin(A)";
@@ -746,9 +746,9 @@
Goal "[| ALL y:X. Finite(y); Finite(X) |] ==> Finite(Union(X))";
by (asm_full_simp_tac (simpset() addsimps [Finite_Fin_iff]) 1);
by (rtac Fin_UnionI 1);
-by (etac Fin.induct 1);
+by (etac Fin_induct 1);
by (Simp_tac 1);
-by (blast_tac (claset() addIs [Fin.consI, impOfSubs Fin_mono]) 1);
+by (blast_tac (claset() addIs [thm "Fin.consI", impOfSubs Fin_mono]) 1);
qed "Finite_Union";
(* Induction principle for Finite(A), by Sidi Ehmety *)
--- a/src/ZF/Finite.ML Fri May 31 12:27:24 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,192 +0,0 @@
-(* Title: ZF/Finite.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Finite powerset operator; finite function space
-
-prove X:Fin(A) ==> |X| < nat
-
-prove: b: Fin(A) ==> inj(b,b)<=surj(b,b)
-*)
-
-(*** Finite powerset operator ***)
-
-Goalw Fin.defs "A<=B ==> Fin(A) <= Fin(B)";
-by (rtac lfp_mono 1);
-by (REPEAT (rtac Fin.bnd_mono 1));
-by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
-qed "Fin_mono";
-
-(* A : Fin(B) ==> A <= B *)
-bind_thm ("FinD", Fin.dom_subset RS subsetD RS PowD);
-
-(** Induction on finite sets **)
-
-(*Discharging x~:y entails extra work*)
-val major::prems = Goal
- "[| b: Fin(A); \
-\ P(0); \
-\ !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) \
-\ |] ==> P(b)";
-by (rtac (major RS Fin.induct) 1);
-by (excluded_middle_tac "a:b" 2);
-by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*)
-by (REPEAT (ares_tac prems 1));
-qed "Fin_induct";
-
-(** Simplification for Fin **)
-Addsimps Fin.intrs;
-
-(*The union of two finite sets is finite.*)
-Goal "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)";
-by (etac Fin_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
-qed "Fin_UnI";
-
-Addsimps [Fin_UnI];
-
-
-(*The union of a set of finite sets is finite.*)
-Goal "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
-by (etac Fin_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "Fin_UnionI";
-
-(*Every subset of a finite set is finite.*)
-Goal "b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
-by (etac Fin_induct 1);
-by (simp_tac (simpset() addsimps [subset_empty_iff]) 1);
-by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
-by Safe_tac;
-by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
-by (Asm_simp_tac 1);
-qed "Fin_subset_lemma";
-
-Goal "[| c<=b; b: Fin(A) |] ==> c: Fin(A)";
-by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
-qed "Fin_subset";
-
-Goal "b: Fin(A) ==> b Int c : Fin(A)";
-by (blast_tac (claset() addIs [Fin_subset]) 1);
-qed "Fin_IntI1";
-
-Goal "c: Fin(A) ==> b Int c : Fin(A)";
-by (blast_tac (claset() addIs [Fin_subset]) 1);
-qed "Fin_IntI2";
-
-Addsimps[Fin_IntI1, Fin_IntI2];
-AddIs[Fin_IntI1, Fin_IntI2];
-
-
-val major::prems = Goal
- "[| c: Fin(A); b: Fin(A); \
-\ P(b); \
-\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
-\ |] ==> c<=b --> P(b-c)";
-by (rtac (major RS Fin_induct) 1);
-by (stac Diff_cons 2);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps (prems@[cons_subset_iff,
- Diff_subset RS Fin_subset]))));
-qed "Fin_0_induct_lemma";
-
-val prems = Goal
- "[| b: Fin(A); \
-\ P(b); \
-\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
-\ |] ==> P(0)";
-by (rtac (Diff_cancel RS subst) 1);
-by (rtac (Fin_0_induct_lemma RS mp) 1);
-by (REPEAT (ares_tac (subset_refl::prems) 1));
-qed "Fin_0_induct";
-
-(*Functions from a finite ordinal*)
-Goal "n: nat ==> n->A <= Fin(nat*A)";
-by (induct_tac "n" 1);
-by (simp_tac (simpset() addsimps [subset_iff]) 1);
-by (asm_simp_tac
- (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
-by (fast_tac (claset() addSIs [Fin.consI]) 1);
-qed "nat_fun_subset_Fin";
-
-
-(*** Finite function space ***)
-
-Goalw FiniteFun.defs
- "[| A<=C; B<=D |] ==> A -||> B <= C -||> D";
-by (rtac lfp_mono 1);
-by (REPEAT (rtac FiniteFun.bnd_mono 1));
-by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1));
-qed "FiniteFun_mono";
-
-Goal "A<=B ==> A -||> A <= B -||> B";
-by (REPEAT (ares_tac [FiniteFun_mono] 1));
-qed "FiniteFun_mono1";
-
-Goal "h: A -||>B ==> h: domain(h) -> B";
-by (etac FiniteFun.induct 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [fun_extend3]) 1);
-qed "FiniteFun_is_fun";
-
-Goal "h: A -||>B ==> domain(h) : Fin(A)";
-by (etac FiniteFun.induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "FiniteFun_domain_Fin";
-
-bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type);
-
-(*Every subset of a finite function is a finite function.*)
-Goal "b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
-by (etac FiniteFun.induct 1);
-by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1);
-by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
-by Safe_tac;
-by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
-by (dtac (spec RS mp) 1 THEN assume_tac 1);
-by (fast_tac (claset() addSIs FiniteFun.intrs) 1);
-qed "FiniteFun_subset_lemma";
-
-Goal "[| c<=b; b: A-||>B |] ==> c: A-||>B";
-by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1));
-qed "FiniteFun_subset";
-
-(** Some further results by Sidi O. Ehmety **)
-
-Goal "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B";
-by (etac Fin.induct 1);
-by (simp_tac (simpset() addsimps FiniteFun.intrs) 1);
-by (Clarify_tac 1);
-by (case_tac "a:b" 1);
-by (rotate_tac ~1 1);
-by (asm_full_simp_tac (simpset() addsimps [cons_absorb]) 1);
-by (subgoal_tac "restrict(f,b) : b -||> B" 1);
-by (blast_tac (claset() addIs [restrict_type2]) 2);
-by (stac fun_cons_restrict_eq 1 THEN assume_tac 1);
-by (full_simp_tac (simpset() addsimps [restrict_def, lam_def]) 1);
-by (blast_tac (claset() addIs [apply_funtype, impOfSubs FiniteFun_mono]
- @FiniteFun.intrs) 1);
-qed_spec_mp "fun_FiniteFunI";
-
-Goal "A: Fin(X) ==> (lam x:A. b(x)) : A -||> {b(x). x:A}";
-by (blast_tac (claset() addIs [fun_FiniteFunI, lam_funtype]) 1);
-qed "lam_FiniteFun";
-
-Goal "f : FiniteFun(A, {y:B. P(y)}) \
-\ <-> f : FiniteFun(A,B) & (ALL x:domain(f). P(f`x))";
-by Auto_tac;
-by (blast_tac (claset() addIs [impOfSubs FiniteFun_mono]) 1);
-by (blast_tac (claset() addDs [Pair_mem_PiD, FiniteFun_is_fun]) 1);
-by (res_inst_tac [("A1", "domain(f)")]
- (subset_refl RSN(2, FiniteFun_mono) RS subsetD) 1);
-by (fast_tac (claset() addDs
- [FiniteFun_domain_Fin, Fin.dom_subset RS subsetD]) 1);
-by (rtac fun_FiniteFunI 1);
-by (etac FiniteFun_domain_Fin 1);
-by (res_inst_tac [("B" , "range(f)")] fun_weaken_type 1);
-by (ALLGOALS
- (blast_tac (claset() addDs
- [FiniteFun_is_fun, range_of_fun, range_type,
- apply_equality])));
-qed "FiniteFun_Collect_iff";
--- a/src/ZF/Finite.thy Fri May 31 12:27:24 2002 +0200
+++ b/src/ZF/Finite.thy Fri May 31 15:06:06 2002 +0200
@@ -3,36 +3,227 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Finite powerset operator
+Finite powerset operator; finite function space
+
+prove X:Fin(A) ==> |X| < nat
+
+prove: b: Fin(A) ==> inj(b,b) <= surj(b,b)
*)
-Finite = Inductive + Epsilon + Nat +
+theory Finite = Inductive + Epsilon + Nat:
(*The natural numbers as a datatype*)
-rep_datatype
- elim natE
- induct nat_induct
- case_eqns nat_case_0, nat_case_succ
- recursor_eqns recursor_0, recursor_succ
+rep_datatype
+ elimination natE
+ induction nat_induct
+ case_eqns nat_case_0 nat_case_succ
+ recursor_eqns recursor_0 recursor_succ
consts
- Fin :: i=>i
- FiniteFun :: [i,i]=>i ("(_ -||>/ _)" [61, 60] 60)
+ Fin :: "i=>i"
+ FiniteFun :: "[i,i]=>i" ("(_ -||>/ _)" [61, 60] 60)
inductive
domains "Fin(A)" <= "Pow(A)"
- intrs
- emptyI "0 : Fin(A)"
- consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"
- type_intrs empty_subsetI, cons_subsetI, PowI
- type_elims "[make_elim PowD]"
+ intros
+ emptyI: "0 : Fin(A)"
+ consI: "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"
+ type_intros empty_subsetI cons_subsetI PowI
+ type_elims PowD [THEN revcut_rl]
inductive
domains "FiniteFun(A,B)" <= "Fin(A*B)"
- intrs
- emptyI "0 : A -||> B"
- consI "[| a: A; b: B; h: A -||> B; a ~: domain(h)
- |] ==> cons(<a,b>,h) : A -||> B"
- type_intrs "Fin.intrs"
+ intros
+ emptyI: "0 : A -||> B"
+ consI: "[| a: A; b: B; h: A -||> B; a ~: domain(h) |]
+ ==> cons(<a,b>,h) : A -||> B"
+ type_intros Fin.intros
+
+
+subsection {* Finite powerset operator *}
+
+lemma Fin_mono: "A<=B ==> Fin(A) <= Fin(B)"
+apply (unfold Fin.defs)
+apply (rule lfp_mono)
+apply (rule Fin.bnd_mono)+
+apply blast
+done
+
+(* A : Fin(B) ==> A <= B *)
+lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD, standard]
+
+(** Induction on finite sets **)
+
+(*Discharging x~:y entails extra work*)
+lemma Fin_induct:
+ "[| b: Fin(A);
+ P(0);
+ !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y))
+ |] ==> P(b)"
+apply (erule Fin.induct, simp)
+apply (case_tac "a:b")
+ apply (erule cons_absorb [THEN ssubst], assumption) (*backtracking!*)
+apply simp
+done
+
+(** Simplification for Fin **)
+declare Fin.intros [simp]
+
+(*The union of two finite sets is finite.*)
+lemma Fin_UnI: "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)"
+apply (erule Fin_induct)
+apply (simp_all add: Un_cons)
+done
+
+declare Fin_UnI [simp]
+
+
+(*The union of a set of finite sets is finite.*)
+lemma Fin_UnionI: "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"
+by (erule Fin_induct, simp_all)
+
+(*Every subset of a finite set is finite.*)
+lemma Fin_subset_lemma [rule_format]: "b: Fin(A) ==> \<forall>z. z<=b --> z: Fin(A)"
+apply (erule Fin_induct)
+apply (simp add: subset_empty_iff)
+apply (simp add: subset_cons_iff distrib_simps, safe)
+apply (erule_tac b = "z" in cons_Diff [THEN subst], simp)
+done
+
+lemma Fin_subset: "[| c<=b; b: Fin(A) |] ==> c: Fin(A)"
+by (blast intro: Fin_subset_lemma)
+
+lemma Fin_IntI1 [intro,simp]: "b: Fin(A) ==> b Int c : Fin(A)"
+by (blast intro: Fin_subset)
+
+lemma Fin_IntI2 [intro,simp]: "c: Fin(A) ==> b Int c : Fin(A)"
+by (blast intro: Fin_subset)
+
+lemma Fin_0_induct_lemma [rule_format]:
+ "[| c: Fin(A); b: Fin(A); P(b);
+ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x})
+ |] ==> c<=b --> P(b-c)"
+apply (erule Fin_induct, simp)
+apply (subst Diff_cons)
+apply (simp add: cons_subset_iff Diff_subset [THEN Fin_subset])
+done
+
+lemma Fin_0_induct:
+ "[| b: Fin(A);
+ P(b);
+ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x})
+ |] ==> P(0)"
+apply (rule Diff_cancel [THEN subst])
+apply (blast intro: Fin_0_induct_lemma)
+done
+
+(*Functions from a finite ordinal*)
+lemma nat_fun_subset_Fin: "n: nat ==> n->A <= Fin(nat*A)"
+apply (induct_tac "n")
+apply (simp add: subset_iff)
+apply (simp add: succ_def mem_not_refl [THEN cons_fun_eq])
+apply (fast intro!: Fin.consI)
+done
+
+
+(*** Finite function space ***)
+
+lemma FiniteFun_mono:
+ "[| A<=C; B<=D |] ==> A -||> B <= C -||> D"
+apply (unfold FiniteFun.defs)
+apply (rule lfp_mono)
+apply (rule FiniteFun.bnd_mono)+
+apply (intro Fin_mono Sigma_mono basic_monos, assumption+)
+done
+
+lemma FiniteFun_mono1: "A<=B ==> A -||> A <= B -||> B"
+by (blast dest: FiniteFun_mono)
+
+lemma FiniteFun_is_fun: "h: A -||>B ==> h: domain(h) -> B"
+apply (erule FiniteFun.induct, simp)
+apply (simp add: fun_extend3)
+done
+
+lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)"
+apply (erule FiniteFun.induct, simp)
+apply simp
+done
+
+lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard]
+
+(*Every subset of a finite function is a finite function.*)
+lemma FiniteFun_subset_lemma [rule_format]:
+ "b: A-||>B ==> ALL z. z<=b --> z: A-||>B"
+apply (erule FiniteFun.induct)
+apply (simp add: subset_empty_iff FiniteFun.intros)
+apply (simp add: subset_cons_iff distrib_simps, safe)
+apply (erule_tac b = "z" in cons_Diff [THEN subst])
+apply (drule spec [THEN mp], assumption)
+apply (fast intro!: FiniteFun.intros)
+done
+
+lemma FiniteFun_subset: "[| c<=b; b: A-||>B |] ==> c: A-||>B"
+by (blast intro: FiniteFun_subset_lemma)
+
+(** Some further results by Sidi O. Ehmety **)
+
+lemma fun_FiniteFunI [rule_format]: "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B"
+apply (erule Fin.induct)
+ apply (simp add: FiniteFun.intros)
+apply clarify
+apply (case_tac "a:b")
+ apply (rotate_tac -1)
+ apply (simp add: cons_absorb)
+apply (subgoal_tac "restrict (f,b) : b -||> B")
+ prefer 2 apply (blast intro: restrict_type2)
+apply (subst fun_cons_restrict_eq, assumption)
+apply (simp add: restrict_def lam_def)
+apply (blast intro: apply_funtype FiniteFun.intros
+ FiniteFun_mono [THEN [2] rev_subsetD])
+done
+
+lemma lam_FiniteFun: "A: Fin(X) ==> (lam x:A. b(x)) : A -||> {b(x). x:A}"
+by (blast intro: fun_FiniteFunI lam_funtype)
+
+lemma FiniteFun_Collect_iff:
+ "f : FiniteFun(A, {y:B. P(y)})
+ <-> f : FiniteFun(A,B) & (ALL x:domain(f). P(f`x))"
+apply auto
+apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD])
+apply (blast dest: Pair_mem_PiD FiniteFun_is_fun)
+apply (rule_tac A1="domain(f)" in
+ subset_refl [THEN [2] FiniteFun_mono, THEN subsetD])
+ apply (fast dest: FiniteFun_domain_Fin Fin.dom_subset [THEN subsetD])
+apply (rule fun_FiniteFunI)
+apply (erule FiniteFun_domain_Fin)
+apply (rule_tac B = "range (f) " in fun_weaken_type)
+ apply (blast dest: FiniteFun_is_fun range_of_fun range_type apply_equality)+
+done
+
+ML
+{*
+val Fin_intros = thms "Fin.intros";
+
+val Fin_mono = thm "Fin_mono";
+val FinD = thm "FinD";
+val Fin_induct = thm "Fin_induct";
+val Fin_UnI = thm "Fin_UnI";
+val Fin_UnionI = thm "Fin_UnionI";
+val Fin_subset = thm "Fin_subset";
+val Fin_IntI1 = thm "Fin_IntI1";
+val Fin_IntI2 = thm "Fin_IntI2";
+val Fin_0_induct = thm "Fin_0_induct";
+val nat_fun_subset_Fin = thm "nat_fun_subset_Fin";
+val FiniteFun_mono = thm "FiniteFun_mono";
+val FiniteFun_mono1 = thm "FiniteFun_mono1";
+val FiniteFun_is_fun = thm "FiniteFun_is_fun";
+val FiniteFun_domain_Fin = thm "FiniteFun_domain_Fin";
+val FiniteFun_apply_type = thm "FiniteFun_apply_type";
+val FiniteFun_subset = thm "FiniteFun_subset";
+val fun_FiniteFunI = thm "fun_FiniteFunI";
+val lam_FiniteFun = thm "lam_FiniteFun";
+val FiniteFun_Collect_iff = thm "FiniteFun_Collect_iff";
+*}
+
end
--- a/src/ZF/Induct/FoldSet.ML Fri May 31 12:27:24 2002 +0200
+++ b/src/ZF/Induct/FoldSet.ML Fri May 31 15:06:06 2002 +0200
@@ -106,7 +106,7 @@
by (subgoal_tac "Finite(cons(xb, Cb)) & x:cons(xb, Cb) " 2);
by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff,
Fin_into_Finite RS Finite_imp_cardinal_cons]) 2);
-by (asm_simp_tac (simpset() addsimps [Fin.consI RS Fin_into_Finite]) 2);
+by (asm_simp_tac (simpset() addsimps [thm "Fin.consI" RS Fin_into_Finite]) 2);
by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A"), ("f1", "f")]
(Fin_imp_fold_set RS exE) 1);
by (blast_tac (claset() addIs [Diff_subset RS Fin_subset]) 1);
@@ -175,7 +175,7 @@
\ ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <-> \
\ (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))";
by Auto_tac;
-by (forward_tac [inst "a" "c" Fin.consI RS FinD RS fold_set_mono RS subsetD] 1);
+by (forward_tac [inst "a" "c" (thm"Fin.consI") RS FinD RS fold_set_mono RS subsetD] 1);
by (assume_tac 1);
by (assume_tac 1);
by (forward_tac [FinD RS fold_set_mono RS subsetD] 2);
--- a/src/ZF/Induct/FoldSet.thy Fri May 31 12:27:24 2002 +0200
+++ b/src/ZF/Induct/FoldSet.thy Fri May 31 15:06:06 2002 +0200
@@ -18,7 +18,7 @@
emptyI "e:B ==> <0, e>:fold_set(A, B, f,e)"
consI "[| x:A; x ~:C; <C,y> : fold_set(A, B,f,e); f(x,y):B |]
==> <cons(x,C), f(x,y)>:fold_set(A, B, f, e)"
- type_intrs "Fin.intrs"
+ type_intrs "Fin_intros"
constdefs
--- a/src/ZF/Induct/Multiset.ML Fri May 31 12:27:24 2002 +0200
+++ b/src/ZF/Induct/Multiset.ML Fri May 31 15:06:06 2002 +0200
@@ -104,7 +104,7 @@
(* the empty multiset is 0 *)
Goal "multiset(0)";
-by (auto_tac (claset() addIs FiniteFun.intrs,
+by (auto_tac (claset() addIs (thms"FiniteFun.intros"),
simpset() addsimps [multiset_iff_Mult_mset_of]));
qed "multiset_0";
Addsimps [multiset_0];
--- a/src/ZF/IsaMakefile Fri May 31 12:27:24 2002 +0200
+++ b/src/ZF/IsaMakefile Fri May 31 15:06:06 2002 +0200
@@ -31,7 +31,7 @@
$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML \
ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \
CardinalArith.ML CardinalArith.thy Cardinal_AC.thy \
- Datatype.ML Datatype.thy Epsilon.thy Finite.ML Finite.thy \
+ Datatype.ML Datatype.thy Epsilon.thy Finite.thy \
Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy \
InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML \
Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy \
--- a/src/ZF/UNITY/Guar.ML Fri May 31 12:27:24 2002 +0200
+++ b/src/ZF/UNITY/Guar.ML Fri May 31 15:06:06 2002 +0200
@@ -417,7 +417,7 @@
by (Clarify_tac 1);
by (subgoal_tac "F component_of (JN F:FF. F)" 1);
by (dres_inst_tac [("X", "X")] component_of_wg 1);
-by (force_tac (claset() addSDs [Fin.dom_subset RS subsetD RS PowD],
+by (force_tac (claset() addSDs [thm"Fin.dom_subset" RS subsetD RS PowD],
simpset()) 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_of_def])));
by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1);