author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 279  7738aed3f84d 
permissions  rwrr 
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 

37  12 
[ a~:b; b: Fin(A) ] ==> card(cons(a,b)) = succ(card(b)) 
0  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 

279  21 
(val thy = Arith.thy addconsts [(["Fin"],"i=>i")] 
22 
val rec_doms = [("Fin","Pow(A)")] 

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

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

25 
val monos = [] 

26 
val con_defs = [] 

70
8a29f8b4aca1
ZF/indsyntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset

27 
val type_intrs = [empty_subsetI, cons_subsetI, PowI] 
0  28 
val type_elims = [make_elim PowD]); 
29 

124  30 
store_theory "Fin" Fin.thy; 
31 

0  32 
val [Fin_0I, Fin_consI] = Fin.intrs; 
33 

34 

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

36 
by (rtac lfp_mono 1); 

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

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

39 
val Fin_mono = result(); 

40 

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

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

43 

44 
(** Induction on finite sets **) 

45 

37  46 
(*Discharging x~:y entails extra work*) 
0  47 
val major::prems = goal Fin.thy 
48 
"[ b: Fin(A); \ 

49 
\ P(0); \ 

37  50 
\ !!x y. [ x: A; y: Fin(A); x~:y; P(y) ] ==> P(cons(x,y)) \ 
0  51 
\ ] ==> P(b)"; 
52 
by (rtac (major RS Fin.induct) 1); 

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

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

55 
by (REPEAT (ares_tac prems 1)); 

56 
val Fin_induct = result(); 

57 

58 
(** Simplification for Fin **) 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

59 
val Fin_ss = arith_ss addsimps Fin.intrs; 
0  60 

55  61 
(*The union of two finite sets is finite.*) 
0  62 
val major::prems = goal Fin.thy 
63 
"[ b: Fin(A); c: Fin(A) ] ==> b Un c : Fin(A)"; 

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

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

65 
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons])))); 
0  66 
val Fin_UnI = result(); 
67 

55  68 
(*The union of a set of finite sets is finite.*) 
0  69 
val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"; 
70 
by (rtac (major RS Fin_induct) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

71 
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI]))); 
0  72 
val Fin_UnionI = result(); 
73 

55  74 
(*Every subset of a finite set is finite.*) 
75 
goal Fin.thy "!!b A. b: Fin(A) ==> ALL z. z<=b > z: Fin(A)"; 

129  76 
by (etac Fin_induct 1); 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

77 
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1); 
0  78 
by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1])); 
79 
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

80 
by (ALLGOALS (asm_simp_tac Fin_ss)); 
55  81 
val Fin_subset_lemma = result(); 
82 

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

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

0  85 
val Fin_subset = result(); 
86 

87 
val major::prems = goal Fin.thy 

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

89 
\ P(b); \ 

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

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

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

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

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

94 
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 
0  95 
Diff_subset RS Fin_subset])))); 
96 
val Fin_0_induct_lemma = result(); 

97 

98 
val prems = goal Fin.thy 

99 
"[ b: Fin(A); \ 

100 
\ P(b); \ 

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

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

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

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

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

106 
val Fin_0_induct = result(); 