author | paulson |
Thu, 11 Jul 2002 17:18:28 +0200 | |
changeset 13350 | 626b79677dfa |
parent 13348 | 374d05460db4 |
child 13352 | 3cd767f8d78b |
permissions | -rw-r--r-- |
13306 | 1 |
header {*Absoluteness for Well-Founded Relations and Well-Founded Recursion*} |
2 |
||
13242 | 3 |
theory WF_absolute = WFrec: |
13223 | 4 |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
5 |
subsection{*Every well-founded relation is a subset of some inverse image of |
13247 | 6 |
an ordinal*} |
7 |
||
8 |
lemma wf_rvimage_Ord: "Ord(i) \<Longrightarrow> wf(rvimage(A, f, Memrel(i)))" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
9 |
by (blast intro: wf_rvimage wf_Memrel) |
13247 | 10 |
|
11 |
||
12 |
constdefs |
|
13 |
wfrank :: "[i,i]=>i" |
|
14 |
"wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))" |
|
15 |
||
16 |
constdefs |
|
17 |
wftype :: "i=>i" |
|
18 |
"wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))" |
|
19 |
||
20 |
lemma wfrank: "wf(r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))" |
|
21 |
by (subst wfrank_def [THEN def_wfrec], simp_all) |
|
22 |
||
23 |
lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
24 |
apply (rule_tac a=a in wf_induct, assumption) |
13247 | 25 |
apply (subst wfrank, assumption) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
26 |
apply (rule Ord_succ [THEN Ord_UN], blast) |
13247 | 27 |
done |
28 |
||
29 |
lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
30 |
apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption) |
13247 | 31 |
apply (rule UN_I [THEN ltI]) |
32 |
apply (simp add: Ord_wfrank vimage_iff)+ |
|
33 |
done |
|
34 |
||
35 |
lemma Ord_wftype: "wf(r) ==> Ord(wftype(r))" |
|
36 |
by (simp add: wftype_def Ord_wfrank) |
|
37 |
||
38 |
lemma wftypeI: "\<lbrakk>wf(r); x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
39 |
apply (simp add: wftype_def) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
40 |
apply (blast intro: wfrank_lt [THEN ltD]) |
13247 | 41 |
done |
42 |
||
43 |
||
44 |
lemma wf_imp_subset_rvimage: |
|
45 |
"[|wf(r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
46 |
apply (rule_tac x="wftype(r)" in exI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
47 |
apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
48 |
apply (simp add: Ord_wftype, clarify) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
49 |
apply (frule subsetD, assumption, clarify) |
13247 | 50 |
apply (simp add: rvimage_iff wfrank_lt [THEN ltD]) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
51 |
apply (blast intro: wftypeI) |
13247 | 52 |
done |
53 |
||
54 |
theorem wf_iff_subset_rvimage: |
|
55 |
"relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r <= rvimage(A, f, Memrel(i)))" |
|
56 |
by (blast dest!: relation_field_times_field wf_imp_subset_rvimage |
|
57 |
intro: wf_rvimage_Ord [THEN wf_subset]) |
|
58 |
||
59 |
||
13223 | 60 |
subsection{*Transitive closure without fixedpoints*} |
61 |
||
62 |
constdefs |
|
63 |
rtrancl_alt :: "[i,i]=>i" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
64 |
"rtrancl_alt(A,r) == |
13223 | 65 |
{p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A. |
13242 | 66 |
(\<exists>x y. p = <x,y> & f`0 = x & f`n = y) & |
13223 | 67 |
(\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)}" |
68 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
69 |
lemma alt_rtrancl_lemma1 [rule_format]: |
13223 | 70 |
"n \<in> nat |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
71 |
==> \<forall>f \<in> succ(n) -> field(r). |
13223 | 72 |
(\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) --> \<langle>f`0, f`n\<rangle> \<in> r^*" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
73 |
apply (induct_tac n) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
74 |
apply (simp_all add: apply_funtype rtrancl_refl, clarify) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
75 |
apply (rename_tac n f) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
76 |
apply (rule rtrancl_into_rtrancl) |
13223 | 77 |
prefer 2 apply assumption |
78 |
apply (drule_tac x="restrict(f,succ(n))" in bspec) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
79 |
apply (blast intro: restrict_type2) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
80 |
apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) |
13223 | 81 |
done |
82 |
||
83 |
lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*" |
|
84 |
apply (simp add: rtrancl_alt_def) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
85 |
apply (blast intro: alt_rtrancl_lemma1) |
13223 | 86 |
done |
87 |
||
88 |
lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
89 |
apply (simp add: rtrancl_alt_def, clarify) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
90 |
apply (frule rtrancl_type [THEN subsetD], clarify, simp) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
91 |
apply (erule rtrancl_induct) |
13223 | 92 |
txt{*Base case, trivial*} |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
93 |
apply (rule_tac x=0 in bexI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
94 |
apply (rule_tac x="lam x:1. xa" in bexI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
95 |
apply simp_all |
13223 | 96 |
txt{*Inductive step*} |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
97 |
apply clarify |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
98 |
apply (rename_tac n f) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
99 |
apply (rule_tac x="succ(n)" in bexI) |
13223 | 100 |
apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
101 |
apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
102 |
apply (blast intro: mem_asym) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
103 |
apply typecheck |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
104 |
apply auto |
13223 | 105 |
done |
106 |
||
107 |
lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*" |
|
108 |
by (blast del: subsetI |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
109 |
intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt) |
13223 | 110 |
|
111 |
||
13242 | 112 |
constdefs |
113 |
||
13324 | 114 |
rtran_closure_mem :: "[i=>o,i,i,i] => o" |
115 |
--{*The property of belonging to @{text "rtran_closure(r)"}*} |
|
116 |
"rtran_closure_mem(M,A,r,p) == |
|
117 |
\<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. |
|
118 |
omega(M,nnat) & n\<in>nnat & successor(M,n,n') & |
|
119 |
(\<exists>f[M]. typed_function(M,n',A,f) & |
|
120 |
(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) & |
|
121 |
fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & |
|
122 |
(\<forall>j[M]. j\<in>n --> |
|
123 |
(\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. |
|
124 |
fun_apply(M,f,j,fj) & successor(M,j,sj) & |
|
125 |
fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))" |
|
126 |
||
13242 | 127 |
rtran_closure :: "[i=>o,i,i] => o" |
13324 | 128 |
"rtran_closure(M,r,s) == |
129 |
\<forall>A[M]. is_field(M,r,A) --> |
|
130 |
(\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" |
|
13242 | 131 |
|
132 |
tran_closure :: "[i=>o,i,i] => o" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
133 |
"tran_closure(M,r,t) == |
13268 | 134 |
\<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" |
13242 | 135 |
|
13324 | 136 |
lemma (in M_axioms) rtran_closure_mem_iff: |
137 |
"[|M(A); M(r); M(p)|] |
|
138 |
==> rtran_closure_mem(M,A,r,p) <-> |
|
139 |
(\<exists>n[M]. n\<in>nat & |
|
140 |
(\<exists>f[M]. f \<in> succ(n) -> A & |
|
141 |
(\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) & |
|
142 |
(\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))" |
|
143 |
apply (simp add: rtran_closure_mem_def typed_apply_abs |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
144 |
Ord_succ_mem_iff nat_0_le [THEN ltD], blast) |
13324 | 145 |
done |
13242 | 146 |
|
147 |
locale M_trancl = M_axioms + |
|
148 |
assumes rtrancl_separation: |
|
13324 | 149 |
"[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))" |
13242 | 150 |
and wellfounded_trancl_separation: |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13306
diff
changeset
|
151 |
"[| M(r); M(Z) |] ==> |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13306
diff
changeset
|
152 |
separation (M, \<lambda>x. |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13306
diff
changeset
|
153 |
\<exists>w[M]. \<exists>wx[M]. \<exists>rp[M]. |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13306
diff
changeset
|
154 |
w \<in> Z & pair(M,w,x,wx) & tran_closure(M,r,rp) & wx \<in> rp)" |
13242 | 155 |
|
156 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
157 |
lemma (in M_trancl) rtran_closure_rtrancl: |
13242 | 158 |
"M(r) ==> rtran_closure(M,r,rtrancl(r))" |
13324 | 159 |
apply (simp add: rtran_closure_def rtran_closure_mem_iff |
160 |
rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
161 |
apply (auto simp add: nat_0_le [THEN ltD] apply_funtype) |
13242 | 162 |
done |
163 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
164 |
lemma (in M_trancl) rtrancl_closed [intro,simp]: |
13242 | 165 |
"M(r) ==> M(rtrancl(r))" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
166 |
apply (insert rtrancl_separation [of r "field(r)"]) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
167 |
apply (simp add: rtrancl_alt_eq_rtrancl [symmetric] |
13324 | 168 |
rtrancl_alt_def rtran_closure_mem_iff) |
13242 | 169 |
done |
170 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
171 |
lemma (in M_trancl) rtrancl_abs [simp]: |
13242 | 172 |
"[| M(r); M(z) |] ==> rtran_closure(M,r,z) <-> z = rtrancl(r)" |
173 |
apply (rule iffI) |
|
174 |
txt{*Proving the right-to-left implication*} |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
175 |
prefer 2 apply (blast intro: rtran_closure_rtrancl) |
13242 | 176 |
apply (rule M_equalityI) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
177 |
apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] |
13324 | 178 |
rtrancl_alt_def rtran_closure_mem_iff) |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
179 |
apply (auto simp add: nat_0_le [THEN ltD] apply_funtype) |
13242 | 180 |
done |
181 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
182 |
lemma (in M_trancl) trancl_closed [intro,simp]: |
13242 | 183 |
"M(r) ==> M(trancl(r))" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
184 |
by (simp add: trancl_def comp_closed rtrancl_closed) |
13242 | 185 |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
186 |
lemma (in M_trancl) trancl_abs [simp]: |
13242 | 187 |
"[| M(r); M(z) |] ==> tran_closure(M,r,z) <-> z = trancl(r)" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
188 |
by (simp add: tran_closure_def trancl_def) |
13242 | 189 |
|
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13306
diff
changeset
|
190 |
lemma (in M_trancl) wellfounded_trancl_separation': |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13306
diff
changeset
|
191 |
"[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & <w,x> \<in> r^+)" |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13306
diff
changeset
|
192 |
by (insert wellfounded_trancl_separation [of r Z], simp) |
13242 | 193 |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
194 |
text{*Alternative proof of @{text wf_on_trancl}; inspiration for the |
13242 | 195 |
relativized version. Original version is on theory WF.*} |
196 |
lemma "[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
197 |
apply (simp add: wf_on_def wf_def) |
13242 | 198 |
apply (safe intro!: equalityI) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
199 |
apply (drule_tac x = "{x\<in>A. \<exists>w. \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
200 |
apply (blast elim: tranclE) |
13242 | 201 |
done |
202 |
||
203 |
lemma (in M_trancl) wellfounded_on_trancl: |
|
204 |
"[| wellfounded_on(M,A,r); r-``A <= A; M(r); M(A) |] |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
205 |
==> wellfounded_on(M,A,r^+)" |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
206 |
apply (simp add: wellfounded_on_def) |
13242 | 207 |
apply (safe intro!: equalityI) |
208 |
apply (rename_tac Z x) |
|
13268 | 209 |
apply (subgoal_tac "M({x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+})") |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
210 |
prefer 2 |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13306
diff
changeset
|
211 |
apply (blast intro: wellfounded_trancl_separation') |
13299 | 212 |
apply (drule_tac x = "{x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+}" in rspec, safe) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
213 |
apply (blast dest: transM, simp) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
214 |
apply (rename_tac y w) |
13242 | 215 |
apply (drule_tac x=w in bspec, assumption, clarify) |
216 |
apply (erule tranclE) |
|
217 |
apply (blast dest: transM) (*transM is needed to prove M(xa)*) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
218 |
apply blast |
13242 | 219 |
done |
220 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
221 |
lemma (in M_trancl) wellfounded_trancl: |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
222 |
"[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)" |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
223 |
apply (rotate_tac -1) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
224 |
apply (simp add: wellfounded_iff_wellfounded_on_field) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
225 |
apply (rule wellfounded_on_subset_A, erule wellfounded_on_trancl) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
226 |
apply blast |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
227 |
apply (simp_all add: trancl_type [THEN field_rel_subset]) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
228 |
done |
13242 | 229 |
|
13223 | 230 |
text{*Relativized to M: Every well-founded relation is a subset of some |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
231 |
inverse image of an ordinal. Key step is the construction (in M) of a |
13223 | 232 |
rank function.*} |
233 |
||
234 |
||
13268 | 235 |
locale M_wfrank = M_trancl + |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
236 |
assumes wfrank_separation: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
237 |
"M(r) ==> |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
238 |
separation (M, \<lambda>x. |
13348 | 239 |
\<forall>rplus[M]. tran_closure(M,r,rplus) --> |
240 |
~ (\<exists>f[M]. M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f)))" |
|
241 |
and wfrank_strong_replacement: |
|
13242 | 242 |
"M(r) ==> |
13348 | 243 |
strong_replacement(M, \<lambda>x z. |
244 |
\<forall>rplus[M]. tran_closure(M,r,rplus) --> |
|
245 |
(\<exists>y[M]. \<exists>f[M]. pair(M,x,y,z) & |
|
246 |
M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f) & |
|
247 |
is_range(M,f,y)))" |
|
13242 | 248 |
and Ord_wfrank_separation: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
249 |
"M(r) ==> |
13348 | 250 |
separation (M, \<lambda>x. |
251 |
\<forall>rplus[M]. tran_closure(M,r,rplus) --> |
|
252 |
~ (\<forall>f[M]. \<forall>rangef[M]. |
|
253 |
is_range(M,f,rangef) --> |
|
254 |
M_is_recfun(M, rplus, x, \<lambda>x f y. is_range(M,f,y), f) --> |
|
255 |
ordinal(M,rangef)))" |
|
256 |
||
257 |
text{*Proving that the relativized instances of Separation or Replacement |
|
258 |
agree with the "real" ones.*} |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
259 |
|
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
260 |
lemma (in M_wfrank) wfrank_separation': |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
261 |
"M(r) ==> |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
262 |
separation |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
263 |
(M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))" |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
264 |
apply (insert wfrank_separation [of r]) |
13350 | 265 |
apply (simp add: is_recfun_abs [of "%x. range"]) |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
266 |
done |
13223 | 267 |
|
13348 | 268 |
lemma (in M_wfrank) wfrank_strong_replacement': |
269 |
"M(r) ==> |
|
270 |
strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. |
|
271 |
pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & |
|
272 |
y = range(f))" |
|
273 |
apply (insert wfrank_strong_replacement [of r]) |
|
13350 | 274 |
apply (simp add: is_recfun_abs [of "%x. range"]) |
13348 | 275 |
done |
276 |
||
277 |
lemma (in M_wfrank) Ord_wfrank_separation': |
|
278 |
"M(r) ==> |
|
279 |
separation (M, \<lambda>x. |
|
280 |
~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) --> Ord(range(f))))" |
|
281 |
apply (insert Ord_wfrank_separation [of r]) |
|
13350 | 282 |
apply (simp add: is_recfun_abs [of "%x. range"]) |
13348 | 283 |
done |
284 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
285 |
text{*This function, defined using replacement, is a rank function for |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
286 |
well-founded relations within the class M.*} |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
287 |
constdefs |
13242 | 288 |
wellfoundedrank :: "[i=>o,i,i] => i" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
289 |
"wellfoundedrank(M,r,A) == |
13268 | 290 |
{p. x\<in>A, \<exists>y[M]. \<exists>f[M]. |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
291 |
p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) & |
13242 | 292 |
y = range(f)}" |
13223 | 293 |
|
13268 | 294 |
lemma (in M_wfrank) exists_wfrank: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
295 |
"[| wellfounded(M,r); M(a); M(r) |] |
13268 | 296 |
==> \<exists>f[M]. is_recfun(r^+, a, %x f. range(f), f)" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
297 |
apply (rule wellfounded_exists_is_recfun) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
298 |
apply (blast intro: wellfounded_trancl) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
299 |
apply (rule trans_trancl) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
300 |
apply (erule wfrank_separation') |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
301 |
apply (erule wfrank_strong_replacement') |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
302 |
apply (simp_all add: trancl_subset_times) |
13223 | 303 |
done |
304 |
||
13268 | 305 |
lemma (in M_wfrank) M_wellfoundedrank: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
306 |
"[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))" |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
307 |
apply (insert wfrank_strong_replacement' [of r]) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
308 |
apply (simp add: wellfoundedrank_def) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
309 |
apply (rule strong_replacement_closed) |
13242 | 310 |
apply assumption+ |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
311 |
apply (rule univalent_is_recfun) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
312 |
apply (blast intro: wellfounded_trancl) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
313 |
apply (rule trans_trancl) |
13254 | 314 |
apply (simp add: trancl_subset_times, blast) |
13223 | 315 |
done |
316 |
||
13268 | 317 |
lemma (in M_wfrank) Ord_wfrank_range [rule_format]: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
318 |
"[| wellfounded(M,r); a\<in>A; M(r); M(A) |] |
13348 | 319 |
==> \<forall>f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
320 |
apply (drule wellfounded_trancl, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
321 |
apply (rule wellfounded_induct, assumption+) |
13254 | 322 |
apply simp |
13348 | 323 |
apply (blast intro: Ord_wfrank_separation', clarify) |
13242 | 324 |
txt{*The reasoning in both cases is that we get @{term y} such that |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
325 |
@{term "\<langle>y, x\<rangle> \<in> r^+"}. We find that |
13242 | 326 |
@{term "f`y = restrict(f, r^+ -`` {y})"}. *} |
327 |
apply (rule OrdI [OF _ Ord_is_Transset]) |
|
328 |
txt{*An ordinal is a transitive set...*} |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
329 |
apply (simp add: Transset_def) |
13242 | 330 |
apply clarify |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
331 |
apply (frule apply_recfun2, assumption) |
13242 | 332 |
apply (force simp add: restrict_iff) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
333 |
txt{*...of ordinals. This second case requires the induction hyp.*} |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
334 |
apply clarify |
13242 | 335 |
apply (rename_tac i y) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
336 |
apply (frule apply_recfun2, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
337 |
apply (frule is_recfun_imp_in_r, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
338 |
apply (frule is_recfun_restrict) |
13242 | 339 |
(*simp_all won't work*) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
340 |
apply (simp add: trans_trancl trancl_subset_times)+ |
13242 | 341 |
apply (drule spec [THEN mp], assumption) |
342 |
apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))") |
|
13348 | 343 |
apply (drule_tac x="restrict(f, r^+ -`` {y})" in rspec) |
344 |
apply assumption |
|
13242 | 345 |
apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) |
346 |
apply (blast dest: pair_components_in_M) |
|
13223 | 347 |
done |
348 |
||
13268 | 349 |
lemma (in M_wfrank) Ord_range_wellfoundedrank: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
350 |
"[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A) |] |
13242 | 351 |
==> Ord (range(wellfoundedrank(M,r,A)))" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
352 |
apply (frule wellfounded_trancl, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
353 |
apply (frule trancl_subset_times) |
13242 | 354 |
apply (simp add: wellfoundedrank_def) |
355 |
apply (rule OrdI [OF _ Ord_is_Transset]) |
|
356 |
prefer 2 |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
357 |
txt{*by our previous result the range consists of ordinals.*} |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
358 |
apply (blast intro: Ord_wfrank_range) |
13242 | 359 |
txt{*We still must show that the range is a transitive set.*} |
13247 | 360 |
apply (simp add: Transset_def, clarify, simp) |
13293 | 361 |
apply (rename_tac x i f u) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
362 |
apply (frule is_recfun_imp_in_r, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
363 |
apply (subgoal_tac "M(u) & M(i) & M(x)") |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
364 |
prefer 2 apply (blast dest: transM, clarify) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
365 |
apply (rule_tac a=u in rangeI) |
13293 | 366 |
apply (rule_tac x=u in ReplaceI) |
367 |
apply simp |
|
368 |
apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI) |
|
369 |
apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2) |
|
370 |
apply simp |
|
371 |
apply blast |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
372 |
txt{*Unicity requirement of Replacement*} |
13242 | 373 |
apply clarify |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
374 |
apply (frule apply_recfun2, assumption) |
13293 | 375 |
apply (simp add: trans_trancl is_recfun_cut) |
13223 | 376 |
done |
377 |
||
13268 | 378 |
lemma (in M_wfrank) function_wellfoundedrank: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
379 |
"[| wellfounded(M,r); M(r); M(A)|] |
13242 | 380 |
==> function(wellfoundedrank(M,r,A))" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
381 |
apply (simp add: wellfoundedrank_def function_def, clarify) |
13242 | 382 |
txt{*Uniqueness: repeated below!*} |
383 |
apply (drule is_recfun_functional, assumption) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
384 |
apply (blast intro: wellfounded_trancl) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
385 |
apply (simp_all add: trancl_subset_times trans_trancl) |
13223 | 386 |
done |
387 |
||
13268 | 388 |
lemma (in M_wfrank) domain_wellfoundedrank: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
389 |
"[| wellfounded(M,r); M(r); M(A)|] |
13242 | 390 |
==> domain(wellfoundedrank(M,r,A)) = A" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
391 |
apply (simp add: wellfoundedrank_def function_def) |
13242 | 392 |
apply (rule equalityI, auto) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
393 |
apply (frule transM, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
394 |
apply (frule_tac a=x in exists_wfrank, assumption+, clarify) |
13293 | 395 |
apply (rule_tac b="range(f)" in domainI) |
396 |
apply (rule_tac x=x in ReplaceI) |
|
397 |
apply simp |
|
13268 | 398 |
apply (rule_tac x=f in rexI, blast, simp_all) |
13242 | 399 |
txt{*Uniqueness (for Replacement): repeated above!*} |
400 |
apply clarify |
|
401 |
apply (drule is_recfun_functional, assumption) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
402 |
apply (blast intro: wellfounded_trancl) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
403 |
apply (simp_all add: trancl_subset_times trans_trancl) |
13223 | 404 |
done |
405 |
||
13268 | 406 |
lemma (in M_wfrank) wellfoundedrank_type: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
407 |
"[| wellfounded(M,r); M(r); M(A)|] |
13242 | 408 |
==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
409 |
apply (frule function_wellfoundedrank [of r A], assumption+) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
410 |
apply (frule function_imp_Pi) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
411 |
apply (simp add: wellfoundedrank_def relation_def) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
412 |
apply blast |
13242 | 413 |
apply (simp add: domain_wellfoundedrank) |
13223 | 414 |
done |
415 |
||
13268 | 416 |
lemma (in M_wfrank) Ord_wellfoundedrank: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
417 |
"[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A; M(r); M(A) |] |
13242 | 418 |
==> Ord(wellfoundedrank(M,r,A) ` a)" |
419 |
by (blast intro: apply_funtype [OF wellfoundedrank_type] |
|
420 |
Ord_in_Ord [OF Ord_range_wellfoundedrank]) |
|
13223 | 421 |
|
13268 | 422 |
lemma (in M_wfrank) wellfoundedrank_eq: |
13242 | 423 |
"[| is_recfun(r^+, a, %x. range, f); |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
424 |
wellfounded(M,r); a \<in> A; M(f); M(r); M(A)|] |
13242 | 425 |
==> wellfoundedrank(M,r,A) ` a = range(f)" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
426 |
apply (rule apply_equality) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
427 |
prefer 2 apply (blast intro: wellfoundedrank_type) |
13242 | 428 |
apply (simp add: wellfoundedrank_def) |
429 |
apply (rule ReplaceI) |
|
13268 | 430 |
apply (rule_tac x="range(f)" in rexI) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
431 |
apply blast |
13268 | 432 |
apply simp_all |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
433 |
txt{*Unicity requirement of Replacement*} |
13242 | 434 |
apply clarify |
435 |
apply (drule is_recfun_functional, assumption) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
436 |
apply (blast intro: wellfounded_trancl) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
437 |
apply (simp_all add: trancl_subset_times trans_trancl) |
13223 | 438 |
done |
439 |
||
13247 | 440 |
|
13268 | 441 |
lemma (in M_wfrank) wellfoundedrank_lt: |
13247 | 442 |
"[| <a,b> \<in> r; |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
443 |
wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|] |
13247 | 444 |
==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
445 |
apply (frule wellfounded_trancl, assumption) |
13247 | 446 |
apply (subgoal_tac "a\<in>A & b\<in>A") |
447 |
prefer 2 apply blast |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
448 |
apply (simp add: lt_def Ord_wellfoundedrank, clarify) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
449 |
apply (frule exists_wfrank [of concl: _ b], assumption+, clarify) |
13247 | 450 |
apply (rename_tac fb) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
451 |
apply (frule is_recfun_restrict [of concl: "r^+" a]) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
452 |
apply (rule trans_trancl, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
453 |
apply (simp_all add: r_into_trancl trancl_subset_times) |
13247 | 454 |
txt{*Still the same goal, but with new @{text is_recfun} assumptions.*} |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
455 |
apply (simp add: wellfoundedrank_eq) |
13247 | 456 |
apply (frule_tac a=a in wellfoundedrank_eq, assumption+) |
457 |
apply (simp_all add: transM [of a]) |
|
458 |
txt{*We have used equations for wellfoundedrank and now must use some |
|
459 |
for @{text is_recfun}. *} |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
460 |
apply (rule_tac a=a in rangeI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
461 |
apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
462 |
r_into_trancl apply_recfun r_into_trancl) |
13247 | 463 |
done |
464 |
||
465 |
||
13268 | 466 |
lemma (in M_wfrank) wellfounded_imp_subset_rvimage: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
467 |
"[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|] |
13247 | 468 |
==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))" |
469 |
apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI) |
|
470 |
apply (rule_tac x="wellfoundedrank(M,r,A)" in exI) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
471 |
apply (simp add: Ord_range_wellfoundedrank, clarify) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
472 |
apply (frule subsetD, assumption, clarify) |
13247 | 473 |
apply (simp add: rvimage_iff wellfoundedrank_lt [THEN ltD]) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
474 |
apply (blast intro: apply_rangeI wellfoundedrank_type) |
13247 | 475 |
done |
476 |
||
13268 | 477 |
lemma (in M_wfrank) wellfounded_imp_wf: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
478 |
"[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)" |
13247 | 479 |
by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage |
480 |
intro: wf_rvimage_Ord [THEN wf_subset]) |
|
481 |
||
13268 | 482 |
lemma (in M_wfrank) wellfounded_on_imp_wf_on: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
483 |
"[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)" |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
484 |
apply (simp add: wellfounded_on_iff_wellfounded wf_on_def) |
13247 | 485 |
apply (rule wellfounded_imp_wf) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
486 |
apply (simp_all add: relation_def) |
13247 | 487 |
done |
488 |
||
489 |
||
13268 | 490 |
theorem (in M_wfrank) wf_abs [simp]: |
13247 | 491 |
"[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
492 |
by (blast intro: wellfounded_imp_wf wf_imp_relativized) |
13247 | 493 |
|
13268 | 494 |
theorem (in M_wfrank) wf_on_abs [simp]: |
13247 | 495 |
"[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
496 |
by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized) |
13247 | 497 |
|
13254 | 498 |
|
499 |
text{*absoluteness for wfrec-defined functions.*} |
|
500 |
||
501 |
(*first use is_recfun, then M_is_recfun*) |
|
502 |
||
503 |
lemma (in M_trancl) wfrec_relativize: |
|
504 |
"[|wf(r); M(a); M(r); |
|
13268 | 505 |
strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M]. |
13254 | 506 |
pair(M,x,y,z) & |
507 |
is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & |
|
508 |
y = H(x, restrict(g, r -`` {x}))); |
|
509 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] |
|
510 |
==> wfrec(r,a,H) = z <-> |
|
13268 | 511 |
(\<exists>f[M]. is_recfun(r^+, a, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & |
13254 | 512 |
z = H(a,restrict(f,r-``{a})))" |
513 |
apply (frule wf_trancl) |
|
514 |
apply (simp add: wftrec_def wfrec_def, safe) |
|
515 |
apply (frule wf_exists_is_recfun |
|
516 |
[of concl: "r^+" a "\<lambda>x f. H(x, restrict(f, r -`` {x}))"]) |
|
517 |
apply (simp_all add: trans_trancl function_restrictI trancl_subset_times) |
|
13268 | 518 |
apply (clarify, rule_tac x=x in rexI) |
13254 | 519 |
apply (simp_all add: the_recfun_eq trans_trancl trancl_subset_times) |
520 |
done |
|
521 |
||
522 |
||
523 |
text{*Assuming @{term r} is transitive simplifies the occurrences of @{text H}. |
|
524 |
The premise @{term "relation(r)"} is necessary |
|
525 |
before we can replace @{term "r^+"} by @{term r}. *} |
|
526 |
theorem (in M_trancl) trans_wfrec_relativize: |
|
527 |
"[|wf(r); trans(r); relation(r); M(r); M(a); |
|
13293 | 528 |
strong_replacement(M, \<lambda>x z. \<exists>y[M]. |
529 |
pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))); |
|
13254 | 530 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] |
13268 | 531 |
==> wfrec(r,a,H) = z <-> (\<exists>f[M]. is_recfun(r,a,H,f) & z = H(a,f))" |
13254 | 532 |
by (simp cong: is_recfun_cong |
533 |
add: wfrec_relativize trancl_eq_r |
|
534 |
is_recfun_restrict_idem domain_restrict_idem) |
|
535 |
||
536 |
||
537 |
lemma (in M_trancl) trans_eq_pair_wfrec_iff: |
|
538 |
"[|wf(r); trans(r); relation(r); M(r); M(y); |
|
13293 | 539 |
strong_replacement(M, \<lambda>x z. \<exists>y[M]. |
540 |
pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))); |
|
13254 | 541 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] |
542 |
==> y = <x, wfrec(r, x, H)> <-> |
|
13268 | 543 |
(\<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)" |
13293 | 544 |
apply safe |
545 |
apply (simp add: trans_wfrec_relativize [THEN iff_sym, of concl: _ x]) |
|
13254 | 546 |
txt{*converse direction*} |
547 |
apply (rule sym) |
|
548 |
apply (simp add: trans_wfrec_relativize, blast) |
|
549 |
done |
|
550 |
||
551 |
||
552 |
subsection{*M is closed under well-founded recursion*} |
|
553 |
||
554 |
text{*Lemma with the awkward premise mentioning @{text wfrec}.*} |
|
13268 | 555 |
lemma (in M_wfrank) wfrec_closed_lemma [rule_format]: |
13254 | 556 |
"[|wf(r); M(r); |
557 |
strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>); |
|
558 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] |
|
559 |
==> M(a) --> M(wfrec(r,a,H))" |
|
560 |
apply (rule_tac a=a in wf_induct, assumption+) |
|
561 |
apply (subst wfrec, assumption, clarify) |
|
562 |
apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" |
|
563 |
in rspec [THEN rspec]) |
|
564 |
apply (simp_all add: function_lam) |
|
565 |
apply (blast intro: dest: pair_components_in_M ) |
|
566 |
done |
|
567 |
||
568 |
text{*Eliminates one instance of replacement.*} |
|
13268 | 569 |
lemma (in M_wfrank) wfrec_replacement_iff: |
570 |
"strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M]. |
|
13254 | 571 |
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)) <-> |
572 |
strong_replacement(M, |
|
13268 | 573 |
\<lambda>x y. \<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)" |
13254 | 574 |
apply simp |
575 |
apply (rule strong_replacement_cong, blast) |
|
576 |
done |
|
577 |
||
578 |
text{*Useful version for transitive relations*} |
|
13268 | 579 |
theorem (in M_wfrank) trans_wfrec_closed: |
13254 | 580 |
"[|wf(r); trans(r); relation(r); M(r); M(a); |
581 |
strong_replacement(M, |
|
13268 | 582 |
\<lambda>x z. \<exists>y[M]. \<exists>g[M]. |
13254 | 583 |
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); |
584 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] |
|
585 |
==> M(wfrec(r,a,H))" |
|
586 |
apply (frule wfrec_replacement_iff [THEN iffD1]) |
|
587 |
apply (rule wfrec_closed_lemma, assumption+) |
|
588 |
apply (simp_all add: wfrec_replacement_iff trans_eq_pair_wfrec_iff) |
|
589 |
done |
|
590 |
||
591 |
section{*Absoluteness without assuming transitivity*} |
|
592 |
lemma (in M_trancl) eq_pair_wfrec_iff: |
|
593 |
"[|wf(r); M(r); M(y); |
|
13268 | 594 |
strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M]. |
13254 | 595 |
pair(M,x,y,z) & |
596 |
is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & |
|
597 |
y = H(x, restrict(g, r -`` {x}))); |
|
598 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] |
|
599 |
==> y = <x, wfrec(r, x, H)> <-> |
|
13268 | 600 |
(\<exists>f[M]. is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & |
13254 | 601 |
y = <x, H(x,restrict(f,r-``{x}))>)" |
602 |
apply safe |
|
13293 | 603 |
apply (simp add: wfrec_relativize [THEN iff_sym, of concl: _ x]) |
13254 | 604 |
txt{*converse direction*} |
605 |
apply (rule sym) |
|
606 |
apply (simp add: wfrec_relativize, blast) |
|
607 |
done |
|
608 |
||
13268 | 609 |
lemma (in M_wfrank) wfrec_closed_lemma [rule_format]: |
13254 | 610 |
"[|wf(r); M(r); |
611 |
strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>); |
|
612 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] |
|
613 |
==> M(a) --> M(wfrec(r,a,H))" |
|
614 |
apply (rule_tac a=a in wf_induct, assumption+) |
|
615 |
apply (subst wfrec, assumption, clarify) |
|
616 |
apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" |
|
617 |
in rspec [THEN rspec]) |
|
618 |
apply (simp_all add: function_lam) |
|
619 |
apply (blast intro: dest: pair_components_in_M ) |
|
620 |
done |
|
621 |
||
622 |
text{*Full version not assuming transitivity, but maybe not very useful.*} |
|
13268 | 623 |
theorem (in M_wfrank) wfrec_closed: |
13254 | 624 |
"[|wf(r); M(r); M(a); |
13268 | 625 |
strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M]. |
13254 | 626 |
pair(M,x,y,z) & |
627 |
is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & |
|
628 |
y = H(x, restrict(g, r -`` {x}))); |
|
629 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] |
|
630 |
==> M(wfrec(r,a,H))" |
|
631 |
apply (frule wfrec_replacement_iff [THEN iffD1]) |
|
632 |
apply (rule wfrec_closed_lemma, assumption+) |
|
633 |
apply (simp_all add: eq_pair_wfrec_iff) |
|
634 |
done |
|
635 |
||
13223 | 636 |
end |