author | paulson |
Tue, 20 May 1997 11:40:28 +0200 | |
changeset 3237 | 4da86d44de33 |
parent 3193 | fafc7e815b70 |
child 3296 | 2ee6c397003d |
permissions | -rw-r--r-- |
3193 | 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 |
(*---------------------------------------------------------------------------- |
|
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
13 |
* "Less than" on the natural numbers |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
14 |
*---------------------------------------------------------------------------*) |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
15 |
|
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
16 |
goalw thy [less_than_def] "wf less_than"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
17 |
by (rtac (wf_pred_nat RS wf_trancl) 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
18 |
qed "wf_less_than"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
19 |
AddIffs [wf_less_than]; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
20 |
|
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
21 |
goalw thy [less_than_def] "trans less_than"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
22 |
by (rtac trans_trancl 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
23 |
qed "trans_less_than"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
24 |
AddIffs [trans_less_than]; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
25 |
|
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
26 |
goalw thy [less_than_def, less_def] "((x,y): less_than) = (x<y)"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
27 |
by (Simp_tac 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
28 |
qed "less_than_iff"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
29 |
AddIffs [less_than_iff]; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
30 |
|
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
31 |
(*---------------------------------------------------------------------------- |
3193 | 32 |
* The inverse image into a wellfounded relation is wellfounded. |
33 |
*---------------------------------------------------------------------------*) |
|
34 |
||
35 |
goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))"; |
|
36 |
by (full_simp_tac (!simpset addsimps [inv_image_def, wf_eq_minimal]) 1); |
|
37 |
by (Step_tac 1); |
|
38 |
by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1); |
|
39 |
by (blast_tac (!claset delrules [allE]) 2); |
|
40 |
by (etac allE 1); |
|
41 |
by (mp_tac 1); |
|
42 |
by (Blast_tac 1); |
|
43 |
qed "wf_inv_image"; |
|
44 |
AddSIs [wf_inv_image]; |
|
45 |
||
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
46 |
goalw thy [trans_def,inv_image_def] |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
47 |
"!!r. trans r ==> trans (inv_image r f)"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
48 |
by (Simp_tac 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
49 |
by (Blast_tac 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
50 |
qed "trans_inv_image"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
51 |
|
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
52 |
|
3193 | 53 |
(*---------------------------------------------------------------------------- |
54 |
* All measures are wellfounded. |
|
55 |
*---------------------------------------------------------------------------*) |
|
56 |
||
57 |
goalw thy [measure_def] "wf (measure f)"; |
|
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
58 |
by (rtac (wf_less_than RS wf_inv_image) 1); |
3193 | 59 |
qed "wf_measure"; |
60 |
AddIffs [wf_measure]; |
|
61 |
||
62 |
(*---------------------------------------------------------------------------- |
|
63 |
* Wellfoundedness of lexicographic combinations |
|
64 |
*---------------------------------------------------------------------------*) |
|
65 |
||
66 |
goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)"; |
|
67 |
by (rtac allI 1); |
|
68 |
by (rtac (surjective_pairing RS ssubst) 1); |
|
69 |
by (Blast_tac 1); |
|
70 |
qed "split_all_pair"; |
|
71 |
||
72 |
val [wfa,wfb] = goalw thy [wf_def,lex_prod_def] |
|
73 |
"[| wf(ra); wf(rb) |] ==> wf(ra**rb)"; |
|
74 |
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); |
|
75 |
by (rtac (wfa RS spec RS mp) 1); |
|
76 |
by (EVERY1 [rtac allI,rtac impI]); |
|
77 |
by (rtac (wfb RS spec RS mp) 1); |
|
78 |
by (Blast_tac 1); |
|
79 |
qed "wf_lex_prod"; |
|
80 |
AddSIs [wf_lex_prod]; |
|
81 |
||
82 |
(*---------------------------------------------------------------------------- |
|
83 |
* Wellfoundedness of relational product |
|
84 |
*---------------------------------------------------------------------------*) |
|
85 |
val [wfa,wfb] = goalw thy [wf_def,rprod_def] |
|
86 |
"[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)"; |
|
87 |
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); |
|
88 |
by (rtac (wfa RS spec RS mp) 1); |
|
89 |
by (EVERY1 [rtac allI,rtac impI]); |
|
90 |
by (rtac (wfb RS spec RS mp) 1); |
|
91 |
by (Blast_tac 1); |
|
92 |
qed "wf_rel_prod"; |
|
93 |
AddSIs [wf_rel_prod]; |
|
94 |
||
95 |
||
96 |
(*--------------------------------------------------------------------------- |
|
97 |
* Wellfoundedness of subsets |
|
98 |
*---------------------------------------------------------------------------*) |
|
99 |
||
100 |
goal thy "!!r. [| wf(r); p<=r |] ==> wf(p)"; |
|
101 |
by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1); |
|
102 |
by (Fast_tac 1); |
|
103 |
qed "wf_subset"; |
|
104 |
||
105 |
(*--------------------------------------------------------------------------- |
|
106 |
* Wellfoundedness of the empty relation. |
|
107 |
*---------------------------------------------------------------------------*) |
|
108 |
||
109 |
goal thy "wf({})"; |
|
110 |
by (simp_tac (!simpset addsimps [wf_def]) 1); |
|
111 |
qed "wf_empty"; |
|
112 |
AddSIs [wf_empty]; |
|
113 |
||
114 |
||
115 |
(*--------------------------------------------------------------------------- |
|
116 |
* Transitivity of WF combinators. |
|
117 |
*---------------------------------------------------------------------------*) |
|
118 |
goalw thy [trans_def, lex_prod_def] |
|
119 |
"!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)"; |
|
120 |
by (Simp_tac 1); |
|
121 |
by (Blast_tac 1); |
|
122 |
qed "trans_lex_prod"; |
|
123 |
AddSIs [trans_lex_prod]; |
|
124 |
||
125 |
goalw thy [trans_def, rprod_def] |
|
126 |
"!!R1 R2. [| trans R1; trans R2 |] ==> trans (rprod R1 R2)"; |
|
127 |
by (Simp_tac 1); |
|
128 |
by (Blast_tac 1); |
|
129 |
qed "trans_rprod"; |
|
130 |
AddSIs [trans_rprod]; |
|
131 |
||
132 |
||
133 |
(*--------------------------------------------------------------------------- |
|
134 |
* Wellfoundedness of proper subset on finite sets. |
|
135 |
*---------------------------------------------------------------------------*) |
|
136 |
goalw thy [finite_psubset_def] "wf(finite_psubset)"; |
|
137 |
by (rtac (wf_measure RS wf_subset) 1); |
|
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
138 |
by (simp_tac (!simpset addsimps [measure_def, inv_image_def, less_than_def, |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
139 |
symmetric less_def])1); |
3193 | 140 |
by (fast_tac (!claset addIs [psubset_card]) 1); |
141 |
qed "wf_finite_psubset"; |
|
142 |
||
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
143 |
goalw thy [finite_psubset_def, trans_def] "trans finite_psubset"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
144 |
by (simp_tac (!simpset addsimps [psubset_def]) 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
145 |
by (Blast_tac 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
146 |
qed "trans_finite_psubset"; |
3193 | 147 |