author | wenzelm |
Mon, 24 Jul 2000 23:51:46 +0200 | |
changeset 9422 | 4b6bc2b347e5 |
parent 9163 | 4d624e34e19a |
child 9443 | 3c2fc90d4e8a |
permissions | -rw-r--r-- |
3193 | 1 |
(* Title: HOL/WF_Rel |
2 |
ID: $Id$ |
|
3 |
Author: Konrad Slind |
|
4 |
Copyright 1996 TU Munich |
|
5 |
||
3296 | 6 |
Derived WF relations: inverse image, lexicographic product, measure, ... |
3193 | 7 |
*) |
8 |
||
9 |
||
10 |
(*---------------------------------------------------------------------------- |
|
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
11 |
* "Less than" on the natural numbers |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
12 |
*---------------------------------------------------------------------------*) |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
13 |
|
5069 | 14 |
Goalw [less_than_def] "wf less_than"; |
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
15 |
by (rtac (wf_pred_nat RS wf_trancl) 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
16 |
qed "wf_less_than"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
17 |
AddIffs [wf_less_than]; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
18 |
|
5069 | 19 |
Goalw [less_than_def] "trans less_than"; |
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
20 |
by (rtac trans_trancl 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
21 |
qed "trans_less_than"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
22 |
AddIffs [trans_less_than]; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
23 |
|
5069 | 24 |
Goalw [less_than_def, less_def] "((x,y): less_than) = (x<y)"; |
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
25 |
by (Simp_tac 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
26 |
qed "less_than_iff"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
27 |
AddIffs [less_than_iff]; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
28 |
|
9163 | 29 |
Goal "(!!n. (ALL m. Suc m <= n --> P m) ==> P n) ==> P n"; |
8254 | 30 |
by (rtac (wf_less_than RS wf_induct) 1); |
8158 | 31 |
by (resolve_tac (premises()) 1); |
32 |
by Auto_tac; |
|
33 |
qed_spec_mp "full_nat_induct"; |
|
34 |
||
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
35 |
(*---------------------------------------------------------------------------- |
3193 | 36 |
* The inverse image into a wellfounded relation is wellfounded. |
37 |
*---------------------------------------------------------------------------*) |
|
38 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
39 |
Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; |
4089 | 40 |
by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1); |
3718 | 41 |
by (Clarify_tac 1); |
9163 | 42 |
by (subgoal_tac "EX (w::'b). w : {w. EX (x::'a). x: Q & (f x = w)}" 1); |
4089 | 43 |
by (blast_tac (claset() delrules [allE]) 2); |
3193 | 44 |
by (etac allE 1); |
45 |
by (mp_tac 1); |
|
46 |
by (Blast_tac 1); |
|
47 |
qed "wf_inv_image"; |
|
48 |
AddSIs [wf_inv_image]; |
|
49 |
||
5069 | 50 |
Goalw [trans_def,inv_image_def] |
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
51 |
"!!r. trans r ==> trans (inv_image r f)"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
52 |
by (Simp_tac 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
53 |
by (Blast_tac 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
54 |
qed "trans_inv_image"; |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
55 |
|
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
56 |
|
3193 | 57 |
(*---------------------------------------------------------------------------- |
58 |
* All measures are wellfounded. |
|
59 |
*---------------------------------------------------------------------------*) |
|
60 |
||
5069 | 61 |
Goalw [measure_def] "wf (measure f)"; |
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
62 |
by (rtac (wf_less_than RS wf_inv_image) 1); |
3193 | 63 |
qed "wf_measure"; |
64 |
AddIffs [wf_measure]; |
|
65 |
||
4643 | 66 |
val measure_induct = standard |
67 |
(asm_full_simplify (simpset() addsimps [measure_def,inv_image_def]) |
|
68 |
(wf_measure RS wf_induct)); |
|
9108 | 69 |
bind_thm ("measure_induct", measure_induct); |
4643 | 70 |
|
3193 | 71 |
(*---------------------------------------------------------------------------- |
72 |
* Wellfoundedness of lexicographic combinations |
|
73 |
*---------------------------------------------------------------------------*) |
|
74 |
||
9422 | 75 |
val [wfa,wfb] = goalw (the_context ()) [wf_def,lex_prod_def] |
8703 | 76 |
"[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"; |
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
77 |
by (EVERY1 [rtac allI,rtac impI]); |
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
78 |
by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1); |
3193 | 79 |
by (rtac (wfa RS spec RS mp) 1); |
80 |
by (EVERY1 [rtac allI,rtac impI]); |
|
81 |
by (rtac (wfb RS spec RS mp) 1); |
|
82 |
by (Blast_tac 1); |
|
83 |
qed "wf_lex_prod"; |
|
84 |
AddSIs [wf_lex_prod]; |
|
85 |
||
86 |
(*--------------------------------------------------------------------------- |
|
87 |
* Transitivity of WF combinators. |
|
88 |
*---------------------------------------------------------------------------*) |
|
5069 | 89 |
Goalw [trans_def, lex_prod_def] |
8703 | 90 |
"!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"; |
3193 | 91 |
by (Simp_tac 1); |
92 |
by (Blast_tac 1); |
|
93 |
qed "trans_lex_prod"; |
|
94 |
AddSIs [trans_lex_prod]; |
|
95 |
||
96 |
||
97 |
(*--------------------------------------------------------------------------- |
|
98 |
* Wellfoundedness of proper subset on finite sets. |
|
99 |
*---------------------------------------------------------------------------*) |
|
5069 | 100 |
Goalw [finite_psubset_def] "wf(finite_psubset)"; |
3193 | 101 |
by (rtac (wf_measure RS wf_subset) 1); |
4089 | 102 |
by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def, |
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
103 |
symmetric less_def])1); |
9076 | 104 |
by (fast_tac (claset() addSEs [psubset_card_mono]) 1); |
3193 | 105 |
qed "wf_finite_psubset"; |
106 |
||
5069 | 107 |
Goalw [finite_psubset_def, trans_def] "trans finite_psubset"; |
4089 | 108 |
by (simp_tac (simpset() addsimps [psubset_def]) 1); |
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
109 |
by (Blast_tac 1); |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset
|
110 |
qed "trans_finite_psubset"; |
3193 | 111 |
|
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
112 |
(*--------------------------------------------------------------------------- |
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
113 |
* Wellfoundedness of finite acyclic relations |
5144 | 114 |
* Cannot go into WF because it needs Finite. |
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
115 |
*---------------------------------------------------------------------------*) |
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
116 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
117 |
Goal "finite r ==> acyclic r --> wf r"; |
3457 | 118 |
by (etac finite_induct 1); |
119 |
by (Blast_tac 1); |
|
120 |
by (split_all_tac 1); |
|
121 |
by (Asm_full_simp_tac 1); |
|
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
122 |
qed_spec_mp "finite_acyclic_wf"; |
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
123 |
|
7031 | 124 |
Goal "[|finite r; acyclic r|] ==> wf (r^-1)"; |
125 |
by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1); |
|
126 |
by (etac (acyclic_converse RS iffD2) 1); |
|
127 |
qed "finite_acyclic_wf_converse"; |
|
4749 | 128 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
129 |
Goal "finite r ==> wf r = acyclic r"; |
4089 | 130 |
by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1); |
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
131 |
qed "wf_iff_acyclic_if_finite"; |
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
132 |
|
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
133 |
|
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
134 |
(*--------------------------------------------------------------------------- |
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
135 |
* A relation is wellfounded iff it has no infinite descending chain |
5144 | 136 |
* Cannot go into WF because it needs type nat. |
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
137 |
*---------------------------------------------------------------------------*) |
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
138 |
|
5069 | 139 |
Goalw [wf_eq_minimal RS eq_reflection] |
9163 | 140 |
"wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))"; |
3457 | 141 |
by (rtac iffI 1); |
142 |
by (rtac notI 1); |
|
143 |
by (etac exE 1); |
|
9163 | 144 |
by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1); |
3457 | 145 |
by (Blast_tac 1); |
146 |
by (etac swap 1); |
|
3446
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3436
diff
changeset
|
147 |
by (Asm_full_simp_tac 1); |
3718 | 148 |
by (Clarify_tac 1); |
9163 | 149 |
by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1); |
3436
d68dbb8f22d3
Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
nipkow
parents:
3413
diff
changeset
|
150 |
by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1); |
3457 | 151 |
by (rtac allI 1); |
152 |
by (Simp_tac 1); |
|
153 |
by (rtac selectI2EX 1); |
|
154 |
by (Blast_tac 1); |
|
155 |
by (Blast_tac 1); |
|
156 |
by (rtac allI 1); |
|
157 |
by (induct_tac "n" 1); |
|
158 |
by (Asm_simp_tac 1); |
|
159 |
by (Simp_tac 1); |
|
160 |
by (rtac selectI2EX 1); |
|
161 |
by (Blast_tac 1); |
|
162 |
by (Blast_tac 1); |
|
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset
|
163 |
qed "wf_iff_no_infinite_down_chain"; |
6803 | 164 |
|
165 |
(*---------------------------------------------------------------------------- |
|
166 |
* Weakly decreasing sequences (w.r.t. some well-founded order) stabilize. |
|
167 |
*---------------------------------------------------------------------------*) |
|
168 |
||
9163 | 169 |
Goal "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"; |
6803 | 170 |
by (induct_tac "k" 1); |
171 |
by (ALLGOALS Simp_tac); |
|
172 |
by (blast_tac (claset() addIs [rtrancl_trans]) 1); |
|
173 |
val lemma = result(); |
|
174 |
||
9163 | 175 |
Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \ |
176 |
\ ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"; |
|
6803 | 177 |
by (etac wf_induct 1); |
178 |
by (Clarify_tac 1); |
|
9163 | 179 |
by (case_tac "EX j. (f (m+j), f m) : r^+" 1); |
6803 | 180 |
by (Clarify_tac 1); |
9163 | 181 |
by (subgoal_tac "EX i. ALL k. f ((m+j)+i+k) = f ((m+j)+i)" 1); |
6803 | 182 |
by (Clarify_tac 1); |
183 |
by (res_inst_tac [("x","j+i")] exI 1); |
|
184 |
by (asm_full_simp_tac (simpset() addsimps add_ac) 1); |
|
185 |
by (Blast_tac 1); |
|
186 |
by (res_inst_tac [("x","0")] exI 1); |
|
187 |
by (Clarsimp_tac 1); |
|
188 |
by (dres_inst_tac [("i","m"), ("k","k")] lemma 1); |
|
9163 | 189 |
by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1); |
6803 | 190 |
val lemma = result(); |
191 |
||
9163 | 192 |
Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \ |
193 |
\ ==> EX i. ALL k. f (i+k) = f i"; |
|
6803 | 194 |
by (dres_inst_tac [("x","0")] (lemma RS spec) 1); |
195 |
by Auto_tac; |
|
196 |
qed "wf_weak_decr_stable"; |
|
197 |
||
198 |
(* special case: <= *) |
|
199 |
||
200 |
Goal "(m, n) : pred_nat^* = (m <= n)"; |
|
201 |
by (simp_tac (simpset() addsimps [less_eq, reflcl_trancl RS sym] |
|
202 |
delsimps [reflcl_trancl]) 1); |
|
203 |
by (arith_tac 1); |
|
204 |
qed "le_eq"; |
|
205 |
||
9163 | 206 |
Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"; |
6803 | 207 |
by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1); |
208 |
by (asm_simp_tac (simpset() addsimps [le_eq]) 1); |
|
209 |
by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1)); |
|
210 |
qed "weak_decr_stable"; |