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