conversion of Finite to Isar format
authorpaulson
Fri May 31 15:06:06 2002 +0200 (2002-05-31)
changeset 13194812b00ed1c03
parent 13193 d5234c261813
child 13195 98975cc13d28
conversion of Finite to Isar format
src/ZF/CardinalArith.ML
src/ZF/Finite.ML
src/ZF/Finite.thy
src/ZF/Induct/FoldSet.ML
src/ZF/Induct/FoldSet.thy
src/ZF/Induct/Multiset.ML
src/ZF/IsaMakefile
src/ZF/UNITY/Guar.ML
     1.1 --- a/src/ZF/CardinalArith.ML	Fri May 31 12:27:24 2002 +0200
     1.2 +++ b/src/ZF/CardinalArith.ML	Fri May 31 15:06:06 2002 +0200
     1.3 @@ -707,7 +707,7 @@
     1.4  
     1.5  Goal "n: nat ==> ALL A. A eqpoll n --> A : Fin(A)";
     1.6  by (induct_tac "n" 1);
     1.7 -by (simp_tac (simpset() addsimps eqpoll_0_iff::Fin.intrs) 1);
     1.8 +by (simp_tac (simpset() addsimps [eqpoll_0_iff]) 1);
     1.9  by (Clarify_tac 1);
    1.10  by (subgoal_tac "EX u. u:A" 1);
    1.11  by (etac exE 1);
    1.12 @@ -716,7 +716,7 @@
    1.13  by (assume_tac 1);
    1.14  by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1);
    1.15  by (assume_tac 1);
    1.16 -by (resolve_tac [Fin.consI] 1);
    1.17 +by (resolve_tac [thm "Fin.consI"] 1);
    1.18  by (Blast_tac 1);
    1.19  by (blast_tac (claset() addIs [subset_consI  RS Fin_mono RS subsetD]) 1); 
    1.20  (*Now for the lemma assumed above*)
    1.21 @@ -729,7 +729,7 @@
    1.22  qed "Finite_into_Fin";
    1.23  
    1.24  Goal "A : Fin(U) ==> Finite(A)";
    1.25 -by (fast_tac (claset() addSIs [Finite_0, Finite_cons] addEs [Fin.induct]) 1);
    1.26 +by (fast_tac (claset() addSIs [Finite_0, Finite_cons] addEs [Fin_induct]) 1);
    1.27  qed "Fin_into_Finite";
    1.28  
    1.29  Goal "Finite(A) <-> A : Fin(A)";
    1.30 @@ -746,9 +746,9 @@
    1.31  Goal "[| ALL y:X. Finite(y);  Finite(X) |] ==> Finite(Union(X))";
    1.32  by (asm_full_simp_tac (simpset() addsimps [Finite_Fin_iff]) 1);
    1.33  by (rtac Fin_UnionI 1);
    1.34 -by (etac Fin.induct 1);
    1.35 +by (etac Fin_induct 1);
    1.36  by (Simp_tac 1);
    1.37 -by (blast_tac (claset() addIs [Fin.consI, impOfSubs Fin_mono]) 1);
    1.38 +by (blast_tac (claset() addIs [thm "Fin.consI", impOfSubs Fin_mono]) 1);
    1.39  qed "Finite_Union";
    1.40  
    1.41  (* Induction principle for Finite(A), by Sidi Ehmety *)
     2.1 --- a/src/ZF/Finite.ML	Fri May 31 12:27:24 2002 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,192 +0,0 @@
     2.4 -(*  Title:      ZF/Finite.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1994  University of Cambridge
     2.8 -
     2.9 -Finite powerset operator; finite function space
    2.10 -
    2.11 -prove X:Fin(A) ==> |X| < nat
    2.12 -
    2.13 -prove:  b: Fin(A) ==> inj(b,b)<=surj(b,b)
    2.14 -*)
    2.15 -
    2.16 -(*** Finite powerset operator ***)
    2.17 -
    2.18 -Goalw Fin.defs "A<=B ==> Fin(A) <= Fin(B)";
    2.19 -by (rtac lfp_mono 1);
    2.20 -by (REPEAT (rtac Fin.bnd_mono 1));
    2.21 -by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
    2.22 -qed "Fin_mono";
    2.23 -
    2.24 -(* A : Fin(B) ==> A <= B *)
    2.25 -bind_thm ("FinD", Fin.dom_subset RS subsetD RS PowD);
    2.26 -
    2.27 -(** Induction on finite sets **)
    2.28 -
    2.29 -(*Discharging x~:y entails extra work*)
    2.30 -val major::prems = Goal
    2.31 -    "[| b: Fin(A);  \
    2.32 -\       P(0);        \
    2.33 -\       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
    2.34 -\    |] ==> P(b)";
    2.35 -by (rtac (major RS Fin.induct) 1);
    2.36 -by (excluded_middle_tac "a:b" 2);
    2.37 -by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);      (*backtracking!*)
    2.38 -by (REPEAT (ares_tac prems 1));
    2.39 -qed "Fin_induct";
    2.40 -
    2.41 -(** Simplification for Fin **)
    2.42 -Addsimps Fin.intrs;
    2.43 -
    2.44 -(*The union of two finite sets is finite.*)
    2.45 -Goal "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
    2.46 -by (etac Fin_induct 1);
    2.47 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
    2.48 -qed "Fin_UnI";
    2.49 -
    2.50 -Addsimps [Fin_UnI];
    2.51 -
    2.52 -
    2.53 -(*The union of a set of finite sets is finite.*)
    2.54 -Goal "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
    2.55 -by (etac Fin_induct 1);
    2.56 -by (ALLGOALS Asm_simp_tac);
    2.57 -qed "Fin_UnionI";
    2.58 -
    2.59 -(*Every subset of a finite set is finite.*)
    2.60 -Goal "b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
    2.61 -by (etac Fin_induct 1);
    2.62 -by (simp_tac (simpset() addsimps [subset_empty_iff]) 1);
    2.63 -by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
    2.64 -by Safe_tac;
    2.65 -by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
    2.66 -by (Asm_simp_tac 1);
    2.67 -qed "Fin_subset_lemma";
    2.68 -
    2.69 -Goal "[| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
    2.70 -by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
    2.71 -qed "Fin_subset";
    2.72 -
    2.73 -Goal "b: Fin(A) ==> b Int c : Fin(A)";
    2.74 -by (blast_tac (claset() addIs [Fin_subset]) 1);
    2.75 -qed "Fin_IntI1";
    2.76 -
    2.77 -Goal "c: Fin(A) ==> b Int c : Fin(A)";
    2.78 -by (blast_tac (claset() addIs [Fin_subset]) 1);
    2.79 -qed "Fin_IntI2";
    2.80 -
    2.81 -Addsimps[Fin_IntI1, Fin_IntI2];
    2.82 -AddIs[Fin_IntI1, Fin_IntI2];
    2.83 -
    2.84 -
    2.85 -val major::prems = Goal
    2.86 -    "[| c: Fin(A);  b: Fin(A);                                  \
    2.87 -\       P(b);                                                   \
    2.88 -\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
    2.89 -\    |] ==> c<=b --> P(b-c)";
    2.90 -by (rtac (major RS Fin_induct) 1);
    2.91 -by (stac Diff_cons 2);
    2.92 -by (ALLGOALS (asm_simp_tac (simpset() addsimps (prems@[cons_subset_iff, 
    2.93 -                                Diff_subset RS Fin_subset]))));
    2.94 -qed "Fin_0_induct_lemma";
    2.95 -
    2.96 -val prems = Goal
    2.97 -    "[| b: Fin(A);                                              \
    2.98 -\       P(b);                                                   \
    2.99 -\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
   2.100 -\    |] ==> P(0)";
   2.101 -by (rtac (Diff_cancel RS subst) 1);
   2.102 -by (rtac (Fin_0_induct_lemma RS mp) 1);
   2.103 -by (REPEAT (ares_tac (subset_refl::prems) 1));
   2.104 -qed "Fin_0_induct";
   2.105 -
   2.106 -(*Functions from a finite ordinal*)
   2.107 -Goal "n: nat ==> n->A <= Fin(nat*A)";
   2.108 -by (induct_tac "n" 1);
   2.109 -by (simp_tac (simpset() addsimps [subset_iff]) 1);
   2.110 -by (asm_simp_tac 
   2.111 -    (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
   2.112 -by (fast_tac (claset() addSIs [Fin.consI]) 1);
   2.113 -qed "nat_fun_subset_Fin";
   2.114 -
   2.115 -
   2.116 -(*** Finite function space ***)
   2.117 -
   2.118 -Goalw FiniteFun.defs
   2.119 -    "[| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D";
   2.120 -by (rtac lfp_mono 1);
   2.121 -by (REPEAT (rtac FiniteFun.bnd_mono 1));
   2.122 -by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1));
   2.123 -qed "FiniteFun_mono";
   2.124 -
   2.125 -Goal "A<=B ==> A -||> A  <=  B -||> B";
   2.126 -by (REPEAT (ares_tac [FiniteFun_mono] 1));
   2.127 -qed "FiniteFun_mono1";
   2.128 -
   2.129 -Goal "h: A -||>B ==> h: domain(h) -> B";
   2.130 -by (etac FiniteFun.induct 1);
   2.131 -by (Simp_tac 1);
   2.132 -by (asm_simp_tac (simpset() addsimps [fun_extend3]) 1);
   2.133 -qed "FiniteFun_is_fun";
   2.134 -
   2.135 -Goal "h: A -||>B ==> domain(h) : Fin(A)";
   2.136 -by (etac FiniteFun.induct 1);
   2.137 -by (Simp_tac 1);
   2.138 -by (Asm_simp_tac 1);
   2.139 -qed "FiniteFun_domain_Fin";
   2.140 -
   2.141 -bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type);
   2.142 -
   2.143 -(*Every subset of a finite function is a finite function.*)
   2.144 -Goal "b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
   2.145 -by (etac FiniteFun.induct 1);
   2.146 -by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1);
   2.147 -by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
   2.148 -by Safe_tac;
   2.149 -by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
   2.150 -by (dtac (spec RS mp) 1 THEN assume_tac 1);
   2.151 -by (fast_tac (claset() addSIs FiniteFun.intrs) 1);
   2.152 -qed "FiniteFun_subset_lemma";
   2.153 -
   2.154 -Goal "[| c<=b;  b: A-||>B |] ==> c: A-||>B";
   2.155 -by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1));
   2.156 -qed "FiniteFun_subset";
   2.157 -
   2.158 -(** Some further results by Sidi O. Ehmety **)
   2.159 -
   2.160 -Goal "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B";
   2.161 -by (etac Fin.induct 1);
   2.162 -by (simp_tac (simpset() addsimps FiniteFun.intrs) 1);
   2.163 -by (Clarify_tac 1);
   2.164 -by (case_tac "a:b" 1);
   2.165 -by (rotate_tac ~1 1);
   2.166 -by (asm_full_simp_tac (simpset() addsimps [cons_absorb]) 1);
   2.167 -by (subgoal_tac "restrict(f,b) : b -||> B" 1);
   2.168 -by (blast_tac (claset() addIs [restrict_type2]) 2);
   2.169 -by (stac fun_cons_restrict_eq 1 THEN assume_tac 1);
   2.170 -by (full_simp_tac (simpset() addsimps [restrict_def, lam_def]) 1);
   2.171 -by (blast_tac (claset() addIs [apply_funtype, impOfSubs FiniteFun_mono]
   2.172 -                              @FiniteFun.intrs) 1);
   2.173 -qed_spec_mp "fun_FiniteFunI";
   2.174 -
   2.175 -Goal "A: Fin(X) ==> (lam x:A. b(x)) : A -||> {b(x). x:A}";
   2.176 -by (blast_tac (claset() addIs [fun_FiniteFunI, lam_funtype]) 1);
   2.177 -qed "lam_FiniteFun";
   2.178 -
   2.179 -Goal "f : FiniteFun(A, {y:B. P(y)})  \
   2.180 -\     <-> f : FiniteFun(A,B) & (ALL x:domain(f). P(f`x))";
   2.181 -by Auto_tac;
   2.182 -by (blast_tac (claset() addIs [impOfSubs FiniteFun_mono]) 1);
   2.183 -by (blast_tac (claset() addDs [Pair_mem_PiD, FiniteFun_is_fun]) 1);
   2.184 -by (res_inst_tac [("A1", "domain(f)")]
   2.185 -    (subset_refl RSN(2, FiniteFun_mono) RS subsetD) 1);
   2.186 -by (fast_tac (claset() addDs
   2.187 -		[FiniteFun_domain_Fin, Fin.dom_subset RS subsetD]) 1);
   2.188 -by (rtac fun_FiniteFunI 1);
   2.189 -by (etac FiniteFun_domain_Fin 1);
   2.190 -by (res_inst_tac [("B" , "range(f)")] fun_weaken_type 1);
   2.191 -by (ALLGOALS
   2.192 -    (blast_tac (claset() addDs
   2.193 -		[FiniteFun_is_fun, range_of_fun, range_type,
   2.194 -		 apply_equality])));
   2.195 -qed "FiniteFun_Collect_iff";
     3.1 --- a/src/ZF/Finite.thy	Fri May 31 12:27:24 2002 +0200
     3.2 +++ b/src/ZF/Finite.thy	Fri May 31 15:06:06 2002 +0200
     3.3 @@ -3,36 +3,227 @@
     3.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5      Copyright   1994  University of Cambridge
     3.6  
     3.7 -Finite powerset operator
     3.8 +Finite powerset operator; finite function space
     3.9 +
    3.10 +prove X:Fin(A) ==> |X| < nat
    3.11 +
    3.12 +prove:  b: Fin(A) ==> inj(b,b) <= surj(b,b)
    3.13  *)
    3.14  
    3.15 -Finite = Inductive + Epsilon + Nat +
    3.16 +theory Finite = Inductive + Epsilon + Nat:
    3.17  
    3.18  (*The natural numbers as a datatype*)
    3.19 -rep_datatype 
    3.20 -  elim		natE
    3.21 -  induct	nat_induct
    3.22 -  case_eqns	nat_case_0, nat_case_succ
    3.23 -  recursor_eqns recursor_0, recursor_succ
    3.24 +rep_datatype
    3.25 +  elimination    natE
    3.26 +  induction	 nat_induct
    3.27 +  case_eqns	 nat_case_0 nat_case_succ
    3.28 +  recursor_eqns  recursor_0 recursor_succ
    3.29  
    3.30  
    3.31  consts
    3.32 -  Fin       :: i=>i
    3.33 -  FiniteFun :: [i,i]=>i         ("(_ -||>/ _)" [61, 60] 60)
    3.34 +  Fin       :: "i=>i"
    3.35 +  FiniteFun :: "[i,i]=>i"         ("(_ -||>/ _)" [61, 60] 60)
    3.36  
    3.37  inductive
    3.38    domains   "Fin(A)" <= "Pow(A)"
    3.39 -  intrs
    3.40 -    emptyI  "0 : Fin(A)"
    3.41 -    consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
    3.42 -  type_intrs empty_subsetI, cons_subsetI, PowI
    3.43 -  type_elims "[make_elim PowD]"
    3.44 +  intros
    3.45 +    emptyI:  "0 : Fin(A)"
    3.46 +    consI:   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
    3.47 +  type_intros  empty_subsetI cons_subsetI PowI
    3.48 +  type_elims   PowD [THEN revcut_rl]
    3.49  
    3.50  inductive
    3.51    domains   "FiniteFun(A,B)" <= "Fin(A*B)"
    3.52 -  intrs
    3.53 -    emptyI  "0 : A -||> B"
    3.54 -    consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   
    3.55 -             |] ==> cons(<a,b>,h) : A -||> B"
    3.56 -  type_intrs "Fin.intrs"
    3.57 +  intros
    3.58 +    emptyI:  "0 : A -||> B"
    3.59 +    consI:   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h) |]
    3.60 +              ==> cons(<a,b>,h) : A -||> B"
    3.61 +  type_intros Fin.intros
    3.62 +
    3.63 +
    3.64 +subsection {* Finite powerset operator *}
    3.65 +
    3.66 +lemma Fin_mono: "A<=B ==> Fin(A) <= Fin(B)"
    3.67 +apply (unfold Fin.defs)
    3.68 +apply (rule lfp_mono)
    3.69 +apply (rule Fin.bnd_mono)+
    3.70 +apply blast
    3.71 +done
    3.72 +
    3.73 +(* A : Fin(B) ==> A <= B *)
    3.74 +lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD, standard]
    3.75 +
    3.76 +(** Induction on finite sets **)
    3.77 +
    3.78 +(*Discharging x~:y entails extra work*)
    3.79 +lemma Fin_induct:
    3.80 +    "[| b: Fin(A);
    3.81 +        P(0);
    3.82 +        !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y))
    3.83 +     |] ==> P(b)"
    3.84 +apply (erule Fin.induct, simp)
    3.85 +apply (case_tac "a:b")
    3.86 + apply (erule cons_absorb [THEN ssubst], assumption) (*backtracking!*)
    3.87 +apply simp
    3.88 +done
    3.89 +
    3.90 +(** Simplification for Fin **)
    3.91 +declare Fin.intros [simp]
    3.92 +
    3.93 +(*The union of two finite sets is finite.*)
    3.94 +lemma Fin_UnI: "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)"
    3.95 +apply (erule Fin_induct)
    3.96 +apply (simp_all add: Un_cons)
    3.97 +done
    3.98 +
    3.99 +declare Fin_UnI [simp]
   3.100 +
   3.101 +
   3.102 +(*The union of a set of finite sets is finite.*)
   3.103 +lemma Fin_UnionI: "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"
   3.104 +by (erule Fin_induct, simp_all)
   3.105 +
   3.106 +(*Every subset of a finite set is finite.*)
   3.107 +lemma Fin_subset_lemma [rule_format]: "b: Fin(A) ==> \<forall>z. z<=b --> z: Fin(A)"
   3.108 +apply (erule Fin_induct)
   3.109 +apply (simp add: subset_empty_iff)
   3.110 +apply (simp add: subset_cons_iff distrib_simps, safe)
   3.111 +apply (erule_tac b = "z" in cons_Diff [THEN subst], simp)
   3.112 +done
   3.113 +
   3.114 +lemma Fin_subset: "[| c<=b;  b: Fin(A) |] ==> c: Fin(A)"
   3.115 +by (blast intro: Fin_subset_lemma)
   3.116 +
   3.117 +lemma Fin_IntI1 [intro,simp]: "b: Fin(A) ==> b Int c : Fin(A)"
   3.118 +by (blast intro: Fin_subset)
   3.119 +
   3.120 +lemma Fin_IntI2 [intro,simp]: "c: Fin(A) ==> b Int c : Fin(A)"
   3.121 +by (blast intro: Fin_subset)
   3.122 +
   3.123 +lemma Fin_0_induct_lemma [rule_format]:
   3.124 +    "[| c: Fin(A);  b: Fin(A); P(b);
   3.125 +        !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x})
   3.126 +     |] ==> c<=b --> P(b-c)"
   3.127 +apply (erule Fin_induct, simp)
   3.128 +apply (subst Diff_cons)
   3.129 +apply (simp add: cons_subset_iff Diff_subset [THEN Fin_subset])
   3.130 +done
   3.131 +
   3.132 +lemma Fin_0_induct:
   3.133 +    "[| b: Fin(A);
   3.134 +        P(b);
   3.135 +        !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x})
   3.136 +     |] ==> P(0)"
   3.137 +apply (rule Diff_cancel [THEN subst])
   3.138 +apply (blast intro: Fin_0_induct_lemma) 
   3.139 +done
   3.140 +
   3.141 +(*Functions from a finite ordinal*)
   3.142 +lemma nat_fun_subset_Fin: "n: nat ==> n->A <= Fin(nat*A)"
   3.143 +apply (induct_tac "n")
   3.144 +apply (simp add: subset_iff)
   3.145 +apply (simp add: succ_def mem_not_refl [THEN cons_fun_eq])
   3.146 +apply (fast intro!: Fin.consI)
   3.147 +done
   3.148 +
   3.149 +
   3.150 +(*** Finite function space ***)
   3.151 +
   3.152 +lemma FiniteFun_mono:
   3.153 +    "[| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D"
   3.154 +apply (unfold FiniteFun.defs)
   3.155 +apply (rule lfp_mono)
   3.156 +apply (rule FiniteFun.bnd_mono)+
   3.157 +apply (intro Fin_mono Sigma_mono basic_monos, assumption+)
   3.158 +done
   3.159 +
   3.160 +lemma FiniteFun_mono1: "A<=B ==> A -||> A  <=  B -||> B"
   3.161 +by (blast dest: FiniteFun_mono)
   3.162 +
   3.163 +lemma FiniteFun_is_fun: "h: A -||>B ==> h: domain(h) -> B"
   3.164 +apply (erule FiniteFun.induct, simp)
   3.165 +apply (simp add: fun_extend3)
   3.166 +done
   3.167 +
   3.168 +lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)"
   3.169 +apply (erule FiniteFun.induct, simp)
   3.170 +apply simp
   3.171 +done
   3.172 +
   3.173 +lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard]
   3.174 +
   3.175 +(*Every subset of a finite function is a finite function.*)
   3.176 +lemma FiniteFun_subset_lemma [rule_format]:
   3.177 +     "b: A-||>B ==> ALL z. z<=b --> z: A-||>B"
   3.178 +apply (erule FiniteFun.induct)
   3.179 +apply (simp add: subset_empty_iff FiniteFun.intros)
   3.180 +apply (simp add: subset_cons_iff distrib_simps, safe)
   3.181 +apply (erule_tac b = "z" in cons_Diff [THEN subst])
   3.182 +apply (drule spec [THEN mp], assumption)
   3.183 +apply (fast intro!: FiniteFun.intros)
   3.184 +done
   3.185 +
   3.186 +lemma FiniteFun_subset: "[| c<=b;  b: A-||>B |] ==> c: A-||>B"
   3.187 +by (blast intro: FiniteFun_subset_lemma)
   3.188 +
   3.189 +(** Some further results by Sidi O. Ehmety **)
   3.190 +
   3.191 +lemma fun_FiniteFunI [rule_format]: "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B"
   3.192 +apply (erule Fin.induct)
   3.193 + apply (simp add: FiniteFun.intros)
   3.194 +apply clarify
   3.195 +apply (case_tac "a:b")
   3.196 + apply (rotate_tac -1)
   3.197 + apply (simp add: cons_absorb)
   3.198 +apply (subgoal_tac "restrict (f,b) : b -||> B")
   3.199 + prefer 2 apply (blast intro: restrict_type2)
   3.200 +apply (subst fun_cons_restrict_eq, assumption)
   3.201 +apply (simp add: restrict_def lam_def)
   3.202 +apply (blast intro: apply_funtype FiniteFun.intros 
   3.203 +                    FiniteFun_mono [THEN [2] rev_subsetD])
   3.204 +done
   3.205 +
   3.206 +lemma lam_FiniteFun: "A: Fin(X) ==> (lam x:A. b(x)) : A -||> {b(x). x:A}"
   3.207 +by (blast intro: fun_FiniteFunI lam_funtype)
   3.208 +
   3.209 +lemma FiniteFun_Collect_iff:
   3.210 +     "f : FiniteFun(A, {y:B. P(y)})
   3.211 +      <-> f : FiniteFun(A,B) & (ALL x:domain(f). P(f`x))"
   3.212 +apply auto
   3.213 +apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD])
   3.214 +apply (blast dest: Pair_mem_PiD FiniteFun_is_fun)
   3.215 +apply (rule_tac A1="domain(f)" in 
   3.216 +       subset_refl [THEN [2] FiniteFun_mono, THEN subsetD])
   3.217 + apply (fast dest: FiniteFun_domain_Fin Fin.dom_subset [THEN subsetD])
   3.218 +apply (rule fun_FiniteFunI)
   3.219 +apply (erule FiniteFun_domain_Fin)
   3.220 +apply (rule_tac B = "range (f) " in fun_weaken_type)
   3.221 + apply (blast dest: FiniteFun_is_fun range_of_fun range_type apply_equality)+
   3.222 +done
   3.223 +
   3.224 +ML
   3.225 +{*
   3.226 +val Fin_intros = thms "Fin.intros";
   3.227 +
   3.228 +val Fin_mono = thm "Fin_mono";
   3.229 +val FinD = thm "FinD";
   3.230 +val Fin_induct = thm "Fin_induct";
   3.231 +val Fin_UnI = thm "Fin_UnI";
   3.232 +val Fin_UnionI = thm "Fin_UnionI";
   3.233 +val Fin_subset = thm "Fin_subset";
   3.234 +val Fin_IntI1 = thm "Fin_IntI1";
   3.235 +val Fin_IntI2 = thm "Fin_IntI2";
   3.236 +val Fin_0_induct = thm "Fin_0_induct";
   3.237 +val nat_fun_subset_Fin = thm "nat_fun_subset_Fin";
   3.238 +val FiniteFun_mono = thm "FiniteFun_mono";
   3.239 +val FiniteFun_mono1 = thm "FiniteFun_mono1";
   3.240 +val FiniteFun_is_fun = thm "FiniteFun_is_fun";
   3.241 +val FiniteFun_domain_Fin = thm "FiniteFun_domain_Fin";
   3.242 +val FiniteFun_apply_type = thm "FiniteFun_apply_type";
   3.243 +val FiniteFun_subset = thm "FiniteFun_subset";
   3.244 +val fun_FiniteFunI = thm "fun_FiniteFunI";
   3.245 +val lam_FiniteFun = thm "lam_FiniteFun";
   3.246 +val FiniteFun_Collect_iff = thm "FiniteFun_Collect_iff";
   3.247 +*}
   3.248 +
   3.249  end
     4.1 --- a/src/ZF/Induct/FoldSet.ML	Fri May 31 12:27:24 2002 +0200
     4.2 +++ b/src/ZF/Induct/FoldSet.ML	Fri May 31 15:06:06 2002 +0200
     4.3 @@ -106,7 +106,7 @@
     4.4  by (subgoal_tac "Finite(cons(xb, Cb)) & x:cons(xb, Cb) " 2);
     4.5  by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, 
     4.6                         Fin_into_Finite RS Finite_imp_cardinal_cons]) 2);
     4.7 -by (asm_simp_tac (simpset() addsimps [Fin.consI RS Fin_into_Finite]) 2);
     4.8 +by (asm_simp_tac (simpset() addsimps [thm "Fin.consI" RS Fin_into_Finite]) 2);
     4.9  by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A"), ("f1", "f")] 
    4.10      (Fin_imp_fold_set RS exE) 1);
    4.11  by (blast_tac (claset() addIs [Diff_subset RS Fin_subset]) 1);
    4.12 @@ -175,7 +175,7 @@
    4.13  \    ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <->  \
    4.14  \         (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))";
    4.15  by Auto_tac;
    4.16 -by (forward_tac [inst "a" "c" Fin.consI RS FinD RS fold_set_mono RS subsetD] 1);
    4.17 +by (forward_tac [inst "a" "c" (thm"Fin.consI") RS FinD RS fold_set_mono RS subsetD] 1);
    4.18  by (assume_tac 1);
    4.19  by (assume_tac 1);
    4.20  by (forward_tac [FinD RS fold_set_mono RS subsetD] 2);
     5.1 --- a/src/ZF/Induct/FoldSet.thy	Fri May 31 12:27:24 2002 +0200
     5.2 +++ b/src/ZF/Induct/FoldSet.thy	Fri May 31 15:06:06 2002 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4    emptyI   "e:B ==> <0, e>:fold_set(A, B, f,e)"
     5.5    consI  "[| x:A; x ~:C;  <C,y> : fold_set(A, B,f,e); f(x,y):B |]
     5.6                ==>  <cons(x,C), f(x,y)>:fold_set(A, B, f, e)"
     5.7 -   type_intrs "Fin.intrs"
     5.8 +   type_intrs "Fin_intros"
     5.9    
    5.10  constdefs
    5.11    
     6.1 --- a/src/ZF/Induct/Multiset.ML	Fri May 31 12:27:24 2002 +0200
     6.2 +++ b/src/ZF/Induct/Multiset.ML	Fri May 31 15:06:06 2002 +0200
     6.3 @@ -104,7 +104,7 @@
     6.4  (* the empty multiset is 0 *)
     6.5  
     6.6  Goal "multiset(0)";
     6.7 -by (auto_tac (claset() addIs FiniteFun.intrs, 
     6.8 +by (auto_tac (claset() addIs (thms"FiniteFun.intros"), 
     6.9          simpset()  addsimps [multiset_iff_Mult_mset_of]));
    6.10  qed "multiset_0";
    6.11  Addsimps [multiset_0];
     7.1 --- a/src/ZF/IsaMakefile	Fri May 31 12:27:24 2002 +0200
     7.2 +++ b/src/ZF/IsaMakefile	Fri May 31 15:06:06 2002 +0200
     7.3 @@ -31,7 +31,7 @@
     7.4  $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML	\
     7.5    ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy		\
     7.6    CardinalArith.ML CardinalArith.thy Cardinal_AC.thy \
     7.7 -  Datatype.ML Datatype.thy Epsilon.thy Finite.ML Finite.thy	\
     7.8 +  Datatype.ML Datatype.thy Epsilon.thy Finite.thy	\
     7.9    Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy 	\
    7.10    InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML	\
    7.11    Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy	\
     8.1 --- a/src/ZF/UNITY/Guar.ML	Fri May 31 12:27:24 2002 +0200
     8.2 +++ b/src/ZF/UNITY/Guar.ML	Fri May 31 15:06:06 2002 +0200
     8.3 @@ -417,7 +417,7 @@
     8.4  by (Clarify_tac 1);
     8.5  by (subgoal_tac "F component_of (JN F:FF. F)" 1);
     8.6  by (dres_inst_tac [("X", "X")] component_of_wg 1);
     8.7 -by (force_tac (claset() addSDs [Fin.dom_subset RS subsetD RS PowD],
     8.8 +by (force_tac (claset() addSDs [thm"Fin.dom_subset" RS subsetD RS PowD],
     8.9                 simpset()) 1);
    8.10  by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_of_def])));
    8.11  by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1);