0

1 
(* Title: ZF/ex/fin.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Finite powerset operator


7 


8 
could define cardinality?


9 


10 
prove X:Fin(A) ==> EX n:nat. EX f. f:bij(X,n)


11 
card(0)=0


12 
[ ~ a:b; b: Fin(A) ] ==> card(cons(a,b)) = succ(card(b))


13 


14 
b: Fin(A) ==> inj(b,b)<=surj(b,b)


15 


16 
Limit(i) ==> Fin(Vfrom(A,i)) <= Un j:i. Fin(Vfrom(A,j))


17 
Fin(univ(A)) <= univ(A)


18 
*)


19 


20 
structure Fin = Inductive_Fun


21 
(val thy = Arith.thy addconsts [(["Fin"],"i=>i")];


22 
val rec_doms = [("Fin","Pow(A)")];


23 
val sintrs =


24 
["0 : Fin(A)",


25 
"[ a: A; b: Fin(A) ] ==> cons(a,b) : Fin(A)"];


26 
val monos = [];


27 
val con_defs = [];


28 
val type_intrs = [Pow_bottom, cons_subsetI, PowI]


29 
val type_elims = [make_elim PowD]);


30 


31 
val [Fin_0I, Fin_consI] = Fin.intrs;


32 


33 


34 
goalw Fin.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";


35 
by (rtac lfp_mono 1);


36 
by (REPEAT (rtac Fin.bnd_mono 1));


37 
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));


38 
val Fin_mono = result();


39 


40 
(* A : Fin(B) ==> A <= B *)


41 
val FinD = Fin.dom_subset RS subsetD RS PowD;


42 


43 
(** Induction on finite sets **)


44 


45 
(*Discharging ~ x:y entails extra work*)


46 
val major::prems = goal Fin.thy


47 
"[ b: Fin(A); \


48 
\ P(0); \


49 
\ !!x y. [ x: A; y: Fin(A); ~ x:y; P(y) ] ==> P(cons(x,y)) \


50 
\ ] ==> P(b)";


51 
by (rtac (major RS Fin.induct) 1);


52 
by (res_inst_tac [("Q","a:b")] (excluded_middle RS disjE) 2);


53 
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*)


54 
by (REPEAT (ares_tac prems 1));


55 
val Fin_induct = result();


56 


57 
(** Simplification for Fin **)


58 
val Fin_ss = arith_ss addcongs mk_congs Fin.thy ["Fin"] addrews Fin.intrs;


59 


60 
(*The union of two finite sets is fin*)


61 
val major::prems = goal Fin.thy


62 
"[ b: Fin(A); c: Fin(A) ] ==> b Un c : Fin(A)";


63 
by (rtac (major RS Fin_induct) 1);


64 
by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews (prems@[Un_0, Un_cons]))));


65 
val Fin_UnI = result();


66 


67 
(*The union of a set of finite sets is fin*)


68 
val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";


69 
by (rtac (major RS Fin_induct) 1);


70 
by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews [Union_0, Union_cons, Fin_UnI])));


71 
val Fin_UnionI = result();


72 


73 
(*Every subset of a finite set is fin*)


74 
val [subs,fin] = goal Fin.thy "[ c<=b; b: Fin(A) ] ==> c: Fin(A)";


75 
by (EVERY1 [subgoal_tac "(ALL z. z<=b > z: Fin(A))",


76 
etac (spec RS mp),


77 
rtac subs]);


78 
by (rtac (fin RS Fin_induct) 1);


79 
by (SIMP_TAC (Fin_ss addrews [subset_empty_iff]) 1);


80 
by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));


81 
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);


82 
by (ALLGOALS (ASM_SIMP_TAC Fin_ss));


83 
val Fin_subset = result();


84 


85 
val major::prems = goal Fin.thy


86 
"[ c: Fin(A); b: Fin(A); \


87 
\ P(b); \


88 
\ !!x y. [ x: A; y: Fin(A); x:y; P(y) ] ==> P(y{x}) \


89 
\ ] ==> c<=b > P(bc)";


90 
by (rtac (major RS Fin_induct) 1);


91 
by (rtac (Diff_cons RS ssubst) 2);


92 
by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews (prems@[Diff_0, cons_subset_iff,


93 
Diff_subset RS Fin_subset]))));


94 
val Fin_0_induct_lemma = result();


95 


96 
val prems = goal Fin.thy


97 
"[ b: Fin(A); \


98 
\ P(b); \


99 
\ !!x y. [ x: A; y: Fin(A); x:y; P(y) ] ==> P(y{x}) \


100 
\ ] ==> P(0)";


101 
by (rtac (Diff_cancel RS subst) 1);


102 
by (rtac (Fin_0_induct_lemma RS mp) 1);


103 
by (REPEAT (ares_tac (subset_refl::prems) 1));


104 
val Fin_0_induct = result();
