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 |
|
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 |
|
516
|
17 |
goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
|
|
18 |
by (rtac lfp_mono 1);
|
|
19 |
by (REPEAT (rtac Fin.bnd_mono 1));
|
|
20 |
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
|
|
21 |
val Fin_mono = result();
|
|
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*)
|
|
29 |
val major::prems = goal Finite.thy
|
|
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);
|
|
36 |
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*)
|
|
37 |
by (REPEAT (ares_tac prems 1));
|
|
38 |
val Fin_induct = result();
|
|
39 |
|
|
40 |
(** Simplification for Fin **)
|
|
41 |
val Fin_ss = arith_ss addsimps Fin.intrs;
|
|
42 |
|
|
43 |
(*The union of two finite sets is finite.*)
|
|
44 |
val major::prems = goal Finite.thy
|
|
45 |
"[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)";
|
|
46 |
by (rtac (major RS Fin_induct) 1);
|
|
47 |
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
|
|
48 |
val Fin_UnI = result();
|
|
49 |
|
|
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);
|
|
53 |
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
|
|
54 |
val Fin_UnionI = result();
|
|
55 |
|
|
56 |
(*Every subset of a finite set is finite.*)
|
|
57 |
goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
|
|
58 |
by (etac Fin_induct 1);
|
|
59 |
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
|
534
|
60 |
by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
|
|
61 |
by (safe_tac ZF_cs);
|
|
62 |
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
|
|
63 |
by (asm_simp_tac Fin_ss 1);
|
516
|
64 |
val Fin_subset_lemma = result();
|
|
65 |
|
|
66 |
goal Finite.thy "!!c b A. [| c<=b; b: Fin(A) |] ==> c: Fin(A)";
|
|
67 |
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
|
|
68 |
val Fin_subset = result();
|
|
69 |
|
|
70 |
val major::prems = goal Finite.thy
|
|
71 |
"[| c: Fin(A); b: Fin(A); \
|
|
72 |
\ P(b); \
|
|
73 |
\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
|
|
74 |
\ |] ==> c<=b --> P(b-c)";
|
|
75 |
by (rtac (major RS Fin_induct) 1);
|
|
76 |
by (rtac (Diff_cons RS ssubst) 2);
|
|
77 |
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff,
|
|
78 |
Diff_subset RS Fin_subset]))));
|
|
79 |
val Fin_0_induct_lemma = result();
|
|
80 |
|
|
81 |
val prems = goal Finite.thy
|
|
82 |
"[| b: Fin(A); \
|
|
83 |
\ P(b); \
|
|
84 |
\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
|
|
85 |
\ |] ==> P(0)";
|
|
86 |
by (rtac (Diff_cancel RS subst) 1);
|
|
87 |
by (rtac (Fin_0_induct_lemma RS mp) 1);
|
|
88 |
by (REPEAT (ares_tac (subset_refl::prems) 1));
|
|
89 |
val Fin_0_induct = result();
|
|
90 |
|
|
91 |
(*Functions from a finite ordinal*)
|
|
92 |
val prems = goal Finite.thy "n: nat ==> n->A <= Fin(nat*A)";
|
|
93 |
by (nat_ind_tac "n" prems 1);
|
|
94 |
by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin.emptyI, subset_iff, cons_iff]) 1);
|
|
95 |
by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
|
|
96 |
by (fast_tac (ZF_cs addSIs [Fin.consI]) 1);
|
|
97 |
val nat_fun_subset_Fin = result();
|
534
|
98 |
|
|
99 |
|
|
100 |
(*** Finite function space ***)
|
|
101 |
|
|
102 |
goalw Finite.thy FiniteFun.defs
|
|
103 |
"!!A B C D. [| A<=C; B<=D |] ==> A -||> B <= C -||> D";
|
|
104 |
by (rtac lfp_mono 1);
|
|
105 |
by (REPEAT (rtac FiniteFun.bnd_mono 1));
|
|
106 |
by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1));
|
|
107 |
val FiniteFun_mono = result();
|
|
108 |
|
|
109 |
goal Finite.thy "!!A B. A<=B ==> A -||> A <= B -||> B";
|
|
110 |
by (REPEAT (ares_tac [FiniteFun_mono] 1));
|
|
111 |
val FiniteFun_mono1 = result();
|
|
112 |
|
|
113 |
goal Finite.thy "!!h. h: A -||>B ==> h: domain(h) -> B";
|
|
114 |
by (etac FiniteFun.induct 1);
|
|
115 |
by (simp_tac (ZF_ss addsimps [empty_fun, domain_0]) 1);
|
|
116 |
by (asm_simp_tac (ZF_ss addsimps [fun_extend3, domain_cons]) 1);
|
|
117 |
val FiniteFun_is_fun = result();
|
|
118 |
|
|
119 |
goal Finite.thy "!!h. h: A -||>B ==> domain(h) : Fin(A)";
|
|
120 |
by (etac FiniteFun.induct 1);
|
|
121 |
by (simp_tac (Fin_ss addsimps [domain_0]) 1);
|
|
122 |
by (asm_simp_tac (Fin_ss addsimps [domain_cons]) 1);
|
|
123 |
val FiniteFun_domain_Fin = result();
|
|
124 |
|
|
125 |
val FiniteFun_apply_type = FiniteFun_is_fun RS apply_type |> standard;
|
|
126 |
|
|
127 |
(*Every subset of a finite function is a finite function.*)
|
|
128 |
goal Finite.thy "!!b A. b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
|
|
129 |
by (etac FiniteFun.induct 1);
|
|
130 |
by (simp_tac (ZF_ss addsimps subset_empty_iff::FiniteFun.intrs) 1);
|
|
131 |
by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
|
|
132 |
by (safe_tac ZF_cs);
|
|
133 |
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
|
|
134 |
by (dtac (spec RS mp) 1 THEN assume_tac 1);
|
|
135 |
by (fast_tac (ZF_cs addSIs FiniteFun.intrs) 1);
|
|
136 |
val FiniteFun_subset_lemma = result();
|
|
137 |
|
|
138 |
goal Finite.thy "!!c b A. [| c<=b; b: A-||>B |] ==> c: A-||>B";
|
|
139 |
by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1));
|
|
140 |
val FiniteFun_subset = result();
|
|
141 |
|