author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46993  7371429c527d 
child 58871  c399ae4b836f 
permissions  rwrr 
13165  1 
(* Title: ZF/WF.thy 
1478  2 
Author: Tobias Nipkow and Lawrence C Paulson 
435  3 
Copyright 1994 University of Cambridge 
0  4 

13165  5 
Derived first for transitive relations, and finally for arbitrary WF relations 
6 
via wf_trancl and trans_trancl. 

7 

8 
It is difficult to derive this general case directly, using r^+ instead of 

9 
r. In is_recfun, the two occurrences of the relation must have the same 

10 
form. Inserting r^+ in the_recfun or wftrec yields a recursion rule with 

11 
r^+ `` {a} instead of r``{a}. This recursion rule is stronger in 

12 
principle, but harder to use, especially to prove wfrec_eclose_eq in 

13 
epsilon.ML. Expanding out the definition of wftrec in wfrec would yield 

14 
a mess. 

0  15 
*) 
16 

13356  17 
header{*WellFounded Recursion*} 
18 

16417  19 
theory WF imports Trancl begin 
13165  20 

24893  21 
definition 
22 
wf :: "i=>o" where 

13165  23 
(*r is a wellfounded relation*) 
46953  24 
"wf(r) == \<forall>Z. Z=0  (\<exists>x\<in>Z. \<forall>y. <y,x>:r \<longrightarrow> ~ y \<in> Z)" 
13165  25 

24893  26 
definition 
27 
wf_on :: "[i,i]=>o" ("wf[_]'(_')") where 

13165  28 
(*r is wellfounded on A*) 
46820  29 
"wf_on(A,r) == wf(r \<inter> A*A)" 
13165  30 

24893  31 
definition 
32 
is_recfun :: "[i, i, [i,i]=>i, i] =>o" where 

46820  33 
"is_recfun(r,a,H,f) == (f = (\<lambda>x\<in>r``{a}. H(x, restrict(f, r``{x}))))" 
13165  34 

24893  35 
definition 
36 
the_recfun :: "[i, i, [i,i]=>i] =>i" where 

13165  37 
"the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))" 
38 

24893  39 
definition 
40 
wftrec :: "[i, i, [i,i]=>i] =>i" where 

13165  41 
"wftrec(r,a,H) == H(a, the_recfun(r,a,H))" 
42 

24893  43 
definition 
44 
wfrec :: "[i, i, [i,i]=>i] =>i" where 

13165  45 
(*public version. Does not require r to be transitive*) 
46 
"wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r``{x})))" 

47 

24893  48 
definition 
49 
wfrec_on :: "[i, i, i, [i,i]=>i] =>i" ("wfrec[_]'(_,_,_')") where 

46820  50 
"wfrec[A](r,a,H) == wfrec(r \<inter> A*A, a, H)" 
13165  51 

52 

13356  53 
subsection{*WellFounded Relations*} 
13165  54 

13634  55 
subsubsection{*Equivalences between @{term wf} and @{term wf_on}*} 
13165  56 

57 
lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)" 

46820  58 
by (unfold wf_def wf_on_def, force) 
13165  59 

46993  60 
lemma wf_on_imp_wf: "[wf[A](r); r \<subseteq> A*A] ==> wf(r)" 
13248  61 
by (simp add: wf_on_def subset_Int_iff) 
62 

13165  63 
lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)" 
64 
by (unfold wf_def wf_on_def, fast) 

65 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

66 
lemma wf_iff_wf_on_field: "wf(r) \<longleftrightarrow> wf[field(r)](r)" 
13165  67 
by (blast intro: wf_imp_wf_on wf_on_field_imp_wf) 
68 

69 
lemma wf_on_subset_A: "[ wf[A](r); B<=A ] ==> wf[B](r)" 

70 
by (unfold wf_on_def wf_def, fast) 

71 

72 
lemma wf_on_subset_r: "[ wf[A](r); s<=r ] ==> wf[A](s)" 

73 
by (unfold wf_on_def wf_def, fast) 

74 

13217  75 
lemma wf_subset: "[wf(s); r<=s] ==> wf(r)" 
76 
by (simp add: wf_def, fast) 

