435

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

363

2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

484

4 
Copyright 1994 University of Cambridge

363

5 


6 
Finite powerset operator


7 

484

8 
prove X:Fin(A) ==> X < nat

363

9 

484

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

363

11 
*)


12 


13 
structure Fin = Inductive_Fun

444

14 
(val thy = Arith.thy > add_consts [("Fin", "i=>i", NoSyn)]

477

15 
val thy_name = "Fin"

363

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


17 
val sintrs = ["0 : Fin(A)",


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


19 
val monos = []


20 
val con_defs = []


21 
val type_intrs = [empty_subsetI, cons_subsetI, PowI]


22 
val type_elims = [make_elim PowD]);


23 


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


25 


26 


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


28 
by (rtac lfp_mono 1);


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


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


31 
val Fin_mono = result();


32 


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


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


35 


36 
(** Induction on finite sets **)


37 


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


39 
val major::prems = goal Fin.thy


40 
"[ b: Fin(A); \


41 
\ P(0); \


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


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


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

437

45 
by (excluded_middle_tac "a:b" 2);

363

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


47 
by (REPEAT (ares_tac prems 1));


48 
val Fin_induct = result();


49 


50 
(** Simplification for Fin **)


51 
val Fin_ss = arith_ss addsimps Fin.intrs;


52 


53 
(*The union of two finite sets is finite.*)


54 
val major::prems = goal Fin.thy


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


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


57 
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));


58 
val Fin_UnI = result();


59 


60 
(*The union of a set of finite sets is finite.*)


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


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


63 
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));


64 
val Fin_UnionI = result();


65 


66 
(*Every subset of a finite set is finite.*)


67 
goal Fin.thy "!!b A. b: Fin(A) ==> ALL z. z<=b > z: Fin(A)";


68 
by (etac Fin_induct 1);


69 
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);


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


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


72 
by (ALLGOALS (asm_simp_tac Fin_ss));


73 
val Fin_subset_lemma = result();


74 


75 
goal Fin.thy "!!c b A. [ c<=b; b: Fin(A) ] ==> c: Fin(A)";


76 
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));


77 
val Fin_subset = result();


78 


79 
val major::prems = goal Fin.thy


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


81 
\ P(b); \


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


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


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


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


86 
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff,


87 
Diff_subset RS Fin_subset]))));


88 
val Fin_0_induct_lemma = result();


89 


90 
val prems = goal Fin.thy


91 
"[ b: Fin(A); \


92 
\ P(b); \


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


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


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


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


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


98 
val Fin_0_induct = result();

484

99 


100 
(*Functions from a finite ordinal*)


101 
val prems = goal Fin.thy "n: nat ==> n>A <= Fin(nat*A)";


102 
by (nat_ind_tac "n" prems 1);


103 
by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin_0I, subset_iff, cons_iff]) 1);


104 
by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);


105 
by (fast_tac (ZF_cs addSIs [Fin_consI]) 1);


106 
val nat_fun_subset_Fin = result();
