author | paulson |
Wed, 26 Jun 2002 18:31:20 +0200 | |
changeset 13251 | 74cb2af8811e |
parent 13247 | e3c289f0724b |
child 13254 | 5146ccaedf42 |
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) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
306 |
apply (simp add: trancl_subset_times) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
307 |
apply blast |
13223 | 308 |
done |
309 |
||
13242 | 310 |
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
|
311 |
"[| wellfounded(M,r); a\<in>A; M(r); M(A) |] |
13242 | 312 |
==> \<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
|
313 |
apply (drule wellfounded_trancl, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
314 |
apply (rule wellfounded_induct, assumption+) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
315 |
apply (simp add:); |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
316 |
apply (blast intro: Ord_wfrank_separation); |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
317 |
apply (clarify) |
13242 | 318 |
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
|
319 |
@{term "\<langle>y, x\<rangle> \<in> r^+"}. We find that |
13242 | 320 |
@{term "f`y = restrict(f, r^+ -`` {y})"}. *} |
321 |
apply (rule OrdI [OF _ Ord_is_Transset]) |
|
322 |
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
|
323 |
apply (simp add: Transset_def) |
13242 | 324 |
apply clarify |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
325 |
apply (frule apply_recfun2, assumption) |
13242 | 326 |
apply (force simp add: restrict_iff) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
327 |
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
|
328 |
apply clarify |
13242 | 329 |
apply (rename_tac i y) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
330 |
apply (frule apply_recfun2, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
331 |
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
|
332 |
apply (frule is_recfun_restrict) |
13242 | 333 |
(*simp_all won't work*) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
334 |
apply (simp add: trans_trancl trancl_subset_times)+ |
13242 | 335 |
apply (drule spec [THEN mp], assumption) |
336 |
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
|
337 |
apply (drule_tac x="restrict(f, r^+ -`` {y})" in spec) |
13242 | 338 |
apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) |
339 |
apply (blast dest: pair_components_in_M) |
|
13223 | 340 |
done |
341 |
||
13242 | 342 |
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
|
343 |
"[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A) |] |
13242 | 344 |
==> Ord (range(wellfoundedrank(M,r,A)))" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
345 |
apply (frule wellfounded_trancl, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
346 |
apply (frule trancl_subset_times) |
13242 | 347 |
apply (simp add: wellfoundedrank_def) |
348 |
apply (rule OrdI [OF _ Ord_is_Transset]) |
|
349 |
prefer 2 |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
350 |
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
|
351 |
apply (blast intro: Ord_wfrank_range) |
13242 | 352 |
txt{*We still must show that the range is a transitive set.*} |
13247 | 353 |
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
|
354 |
apply (rename_tac x i f u) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
355 |
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
|
356 |
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
|
357 |
prefer 2 apply (blast dest: transM, clarify) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
358 |
apply (rule_tac a=u in rangeI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
359 |
apply (rule ReplaceI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
360 |
apply (rule_tac x=i in exI, simp) |
13242 | 361 |
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
|
362 |
apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2) |
13242 | 363 |
apply blast |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
364 |
txt{*Unicity requirement of Replacement*} |
13242 | 365 |
apply clarify |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
366 |
apply (frule apply_recfun2, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
367 |
apply (simp add: trans_trancl is_recfun_cut)+ |
13223 | 368 |
done |
369 |
||
13242 | 370 |
lemma (in M_recursion) function_wellfoundedrank: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
371 |
"[| wellfounded(M,r); M(r); M(A)|] |
13242 | 372 |
==> function(wellfoundedrank(M,r,A))" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
373 |
apply (simp add: wellfoundedrank_def function_def, clarify) |
13242 | 374 |
txt{*Uniqueness: repeated below!*} |
375 |
apply (drule is_recfun_functional, assumption) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
376 |
apply (blast intro: wellfounded_trancl) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
377 |
apply (simp_all add: trancl_subset_times trans_trancl) |
13223 | 378 |
done |
379 |
||
13242 | 380 |
lemma (in M_recursion) domain_wellfoundedrank: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
381 |
"[| wellfounded(M,r); M(r); M(A)|] |
13242 | 382 |
==> domain(wellfoundedrank(M,r,A)) = A" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
383 |
apply (simp add: wellfoundedrank_def function_def) |
13242 | 384 |
apply (rule equalityI, auto) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
385 |
apply (frule transM, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
386 |
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
|
387 |
apply (rule domainI) |
13242 | 388 |
apply (rule ReplaceI) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
389 |
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
|
390 |
apply simp |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
391 |
apply (rule_tac x=f in exI, blast, assumption) |
13242 | 392 |
txt{*Uniqueness (for Replacement): repeated above!*} |
393 |
apply clarify |
|
394 |
apply (drule is_recfun_functional, assumption) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
395 |
apply (blast intro: wellfounded_trancl) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
396 |
apply (simp_all add: trancl_subset_times trans_trancl) |
13223 | 397 |
done |
398 |
||
13242 | 399 |
lemma (in M_recursion) wellfoundedrank_type: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
400 |
"[| wellfounded(M,r); M(r); M(A)|] |
13242 | 401 |
==> 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
|
402 |
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
|
403 |
apply (frule function_imp_Pi) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
404 |
apply (simp add: wellfoundedrank_def relation_def) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
405 |
apply blast |
13242 | 406 |
apply (simp add: domain_wellfoundedrank) |
13223 | 407 |
done |
408 |
||
13242 | 409 |
lemma (in M_recursion) Ord_wellfoundedrank: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
410 |
"[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A; M(r); M(A) |] |
13242 | 411 |
==> Ord(wellfoundedrank(M,r,A) ` a)" |
412 |
by (blast intro: apply_funtype [OF wellfoundedrank_type] |
|
413 |
Ord_in_Ord [OF Ord_range_wellfoundedrank]) |
|
13223 | 414 |
|
13242 | 415 |
lemma (in M_recursion) wellfoundedrank_eq: |
416 |
"[| 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
|
417 |
wellfounded(M,r); a \<in> A; M(f); M(r); M(A)|] |
13242 | 418 |
==> 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
|
419 |
apply (rule apply_equality) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
420 |
prefer 2 apply (blast intro: wellfoundedrank_type) |
13242 | 421 |
apply (simp add: wellfoundedrank_def) |
422 |
apply (rule ReplaceI) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
423 |
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
|
424 |
apply blast |
13242 | 425 |
apply assumption |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
426 |
txt{*Unicity requirement of Replacement*} |
13242 | 427 |
apply clarify |
428 |
apply (drule is_recfun_functional, assumption) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
429 |
apply (blast intro: wellfounded_trancl) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
430 |
apply (simp_all add: trancl_subset_times trans_trancl) |
13223 | 431 |
done |
432 |
||
13247 | 433 |
|
434 |
lemma (in M_recursion) wellfoundedrank_lt: |
|
435 |
"[| <a,b> \<in> r; |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
436 |
wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|] |
13247 | 437 |
==> 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
|
438 |
apply (frule wellfounded_trancl, assumption) |
13247 | 439 |
apply (subgoal_tac "a\<in>A & b\<in>A") |
440 |
prefer 2 apply blast |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
441 |
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
|
442 |
apply (frule exists_wfrank [of concl: _ b], assumption+, clarify) |
13247 | 443 |
apply (rename_tac fb) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
444 |
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
|
445 |
apply (rule trans_trancl, assumption) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
446 |
apply (simp_all add: r_into_trancl trancl_subset_times) |
13247 | 447 |
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
|
448 |
apply (simp add: wellfoundedrank_eq) |
13247 | 449 |
apply (frule_tac a=a in wellfoundedrank_eq, assumption+) |
450 |
apply (simp_all add: transM [of a]) |
|
451 |
txt{*We have used equations for wellfoundedrank and now must use some |
|
452 |
for @{text is_recfun}. *} |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
453 |
apply (rule_tac a=a in rangeI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
454 |
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
|
455 |
r_into_trancl apply_recfun r_into_trancl) |
13247 | 456 |
done |
457 |
||
458 |
||
459 |
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
|
460 |
"[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|] |
13247 | 461 |
==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))" |
462 |
apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI) |
|
463 |
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
|
464 |
apply (simp add: Ord_range_wellfoundedrank, clarify) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
465 |
apply (frule subsetD, assumption, clarify) |
13247 | 466 |
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
|
467 |
apply (blast intro: apply_rangeI wellfoundedrank_type) |
13247 | 468 |
done |
469 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
470 |
lemma (in M_recursion) wellfounded_imp_wf: |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
471 |
"[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)" |
13247 | 472 |
by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage |
473 |
intro: wf_rvimage_Ord [THEN wf_subset]) |
|
474 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
475 |
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
|
476 |
"[|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
|
477 |
apply (simp add: wellfounded_on_iff_wellfounded wf_on_def) |
13247 | 478 |
apply (rule wellfounded_imp_wf) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
479 |
apply (simp_all add: relation_def) |
13247 | 480 |
done |
481 |
||
482 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
483 |
theorem (in M_recursion) wf_abs [simp]: |
13247 | 484 |
"[|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
|
485 |
by (blast intro: wellfounded_imp_wf wf_imp_relativized) |
13247 | 486 |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
487 |
theorem (in M_recursion) wf_on_abs [simp]: |
13247 | 488 |
"[|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
|
489 |
by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized) |
13247 | 490 |
|
13223 | 491 |
end |