author | wenzelm |
Thu, 14 Oct 1999 15:04:36 +0200 | |
changeset 7866 | 3ccaa11b6df9 |
parent 6070 | 032babd0120b |
child 8181 | ee74d3843214 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/Finite.ML |
516 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
516 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
534 | 6 |
Finite powerset operator; finite function space |
516 | 7 |
|
8 |
prove X:Fin(A) ==> |X| < nat |
|
9 |
||
10 |
prove: b: Fin(A) ==> inj(b,b)<=surj(b,b) |
|
11 |
*) |
|
12 |
||
534 | 13 |
(*** Finite powerset operator ***) |
14 |
||
5137 | 15 |
Goalw Fin.defs "A<=B ==> Fin(A) <= Fin(B)"; |
516 | 16 |
by (rtac lfp_mono 1); |
17 |
by (REPEAT (rtac Fin.bnd_mono 1)); |
|
18 |
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1)); |
|
760 | 19 |
qed "Fin_mono"; |
516 | 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*) |
|
5268 | 27 |
val major::prems = Goal |
516 | 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); |
|
1461 | 34 |
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) |
516 | 35 |
by (REPEAT (ares_tac prems 1)); |
760 | 36 |
qed "Fin_induct"; |
516 | 37 |
|
38 |
(** Simplification for Fin **) |
|
2469 | 39 |
Addsimps Fin.intrs; |
516 | 40 |
|
41 |
(*The union of two finite sets is finite.*) |
|
5268 | 42 |
Goal "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)"; |
2469 | 43 |
by (etac Fin_induct 1); |
4091 | 44 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons]))); |
760 | 45 |
qed "Fin_UnI"; |
516 | 46 |
|
2469 | 47 |
Addsimps [Fin_UnI]; |
48 |
||
5412 | 49 |
|
516 | 50 |
(*The union of a set of finite sets is finite.*) |
51 |
val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"; |
|
52 |
by (rtac (major RS Fin_induct) 1); |
|
2469 | 53 |
by (ALLGOALS Asm_simp_tac); |
760 | 54 |
qed "Fin_UnionI"; |
516 | 55 |
|
56 |
(*Every subset of a finite set is finite.*) |
|
5137 | 57 |
Goal "b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)"; |
516 | 58 |
by (etac Fin_induct 1); |
4091 | 59 |
by (simp_tac (simpset() addsimps [subset_empty_iff]) 1); |
60 |
by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1); |
|
4152 | 61 |
by Safe_tac; |
534 | 62 |
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1); |
2469 | 63 |
by (Asm_simp_tac 1); |
760 | 64 |
qed "Fin_subset_lemma"; |
516 | 65 |
|
5137 | 66 |
Goal "[| c<=b; b: Fin(A) |] ==> c: Fin(A)"; |
516 | 67 |
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1)); |
760 | 68 |
qed "Fin_subset"; |
516 | 69 |
|
5412 | 70 |
Goal "b: Fin(A) ==> b Int c : Fin(A)"; |
71 |
by (blast_tac (claset() addIs [Fin_subset]) 1); |
|
72 |
qed "Fin_IntI1"; |
|
73 |
||
74 |
Goal "c: Fin(A) ==> b Int c : Fin(A)"; |
|
75 |
by (blast_tac (claset() addIs [Fin_subset]) 1); |
|
76 |
qed "Fin_IntI2"; |
|
77 |
||
78 |
Addsimps[Fin_IntI1, Fin_IntI2]; |
|
79 |
AddIs[Fin_IntI1, Fin_IntI2]; |
|
80 |
||
81 |
||
5268 | 82 |
val major::prems = Goal |
1461 | 83 |
"[| c: Fin(A); b: Fin(A); \ |
84 |
\ P(b); \ |
|
516 | 85 |
\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
86 |
\ |] ==> c<=b --> P(b-c)"; |
|
87 |
by (rtac (major RS Fin_induct) 1); |
|
2033 | 88 |
by (stac Diff_cons 2); |
4091 | 89 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps (prems@[cons_subset_iff, |
1461 | 90 |
Diff_subset RS Fin_subset])))); |
760 | 91 |
qed "Fin_0_induct_lemma"; |
516 | 92 |
|
5268 | 93 |
val prems = Goal |
1461 | 94 |
"[| b: Fin(A); \ |
95 |
\ P(b); \ |
|
516 | 96 |
\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
97 |
\ |] ==> P(0)"; |
|
98 |
by (rtac (Diff_cancel RS subst) 1); |
|
99 |
by (rtac (Fin_0_induct_lemma RS mp) 1); |
|
100 |
by (REPEAT (ares_tac (subset_refl::prems) 1)); |
|
760 | 101 |
qed "Fin_0_induct"; |
516 | 102 |
|
103 |
(*Functions from a finite ordinal*) |
|
5268 | 104 |
Goal "n: nat ==> n->A <= Fin(nat*A)"; |
6070 | 105 |
by (induct_tac "n" 1); |
4091 | 106 |
by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1); |
5268 | 107 |
by (asm_simp_tac |
108 |
(simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1); |
|
4091 | 109 |
by (fast_tac (claset() addSIs [Fin.consI]) 1); |
760 | 110 |
qed "nat_fun_subset_Fin"; |
534 | 111 |
|
112 |
||
113 |
(*** Finite function space ***) |
|
114 |
||
5067 | 115 |
Goalw FiniteFun.defs |
534 | 116 |
"!!A B C D. [| A<=C; B<=D |] ==> A -||> B <= C -||> D"; |
117 |
by (rtac lfp_mono 1); |
|
118 |
by (REPEAT (rtac FiniteFun.bnd_mono 1)); |
|
119 |
by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1)); |
|
760 | 120 |
qed "FiniteFun_mono"; |
534 | 121 |
|
5137 | 122 |
Goal "A<=B ==> A -||> A <= B -||> B"; |
534 | 123 |
by (REPEAT (ares_tac [FiniteFun_mono] 1)); |
760 | 124 |
qed "FiniteFun_mono1"; |
534 | 125 |
|
5137 | 126 |
Goal "h: A -||>B ==> h: domain(h) -> B"; |
534 | 127 |
by (etac FiniteFun.induct 1); |
4091 | 128 |
by (simp_tac (simpset() addsimps [empty_fun, domain_0]) 1); |
129 |
by (asm_simp_tac (simpset() addsimps [fun_extend3, domain_cons]) 1); |
|
760 | 130 |
qed "FiniteFun_is_fun"; |
534 | 131 |
|
5137 | 132 |
Goal "h: A -||>B ==> domain(h) : Fin(A)"; |
534 | 133 |
by (etac FiniteFun.induct 1); |
4091 | 134 |
by (simp_tac (simpset() addsimps [domain_0]) 1); |
135 |
by (asm_simp_tac (simpset() addsimps [domain_cons]) 1); |
|
760 | 136 |
qed "FiniteFun_domain_Fin"; |
534 | 137 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
760
diff
changeset
|
138 |
bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type); |
534 | 139 |
|
140 |
(*Every subset of a finite function is a finite function.*) |
|
5137 | 141 |
Goal "b: A-||>B ==> ALL z. z<=b --> z: A-||>B"; |
534 | 142 |
by (etac FiniteFun.induct 1); |
4091 | 143 |
by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1); |
144 |
by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1); |
|
4152 | 145 |
by Safe_tac; |
534 | 146 |
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1); |
147 |
by (dtac (spec RS mp) 1 THEN assume_tac 1); |
|
4091 | 148 |
by (fast_tac (claset() addSIs FiniteFun.intrs) 1); |
760 | 149 |
qed "FiniteFun_subset_lemma"; |
534 | 150 |
|
5137 | 151 |
Goal "[| c<=b; b: A-||>B |] ==> c: A-||>B"; |
534 | 152 |
by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1)); |
760 | 153 |
qed "FiniteFun_subset"; |
534 | 154 |