77 

13634  78 
subsubsection{*Introduction Rules for @{term wf_on}*} 
13165  79 

13634  80 
text{*If every nonempty subset of @{term A} has an @{term r}minimal element 
81 
then we have @{term "wf[A](r)"}.*} 

13165  82 
lemma wf_onI: 
46953  83 
assumes prem: "!!Z u. [ Z<=A; u \<in> Z; \<forall>x\<in>Z. \<exists>y\<in>Z. <y,x>:r ] ==> False" 
13165  84 
shows "wf[A](r)" 
85 
apply (unfold wf_on_def wf_def) 

86 
apply (rule equals0I [THEN disjCI, THEN allI]) 

13784  87 
apply (rule_tac Z = Z in prem, blast+) 
13165  88 
done 
89 

13634  90 
text{*If @{term r} allows wellfounded induction over @{term A} 
91 
then we have @{term "wf[A](r)"}. Premise is equivalent to 

46953  92 
@{prop "!!B. \<forall>x\<in>A. (\<forall>y. <y,x>: r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B ==> A<=B"} *} 
13165  93 
lemma wf_onI2: 
46953  94 
assumes prem: "!!y B. [ \<forall>x\<in>A. (\<forall>y\<in>A. <y,x>:r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B; y \<in> A ] 
95 
==> y \<in> B" 

13165  96 
shows "wf[A](r)" 
97 
apply (rule wf_onI) 

98 
apply (rule_tac c=u in prem [THEN DiffE]) 

46820  99 
prefer 3 apply blast 
13165  100 
apply fast+ 
101 
done 

102 

103 

13634  104 
subsubsection{*Wellfounded Induction*} 
13165  105 

13634  106 
text{*Consider the least @{term z} in @{term "domain(r)"} such that 
107 
@{term "P(z)"} does not hold...*} 

46993  108 
lemma wf_induct_raw: 
13165  109 
"[ wf(r); 
46820  110 
!!x.[ \<forall>y. <y,x>: r \<longrightarrow> P(y) ] ==> P(x) ] 
13634  111 
==> P(a)" 
46820  112 
apply (unfold wf_def) 
113 
apply (erule_tac x = "{z \<in> domain(r). ~ P(z)}" in allE) 

114 
apply blast 

13165  115 
done 
435  116 

46993  117 
lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, induct set: wf] 
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13175
diff
changeset

118 

13634  119 
text{*The form of this rule is designed to match @{text wfI}*} 
13165  120 
lemma wf_induct2: 
46953  121 
"[ wf(r); a \<in> A; field(r)<=A; 
122 
!!x.[ x \<in> A; \<forall>y. <y,x>: r \<longrightarrow> P(y) ] ==> P(x) ] 

13165  123 
==> P(a)" 
46953  124 
apply (erule_tac P="a \<in> A" in rev_mp) 
46820  125 
apply (erule_tac a=a in wf_induct, blast) 
13165  126 
done 
127 

46820  128 
lemma field_Int_square: "field(r \<inter> A*A) \<subseteq> A" 
13165  129 
by blast 
130 

46993  131 
lemma wf_on_induct_raw [consumes 2, induct set: wf_on]: 
46953  132 
"[ wf[A](r); a \<in> A; 
133 
!!x.[ x \<in> A; \<forall>y\<in>A. <y,x>: r \<longrightarrow> P(y) ] ==> P(x) 

13165  134 
] ==> P(a)" 
46820  135 
apply (unfold wf_on_def) 
13165  136 
apply (erule wf_induct2, assumption) 
137 
apply (rule field_Int_square, blast) 

138 
done 

139 

46993  140 
lemmas wf_on_induct = 
141 
wf_on_induct_raw [rule_format, consumes 2, case_names step, induct set: wf_on] 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13175
diff
changeset

142 

fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13175
diff
changeset

143 

46820  144 
text{*If @{term r} allows wellfounded induction 
13634  145 
then we have @{term "wf(r)"}.*} 
13165  146 
lemma wfI: 
147 
"[ field(r)<=A; 

