|
1 (* Title: HOL/Finite.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Finite powerset operator |
|
7 *) |
|
8 |
|
9 open Finite; |
|
10 |
|
11 goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)"; |
|
12 br lfp_mono 1; |
|
13 by (REPEAT (ares_tac basic_monos 1)); |
|
14 qed "Fin_mono"; |
|
15 |
|
16 goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)"; |
|
17 by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1); |
|
18 qed "Fin_subset_Pow"; |
|
19 |
|
20 (* A : Fin(B) ==> A <= B *) |
|
21 val FinD = Fin_subset_Pow RS subsetD RS PowD; |
|
22 |
|
23 (*Discharging ~ x:y entails extra work*) |
|
24 val major::prems = goal Finite.thy |
|
25 "[| F:Fin(A); P({}); \ |
|
26 \ !!F x. [| x:A; F:Fin(A); x~:F; P(F) |] ==> P(insert x F) \ |
|
27 \ |] ==> P(F)"; |
|
28 by (rtac (major RS Fin.induct) 1); |
|
29 by (excluded_middle_tac "a:b" 2); |
|
30 by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) |
|
31 by (REPEAT (ares_tac prems 1)); |
|
32 qed "Fin_induct"; |
|
33 |
|
34 (** Simplification for Fin **) |
|
35 |
|
36 val Fin_ss = set_ss addsimps Fin.intrs; |
|
37 |
|
38 (*The union of two finite sets is finite*) |
|
39 val major::prems = goal Finite.thy |
|
40 "[| F: Fin(A); G: Fin(A) |] ==> F Un G : Fin(A)"; |
|
41 by (rtac (major RS Fin_induct) 1); |
|
42 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left])))); |
|
43 qed "Fin_UnI"; |
|
44 |
|
45 (*Every subset of a finite set is finite*) |
|
46 val [subs,fin] = goal Finite.thy "[| A<=B; B: Fin(M) |] ==> A: Fin(M)"; |
|
47 by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)", |
|
48 rtac mp, etac spec, |
|
49 rtac subs]); |
|
50 by (rtac (fin RS Fin_induct) 1); |
|
51 by (simp_tac (Fin_ss addsimps [subset_Un_eq]) 1); |
|
52 by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1])); |
|
53 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2); |
|
54 by (ALLGOALS (asm_simp_tac Fin_ss)); |
|
55 qed "Fin_subset"; |
|
56 |
|
57 (*The image of a finite set is finite*) |
|
58 val major::_ = goal Finite.thy |
|
59 "F: Fin(A) ==> h``F : Fin(h``A)"; |
|
60 by (rtac (major RS Fin_induct) 1); |
|
61 by (simp_tac Fin_ss 1); |
|
62 by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin.insertI, image_insert]) 1); |
|
63 qed "Fin_imageI"; |
|
64 |
|
65 val major::prems = goal Finite.thy |
|
66 "[| c: Fin(A); b: Fin(A); \ |
|
67 \ P(b); \ |
|
68 \ !!(x::'a) y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
|
69 \ |] ==> c<=b --> P(b-c)"; |
|
70 by (rtac (major RS Fin_induct) 1); |
|
71 by (rtac (Diff_insert RS ssubst) 2); |
|
72 by (ALLGOALS (asm_simp_tac |
|
73 (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset])))); |
|
74 qed "Fin_empty_induct_lemma"; |
|
75 |
|
76 val prems = goal Finite.thy |
|
77 "[| b: Fin(A); \ |
|
78 \ P(b); \ |
|
79 \ !!x y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
|
80 \ |] ==> P({})"; |
|
81 by (rtac (Diff_cancel RS subst) 1); |
|
82 by (rtac (Fin_empty_induct_lemma RS mp) 1); |
|
83 by (REPEAT (ares_tac (subset_refl::prems) 1)); |
|
84 qed "Fin_empty_induct"; |