|
1 open Finite; |
|
2 |
|
3 (** Monotonicity and unfolding of the function **) |
|
4 |
|
5 goal Finite.thy "mono(%F. insert({}, UN x:A. insert(x)``F))"; |
|
6 by (rtac monoI 1); |
|
7 by (fast_tac set_cs 1); |
|
8 val Fin_bnd_mono = result(); |
|
9 |
|
10 goalw Finite.thy [Fin_def] "!!A B. A<=B ==> Fin(A) <= Fin(B)"; |
|
11 br lfp_mono 1; |
|
12 by(fast_tac set_cs 1); |
|
13 val Fin_mono = result(); |
|
14 |
|
15 goalw Finite.thy [Fin_def] "Fin(A) <= {B. B <= A}"; |
|
16 by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1); |
|
17 val Fin_subset_Pow = result(); |
|
18 |
|
19 (* A : Fin(B) ==> A <= B *) |
|
20 val FinD = Fin_subset_Pow RS subsetD RS CollectD; |
|
21 |
|
22 val Fin_unfold = Fin_bnd_mono RS (Fin_def RS def_lfp_Tarski); |
|
23 |
|
24 goal Finite.thy "{} : Fin(A)"; |
|
25 by (rtac (Fin_unfold RS ssubst) 1); |
|
26 by (rtac insertI1 1); |
|
27 val Fin_0I = result(); |
|
28 |
|
29 goal Finite.thy "!!a. [| a:A; F:Fin(A) |] ==> insert(a,F) : Fin(A)"; |
|
30 by (rtac (Fin_unfold RS ssubst) 1); |
|
31 by(fast_tac set_cs 1); |
|
32 val Fin_insertI = result(); |
|
33 |
|
34 (*Discharging ~ x:y entails extra work*) |
|
35 val major::prems = goal Finite.thy |
|
36 "[| F:Fin(A); P({}); \ |
|
37 \ !!F x. [| x:A; F:Fin(A); ~x:F; P(F) |] ==> P(insert(x,F)) \ |
|
38 \ |] ==> P(F)"; |
|
39 by (rtac (major RS (Fin_def RS def_induct)) 1); |
|
40 by (rtac Fin_bnd_mono 1); |
|
41 by (safe_tac set_cs); |
|
42 (*Excluded middle on x:y would be more straightforward; |
|
43 actual proof is inspired by Dov Gabbay's Restart Rule*) |
|
44 by (rtac classical 2); |
|
45 by (REPEAT (ares_tac prems 1)); |
|
46 by (etac contrapos 1); |
|
47 by (rtac (insert_absorb RS ssubst) 1); |
|
48 by (REPEAT (assume_tac 1)); |
|
49 val Fin_induct = result(); |
|
50 |
|
51 (** Simplification for Fin **) |
|
52 |
|
53 val Fin_ss = set_ss addsimps [Fin_0I, Fin_insertI]; |
|
54 |
|
55 (*The union of two finite sets is finite*) |
|
56 val major::prems = goal Finite.thy |
|
57 "[| F: Fin(A); G: Fin(A) |] ==> F Un G : Fin(A)"; |
|
58 by (rtac (major RS Fin_induct) 1); |
|
59 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left])))); |
|
60 val Fin_UnI = result(); |
|
61 |
|
62 (*Every subset of a finite set is finite*) |
|
63 val [subs,fin] = goal Finite.thy "[| A<=B; B: Fin(M) |] ==> A: Fin(M)"; |
|
64 by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)", |
|
65 rtac mp, etac spec, |
|
66 rtac subs]); |
|
67 by (rtac (fin RS Fin_induct) 1); |
|
68 by (simp_tac (Fin_ss addsimps [subset_Un_eq]) 1); |
|
69 by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1])); |
|
70 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2); |
|
71 by (ALLGOALS (asm_simp_tac Fin_ss)); |
|
72 val Fin_subset = result(); |
|
73 |
|
74 (*The image of a finite set is finite*) |
|
75 val major::_ = goal Finite.thy |
|
76 "F: Fin(A) ==> h``F : Fin(h``A)"; |
|
77 by (rtac (major RS Fin_induct) 1); |
|
78 by (simp_tac Fin_ss 1); |
|
79 by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin_insertI,image_insert]) 1); |
|
80 val Fin_imageI = result(); |
|
81 |
|
82 val major::prems = goal Finite.thy |
|
83 "[| c: Fin(A); b: Fin(A); \ |
|
84 \ P(b); \ |
|
85 \ !!(x::'a) 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); |
|
88 by (rtac (Diff_insert RS ssubst) 2); |
|
89 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[insert_subset_iff, |
|
90 Diff_subset RS Fin_subset])))); |
|
91 val Fin_empty_induct_lemma = result(); |
|
92 |
|
93 val prems = goal Finite.thy |
|
94 "[| b: Fin(A); \ |
|
95 \ P(b); \ |
|
96 \ !!x y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
|
97 \ |] ==> P({})"; |
|
98 by (rtac (Diff_cancel RS subst) 1); |
|
99 by (rtac (Fin_empty_induct_lemma RS mp) 1); |
|
100 by (REPEAT (ares_tac (subset_refl::prems) 1)); |
|
101 val Fin_empty_induct = result(); |