46953  148 
!!y B. [ \<forall>x\<in>A. (\<forall>y\<in>A. <y,x>:r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B; y \<in> A] 
149 
==> y \<in> B ] 

13165  150 
==> wf(r)" 
151 
apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf]) 

152 
apply (rule wf_onI2) 

46820  153 
prefer 2 apply blast 
154 
apply blast 

13165  155 
done 
156 

157 

13356  158 
subsection{*Basic Properties of WellFounded Relations*} 
13165  159 

46820  160 
lemma wf_not_refl: "wf(r) ==> <a,a> \<notin> r" 
13165  161 
by (erule_tac a=a in wf_induct, blast) 
162 

46820  163 
lemma wf_not_sym [rule_format]: "wf(r) ==> \<forall>x. <a,x>:r \<longrightarrow> <x,a> \<notin> r" 
13165  164 
by (erule_tac a=a in wf_induct, blast) 
165 

46820  166 
(* @{term"[ wf(r); <a,x> \<in> r; ~P ==> <x,a> \<in> r ] ==> P"} *) 
45602  167 
lemmas wf_asym = wf_not_sym [THEN swap] 
13165  168 

46953  169 
lemma wf_on_not_refl: "[ wf[A](r); a \<in> A ] ==> <a,a> \<notin> r" 
13269  170 
by (erule_tac a=a in wf_on_induct, assumption, blast) 
0  171 

13165  172 
lemma wf_on_not_sym [rule_format]: 
46953  173 
"[ wf[A](r); a \<in> A ] ==> \<forall>b\<in>A. <a,b>:r \<longrightarrow> <b,a>\<notin>r" 
13269  174 
apply (erule_tac a=a in wf_on_induct, assumption, blast) 
13165  175 
done 
176 

177 
lemma wf_on_asym: 

46820  178 
"[ wf[A](r); ~Z ==> <a,b> \<in> r; 
179 
<b,a> \<notin> r ==> Z; ~Z ==> a \<in> A; ~Z ==> b \<in> A ] ==> Z" 

180 
by (blast dest: wf_on_not_sym) 

13165  181 

182 

183 
(*Needed to prove well_ordI. Could also reason that wf[A](r) means 

46820  184 
wf(r \<inter> A*A); thus wf( (r \<inter> A*A)^+ ) and use wf_not_refl *) 
13165  185 
lemma wf_on_chain3: 
46953  186 
"[ wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a \<in> A; b \<in> A; c \<in> A ] ==> P" 
46820  187 
apply (subgoal_tac "\<forall>y\<in>A. \<forall>z\<in>A. <a,y>:r \<longrightarrow> <y,z>:r \<longrightarrow> <z,a>:r \<longrightarrow> P", 
188 
blast) 

13269  189 
apply (erule_tac a=a in wf_on_induct, assumption, blast) 
13165  190 
done 
191 

192 

193 

46820  194 
text{*transitive closure of a WF relation is WF provided 
13634  195 
@{term A} is downward closed*} 
13165  196 
lemma wf_on_trancl: 
46820  197 
"[ wf[A](r); r``A \<subseteq> A ] ==> wf[A](r^+)" 
13165  198 
apply (rule wf_onI2) 
199 
apply (frule bspec [THEN mp], assumption+) 

13784  200 
apply (erule_tac a = y in wf_on_induct, assumption) 
46820  201 
apply (blast elim: tranclE, blast) 
13165  202 
done 
203 

204 
lemma wf_trancl: "wf(r) ==> wf(r^+)" 

205 
apply (simp add: wf_iff_wf_on_field) 

46820  206 
apply (rule wf_on_subset_A) 
13165  207 
apply (erule wf_on_trancl) 
46820  208 
apply blast 
13165  209 
apply (rule trancl_type [THEN field_rel_subset]) 
210 
done 

211 

212 

13634  213 
text{*@{term "r``{a}"} is the set of everything under @{term a} in @{term r}*} 
13165  214 

45602  215 
lemmas underI = vimage_singleton_iff [THEN iffD2] 
216 
lemmas underD = vimage_singleton_iff [THEN iffD1] 

13165  217 

13634  218 

219 
subsection{*The Predicate @{term is_recfun}*} 

