author | paulson |
Fri, 21 Aug 1998 16:14:34 +0200 | |
changeset 5359 | bd539b72d484 |
parent 5268 | 59ef39008514 |
child 5412 | 0c2472c74c24 |
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 |
||
13 |
open Finite; |
|
14 |
||
534 | 15 |
(*** Finite powerset operator ***) |
16 |
||
5137 | 17 |
Goalw Fin.defs "A<=B ==> Fin(A) <= Fin(B)"; |
516 | 18 |
by (rtac lfp_mono 1); |
19 |
by (REPEAT (rtac Fin.bnd_mono 1)); |
|
20 |
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1)); |
|
760 | 21 |
qed "Fin_mono"; |
516 | 22 |
|
23 |
(* A : Fin(B) ==> A <= B *) |
|
24 |
val FinD = Fin.dom_subset RS subsetD RS PowD; |
|
25 |
||
26 |
(** Induction on finite sets **) |
|
27 |
||
28 |
(*Discharging x~:y entails extra work*) |
|
5268 | 29 |
val major::prems = Goal |
516 | 30 |
"[| b: Fin(A); \ |
31 |
\ P(0); \ |
|
32 |
\ !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) \ |
|
33 |
\ |] ==> P(b)"; |
|
34 |
by (rtac (major RS Fin.induct) 1); |
|
35 |
by (excluded_middle_tac "a:b" 2); |
|
1461 | 36 |
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) |
516 | 37 |
by (REPEAT (ares_tac prems 1)); |
760 | 38 |
qed "Fin_induct"; |
516 | 39 |
|
40 |
(** Simplification for Fin **) |
|
2469 | 41 |
Addsimps Fin.intrs; |
516 | 42 |
|
43 |
(*The union of two finite sets is finite.*) |
|
5268 | 44 |
Goal "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)"; |
2469 | 45 |
by (etac Fin_induct 1); |
4091 | 46 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons]))); |
760 | 47 |
qed "Fin_UnI"; |
516 | 48 |
|
2469 | 49 |
Addsimps [Fin_UnI]; |
50 |
||
516 | 51 |
(*The union of a set of finite sets is finite.*) |
52 |
val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"; |
|
53 |
by (rtac (major RS Fin_induct) 1); |
|
2469 | 54 |
by (ALLGOALS Asm_simp_tac); |
760 | 55 |
qed "Fin_UnionI"; |
516 | 56 |
|
57 |
(*Every subset of a finite set is finite.*) |
|
5137 | 58 |
Goal "b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)"; |
516 | 59 |
by (etac Fin_induct 1); |
4091 | 60 |
by (simp_tac (simpset() addsimps [subset_empty_iff]) 1); |
61 |
by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1); |
|
4152 | 62 |
by Safe_tac; |
534 | 63 |
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1); |
2469 | 64 |
by (Asm_simp_tac 1); |
760 | 65 |
qed "Fin_subset_lemma"; |
516 | 66 |
|
5137 | 67 |
Goal "[| c<=b; b: Fin(A) |] ==> c: Fin(A)"; |
516 | 68 |
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1)); |
760 | 69 |
qed "Fin_subset"; |
516 | 70 |
|
5268 | 71 |
val major::prems = Goal |
1461 | 72 |
"[| c: Fin(A); b: Fin(A); \ |
73 |
\ P(b); \ |
|
516 | 74 |
\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
75 |
\ |] ==> c<=b --> P(b-c)"; |
|
76 |
by (rtac (major RS Fin_induct) 1); |
|
2033 | 77 |
by (stac Diff_cons 2); |
4091 | 78 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps (prems@[cons_subset_iff, |
1461 | 79 |
Diff_subset RS Fin_subset])))); |
760 | 80 |
qed "Fin_0_induct_lemma"; |
516 | 81 |
|
5268 | 82 |
val prems = Goal |
1461 | 83 |
"[| b: Fin(A); \ |
84 |
\ P(b); \ |
|
516 | 85 |
\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
86 |
\ |] ==> P(0)"; |
|
87 |
by (rtac (Diff_cancel RS subst) 1); |
|
88 |
by (rtac (Fin_0_induct_lemma RS mp) 1); |
|
89 |
by (REPEAT (ares_tac (subset_refl::prems) 1)); |
|
760 | 90 |
qed "Fin_0_induct"; |
516 | 91 |
|
92 |
(*Functions from a finite ordinal*) |
|
5268 | 93 |
Goal "n: nat ==> n->A <= Fin(nat*A)"; |
94 |
by (nat_ind_tac "n" [] 1); |
|
4091 | 95 |
by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1); |
5268 | 96 |
by (asm_simp_tac |
97 |
(simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1); |
|
4091 | 98 |
by (fast_tac (claset() addSIs [Fin.consI]) 1); |
760 | 99 |
qed "nat_fun_subset_Fin"; |
534 | 100 |
|
101 |
||
102 |
(*** Finite function space ***) |
|
103 |
||
5067 | 104 |
Goalw FiniteFun.defs |
534 | 105 |
"!!A B C D. [| A<=C; B<=D |] ==> A -||> B <= C -||> D"; |
106 |
by (rtac lfp_mono 1); |
|
107 |
by (REPEAT (rtac FiniteFun.bnd_mono 1)); |
|
108 |
by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1)); |
|
760 | 109 |
qed "FiniteFun_mono"; |
534 | 110 |
|
5137 | 111 |
Goal "A<=B ==> A -||> A <= B -||> B"; |
534 | 112 |
by (REPEAT (ares_tac [FiniteFun_mono] 1)); |
760 | 113 |
qed "FiniteFun_mono1"; |
534 | 114 |
|
5137 | 115 |
Goal "h: A -||>B ==> h: domain(h) -> B"; |
534 | 116 |
by (etac FiniteFun.induct 1); |
4091 | 117 |
by (simp_tac (simpset() addsimps [empty_fun, domain_0]) 1); |
118 |
by (asm_simp_tac (simpset() addsimps [fun_extend3, domain_cons]) 1); |
|
760 | 119 |
qed "FiniteFun_is_fun"; |
534 | 120 |
|
5137 | 121 |
Goal "h: A -||>B ==> domain(h) : Fin(A)"; |
534 | 122 |
by (etac FiniteFun.induct 1); |
4091 | 123 |
by (simp_tac (simpset() addsimps [domain_0]) 1); |
124 |
by (asm_simp_tac (simpset() addsimps [domain_cons]) 1); |
|
760 | 125 |
qed "FiniteFun_domain_Fin"; |
534 | 126 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
760
diff
changeset
|
127 |
bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type); |
534 | 128 |
|
129 |
(*Every subset of a finite function is a finite function.*) |
|
5137 | 130 |
Goal "b: A-||>B ==> ALL z. z<=b --> z: A-||>B"; |
534 | 131 |
by (etac FiniteFun.induct 1); |
4091 | 132 |
by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1); |
133 |
by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1); |
|
4152 | 134 |
by Safe_tac; |
534 | 135 |
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1); |
136 |
by (dtac (spec RS mp) 1 THEN assume_tac 1); |
|
4091 | 137 |
by (fast_tac (claset() addSIs FiniteFun.intrs) 1); |
760 | 138 |
qed "FiniteFun_subset_lemma"; |
534 | 139 |
|
5137 | 140 |
Goal "[| c<=b; b: A-||>B |] ==> c: A-||>B"; |
534 | 141 |
by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1)); |
760 | 142 |
qed "FiniteFun_subset"; |
534 | 143 |