author | wenzelm |
Sat, 15 Apr 2000 15:00:57 +0200 | |
changeset 8717 | 20c42415c07d |
parent 279 | 7738aed3f84d |
permissions | -rw-r--r-- |
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/ind-syntax/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(b-c)"; |
|
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(); |