author | paulson |
Thu, 15 May 1997 14:28:32 +0200 | |
changeset 3198 | 295287618e30 |
parent 2935 | 998cb95fdd43 |
child 3320 | 3a5e4930fb77 |
permissions | -rw-r--r-- |
1475 | 1 |
(* Title: HOL/wf.ML |
923 | 2 |
ID: $Id$ |
1475 | 3 |
Author: Tobias Nipkow, with minor changes by Konrad Slind |
4 |
Copyright 1992 University of Cambridge/1995 TU Munich |
|
923 | 5 |
|
3198 | 6 |
Wellfoundedness, induction, and recursion |
923 | 7 |
*) |
8 |
||
9 |
open WF; |
|
10 |
||
950 | 11 |
val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); |
923 | 12 |
val H_cong1 = refl RS H_cong; |
13 |
||
14 |
(*Restriction to domain A. If r is well-founded over A then wf(r)*) |
|
15 |
val [prem1,prem2] = goalw WF.thy [wf_def] |
|
1642 | 16 |
"[| r <= A Times A; \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
17 |
\ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ |
923 | 18 |
\ ==> wf(r)"; |
19 |
by (strip_tac 1); |
|
20 |
by (rtac allE 1); |
|
21 |
by (assume_tac 1); |
|
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1771
diff
changeset
|
22 |
by (best_tac (!claset addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); |
923 | 23 |
qed "wfI"; |
24 |
||
25 |
val major::prems = goalw WF.thy [wf_def] |
|
26 |
"[| wf(r); \ |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
27 |
\ !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \ |
923 | 28 |
\ |] ==> P(a)"; |
29 |
by (rtac (major RS spec RS mp RS spec) 1); |
|
2935 | 30 |
by (blast_tac (!claset addIs prems) 1); |
923 | 31 |
qed "wf_induct"; |
32 |
||
33 |
(*Perform induction on i, then prove the wf(r) subgoal using prems. *) |
|
34 |
fun wf_ind_tac a prems i = |
|
35 |
EVERY [res_inst_tac [("a",a)] wf_induct i, |
|
1465 | 36 |
rename_last_tac a ["1"] (i+1), |
37 |
ares_tac prems i]; |
|
923 | 38 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
39 |
val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P"; |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
40 |
by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1); |
2935 | 41 |
by (blast_tac (!claset addIs prems) 1); |
923 | 42 |
by (wf_ind_tac "a" prems 1); |
2935 | 43 |
by (Blast_tac 1); |
923 | 44 |
qed "wf_asym"; |
45 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
46 |
val prems = goal WF.thy "[| wf(r); (a,a): r |] ==> P"; |
923 | 47 |
by (rtac wf_asym 1); |
48 |
by (REPEAT (resolve_tac prems 1)); |
|
1618 | 49 |
qed "wf_irrefl"; |
923 | 50 |
|
1475 | 51 |
(*transitive closure of a wf relation is wf! *) |
923 | 52 |
val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; |
53 |
by (rewtac wf_def); |
|
54 |
by (strip_tac 1); |
|
55 |
(*must retain the universal formula for later use!*) |
|
56 |
by (rtac allE 1 THEN assume_tac 1); |
|
57 |
by (etac mp 1); |
|
58 |
by (res_inst_tac [("a","x")] (prem RS wf_induct) 1); |
|
59 |
by (rtac (impI RS allI) 1); |
|
60 |
by (etac tranclE 1); |
|
2935 | 61 |
by (Blast_tac 1); |
62 |
by (Blast_tac 1); |
|
923 | 63 |
qed "wf_trancl"; |
64 |
||
65 |
||
3198 | 66 |
(*---------------------------------------------------------------------------- |
67 |
* Minimal-element characterization of well-foundedness |
|
68 |
*---------------------------------------------------------------------------*) |
|
69 |
||
70 |
val wfr::_ = goalw WF.thy [wf_def] |
|
71 |
"wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)"; |
|
72 |
by (rtac (wfr RS spec RS mp RS spec) 1); |
|
73 |
by (Blast_tac 1); |
|
74 |
val lemma1 = result(); |
|
75 |
||
76 |
goalw WF.thy [wf_def] |
|
77 |
"!!r. (! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r"; |
|
78 |
by (strip_tac 1); |
|
79 |
by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1); |
|
80 |
by (Blast_tac 1); |
|
81 |
val lemma2 = result(); |
|
82 |
||
83 |
goal WF.thy "wf r = (! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q))"; |
|
84 |
by (blast_tac (!claset addSIs [lemma1, lemma2]) 1); |
|
85 |
qed "wf_eq_minimal"; |
|
86 |
||
87 |
||
923 | 88 |
(** cut **) |
89 |
||
90 |
(*This rewrite rule works upon formulae; thus it requires explicit use of |
|
91 |
H_cong to expose the equality*) |
|
92 |
goalw WF.thy [cut_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
93 |
"(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))"; |
1552 | 94 |
by (simp_tac (HOL_ss addsimps [expand_fun_eq] |
1475 | 95 |
setloop (split_tac [expand_if])) 1); |
96 |
qed "cuts_eq"; |
|
923 | 97 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
98 |
goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)"; |
1552 | 99 |
by (asm_simp_tac HOL_ss 1); |
923 | 100 |
qed "cut_apply"; |
101 |
||
102 |
(*** is_recfun ***) |
|
103 |
||
104 |
goalw WF.thy [is_recfun_def,cut_def] |
|
1475 | 105 |
"!!f. [| is_recfun r H a f; ~(b,a):r |] ==> f(b) = (@z.True)"; |
923 | 106 |
by (etac ssubst 1); |
1552 | 107 |
by (asm_simp_tac HOL_ss 1); |
923 | 108 |
qed "is_recfun_undef"; |
109 |
||
110 |
(*** NOTE! some simplifications need a different finish_tac!! ***) |
|
111 |
fun indhyp_tac hyps = |
|
112 |
(cut_facts_tac hyps THEN' |
|
113 |
DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
|
1465 | 114 |
eresolve_tac [transD, mp, allE])); |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2031
diff
changeset
|
115 |
val wf_super_ss = HOL_ss addSolver indhyp_tac; |
923 | 116 |
|
117 |
val prems = goalw WF.thy [is_recfun_def,cut_def] |
|
1475 | 118 |
"[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
119 |
\ (x,a):r --> (x,b):r --> f(x)=g(x)"; |
923 | 120 |
by (cut_facts_tac prems 1); |
121 |
by (etac wf_induct 1); |
|
122 |
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); |
|
123 |
by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1); |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset
|
124 |
qed_spec_mp "is_recfun_equal"; |
923 | 125 |
|
126 |
||
127 |
val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def] |
|
128 |
"[| wf(r); trans(r); \ |
|
1475 | 129 |
\ is_recfun r H a f; is_recfun r H b g; (b,a):r |] ==> \ |
923 | 130 |
\ cut f r b = g"; |
131 |
val gundef = recgb RS is_recfun_undef |
|
132 |
and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal))); |
|
133 |
by (cut_facts_tac prems 1); |
|
134 |
by (rtac ext 1); |
|
135 |
by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg] |
|
136 |
setloop (split_tac [expand_if])) 1); |
|
137 |
qed "is_recfun_cut"; |
|
138 |
||
139 |
(*** Main Existence Lemma -- Basic Properties of the_recfun ***) |
|
140 |
||
141 |
val prems = goalw WF.thy [the_recfun_def] |
|
1475 | 142 |
"is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)"; |
143 |
by (res_inst_tac [("P", "is_recfun r H a")] selectI 1); |
|
923 | 144 |
by (resolve_tac prems 1); |
145 |
qed "is_the_recfun"; |
|
146 |
||
147 |
val prems = goal WF.thy |
|
1475 | 148 |
"[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)"; |
149 |
by (cut_facts_tac prems 1); |
|
150 |
by (wf_ind_tac "a" prems 1); |
|
151 |
by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")] |
|
152 |
is_the_recfun 1); |
|
1552 | 153 |
by (rewtac is_recfun_def); |
2031 | 154 |
by (stac cuts_eq 1); |
1475 | 155 |
by (rtac allI 1); |
156 |
by (rtac impI 1); |
|
157 |
by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1); |
|
158 |
by (subgoal_tac |
|
159 |
"the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1); |
|
160 |
by (etac allE 2); |
|
161 |
by (dtac impE 2); |
|
162 |
by (atac 2); |
|
163 |
by (atac 3); |
|
164 |
by (atac 2); |
|
165 |
by (etac ssubst 1); |
|
166 |
by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); |
|
167 |
by (rtac allI 1); |
|
168 |
by (rtac impI 1); |
|
169 |
by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1); |
|
170 |
by (res_inst_tac [("f1","H"),("x","ya")](arg_cong RS fun_cong) 1); |
|
171 |
by (fold_tac [is_recfun_def]); |
|
172 |
by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1); |
|
923 | 173 |
qed "unfold_the_recfun"; |
174 |
||
1475 | 175 |
val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun; |
923 | 176 |
|
1475 | 177 |
(*--------------Old proof----------------------------------------------------- |
923 | 178 |
val prems = goal WF.thy |
1475 | 179 |
"[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)"; |
180 |
by (cut_facts_tac prems 1); |
|
181 |
by (wf_ind_tac "a" prems 1); |
|
182 |
by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1); |
|
183 |
by (rewrite_goals_tac [is_recfun_def, wftrec_def]); |
|
2031 | 184 |
by (stac cuts_eq 1); |
1475 | 185 |
(*Applying the substitution: must keep the quantified assumption!!*) |
186 |
by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac, |
|
187 |
etac (mp RS ssubst), atac]); |
|
188 |
by (fold_tac [is_recfun_def]); |
|
189 |
by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1); |
|
190 |
qed "unfold_the_recfun"; |
|
191 |
---------------------------------------------------------------------------*) |
|
923 | 192 |
|
193 |
(** Removal of the premise trans(r) **) |
|
1475 | 194 |
val th = rewrite_rule[is_recfun_def] |
195 |
(trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun))); |
|
923 | 196 |
|
197 |
goalw WF.thy [wfrec_def] |
|
1475 | 198 |
"!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; |
199 |
by (rtac H_cong 1); |
|
200 |
by (rtac refl 2); |
|
201 |
by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); |
|
202 |
by (rtac allI 1); |
|
203 |
by (rtac impI 1); |
|
204 |
by (simp_tac(HOL_ss addsimps [wfrec_def]) 1); |
|
205 |
by (res_inst_tac [("a1","a")] (th RS ssubst) 1); |
|
206 |
by (atac 1); |
|
207 |
by (forward_tac[wf_trancl] 1); |
|
208 |
by (forward_tac[r_into_trancl] 1); |
|
209 |
by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1); |
|
210 |
by (rtac H_cong 1); (*expose the equality of cuts*) |
|
211 |
by (rtac refl 2); |
|
212 |
by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); |
|
213 |
by (strip_tac 1); |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset
|
214 |
by (res_inst_tac [("r","r^+")] is_recfun_equal 1); |
1475 | 215 |
by (atac 1); |
216 |
by (rtac trans_trancl 1); |
|
217 |
by (rtac unfold_the_recfun 1); |
|
218 |
by (atac 1); |
|
219 |
by (rtac trans_trancl 1); |
|
220 |
by (rtac unfold_the_recfun 1); |
|
221 |
by (atac 1); |
|
222 |
by (rtac trans_trancl 1); |
|
223 |
by (rtac transD 1); |
|
224 |
by (rtac trans_trancl 1); |
|
225 |
by (forw_inst_tac [("a","ya")] r_into_trancl 1); |
|
226 |
by (atac 1); |
|
227 |
by (atac 1); |
|
228 |
by (forw_inst_tac [("a","ya")] r_into_trancl 1); |
|
229 |
by (atac 1); |
|
230 |
qed "wfrec"; |
|
231 |
||
232 |
(*--------------Old proof----------------------------------------------------- |
|
233 |
goalw WF.thy [wfrec_def] |
|
234 |
"!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; |
|
923 | 235 |
by (etac (wf_trancl RS wftrec RS ssubst) 1); |
236 |
by (rtac trans_trancl 1); |
|
237 |
by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*) |
|
1475 | 238 |
by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); |
923 | 239 |
qed "wfrec"; |
1475 | 240 |
---------------------------------------------------------------------------*) |
923 | 241 |
|
1475 | 242 |
(*--------------------------------------------------------------------------- |
243 |
* This form avoids giant explosions in proofs. NOTE USE OF == |
|
244 |
*---------------------------------------------------------------------------*) |
|
923 | 245 |
val rew::prems = goal WF.thy |
1475 | 246 |
"[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a"; |
923 | 247 |
by (rewtac rew); |
248 |
by (REPEAT (resolve_tac (prems@[wfrec]) 1)); |
|
249 |
qed "def_wfrec"; |
|
1475 | 250 |
|
3198 | 251 |
|
252 |
(**** TFL variants ****) |
|
253 |
||
254 |
goal WF.thy |
|
255 |
"!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))"; |
|
256 |
by (strip_tac 1); |
|
257 |
by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1); |
|
258 |
by (assume_tac 1); |
|
259 |
by (Blast_tac 1); |
|
260 |
qed"tfl_wf_induct"; |
|
261 |
||
262 |
goal WF.thy "!f R. (x,a):R --> (cut f R a)(x) = f(x)"; |
|
263 |
by (strip_tac 1); |
|
264 |
by (rtac cut_apply 1); |
|
265 |
by (assume_tac 1); |
|
266 |
qed"tfl_cut_apply"; |
|
267 |
||
268 |
goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)"; |
|
269 |
by (strip_tac 1); |
|
270 |
by (res_inst_tac [("r","R"), ("H","M"), |
|
271 |
("a","x"), ("f","f")] (eq_reflection RS def_wfrec) 1); |
|
272 |
by (assume_tac 1); |
|
273 |
by (assume_tac 1); |
|
274 |
qed "tfl_wfrec"; |
|
275 |