|
1 (* Title: HOL/WF_Rel |
|
2 ID: $Id$ |
|
3 Author: Konrad Slind |
|
4 Copyright 1996 TU Munich |
|
5 |
|
6 Derived wellfounded relations: inverse image, relational product, measure, ... |
|
7 *) |
|
8 |
|
9 open WF_Rel; |
|
10 |
|
11 |
|
12 (*---------------------------------------------------------------------------- |
|
13 * The inverse image into a wellfounded relation is wellfounded. |
|
14 *---------------------------------------------------------------------------*) |
|
15 |
|
16 goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))"; |
|
17 by (full_simp_tac (!simpset addsimps [inv_image_def, wf_eq_minimal]) 1); |
|
18 by (Step_tac 1); |
|
19 by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1); |
|
20 by (blast_tac (!claset delrules [allE]) 2); |
|
21 by (etac allE 1); |
|
22 by (mp_tac 1); |
|
23 by (Blast_tac 1); |
|
24 qed "wf_inv_image"; |
|
25 AddSIs [wf_inv_image]; |
|
26 |
|
27 (*---------------------------------------------------------------------------- |
|
28 * All measures are wellfounded. |
|
29 *---------------------------------------------------------------------------*) |
|
30 |
|
31 goalw thy [measure_def] "wf (measure f)"; |
|
32 by (rtac wf_inv_image 1); |
|
33 by (rtac wf_trancl 1); |
|
34 by (rtac wf_pred_nat 1); |
|
35 qed "wf_measure"; |
|
36 AddIffs [wf_measure]; |
|
37 |
|
38 (*---------------------------------------------------------------------------- |
|
39 * Wellfoundedness of lexicographic combinations |
|
40 *---------------------------------------------------------------------------*) |
|
41 |
|
42 goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)"; |
|
43 by (rtac allI 1); |
|
44 by (rtac (surjective_pairing RS ssubst) 1); |
|
45 by (Blast_tac 1); |
|
46 qed "split_all_pair"; |
|
47 |
|
48 val [wfa,wfb] = goalw thy [wf_def,lex_prod_def] |
|
49 "[| wf(ra); wf(rb) |] ==> wf(ra**rb)"; |
|
50 by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); |
|
51 by (rtac (wfa RS spec RS mp) 1); |
|
52 by (EVERY1 [rtac allI,rtac impI]); |
|
53 by (rtac (wfb RS spec RS mp) 1); |
|
54 by (Blast_tac 1); |
|
55 qed "wf_lex_prod"; |
|
56 AddSIs [wf_lex_prod]; |
|
57 |
|
58 (*---------------------------------------------------------------------------- |
|
59 * Wellfoundedness of relational product |
|
60 *---------------------------------------------------------------------------*) |
|
61 val [wfa,wfb] = goalw thy [wf_def,rprod_def] |
|
62 "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)"; |
|
63 by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); |
|
64 by (rtac (wfa RS spec RS mp) 1); |
|
65 by (EVERY1 [rtac allI,rtac impI]); |
|
66 by (rtac (wfb RS spec RS mp) 1); |
|
67 by (Blast_tac 1); |
|
68 qed "wf_rel_prod"; |
|
69 AddSIs [wf_rel_prod]; |
|
70 |
|
71 |
|
72 (*--------------------------------------------------------------------------- |
|
73 * Wellfoundedness of subsets |
|
74 *---------------------------------------------------------------------------*) |
|
75 |
|
76 goal thy "!!r. [| wf(r); p<=r |] ==> wf(p)"; |
|
77 by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1); |
|
78 by (Fast_tac 1); |
|
79 qed "wf_subset"; |
|
80 |
|
81 (*--------------------------------------------------------------------------- |
|
82 * Wellfoundedness of the empty relation. |
|
83 *---------------------------------------------------------------------------*) |
|
84 |
|
85 goal thy "wf({})"; |
|
86 by (simp_tac (!simpset addsimps [wf_def]) 1); |
|
87 qed "wf_empty"; |
|
88 AddSIs [wf_empty]; |
|
89 |
|
90 |
|
91 (*--------------------------------------------------------------------------- |
|
92 * Transitivity of WF combinators. |
|
93 *---------------------------------------------------------------------------*) |
|
94 goalw thy [trans_def, lex_prod_def] |
|
95 "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)"; |
|
96 by (Simp_tac 1); |
|
97 by (Blast_tac 1); |
|
98 qed "trans_lex_prod"; |
|
99 AddSIs [trans_lex_prod]; |
|
100 |
|
101 goalw thy [trans_def, rprod_def] |
|
102 "!!R1 R2. [| trans R1; trans R2 |] ==> trans (rprod R1 R2)"; |
|
103 by (Simp_tac 1); |
|
104 by (Blast_tac 1); |
|
105 qed "trans_rprod"; |
|
106 AddSIs [trans_rprod]; |
|
107 |
|
108 |
|
109 (*--------------------------------------------------------------------------- |
|
110 * Wellfoundedness of proper subset on finite sets. |
|
111 *---------------------------------------------------------------------------*) |
|
112 goalw thy [finite_psubset_def] "wf(finite_psubset)"; |
|
113 by (rtac (wf_measure RS wf_subset) 1); |
|
114 by (simp_tac (!simpset addsimps[measure_def, inv_image_def, |
|
115 symmetric less_def])1); |
|
116 by (fast_tac (!claset addIs [psubset_card]) 1); |
|
117 qed "wf_finite_psubset"; |
|
118 |
|
119 |