0  220 

46953  221 
lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f \<in> r``{a} > range(f)" 
13165  222 
apply (unfold is_recfun_def) 
223 
apply (erule ssubst) 

224 
apply (rule lamI [THEN rangeI, THEN lam_type], assumption) 

225 
done 

226 

13269  227 
lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function] 
228 

13165  229 
lemma apply_recfun: 
230 
"[ is_recfun(r,a,H,f); <x,a>:r ] ==> f`x = H(x, restrict(f,r``{x}))" 

46820  231 
apply (unfold is_recfun_def) 
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13165
diff
changeset

232 
txt{*replace f only on the lefthand side*} 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13165
diff
changeset

233 
apply (erule_tac P = "%x.?t(x) = ?u" in ssubst) 
46820  234 
apply (simp add: underI) 
13165  235 
done 
236 

237 
lemma is_recfun_equal [rule_format]: 

238 
"[ wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) ] 

46820  239 
==> <x,a>:r \<longrightarrow> <x,b>:r \<longrightarrow> f`x=g`x" 
13784  240 
apply (frule_tac f = f in is_recfun_type) 
241 
apply (frule_tac f = g in is_recfun_type) 

13165  242 
apply (simp add: is_recfun_def) 
243 
apply (erule_tac a=x in wf_induct) 

244 
apply (intro impI) 

245 
apply (elim ssubst) 

246 
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def) 

247 
apply (rule_tac t = "%z. H (?x,z) " in subst_context) 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

248 
apply (subgoal_tac "\<forall>y\<in>r``{x}. \<forall>z. <y,z>:f \<longleftrightarrow> <y,z>:g") 
13165  249 
apply (blast dest: transD) 
250 
apply (simp add: apply_iff) 

251 
apply (blast dest: transD intro: sym) 

252 
done 

253 

254 
lemma is_recfun_cut: 

255 
"[ wf(r); trans(r); 

256 
is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>:r ] 

257 
==> restrict(f, r``{b}) = g" 

13784  258 
apply (frule_tac f = f in is_recfun_type) 
13165  259 
apply (rule fun_extension) 
260 
apply (blast dest: transD intro: restrict_type2) 

261 
apply (erule is_recfun_type, simp) 

262 
apply (blast dest: transD intro: is_recfun_equal) 

263 
done 

264 

13356  265 
subsection{*Recursion: Main Existence Lemma*} 
435  266 

13165  267 
lemma is_recfun_functional: 
268 
"[ wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) ] ==> f=g" 

269 
by (blast intro: fun_extension is_recfun_type is_recfun_equal) 

270 

13248  271 
lemma the_recfun_eq: 
272 
"[ is_recfun(r,a,H,f); wf(r); trans(r) ] ==> the_recfun(r,a,H) = f" 

273 
apply (unfold the_recfun_def) 

274 
apply (blast intro: is_recfun_functional) 

275 
done 

276 

13165  277 
(*If some f satisfies is_recfun(r,a,H,) then so does the_recfun(r,a,H) *) 
278 
lemma is_the_recfun: 

279 
"[ is_recfun(r,a,H,f); wf(r); trans(r) ] 

280 
==> is_recfun(r, a, H, the_recfun(r,a,H))" 

13248  281 
by (simp add: the_recfun_eq) 
13165  282 

283 
lemma unfold_the_recfun: 

284 
"[ wf(r); trans(r) ] ==> is_recfun(r, a, H, the_recfun(r,a,H))" 

285 
apply (rule_tac a=a in wf_induct, assumption) 

46820  286 
apply (rename_tac a1) 
287 
apply (rule_tac f = "\<lambda>y\<in>r``{a1}. wftrec (r,y,H)" in is_the_recfun) 

13165  288 
apply typecheck 
289 
apply (unfold is_recfun_def wftrec_def) 

13634  290 
{*Applying the substitution: must keep the quantified assumption!*} 
46820  291 
apply (rule lam_cong [OF refl]) 
292 
apply (drule underD) 

13165  293 
apply (fold is_recfun_def) 
294 
apply (rule_tac t = "%z. H(?x,z)" in subst_context) 

