author | paulson |
Tue, 10 Sep 2002 16:51:31 +0200 | |
changeset 13564 | 1500a2e48d44 |
parent 13506 | acc18a5d2b1a |
child 13566 | 52a419210d5c |
permissions | -rw-r--r-- |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
1 |
(* Title: ZF/Constructible/Rec_Separation.thy |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
2 |
ID: $Id$ |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
4 |
Copyright 2002 University of Cambridge |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
5 |
*) |
13429 | 6 |
|
7 |
header {*Separation for Facts About Recursion*} |
|
13348 | 8 |
|
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13493
diff
changeset
|
9 |
theory Rec_Separation = Separation + Internalize: |
13348 | 10 |
|
11 |
text{*This theory proves all instances needed for locales @{text |
|
12 |
"M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*} |
|
13 |
||
13363 | 14 |
lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i" |
13428 | 15 |
by simp |
13363 | 16 |
|
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
17 |
|
13348 | 18 |
subsection{*The Locale @{text "M_trancl"}*} |
19 |
||
20 |
subsubsection{*Separation for Reflexive/Transitive Closure*} |
|
21 |
||
22 |
text{*First, The Defining Formula*} |
|
23 |
||
24 |
(* "rtran_closure_mem(M,A,r,p) == |
|
13428 | 25 |
\<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. |
13348 | 26 |
omega(M,nnat) & n\<in>nnat & successor(M,n,n') & |
27 |
(\<exists>f[M]. typed_function(M,n',A,f) & |
|
13428 | 28 |
(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) & |
29 |
fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & |
|
30 |
(\<forall>j[M]. j\<in>n --> |
|
31 |
(\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. |
|
32 |
fun_apply(M,f,j,fj) & successor(M,j,sj) & |
|
33 |
fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*) |
|
13348 | 34 |
constdefs rtran_closure_mem_fm :: "[i,i,i]=>i" |
13428 | 35 |
"rtran_closure_mem_fm(A,r,p) == |
13348 | 36 |
Exists(Exists(Exists( |
37 |
And(omega_fm(2), |
|
38 |
And(Member(1,2), |
|
39 |
And(succ_fm(1,0), |
|
40 |
Exists(And(typed_function_fm(1, A#+4, 0), |
|
13428 | 41 |
And(Exists(Exists(Exists( |
42 |
And(pair_fm(2,1,p#+7), |
|
43 |
And(empty_fm(0), |
|
44 |
And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))), |
|
45 |
Forall(Implies(Member(0,3), |
|
46 |
Exists(Exists(Exists(Exists( |
|
47 |
And(fun_apply_fm(5,4,3), |
|
48 |
And(succ_fm(4,2), |
|
49 |
And(fun_apply_fm(5,2,1), |
|
50 |
And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))" |
|
13348 | 51 |
|
52 |
||
53 |
lemma rtran_closure_mem_type [TC]: |
|
54 |
"[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula" |
|
13428 | 55 |
by (simp add: rtran_closure_mem_fm_def) |
13348 | 56 |
|
57 |
lemma arity_rtran_closure_mem_fm [simp]: |
|
13428 | 58 |
"[| x \<in> nat; y \<in> nat; z \<in> nat |] |
13348 | 59 |
==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" |
13428 | 60 |
by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac) |
13348 | 61 |
|
62 |
lemma sats_rtran_closure_mem_fm [simp]: |
|
63 |
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
13428 | 64 |
==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> |
13348 | 65 |
rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))" |
66 |
by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def) |
|
67 |
||
68 |
lemma rtran_closure_mem_iff_sats: |
|
13428 | 69 |
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
13348 | 70 |
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
71 |
==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)" |
|
72 |
by (simp add: sats_rtran_closure_mem_fm) |
|
73 |
||
74 |
theorem rtran_closure_mem_reflection: |
|
13428 | 75 |
"REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)), |
13348 | 76 |
\<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]" |
77 |
apply (simp only: rtran_closure_mem_def setclass_simps) |
|
13428 | 78 |
apply (intro FOL_reflections function_reflections fun_plus_reflections) |
13348 | 79 |
done |
80 |
||
81 |
text{*Separation for @{term "rtrancl(r)"}.*} |
|
82 |
lemma rtrancl_separation: |
|
83 |
"[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))" |
|
13428 | 84 |
apply (rule separation_CollectI) |
13505 | 85 |
apply (rule_tac A="{r,A,z}" in subset_LsetE, blast) |
13348 | 86 |
apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption) |
13428 | 87 |
apply (drule subset_Lset_ltD, assumption) |
13348 | 88 |
apply (erule reflection_imp_L_separation) |
89 |
apply (simp_all add: lt_Ord2) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
90 |
apply (rule DPow_LsetI) |
13348 | 91 |
apply (rename_tac u) |
92 |
apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats) |
|
93 |
apply (rule sep_rules | simp)+ |
|
94 |
done |
|
95 |
||
96 |
||
97 |
subsubsection{*Reflexive/Transitive Closure, Internalized*} |
|
98 |
||
13428 | 99 |
(* "rtran_closure(M,r,s) == |
13348 | 100 |
\<forall>A[M]. is_field(M,r,A) --> |
13428 | 101 |
(\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *) |
13348 | 102 |
constdefs rtran_closure_fm :: "[i,i]=>i" |
13428 | 103 |
"rtran_closure_fm(r,s) == |
13348 | 104 |
Forall(Implies(field_fm(succ(r),0), |
105 |
Forall(Iff(Member(0,succ(succ(s))), |
|
106 |
rtran_closure_mem_fm(1,succ(succ(r)),0)))))" |
|
107 |
||
108 |
lemma rtran_closure_type [TC]: |
|
109 |
"[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula" |
|
13428 | 110 |
by (simp add: rtran_closure_fm_def) |
13348 | 111 |
|
112 |
lemma arity_rtran_closure_fm [simp]: |
|
13428 | 113 |
"[| x \<in> nat; y \<in> nat |] |
13348 | 114 |
==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)" |
115 |
by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
116 |
||
117 |
lemma sats_rtran_closure_fm [simp]: |
|
118 |
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
|
13428 | 119 |
==> sats(A, rtran_closure_fm(x,y), env) <-> |
13348 | 120 |
rtran_closure(**A, nth(x,env), nth(y,env))" |
121 |
by (simp add: rtran_closure_fm_def rtran_closure_def) |
|
122 |
||
123 |
lemma rtran_closure_iff_sats: |
|
13428 | 124 |
"[| nth(i,env) = x; nth(j,env) = y; |
13348 | 125 |
i \<in> nat; j \<in> nat; env \<in> list(A)|] |
126 |
==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)" |
|
127 |
by simp |
|
128 |
||
129 |
theorem rtran_closure_reflection: |
|
13428 | 130 |
"REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)), |
13348 | 131 |
\<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]" |
132 |
apply (simp only: rtran_closure_def setclass_simps) |
|
133 |
apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection) |
|
134 |
done |
|
135 |
||
136 |
||
137 |
subsubsection{*Transitive Closure of a Relation, Internalized*} |
|
138 |
||
139 |
(* "tran_closure(M,r,t) == |
|
140 |
\<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *) |
|
141 |
constdefs tran_closure_fm :: "[i,i]=>i" |
|
13428 | 142 |
"tran_closure_fm(r,s) == |
13348 | 143 |
Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" |
144 |
||
145 |
lemma tran_closure_type [TC]: |
|
146 |
"[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula" |
|
13428 | 147 |
by (simp add: tran_closure_fm_def) |
13348 | 148 |
|
149 |
lemma arity_tran_closure_fm [simp]: |
|
13428 | 150 |
"[| x \<in> nat; y \<in> nat |] |
13348 | 151 |
==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)" |
152 |
by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
153 |
||
154 |
lemma sats_tran_closure_fm [simp]: |
|
155 |
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
|
13428 | 156 |
==> sats(A, tran_closure_fm(x,y), env) <-> |
13348 | 157 |
tran_closure(**A, nth(x,env), nth(y,env))" |
158 |
by (simp add: tran_closure_fm_def tran_closure_def) |
|
159 |
||
160 |
lemma tran_closure_iff_sats: |
|
13428 | 161 |
"[| nth(i,env) = x; nth(j,env) = y; |
13348 | 162 |
i \<in> nat; j \<in> nat; env \<in> list(A)|] |
163 |
==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)" |
|
164 |
by simp |
|
165 |
||
166 |
theorem tran_closure_reflection: |
|
13428 | 167 |
"REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)), |
13348 | 168 |
\<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]" |
169 |
apply (simp only: tran_closure_def setclass_simps) |
|
13428 | 170 |
apply (intro FOL_reflections function_reflections |
13348 | 171 |
rtran_closure_reflection composition_reflection) |
172 |
done |
|
173 |
||
174 |
||
13506 | 175 |
subsubsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*} |
13348 | 176 |
|
177 |
lemma wellfounded_trancl_reflects: |
|
13428 | 178 |
"REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. |
179 |
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp, |
|
180 |
\<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i). |
|
13348 | 181 |
w \<in> Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) & |
182 |
wx \<in> rp]" |
|
13428 | 183 |
by (intro FOL_reflections function_reflections fun_plus_reflections |
13348 | 184 |
tran_closure_reflection) |
185 |
||
186 |
||
187 |
lemma wellfounded_trancl_separation: |
|
13428 | 188 |
"[| L(r); L(Z) |] ==> |
189 |
separation (L, \<lambda>x. |
|
190 |
\<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. |
|
191 |
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)" |
|
192 |
apply (rule separation_CollectI) |
|
13505 | 193 |
apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast) |
13348 | 194 |
apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption) |
13428 | 195 |
apply (drule subset_Lset_ltD, assumption) |
13348 | 196 |
apply (erule reflection_imp_L_separation) |
197 |
apply (simp_all add: lt_Ord2) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
198 |
apply (rule DPow_LsetI) |
13428 | 199 |
apply (rename_tac u) |
13348 | 200 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13428 | 201 |
apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats) |
13348 | 202 |
apply (rule sep_rules tran_closure_iff_sats | simp)+ |
203 |
done |
|
204 |
||
13363 | 205 |
|
206 |
subsubsection{*Instantiating the locale @{text M_trancl}*} |
|
13428 | 207 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
208 |
lemma M_trancl_axioms_L: "M_trancl_axioms(L)" |
13428 | 209 |
apply (rule M_trancl_axioms.intro) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
210 |
apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+ |
13428 | 211 |
done |
13363 | 212 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
213 |
theorem M_trancl_L: "PROP M_trancl(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
214 |
by (rule M_trancl.intro |
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset
|
215 |
[OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L]) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
216 |
|
13428 | 217 |
lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L] |
218 |
and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L] |
|
219 |
and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L] |
|
220 |
and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L] |
|
221 |
and trancl_closed = M_trancl.trancl_closed [OF M_trancl_L] |
|
222 |
and trancl_abs = M_trancl.trancl_abs [OF M_trancl_L] |
|
223 |
and wellfounded_on_trancl = M_trancl.wellfounded_on_trancl [OF M_trancl_L] |
|
224 |
and wellfounded_trancl = M_trancl.wellfounded_trancl [OF M_trancl_L] |
|
225 |
and wfrec_relativize = M_trancl.wfrec_relativize [OF M_trancl_L] |
|
226 |
and trans_wfrec_relativize = M_trancl.trans_wfrec_relativize [OF M_trancl_L] |
|
227 |
and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L] |
|
228 |
and trans_eq_pair_wfrec_iff = M_trancl.trans_eq_pair_wfrec_iff [OF M_trancl_L] |
|
229 |
and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L] |
|
13363 | 230 |
|
231 |
declare rtrancl_closed [intro,simp] |
|
232 |
declare rtrancl_abs [simp] |
|
233 |
declare trancl_closed [intro,simp] |
|
234 |
declare trancl_abs [simp] |
|
235 |
||
236 |
||
237 |
subsection{*The Locale @{text "M_wfrank"}*} |
|
238 |
||
239 |
subsubsection{*Separation for @{term "wfrank"}*} |
|
13348 | 240 |
|
241 |
lemma wfrank_Reflects: |
|
242 |
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> |
|
13352 | 243 |
~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)), |
13348 | 244 |
\<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) --> |
13428 | 245 |
~ (\<exists>f \<in> Lset(i). |
246 |
M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), |
|
13352 | 247 |
rplus, x, f))]" |
13428 | 248 |
by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection) |
13348 | 249 |
|
250 |
lemma wfrank_separation: |
|
251 |
"L(r) ==> |
|
252 |
separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> |
|
13352 | 253 |
~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))" |
13428 | 254 |
apply (rule separation_CollectI) |
13505 | 255 |
apply (rule_tac A="{r,z}" in subset_LsetE, blast) |
13348 | 256 |
apply (rule ReflectsE [OF wfrank_Reflects], assumption) |
13428 | 257 |
apply (drule subset_Lset_ltD, assumption) |
13348 | 258 |
apply (erule reflection_imp_L_separation) |
259 |
apply (simp_all add: lt_Ord2, clarify) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
260 |
apply (rule DPow_LsetI) |
13428 | 261 |
apply (rename_tac u) |
13348 | 262 |
apply (rule ball_iff_sats imp_iff_sats)+ |
263 |
apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats) |
|
13441 | 264 |
apply (rule sep_rules | simp)+ |
13348 | 265 |
apply (rule sep_rules is_recfun_iff_sats | simp)+ |
266 |
done |
|
267 |
||
268 |
||
13363 | 269 |
subsubsection{*Replacement for @{term "wfrank"}*} |
13348 | 270 |
|
271 |
lemma wfrank_replacement_Reflects: |
|
13428 | 272 |
"REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A & |
13348 | 273 |
(\<forall>rplus[L]. tran_closure(L,r,rplus) --> |
13428 | 274 |
(\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) & |
13352 | 275 |
M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & |
13348 | 276 |
is_range(L,f,y))), |
13428 | 277 |
\<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A & |
13348 | 278 |
(\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) --> |
13428 | 279 |
(\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z) & |
13352 | 280 |
M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) & |
13348 | 281 |
is_range(**Lset(i),f,y)))]" |
282 |
by (intro FOL_reflections function_reflections fun_plus_reflections |
|
283 |
is_recfun_reflection tran_closure_reflection) |
|
284 |
||
285 |
||
286 |
lemma wfrank_strong_replacement: |
|
287 |
"L(r) ==> |
|
13428 | 288 |
strong_replacement(L, \<lambda>x z. |
13348 | 289 |
\<forall>rplus[L]. tran_closure(L,r,rplus) --> |
13428 | 290 |
(\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) & |
13352 | 291 |
M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & |
13348 | 292 |
is_range(L,f,y)))" |
13428 | 293 |
apply (rule strong_replacementI) |
13348 | 294 |
apply (rule rallI) |
13428 | 295 |
apply (rename_tac B) |
296 |
apply (rule separation_CollectI) |
|
13505 | 297 |
apply (rule_tac A="{B,r,z}" in subset_LsetE, blast) |
13348 | 298 |
apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption) |
13428 | 299 |
apply (drule subset_Lset_ltD, assumption) |
13348 | 300 |
apply (erule reflection_imp_L_separation) |
301 |
apply (simp_all add: lt_Ord2) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
302 |
apply (rule DPow_LsetI) |
13428 | 303 |
apply (rename_tac u) |
13348 | 304 |
apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+ |
13428 | 305 |
apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats) |
13441 | 306 |
apply (rule sep_rules list.intros app_type tran_closure_iff_sats is_recfun_iff_sats | simp)+ |
13348 | 307 |
done |
308 |
||
309 |
||
13363 | 310 |
subsubsection{*Separation for Proving @{text Ord_wfrank_range}*} |
13348 | 311 |
|
312 |
lemma Ord_wfrank_Reflects: |
|
13428 | 313 |
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> |
314 |
~ (\<forall>f[L]. \<forall>rangef[L]. |
|
13348 | 315 |
is_range(L,f,rangef) --> |
13352 | 316 |
M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) --> |
13348 | 317 |
ordinal(L,rangef)), |
13428 | 318 |
\<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) --> |
319 |
~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i). |
|
13348 | 320 |
is_range(**Lset(i),f,rangef) --> |
13428 | 321 |
M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y), |
13352 | 322 |
rplus, x, f) --> |
13348 | 323 |
ordinal(**Lset(i),rangef))]" |
13428 | 324 |
by (intro FOL_reflections function_reflections is_recfun_reflection |
13348 | 325 |
tran_closure_reflection ordinal_reflection) |
326 |
||
327 |
lemma Ord_wfrank_separation: |
|
328 |
"L(r) ==> |
|
329 |
separation (L, \<lambda>x. |
|
13428 | 330 |
\<forall>rplus[L]. tran_closure(L,r,rplus) --> |
331 |
~ (\<forall>f[L]. \<forall>rangef[L]. |
|
13348 | 332 |
is_range(L,f,rangef) --> |
13352 | 333 |
M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) --> |
13428 | 334 |
ordinal(L,rangef)))" |
335 |
apply (rule separation_CollectI) |
|
13505 | 336 |
apply (rule_tac A="{r,z}" in subset_LsetE, blast) |
13348 | 337 |
apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption) |
13428 | 338 |
apply (drule subset_Lset_ltD, assumption) |
13348 | 339 |
apply (erule reflection_imp_L_separation) |
340 |
apply (simp_all add: lt_Ord2, clarify) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
341 |
apply (rule DPow_LsetI) |
13428 | 342 |
apply (rename_tac u) |
13348 | 343 |
apply (rule ball_iff_sats imp_iff_sats)+ |
344 |
apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats) |
|
345 |
apply (rule sep_rules is_recfun_iff_sats | simp)+ |
|
346 |
done |
|
347 |
||
348 |
||
13363 | 349 |
subsubsection{*Instantiating the locale @{text M_wfrank}*} |
13428 | 350 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
351 |
lemma M_wfrank_axioms_L: "M_wfrank_axioms(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
352 |
apply (rule M_wfrank_axioms.intro) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
353 |
apply (assumption | rule |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
354 |
wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+ |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
355 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
356 |
|
13428 | 357 |
theorem M_wfrank_L: "PROP M_wfrank(L)" |
358 |
apply (rule M_wfrank.intro) |
|
13429 | 359 |
apply (rule M_trancl.axioms [OF M_trancl_L])+ |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
360 |
apply (rule M_wfrank_axioms_L) |
13428 | 361 |
done |
13363 | 362 |
|
13428 | 363 |
lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L] |
364 |
and exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L] |
|
365 |
and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L] |
|
366 |
and Ord_wfrank_range = M_wfrank.Ord_wfrank_range [OF M_wfrank_L] |
|
367 |
and Ord_range_wellfoundedrank = M_wfrank.Ord_range_wellfoundedrank [OF M_wfrank_L] |
|
368 |
and function_wellfoundedrank = M_wfrank.function_wellfoundedrank [OF M_wfrank_L] |
|
369 |
and domain_wellfoundedrank = M_wfrank.domain_wellfoundedrank [OF M_wfrank_L] |
|
370 |
and wellfoundedrank_type = M_wfrank.wellfoundedrank_type [OF M_wfrank_L] |
|
371 |
and Ord_wellfoundedrank = M_wfrank.Ord_wellfoundedrank [OF M_wfrank_L] |
|
372 |
and wellfoundedrank_eq = M_wfrank.wellfoundedrank_eq [OF M_wfrank_L] |
|
373 |
and wellfoundedrank_lt = M_wfrank.wellfoundedrank_lt [OF M_wfrank_L] |
|
374 |
and wellfounded_imp_subset_rvimage = M_wfrank.wellfounded_imp_subset_rvimage [OF M_wfrank_L] |
|
375 |
and wellfounded_imp_wf = M_wfrank.wellfounded_imp_wf [OF M_wfrank_L] |
|
376 |
and wellfounded_on_imp_wf_on = M_wfrank.wellfounded_on_imp_wf_on [OF M_wfrank_L] |
|
377 |
and wf_abs = M_wfrank.wf_abs [OF M_wfrank_L] |
|
378 |
and wf_on_abs = M_wfrank.wf_on_abs [OF M_wfrank_L] |
|
379 |
and wfrec_replacement_iff = M_wfrank.wfrec_replacement_iff [OF M_wfrank_L] |
|
380 |
and trans_wfrec_closed = M_wfrank.trans_wfrec_closed [OF M_wfrank_L] |
|
381 |
and wfrec_closed = M_wfrank.wfrec_closed [OF M_wfrank_L] |
|
13363 | 382 |
|
383 |
declare iterates_closed [intro,simp] |
|
384 |
declare Ord_wfrank_range [rule_format] |
|
385 |
declare wf_abs [simp] |
|
386 |
declare wf_on_abs [simp] |
|
387 |
||
388 |
||
13428 | 389 |
subsection{*@{term L} is Closed Under the Operator @{term list}*} |
13363 | 390 |
|
13386 | 391 |
subsubsection{*Instances of Replacement for Lists*} |
392 |
||
13363 | 393 |
lemma list_replacement1_Reflects: |
394 |
"REFLECTS |
|
395 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
|
396 |
is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)), |
|
397 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and> |
|
13428 | 398 |
is_wfrec(**Lset(i), |
399 |
iterates_MH(**Lset(i), |
|
13363 | 400 |
is_list_functor(**Lset(i), A), 0), memsn, u, y))]" |
13428 | 401 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
402 |
iterates_MH_reflection list_functor_reflection) |
|
13363 | 403 |
|
13441 | 404 |
|
13428 | 405 |
lemma list_replacement1: |
13363 | 406 |
"L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" |
407 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
13428 | 408 |
apply (rule strong_replacementI) |
13363 | 409 |
apply (rule rallI) |
13428 | 410 |
apply (rename_tac B) |
411 |
apply (rule separation_CollectI) |
|
412 |
apply (insert nonempty) |
|
413 |
apply (subgoal_tac "L(Memrel(succ(n)))") |
|
13505 | 414 |
apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast) |
13363 | 415 |
apply (rule ReflectsE [OF list_replacement1_Reflects], assumption) |
13428 | 416 |
apply (drule subset_Lset_ltD, assumption) |
13363 | 417 |
apply (erule reflection_imp_L_separation) |
13386 | 418 |
apply (simp_all add: lt_Ord2 Memrel_closed) |
13428 | 419 |
apply (elim conjE) |
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
420 |
apply (rule DPow_LsetI) |
13428 | 421 |
apply (rename_tac v) |
13363 | 422 |
apply (rule bex_iff_sats conj_iff_sats)+ |
423 |
apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats) |
|
13434 | 424 |
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
13441 | 425 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13363 | 426 |
done |
427 |
||
13441 | 428 |
|
13363 | 429 |
lemma list_replacement2_Reflects: |
430 |
"REFLECTS |
|
431 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and> |
|
432 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and> |
|
433 |
is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0), |
|
434 |
msn, u, x)), |
|
435 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
|
13428 | 436 |
(\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). |
13363 | 437 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 438 |
is_wfrec (**Lset(i), |
13363 | 439 |
iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0), |
440 |
msn, u, x))]" |
|
13428 | 441 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
442 |
iterates_MH_reflection list_functor_reflection) |
|
13363 | 443 |
|
444 |
||
13428 | 445 |
lemma list_replacement2: |
446 |
"L(A) ==> strong_replacement(L, |
|
447 |
\<lambda>n y. n\<in>nat & |
|
13363 | 448 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 449 |
is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), |
13363 | 450 |
msn, n, y)))" |
13428 | 451 |
apply (rule strong_replacementI) |
13363 | 452 |
apply (rule rallI) |
13428 | 453 |
apply (rename_tac B) |
454 |
apply (rule separation_CollectI) |
|
455 |
apply (insert nonempty) |
|
456 |
apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE) |
|
457 |
apply (blast intro: L_nat) |
|
13363 | 458 |
apply (rule ReflectsE [OF list_replacement2_Reflects], assumption) |
13428 | 459 |
apply (drule subset_Lset_ltD, assumption) |
13363 | 460 |
apply (erule reflection_imp_L_separation) |
461 |
apply (simp_all add: lt_Ord2) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
462 |
apply (rule DPow_LsetI) |
13428 | 463 |
apply (rename_tac v) |
13363 | 464 |
apply (rule bex_iff_sats conj_iff_sats)+ |
465 |
apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats) |
|
13434 | 466 |
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
13441 | 467 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13363 | 468 |
done |
469 |
||
13386 | 470 |
|
13428 | 471 |
subsection{*@{term L} is Closed Under the Operator @{term formula}*} |
13386 | 472 |
|
473 |
subsubsection{*Instances of Replacement for Formulas*} |
|
474 |
||
475 |
lemma formula_replacement1_Reflects: |
|
476 |
"REFLECTS |
|
477 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
|
478 |
is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)), |
|
479 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and> |
|
13428 | 480 |
is_wfrec(**Lset(i), |
481 |
iterates_MH(**Lset(i), |
|
13386 | 482 |
is_formula_functor(**Lset(i)), 0), memsn, u, y))]" |
13428 | 483 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
484 |
iterates_MH_reflection formula_functor_reflection) |
|
13386 | 485 |
|
13428 | 486 |
lemma formula_replacement1: |
13386 | 487 |
"iterates_replacement(L, is_formula_functor(L), 0)" |
488 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
13428 | 489 |
apply (rule strong_replacementI) |
13386 | 490 |
apply (rule rallI) |
13428 | 491 |
apply (rename_tac B) |
492 |
apply (rule separation_CollectI) |
|
493 |
apply (insert nonempty) |
|
494 |
apply (subgoal_tac "L(Memrel(succ(n)))") |
|
13505 | 495 |
apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast) |
13386 | 496 |
apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption) |
13428 | 497 |
apply (drule subset_Lset_ltD, assumption) |
13386 | 498 |
apply (erule reflection_imp_L_separation) |
499 |
apply (simp_all add: lt_Ord2 Memrel_closed) |
|
500 |
apply (rule DPow_LsetI) |
|
13428 | 501 |
apply (rename_tac v) |
13386 | 502 |
apply (rule bex_iff_sats conj_iff_sats)+ |
503 |
apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats) |
|
13434 | 504 |
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
13441 | 505 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13386 | 506 |
done |
507 |
||
508 |
lemma formula_replacement2_Reflects: |
|
509 |
"REFLECTS |
|
510 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and> |
|
511 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and> |
|
512 |
is_wfrec (L, iterates_MH (L, is_formula_functor(L), 0), |
|
513 |
msn, u, x)), |
|
514 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
|
13428 | 515 |
(\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). |
13386 | 516 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 517 |
is_wfrec (**Lset(i), |
13386 | 518 |
iterates_MH (**Lset(i), is_formula_functor(**Lset(i)), 0), |
519 |
msn, u, x))]" |
|
13428 | 520 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
521 |
iterates_MH_reflection formula_functor_reflection) |
|
13386 | 522 |
|
523 |
||
13428 | 524 |
lemma formula_replacement2: |
525 |
"strong_replacement(L, |
|
526 |
\<lambda>n y. n\<in>nat & |
|
13386 | 527 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 528 |
is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0), |
13386 | 529 |
msn, n, y)))" |
13428 | 530 |
apply (rule strong_replacementI) |
13386 | 531 |
apply (rule rallI) |
13428 | 532 |
apply (rename_tac B) |
533 |
apply (rule separation_CollectI) |
|
534 |
apply (insert nonempty) |
|
535 |
apply (rule_tac A="{B,z,0,nat}" in subset_LsetE) |
|
536 |
apply (blast intro: L_nat) |
|
13386 | 537 |
apply (rule ReflectsE [OF formula_replacement2_Reflects], assumption) |
13428 | 538 |
apply (drule subset_Lset_ltD, assumption) |
13386 | 539 |
apply (erule reflection_imp_L_separation) |
540 |
apply (simp_all add: lt_Ord2) |
|
541 |
apply (rule DPow_LsetI) |
|
13428 | 542 |
apply (rename_tac v) |
13386 | 543 |
apply (rule bex_iff_sats conj_iff_sats)+ |
544 |
apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats) |
|
13434 | 545 |
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
13441 | 546 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13386 | 547 |
done |
548 |
||
549 |
text{*NB The proofs for type @{term formula} are virtually identical to those |
|
550 |
for @{term "list(A)"}. It was a cut-and-paste job! *} |
|
551 |
||
13387 | 552 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
553 |
subsubsection{*The Formula @{term is_nth}, Internalized*} |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
554 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
555 |
(* "is_nth(M,n,l,Z) == |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
556 |
\<exists>X[M]. \<exists>sn[M]. \<exists>msn[M]. |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
557 |
2 1 0 |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
558 |
successor(M,n,sn) & membership(M,sn,msn) & |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
559 |
is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) & |
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
560 |
is_hd(M,X,Z)" *) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
561 |
constdefs nth_fm :: "[i,i,i]=>i" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
562 |
"nth_fm(n,l,Z) == |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
563 |
Exists(Exists(Exists( |
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
564 |
And(succ_fm(n#+3,1), |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
565 |
And(Memrel_fm(1,0), |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
566 |
And(is_wfrec_fm(iterates_MH_fm(tl_fm(1,0),l#+8,2,1,0), 0, n#+3, 2), hd_fm(2,Z#+3)))))))" |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
567 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
568 |
lemma nth_fm_type [TC]: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
569 |
"[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> nth_fm(x,y,z) \<in> formula" |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
570 |
by (simp add: nth_fm_def) |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
571 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
572 |
lemma sats_nth_fm [simp]: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
573 |
"[| x < length(env); y \<in> nat; z \<in> nat; env \<in> list(A)|] |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
574 |
==> sats(A, nth_fm(x,y,z), env) <-> |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
575 |
is_nth(**A, nth(x,env), nth(y,env), nth(z,env))" |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
576 |
apply (frule lt_length_in_nat, assumption) |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
577 |
apply (simp add: nth_fm_def is_nth_def sats_is_wfrec_fm sats_iterates_MH_fm) |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
578 |
done |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
579 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
580 |
lemma nth_iff_sats: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
581 |
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
582 |
i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|] |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
583 |
==> is_nth(**A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)" |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
584 |
by (simp add: sats_nth_fm) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
585 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
586 |
theorem nth_reflection: |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
587 |
"REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)), |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
588 |
\<lambda>i x. is_nth(**Lset(i), f(x), g(x), h(x))]" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
589 |
apply (simp only: is_nth_def setclass_simps) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
590 |
apply (intro FOL_reflections function_reflections is_wfrec_reflection |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
591 |
iterates_MH_reflection hd_reflection tl_reflection) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
592 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
593 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
594 |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
595 |
subsubsection{*An Instance of Replacement for @{term nth}*} |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
596 |
|
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
597 |
lemma nth_replacement_Reflects: |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
598 |
"REFLECTS |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
599 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
600 |
is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)), |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
601 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and> |
13428 | 602 |
is_wfrec(**Lset(i), |
603 |
iterates_MH(**Lset(i), |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
604 |
is_tl(**Lset(i)), z), memsn, u, y))]" |
13428 | 605 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
606 |
iterates_MH_reflection list_functor_reflection tl_reflection) |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
607 |
|
13428 | 608 |
lemma nth_replacement: |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
609 |
"L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)" |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
610 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
13428 | 611 |
apply (rule strong_replacementI) |
612 |
apply (rule rallI) |
|
613 |
apply (rule separation_CollectI) |
|
614 |
apply (subgoal_tac "L(Memrel(succ(n)))") |
|
13505 | 615 |
apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast) |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
616 |
apply (rule ReflectsE [OF nth_replacement_Reflects], assumption) |
13428 | 617 |
apply (drule subset_Lset_ltD, assumption) |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
618 |
apply (erule reflection_imp_L_separation) |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
619 |
apply (simp_all add: lt_Ord2 Memrel_closed) |
13428 | 620 |
apply (elim conjE) |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
621 |
apply (rule DPow_LsetI) |
13428 | 622 |
apply (rename_tac v) |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
623 |
apply (rule bex_iff_sats conj_iff_sats)+ |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
624 |
apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 625 |
apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats |
13441 | 626 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
627 |
done |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
628 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
629 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
630 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
631 |
subsubsection{*Instantiating the locale @{text M_datatypes}*} |
13428 | 632 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
633 |
lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)" |
13428 | 634 |
apply (rule M_datatypes_axioms.intro) |
635 |
apply (assumption | rule |
|
636 |
list_replacement1 list_replacement2 |
|
637 |
formula_replacement1 formula_replacement2 |
|
638 |
nth_replacement)+ |
|
639 |
done |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
640 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
641 |
theorem M_datatypes_L: "PROP M_datatypes(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
642 |
apply (rule M_datatypes.intro) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
643 |
apply (rule M_wfrank.axioms [OF M_wfrank_L])+ |
13441 | 644 |
apply (rule M_datatypes_axioms_L) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
645 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
646 |
|
13428 | 647 |
lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L] |
648 |
and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L] |
|
649 |
and list_abs = M_datatypes.list_abs [OF M_datatypes_L] |
|
650 |
and formula_abs = M_datatypes.formula_abs [OF M_datatypes_L] |
|
651 |
and nth_abs = M_datatypes.nth_abs [OF M_datatypes_L] |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
652 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
653 |
declare list_closed [intro,simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
654 |
declare formula_closed [intro,simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
655 |
declare list_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
656 |
declare formula_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
657 |
declare nth_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
658 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
659 |
|
13428 | 660 |
subsection{*@{term L} is Closed Under the Operator @{term eclose}*} |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
661 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
662 |
subsubsection{*Instances of Replacement for @{term eclose}*} |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
663 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
664 |
lemma eclose_replacement1_Reflects: |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
665 |
"REFLECTS |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
666 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
667 |
is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)), |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
668 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and> |
13428 | 669 |
is_wfrec(**Lset(i), |
670 |
iterates_MH(**Lset(i), big_union(**Lset(i)), A), |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
671 |
memsn, u, y))]" |
13428 | 672 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
673 |
iterates_MH_reflection) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
674 |
|
13428 | 675 |
lemma eclose_replacement1: |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
676 |
"L(A) ==> iterates_replacement(L, big_union(L), A)" |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
677 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
13428 | 678 |
apply (rule strong_replacementI) |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
679 |
apply (rule rallI) |
13428 | 680 |
apply (rename_tac B) |
681 |
apply (rule separation_CollectI) |
|
682 |
apply (subgoal_tac "L(Memrel(succ(n)))") |
|
13505 | 683 |
apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast) |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
684 |
apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption) |
13428 | 685 |
apply (drule subset_Lset_ltD, assumption) |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
686 |
apply (erule reflection_imp_L_separation) |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
687 |
apply (simp_all add: lt_Ord2 Memrel_closed) |
13428 | 688 |
apply (elim conjE) |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
689 |
apply (rule DPow_LsetI) |
13428 | 690 |
apply (rename_tac v) |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
691 |
apply (rule bex_iff_sats conj_iff_sats)+ |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
692 |
apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 693 |
apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats |
13441 | 694 |
is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+ |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
695 |
done |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
696 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
697 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
698 |
lemma eclose_replacement2_Reflects: |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
699 |
"REFLECTS |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
700 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and> |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
701 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and> |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
702 |
is_wfrec (L, iterates_MH (L, big_union(L), A), |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
703 |
msn, u, x)), |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
704 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
13428 | 705 |
(\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
706 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 707 |
is_wfrec (**Lset(i), |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
708 |
iterates_MH (**Lset(i), big_union(**Lset(i)), A), |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
709 |
msn, u, x))]" |
13428 | 710 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
711 |
iterates_MH_reflection) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
712 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
713 |
|
13428 | 714 |
lemma eclose_replacement2: |
715 |
"L(A) ==> strong_replacement(L, |
|
716 |
\<lambda>n y. n\<in>nat & |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
717 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 718 |
is_wfrec(L, iterates_MH(L,big_union(L), A), |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
719 |
msn, n, y)))" |
13428 | 720 |
apply (rule strong_replacementI) |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
721 |
apply (rule rallI) |
13428 | 722 |
apply (rename_tac B) |
723 |
apply (rule separation_CollectI) |
|
724 |
apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) |
|
725 |
apply (blast intro: L_nat) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
726 |
apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption) |
13428 | 727 |
apply (drule subset_Lset_ltD, assumption) |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
728 |
apply (erule reflection_imp_L_separation) |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
729 |
apply (simp_all add: lt_Ord2) |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
730 |
apply (rule DPow_LsetI) |
13428 | 731 |
apply (rename_tac v) |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
732 |
apply (rule bex_iff_sats conj_iff_sats)+ |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
733 |
apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats) |
13434 | 734 |
apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats |
13441 | 735 |
is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+ |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
736 |
done |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
737 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
738 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
739 |
subsubsection{*Instantiating the locale @{text M_eclose}*} |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
740 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
741 |
lemma M_eclose_axioms_L: "M_eclose_axioms(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
742 |
apply (rule M_eclose_axioms.intro) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
743 |
apply (assumption | rule eclose_replacement1 eclose_replacement2)+ |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
744 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
745 |
|
13428 | 746 |
theorem M_eclose_L: "PROP M_eclose(L)" |
747 |
apply (rule M_eclose.intro) |
|
13429 | 748 |
apply (rule M_datatypes.axioms [OF M_datatypes_L])+ |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
749 |
apply (rule M_eclose_axioms_L) |
13428 | 750 |
done |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
751 |
|
13428 | 752 |
lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L] |
753 |
and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L] |
|
13440 | 754 |
and transrec_replacementI = M_eclose.transrec_replacementI [OF M_eclose_L] |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
755 |
|
13348 | 756 |
end |