0
|
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);
|
58
|
89 |
by (ALLGOALS (asm_simp_tac
|
|
90 |
(Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
|
0
|
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();
|