295 
apply (rule fun_extension) 

296 
apply (blast intro: is_recfun_type) 

297 
apply (rule lam_type [THEN restrict_type2]) 

298 
apply blast 

299 
apply (blast dest: transD) 

46993  300 
apply atomize 
13165  301 
apply (frule spec [THEN mp], assumption) 
46820  302 
apply (subgoal_tac "<xa,a1> \<in> r") 
13784  303 
apply (drule_tac x1 = xa in spec [THEN mp], assumption) 
46820  304 
apply (simp add: vimage_singleton_iff 
13165  305 
apply_recfun is_recfun_cut) 
306 
apply (blast dest: transD) 

307 
done 

308 

309 

13356  310 
subsection{*Unfolding @{term "wftrec(r,a,H)"}*} 
13165  311 

312 
lemma the_recfun_cut: 

313 
"[ wf(r); trans(r); <b,a>:r ] 

314 
==> restrict(the_recfun(r,a,H), r``{b}) = the_recfun(r,b,H)" 

13269  315 
by (blast intro: is_recfun_cut unfold_the_recfun) 
0  316 

13165  317 
(*NOT SUITABLE FOR REWRITING: it is recursive!*) 
318 
lemma wftrec: 

319 
"[ wf(r); trans(r) ] ==> 

46820  320 
wftrec(r,a,H) = H(a, \<lambda>x\<in>r``{a}. wftrec(r,x,H))" 
13165  321 
apply (unfold wftrec_def) 
322 
apply (subst unfold_the_recfun [unfolded is_recfun_def]) 

323 
apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut) 

324 
done 

325 

13634  326 

327 
subsubsection{*Removal of the Premise @{term "trans(r)"}*} 

13165  328 

329 
(*NOT SUITABLE FOR REWRITING: it is recursive!*) 

330 
lemma wfrec: 

46820  331 
"wf(r) ==> wfrec(r,a,H) = H(a, \<lambda>x\<in>r``{a}. wfrec(r,x,H))" 
332 
apply (unfold wfrec_def) 

13165  333 
apply (erule wf_trancl [THEN wftrec, THEN ssubst]) 
334 
apply (rule trans_trancl) 

335 
apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context]) 

336 
apply (erule r_into_trancl) 

337 
apply (rule subset_refl) 

338 
done 

0  339 

13165  340 
(*This form avoids giant explosions in proofs. NOTE USE OF == *) 
341 
lemma def_wfrec: 

342 
"[ !!x. h(x)==wfrec(r,x,H); wf(r) ] ==> 

46820  343 
h(a) = H(a, \<lambda>x\<in>r``{a}. h(x))" 
13165  344 
apply simp 
46820  345 
apply (elim wfrec) 
13165  346 
done 
347 

348 
lemma wfrec_type: 

46953  349 
"[ wf(r); a \<in> A; field(r)<=A; 
350 
!!x u. [ x \<in> A; u \<in> Pi(r``{x}, B) ] ==> H(x,u) \<in> B(x) 

46820  351 
] ==> wfrec(r,a,H) \<in> B(a)" 
13784  352 
apply (rule_tac a = a in wf_induct2, assumption+) 
13165  353 
apply (subst wfrec, assumption) 
46820  354 
apply (simp add: lam_type underD) 
13165  355 
done 
356 

357 

358 
lemma wfrec_on: 

46953  359 
"[ wf[A](r); a \<in> A ] ==> 
46820  360 
wfrec[A](r,a,H) = H(a, \<lambda>x\<in>(r``{a}) \<inter> A. wfrec[A](r,x,H))" 
13165  361 
apply (unfold wf_on_def wfrec_on_def) 
362 
apply (erule wfrec [THEN trans]) 

363 
apply (simp add: vimage_Int_square cons_subset_iff) 

364 
done 

0  365 

13634  366 
text{*Minimalelement characterization of wellfoundedness*} 
13165  367 
lemma wf_eq_minimal: 
46953  368 
"wf(r) \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. <y,z>:r \<longrightarrow> y\<notin>Q))" 
13634  369 
by (unfold wf_def, blast) 
370 

0  371 
end 