516

1 
(* Title: ZF/Finite.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
Finite powerset operator


7 


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


9 


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


11 
*)


12 


13 
open Finite;


14 


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


16 
by (rtac lfp_mono 1);


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


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


19 
val Fin_mono = result();


20 


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


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


23 


24 
(** Induction on finite sets **)


25 


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


27 
val major::prems = goal Finite.thy


28 
"[ b: Fin(A); \


29 
\ P(0); \


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


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


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


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


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


35 
by (REPEAT (ares_tac prems 1));


36 
val Fin_induct = result();


37 


38 
(** Simplification for Fin **)


39 
val Fin_ss = arith_ss addsimps Fin.intrs;


40 


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


42 
val major::prems = goal Finite.thy


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


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


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


46 
val Fin_UnI = result();


47 


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


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


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


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


52 
val Fin_UnionI = result();


53 


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


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


56 
by (etac Fin_induct 1);


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


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


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


60 
by (ALLGOALS (asm_simp_tac Fin_ss));


61 
val Fin_subset_lemma = result();


62 


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


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


65 
val Fin_subset = result();


66 


67 
val major::prems = goal Finite.thy


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


69 
\ P(b); \


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


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


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


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


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


75 
Diff_subset RS Fin_subset]))));


76 
val Fin_0_induct_lemma = result();


77 


78 
val prems = goal Finite.thy


79 
"[ b: Fin(A); \


80 
\ P(b); \


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


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


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


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


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


86 
val Fin_0_induct = result();


87 


88 
(*Functions from a finite ordinal*)


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


90 
by (nat_ind_tac "n" prems 1);


91 
by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin.emptyI, subset_iff, cons_iff]) 1);


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


93 
by (fast_tac (ZF_cs addSIs [Fin.consI]) 1);


94 
val nat_fun_subset_Fin = result();
