author | paulson |
Wed, 11 Sep 2002 16:55:37 +0200 | |
changeset 13566 | 52a419210d5c |
parent 13564 | 1500a2e48d44 |
child 13634 | 99a593b49b04 |
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 |
||
13566 | 74 |
lemma 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))" |
|
13566 | 84 |
apply (rule gen_separation [OF rtran_closure_mem_reflection, of "{r,A}"], simp) |
85 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
86 |
apply (rule DPow_LsetI) |
13566 | 87 |
apply (rule_tac env = "[x,r,A]" in rtran_closure_mem_iff_sats) |
13348 | 88 |
apply (rule sep_rules | simp)+ |
89 |
done |
|
90 |
||
91 |
||
92 |
subsubsection{*Reflexive/Transitive Closure, Internalized*} |
|
93 |
||
13428 | 94 |
(* "rtran_closure(M,r,s) == |
13348 | 95 |
\<forall>A[M]. is_field(M,r,A) --> |
13428 | 96 |
(\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *) |
13348 | 97 |
constdefs rtran_closure_fm :: "[i,i]=>i" |
13428 | 98 |
"rtran_closure_fm(r,s) == |
13348 | 99 |
Forall(Implies(field_fm(succ(r),0), |
100 |
Forall(Iff(Member(0,succ(succ(s))), |
|
101 |
rtran_closure_mem_fm(1,succ(succ(r)),0)))))" |
|
102 |
||
103 |
lemma rtran_closure_type [TC]: |
|
104 |
"[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula" |
|
13428 | 105 |
by (simp add: rtran_closure_fm_def) |
13348 | 106 |
|
107 |
lemma arity_rtran_closure_fm [simp]: |
|
13428 | 108 |
"[| x \<in> nat; y \<in> nat |] |
13348 | 109 |
==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)" |
110 |
by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
111 |
||
112 |
lemma sats_rtran_closure_fm [simp]: |
|
113 |
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
|
13428 | 114 |
==> sats(A, rtran_closure_fm(x,y), env) <-> |
13348 | 115 |
rtran_closure(**A, nth(x,env), nth(y,env))" |
116 |
by (simp add: rtran_closure_fm_def rtran_closure_def) |
|
117 |
||
118 |
lemma rtran_closure_iff_sats: |
|
13428 | 119 |
"[| nth(i,env) = x; nth(j,env) = y; |
13348 | 120 |
i \<in> nat; j \<in> nat; env \<in> list(A)|] |
121 |
==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)" |
|
122 |
by simp |
|
123 |
||
124 |
theorem rtran_closure_reflection: |
|
13428 | 125 |
"REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)), |
13348 | 126 |
\<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]" |
127 |
apply (simp only: rtran_closure_def setclass_simps) |
|
128 |
apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection) |
|
129 |
done |
|
130 |
||
131 |
||
132 |
subsubsection{*Transitive Closure of a Relation, Internalized*} |
|
133 |
||
134 |
(* "tran_closure(M,r,t) == |
|
135 |
\<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *) |
|
136 |
constdefs tran_closure_fm :: "[i,i]=>i" |
|
13428 | 137 |
"tran_closure_fm(r,s) == |
13348 | 138 |
Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" |
139 |
||
140 |
lemma tran_closure_type [TC]: |
|
141 |
"[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula" |
|
13428 | 142 |
by (simp add: tran_closure_fm_def) |
13348 | 143 |
|
144 |
lemma arity_tran_closure_fm [simp]: |
|
13428 | 145 |
"[| x \<in> nat; y \<in> nat |] |
13348 | 146 |
==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)" |
147 |
by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
148 |
||
149 |
lemma sats_tran_closure_fm [simp]: |
|
150 |
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
|
13428 | 151 |
==> sats(A, tran_closure_fm(x,y), env) <-> |
13348 | 152 |
tran_closure(**A, nth(x,env), nth(y,env))" |
153 |
by (simp add: tran_closure_fm_def tran_closure_def) |
|
154 |
||
155 |
lemma tran_closure_iff_sats: |
|
13428 | 156 |
"[| nth(i,env) = x; nth(j,env) = y; |
13348 | 157 |
i \<in> nat; j \<in> nat; env \<in> list(A)|] |
158 |
==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)" |
|
159 |
by simp |
|
160 |
||
161 |
theorem tran_closure_reflection: |
|
13428 | 162 |
"REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)), |
13348 | 163 |
\<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]" |
164 |
apply (simp only: tran_closure_def setclass_simps) |
|
13428 | 165 |
apply (intro FOL_reflections function_reflections |
13348 | 166 |
rtran_closure_reflection composition_reflection) |
167 |
done |
|
168 |
||
169 |
||
13506 | 170 |
subsubsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*} |
13348 | 171 |
|
172 |
lemma wellfounded_trancl_reflects: |
|
13428 | 173 |
"REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. |
174 |
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp, |
|
175 |
\<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i). |
|
13348 | 176 |
w \<in> Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) & |
177 |
wx \<in> rp]" |
|
13428 | 178 |
by (intro FOL_reflections function_reflections fun_plus_reflections |
13348 | 179 |
tran_closure_reflection) |
180 |
||
181 |
lemma wellfounded_trancl_separation: |
|
13428 | 182 |
"[| L(r); L(Z) |] ==> |
183 |
separation (L, \<lambda>x. |
|
184 |
\<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. |
|
185 |
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)" |
|
13566 | 186 |
apply (rule gen_separation [OF wellfounded_trancl_reflects, of "{r,Z}"], simp) |
187 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
188 |
apply (rule DPow_LsetI) |
13348 | 189 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 190 |
apply (rule_tac env = "[w,x,r,Z]" in mem_iff_sats) |
13348 | 191 |
apply (rule sep_rules tran_closure_iff_sats | simp)+ |
192 |
done |
|
193 |
||
13363 | 194 |
|
195 |
subsubsection{*Instantiating the locale @{text M_trancl}*} |
|
13428 | 196 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
197 |
lemma M_trancl_axioms_L: "M_trancl_axioms(L)" |
13428 | 198 |
apply (rule M_trancl_axioms.intro) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
199 |
apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+ |
13428 | 200 |
done |
13363 | 201 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
202 |
theorem M_trancl_L: "PROP M_trancl(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
203 |
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
|
204 |
[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
|
205 |
|
13428 | 206 |
lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L] |
207 |
and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L] |
|
208 |
and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L] |
|
209 |
and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L] |
|
210 |
and trancl_closed = M_trancl.trancl_closed [OF M_trancl_L] |
|
211 |
and trancl_abs = M_trancl.trancl_abs [OF M_trancl_L] |
|
212 |
and wellfounded_on_trancl = M_trancl.wellfounded_on_trancl [OF M_trancl_L] |
|
213 |
and wellfounded_trancl = M_trancl.wellfounded_trancl [OF M_trancl_L] |
|
214 |
and wfrec_relativize = M_trancl.wfrec_relativize [OF M_trancl_L] |
|
215 |
and trans_wfrec_relativize = M_trancl.trans_wfrec_relativize [OF M_trancl_L] |
|
216 |
and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L] |
|
217 |
and trans_eq_pair_wfrec_iff = M_trancl.trans_eq_pair_wfrec_iff [OF M_trancl_L] |
|
218 |
and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L] |
|
13363 | 219 |
|
220 |
declare rtrancl_closed [intro,simp] |
|
221 |
declare rtrancl_abs [simp] |
|
222 |
declare trancl_closed [intro,simp] |
|
223 |
declare trancl_abs [simp] |
|
224 |
||
225 |
||
226 |
subsection{*The Locale @{text "M_wfrank"}*} |
|
227 |
||
228 |
subsubsection{*Separation for @{term "wfrank"}*} |
|
13348 | 229 |
|
230 |
lemma wfrank_Reflects: |
|
231 |
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> |
|
13352 | 232 |
~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)), |
13348 | 233 |
\<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) --> |
13428 | 234 |
~ (\<exists>f \<in> Lset(i). |
235 |
M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), |
|
13352 | 236 |
rplus, x, f))]" |
13428 | 237 |
by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection) |
13348 | 238 |
|
239 |
lemma wfrank_separation: |
|
240 |
"L(r) ==> |
|
241 |
separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> |
|
13352 | 242 |
~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))" |
13566 | 243 |
apply (rule gen_separation [OF wfrank_Reflects], simp) |
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
244 |
apply (rule DPow_LsetI) |
13348 | 245 |
apply (rule ball_iff_sats imp_iff_sats)+ |
13566 | 246 |
apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats) |
13348 | 247 |
apply (rule sep_rules is_recfun_iff_sats | simp)+ |
248 |
done |
|
249 |
||
250 |
||
13363 | 251 |
subsubsection{*Replacement for @{term "wfrank"}*} |
13348 | 252 |
|
253 |
lemma wfrank_replacement_Reflects: |
|
13428 | 254 |
"REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A & |
13348 | 255 |
(\<forall>rplus[L]. tran_closure(L,r,rplus) --> |
13428 | 256 |
(\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) & |
13352 | 257 |
M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & |
13348 | 258 |
is_range(L,f,y))), |
13428 | 259 |
\<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A & |
13348 | 260 |
(\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) --> |
13428 | 261 |
(\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z) & |
13352 | 262 |
M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) & |
13348 | 263 |
is_range(**Lset(i),f,y)))]" |
264 |
by (intro FOL_reflections function_reflections fun_plus_reflections |
|
265 |
is_recfun_reflection tran_closure_reflection) |
|
266 |
||
267 |
lemma wfrank_strong_replacement: |
|
268 |
"L(r) ==> |
|
13428 | 269 |
strong_replacement(L, \<lambda>x z. |
13348 | 270 |
\<forall>rplus[L]. tran_closure(L,r,rplus) --> |
13428 | 271 |
(\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) & |
13352 | 272 |
M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & |
13348 | 273 |
is_range(L,f,y)))" |
13428 | 274 |
apply (rule strong_replacementI) |
13566 | 275 |
apply (rule_tac u="{r,A}" in gen_separation [OF wfrank_replacement_Reflects], |
276 |
simp) |
|
277 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
278 |
apply (rule DPow_LsetI) |
13348 | 279 |
apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+ |
13566 | 280 |
apply (rule_tac env = "[x,z,A,r]" in mem_iff_sats) |
281 |
apply (rule sep_rules list.intros app_type tran_closure_iff_sats |
|
282 |
is_recfun_iff_sats | simp)+ |
|
13348 | 283 |
done |
284 |
||
285 |
||
13363 | 286 |
subsubsection{*Separation for Proving @{text Ord_wfrank_range}*} |
13348 | 287 |
|
288 |
lemma Ord_wfrank_Reflects: |
|
13428 | 289 |
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> |
290 |
~ (\<forall>f[L]. \<forall>rangef[L]. |
|
13348 | 291 |
is_range(L,f,rangef) --> |
13352 | 292 |
M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) --> |
13348 | 293 |
ordinal(L,rangef)), |
13428 | 294 |
\<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) --> |
295 |
~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i). |
|
13348 | 296 |
is_range(**Lset(i),f,rangef) --> |
13428 | 297 |
M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y), |
13352 | 298 |
rplus, x, f) --> |
13348 | 299 |
ordinal(**Lset(i),rangef))]" |
13428 | 300 |
by (intro FOL_reflections function_reflections is_recfun_reflection |
13348 | 301 |
tran_closure_reflection ordinal_reflection) |
302 |
||
303 |
lemma Ord_wfrank_separation: |
|
304 |
"L(r) ==> |
|
305 |
separation (L, \<lambda>x. |
|
13428 | 306 |
\<forall>rplus[L]. tran_closure(L,r,rplus) --> |
307 |
~ (\<forall>f[L]. \<forall>rangef[L]. |
|
13348 | 308 |
is_range(L,f,rangef) --> |
13352 | 309 |
M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) --> |
13428 | 310 |
ordinal(L,rangef)))" |
13566 | 311 |
apply (rule gen_separation [OF Ord_wfrank_Reflects], simp) |
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
312 |
apply (rule DPow_LsetI) |
13348 | 313 |
apply (rule ball_iff_sats imp_iff_sats)+ |
13566 | 314 |
apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats) |
13348 | 315 |
apply (rule sep_rules is_recfun_iff_sats | simp)+ |
316 |
done |
|
317 |
||
318 |
||
13363 | 319 |
subsubsection{*Instantiating the locale @{text M_wfrank}*} |
13428 | 320 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
321 |
lemma M_wfrank_axioms_L: "M_wfrank_axioms(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
322 |
apply (rule M_wfrank_axioms.intro) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
323 |
apply (assumption | rule |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
324 |
wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+ |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
325 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
326 |
|
13428 | 327 |
theorem M_wfrank_L: "PROP M_wfrank(L)" |
328 |
apply (rule M_wfrank.intro) |
|
13429 | 329 |
apply (rule M_trancl.axioms [OF M_trancl_L])+ |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
330 |
apply (rule M_wfrank_axioms_L) |
13428 | 331 |
done |
13363 | 332 |
|
13428 | 333 |
lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L] |
334 |
and exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L] |
|
335 |
and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L] |
|
336 |
and Ord_wfrank_range = M_wfrank.Ord_wfrank_range [OF M_wfrank_L] |
|
337 |
and Ord_range_wellfoundedrank = M_wfrank.Ord_range_wellfoundedrank [OF M_wfrank_L] |
|
338 |
and function_wellfoundedrank = M_wfrank.function_wellfoundedrank [OF M_wfrank_L] |
|
339 |
and domain_wellfoundedrank = M_wfrank.domain_wellfoundedrank [OF M_wfrank_L] |
|
340 |
and wellfoundedrank_type = M_wfrank.wellfoundedrank_type [OF M_wfrank_L] |
|
341 |
and Ord_wellfoundedrank = M_wfrank.Ord_wellfoundedrank [OF M_wfrank_L] |
|
342 |
and wellfoundedrank_eq = M_wfrank.wellfoundedrank_eq [OF M_wfrank_L] |
|
343 |
and wellfoundedrank_lt = M_wfrank.wellfoundedrank_lt [OF M_wfrank_L] |
|
344 |
and wellfounded_imp_subset_rvimage = M_wfrank.wellfounded_imp_subset_rvimage [OF M_wfrank_L] |
|
345 |
and wellfounded_imp_wf = M_wfrank.wellfounded_imp_wf [OF M_wfrank_L] |
|
346 |
and wellfounded_on_imp_wf_on = M_wfrank.wellfounded_on_imp_wf_on [OF M_wfrank_L] |
|
347 |
and wf_abs = M_wfrank.wf_abs [OF M_wfrank_L] |
|
348 |
and wf_on_abs = M_wfrank.wf_on_abs [OF M_wfrank_L] |
|
349 |
and wfrec_replacement_iff = M_wfrank.wfrec_replacement_iff [OF M_wfrank_L] |
|
350 |
and trans_wfrec_closed = M_wfrank.trans_wfrec_closed [OF M_wfrank_L] |
|
351 |
and wfrec_closed = M_wfrank.wfrec_closed [OF M_wfrank_L] |
|
13363 | 352 |
|
353 |
declare iterates_closed [intro,simp] |
|
354 |
declare Ord_wfrank_range [rule_format] |
|
355 |
declare wf_abs [simp] |
|
356 |
declare wf_on_abs [simp] |
|
357 |
||
358 |
||
13428 | 359 |
subsection{*@{term L} is Closed Under the Operator @{term list}*} |
13363 | 360 |
|
13386 | 361 |
subsubsection{*Instances of Replacement for Lists*} |
362 |
||
13363 | 363 |
lemma list_replacement1_Reflects: |
364 |
"REFLECTS |
|
365 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
|
366 |
is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)), |
|
367 |
\<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 | 368 |
is_wfrec(**Lset(i), |
369 |
iterates_MH(**Lset(i), |
|
13363 | 370 |
is_list_functor(**Lset(i), A), 0), memsn, u, y))]" |
13428 | 371 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
372 |
iterates_MH_reflection list_functor_reflection) |
|
13363 | 373 |
|
13441 | 374 |
|
13428 | 375 |
lemma list_replacement1: |
13363 | 376 |
"L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" |
377 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
13428 | 378 |
apply (rule strong_replacementI) |
379 |
apply (rename_tac B) |
|
13566 | 380 |
apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" |
381 |
in gen_separation [OF list_replacement1_Reflects], |
|
382 |
simp add: nonempty) |
|
383 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
384 |
apply (rule DPow_LsetI) |
13363 | 385 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 386 |
apply (rule_tac env = "[u,x,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 387 |
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
13441 | 388 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13363 | 389 |
done |
390 |
||
13441 | 391 |
|
13363 | 392 |
lemma list_replacement2_Reflects: |
393 |
"REFLECTS |
|
394 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and> |
|
395 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and> |
|
396 |
is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0), |
|
397 |
msn, u, x)), |
|
398 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
|
13428 | 399 |
(\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). |
13363 | 400 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 401 |
is_wfrec (**Lset(i), |
13363 | 402 |
iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0), |
403 |
msn, u, x))]" |
|
13428 | 404 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
405 |
iterates_MH_reflection list_functor_reflection) |
|
13363 | 406 |
|
407 |
||
13428 | 408 |
lemma list_replacement2: |
409 |
"L(A) ==> strong_replacement(L, |
|
410 |
\<lambda>n y. n\<in>nat & |
|
13363 | 411 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 412 |
is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), |
13363 | 413 |
msn, n, y)))" |
13428 | 414 |
apply (rule strong_replacementI) |
415 |
apply (rename_tac B) |
|
13566 | 416 |
apply (rule_tac u="{A,B,0,nat}" |
417 |
in gen_separation [OF list_replacement2_Reflects], |
|
418 |
simp add: L_nat nonempty) |
|
419 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset
|
420 |
apply (rule DPow_LsetI) |
13363 | 421 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 422 |
apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats) |
13434 | 423 |
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
13441 | 424 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13363 | 425 |
done |
426 |
||
13386 | 427 |
|
13428 | 428 |
subsection{*@{term L} is Closed Under the Operator @{term formula}*} |
13386 | 429 |
|
430 |
subsubsection{*Instances of Replacement for Formulas*} |
|
431 |
||
432 |
lemma formula_replacement1_Reflects: |
|
433 |
"REFLECTS |
|
434 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
|
435 |
is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)), |
|
436 |
\<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 | 437 |
is_wfrec(**Lset(i), |
438 |
iterates_MH(**Lset(i), |
|
13386 | 439 |
is_formula_functor(**Lset(i)), 0), memsn, u, y))]" |
13428 | 440 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
441 |
iterates_MH_reflection formula_functor_reflection) |
|
13386 | 442 |
|
13428 | 443 |
lemma formula_replacement1: |
13386 | 444 |
"iterates_replacement(L, is_formula_functor(L), 0)" |
445 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
13428 | 446 |
apply (rule strong_replacementI) |
447 |
apply (rename_tac B) |
|
13566 | 448 |
apply (rule_tac u="{B,n,0,Memrel(succ(n))}" |
449 |
in gen_separation [OF formula_replacement1_Reflects], |
|
450 |
simp add: nonempty) |
|
451 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13386 | 452 |
apply (rule DPow_LsetI) |
453 |
apply (rule bex_iff_sats conj_iff_sats)+ |
|
13566 | 454 |
apply (rule_tac env = "[u,x,n,B,0,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 455 |
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
13441 | 456 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13386 | 457 |
done |
458 |
||
459 |
lemma formula_replacement2_Reflects: |
|
460 |
"REFLECTS |
|
461 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and> |
|
462 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and> |
|
463 |
is_wfrec (L, iterates_MH (L, is_formula_functor(L), 0), |
|
464 |
msn, u, x)), |
|
465 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
|
13428 | 466 |
(\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). |
13386 | 467 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 468 |
is_wfrec (**Lset(i), |
13386 | 469 |
iterates_MH (**Lset(i), is_formula_functor(**Lset(i)), 0), |
470 |
msn, u, x))]" |
|
13428 | 471 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
472 |
iterates_MH_reflection formula_functor_reflection) |
|
13386 | 473 |
|
474 |
||
13428 | 475 |
lemma formula_replacement2: |
476 |
"strong_replacement(L, |
|
477 |
\<lambda>n y. n\<in>nat & |
|
13386 | 478 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 479 |
is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0), |
13386 | 480 |
msn, n, y)))" |
13428 | 481 |
apply (rule strong_replacementI) |
482 |
apply (rename_tac B) |
|
13566 | 483 |
apply (rule_tac u="{B,0,nat}" |
484 |
in gen_separation [OF formula_replacement2_Reflects], |
|
485 |
simp add: nonempty L_nat) |
|
486 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13386 | 487 |
apply (rule DPow_LsetI) |
488 |
apply (rule bex_iff_sats conj_iff_sats)+ |
|
13566 | 489 |
apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats) |
13434 | 490 |
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
13441 | 491 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13386 | 492 |
done |
493 |
||
494 |
text{*NB The proofs for type @{term formula} are virtually identical to those |
|
495 |
for @{term "list(A)"}. It was a cut-and-paste job! *} |
|
496 |
||
13387 | 497 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
498 |
subsubsection{*The Formula @{term is_nth}, Internalized*} |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
499 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
500 |
(* "is_nth(M,n,l,Z) == |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
501 |
\<exists>X[M]. \<exists>sn[M]. \<exists>msn[M]. |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
502 |
2 1 0 |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
503 |
successor(M,n,sn) & membership(M,sn,msn) & |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
504 |
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
|
505 |
is_hd(M,X,Z)" *) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
506 |
constdefs nth_fm :: "[i,i,i]=>i" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
507 |
"nth_fm(n,l,Z) == |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
508 |
Exists(Exists(Exists( |
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
509 |
And(succ_fm(n#+3,1), |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
510 |
And(Memrel_fm(1,0), |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
511 |
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
|
512 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
513 |
lemma nth_fm_type [TC]: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
514 |
"[| 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
|
515 |
by (simp add: nth_fm_def) |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
516 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
517 |
lemma sats_nth_fm [simp]: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
518 |
"[| 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
|
519 |
==> sats(A, nth_fm(x,y,z), env) <-> |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
520 |
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
|
521 |
apply (frule lt_length_in_nat, assumption) |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
522 |
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
|
523 |
done |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
524 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
525 |
lemma nth_iff_sats: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
526 |
"[| 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
|
527 |
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
|
528 |
==> 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
|
529 |
by (simp add: sats_nth_fm) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
530 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
531 |
theorem nth_reflection: |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
532 |
"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
|
533 |
\<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
|
534 |
apply (simp only: is_nth_def setclass_simps) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
535 |
apply (intro FOL_reflections function_reflections is_wfrec_reflection |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
536 |
iterates_MH_reflection hd_reflection tl_reflection) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
537 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
538 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
539 |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
540 |
subsubsection{*An Instance of Replacement for @{term nth}*} |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
541 |
|
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
542 |
lemma nth_replacement_Reflects: |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
543 |
"REFLECTS |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
544 |
[\<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
|
545 |
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
|
546 |
\<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 | 547 |
is_wfrec(**Lset(i), |
548 |
iterates_MH(**Lset(i), |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
549 |
is_tl(**Lset(i)), z), memsn, u, y))]" |
13428 | 550 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
551 |
iterates_MH_reflection list_functor_reflection tl_reflection) |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
552 |
|
13428 | 553 |
lemma nth_replacement: |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
554 |
"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
|
555 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
13428 | 556 |
apply (rule strong_replacementI) |
13566 | 557 |
apply (rule_tac u="{A,n,w,Memrel(succ(n))}" |
558 |
in gen_separation [OF nth_replacement_Reflects], |
|
559 |
simp add: nonempty) |
|
560 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
561 |
apply (rule DPow_LsetI) |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
562 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 563 |
apply (rule_tac env = "[u,x,A,w,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 564 |
apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats |
13441 | 565 |
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
|
566 |
done |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
567 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
568 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
569 |
subsubsection{*Instantiating the locale @{text M_datatypes}*} |
13428 | 570 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
571 |
lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)" |
13428 | 572 |
apply (rule M_datatypes_axioms.intro) |
573 |
apply (assumption | rule |
|
574 |
list_replacement1 list_replacement2 |
|
575 |
formula_replacement1 formula_replacement2 |
|
576 |
nth_replacement)+ |
|
577 |
done |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
578 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
579 |
theorem M_datatypes_L: "PROP M_datatypes(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
580 |
apply (rule M_datatypes.intro) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
581 |
apply (rule M_wfrank.axioms [OF M_wfrank_L])+ |
13441 | 582 |
apply (rule M_datatypes_axioms_L) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
583 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
584 |
|
13428 | 585 |
lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L] |
586 |
and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L] |
|
587 |
and list_abs = M_datatypes.list_abs [OF M_datatypes_L] |
|
588 |
and formula_abs = M_datatypes.formula_abs [OF M_datatypes_L] |
|
589 |
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
|
590 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
591 |
declare list_closed [intro,simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
592 |
declare formula_closed [intro,simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
593 |
declare list_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
594 |
declare formula_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
595 |
declare nth_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
596 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
597 |
|
13428 | 598 |
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
|
599 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
600 |
subsubsection{*Instances of Replacement for @{term eclose}*} |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
601 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
602 |
lemma eclose_replacement1_Reflects: |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
603 |
"REFLECTS |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
604 |
[\<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
|
605 |
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
|
606 |
\<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 | 607 |
is_wfrec(**Lset(i), |
608 |
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
|
609 |
memsn, u, y))]" |
13428 | 610 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
611 |
iterates_MH_reflection) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
612 |
|
13428 | 613 |
lemma eclose_replacement1: |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
614 |
"L(A) ==> iterates_replacement(L, big_union(L), A)" |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
615 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
13428 | 616 |
apply (rule strong_replacementI) |
617 |
apply (rename_tac B) |
|
13566 | 618 |
apply (rule_tac u="{B,A,n,Memrel(succ(n))}" |
619 |
in gen_separation [OF eclose_replacement1_Reflects], simp) |
|
620 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
621 |
apply (rule DPow_LsetI) |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
622 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 623 |
apply (rule_tac env = "[u,x,A,n,B,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 624 |
apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats |
13441 | 625 |
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
|
626 |
done |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
627 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
628 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
629 |
lemma eclose_replacement2_Reflects: |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
630 |
"REFLECTS |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
631 |
[\<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
|
632 |
(\<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
|
633 |
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
|
634 |
msn, u, x)), |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
635 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
13428 | 636 |
(\<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
|
637 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 638 |
is_wfrec (**Lset(i), |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
639 |
iterates_MH (**Lset(i), big_union(**Lset(i)), A), |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
640 |
msn, u, x))]" |
13428 | 641 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
642 |
iterates_MH_reflection) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
643 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
644 |
|
13428 | 645 |
lemma eclose_replacement2: |
646 |
"L(A) ==> strong_replacement(L, |
|
647 |
\<lambda>n y. n\<in>nat & |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
648 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 649 |
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
|
650 |
msn, n, y)))" |
13428 | 651 |
apply (rule strong_replacementI) |
652 |
apply (rename_tac B) |
|
13566 | 653 |
apply (rule_tac u="{A,B,nat}" |
654 |
in gen_separation [OF eclose_replacement2_Reflects], simp add: L_nat) |
|
655 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
656 |
apply (rule DPow_LsetI) |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
657 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 658 |
apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats) |
13434 | 659 |
apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats |
13441 | 660 |
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
|
661 |
done |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
662 |
|
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 |
subsubsection{*Instantiating the locale @{text M_eclose}*} |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
665 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
666 |
lemma M_eclose_axioms_L: "M_eclose_axioms(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
667 |
apply (rule M_eclose_axioms.intro) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
668 |
apply (assumption | rule eclose_replacement1 eclose_replacement2)+ |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
669 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
670 |
|
13428 | 671 |
theorem M_eclose_L: "PROP M_eclose(L)" |
672 |
apply (rule M_eclose.intro) |
|
13429 | 673 |
apply (rule M_datatypes.axioms [OF M_datatypes_L])+ |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
674 |
apply (rule M_eclose_axioms_L) |
13428 | 675 |
done |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
676 |
|
13428 | 677 |
lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L] |
678 |
and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L] |
|
13440 | 679 |
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
|
680 |
|
13348 | 681 |
end |