author | paulson |
Wed, 09 Oct 2002 11:07:13 +0200 | |
changeset 13634 | 99a593b49b04 |
parent 13566 | 52a419210d5c |
child 13647 | 7f6f0ffc45c3 |
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 |
13634 | 2 |
ID: $Id$ |
13437
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 |
*) |
13429 | 5 |
|
6 |
header {*Separation for Facts About Recursion*} |
|
13348 | 7 |
|
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13493
diff
changeset
|
8 |
theory Rec_Separation = Separation + Internalize: |
13348 | 9 |
|
10 |
text{*This theory proves all instances needed for locales @{text |
|
13634 | 11 |
"M_trancl"} and @{text "M_datatypes"}*} |
13348 | 12 |
|
13363 | 13 |
lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i" |
13428 | 14 |
by simp |
13363 | 15 |
|
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
16 |
|
13348 | 17 |
subsection{*The Locale @{text "M_trancl"}*} |
18 |
||
19 |
subsubsection{*Separation for Reflexive/Transitive Closure*} |
|
20 |
||
21 |
text{*First, The Defining Formula*} |
|
22 |
||
23 |
(* "rtran_closure_mem(M,A,r,p) == |
|
13428 | 24 |
\<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. |
13348 | 25 |
omega(M,nnat) & n\<in>nnat & successor(M,n,n') & |
26 |
(\<exists>f[M]. typed_function(M,n',A,f) & |
|
13428 | 27 |
(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) & |
28 |
fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & |
|
29 |
(\<forall>j[M]. j\<in>n --> |
|
30 |
(\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. |
|
31 |
fun_apply(M,f,j,fj) & successor(M,j,sj) & |
|
32 |
fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*) |
|
13348 | 33 |
constdefs rtran_closure_mem_fm :: "[i,i,i]=>i" |
13428 | 34 |
"rtran_closure_mem_fm(A,r,p) == |
13348 | 35 |
Exists(Exists(Exists( |
36 |
And(omega_fm(2), |
|
37 |
And(Member(1,2), |
|
38 |
And(succ_fm(1,0), |
|
39 |
Exists(And(typed_function_fm(1, A#+4, 0), |
|
13428 | 40 |
And(Exists(Exists(Exists( |
41 |
And(pair_fm(2,1,p#+7), |
|
42 |
And(empty_fm(0), |
|
43 |
And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))), |
|
44 |
Forall(Implies(Member(0,3), |
|
45 |
Exists(Exists(Exists(Exists( |
|
46 |
And(fun_apply_fm(5,4,3), |
|
47 |
And(succ_fm(4,2), |
|
48 |
And(fun_apply_fm(5,2,1), |
|
49 |
And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))" |
|
13348 | 50 |
|
51 |
||
52 |
lemma rtran_closure_mem_type [TC]: |
|
53 |
"[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula" |
|
13428 | 54 |
by (simp add: rtran_closure_mem_fm_def) |
13348 | 55 |
|
56 |
lemma arity_rtran_closure_mem_fm [simp]: |
|
13428 | 57 |
"[| x \<in> nat; y \<in> nat; z \<in> nat |] |
13348 | 58 |
==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" |
13428 | 59 |
by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac) |
13348 | 60 |
|
61 |
lemma sats_rtran_closure_mem_fm [simp]: |
|
62 |
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
13428 | 63 |
==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> |
13348 | 64 |
rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))" |
65 |
by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def) |
|
66 |
||
67 |
lemma rtran_closure_mem_iff_sats: |
|
13428 | 68 |
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
13348 | 69 |
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
70 |
==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)" |
|
71 |
by (simp add: sats_rtran_closure_mem_fm) |
|
72 |
||
13566 | 73 |
lemma rtran_closure_mem_reflection: |
13428 | 74 |
"REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)), |
13348 | 75 |
\<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]" |
76 |
apply (simp only: rtran_closure_mem_def setclass_simps) |
|
13428 | 77 |
apply (intro FOL_reflections function_reflections fun_plus_reflections) |
13348 | 78 |
done |
79 |
||
80 |
text{*Separation for @{term "rtrancl(r)"}.*} |
|
81 |
lemma rtrancl_separation: |
|
82 |
"[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))" |
|
13566 | 83 |
apply (rule gen_separation [OF rtran_closure_mem_reflection, of "{r,A}"], simp) |
84 |
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
|
85 |
apply (rule DPow_LsetI) |
13566 | 86 |
apply (rule_tac env = "[x,r,A]" in rtran_closure_mem_iff_sats) |
13348 | 87 |
apply (rule sep_rules | simp)+ |
88 |
done |
|
89 |
||
90 |
||
91 |
subsubsection{*Reflexive/Transitive Closure, Internalized*} |
|
92 |
||
13428 | 93 |
(* "rtran_closure(M,r,s) == |
13348 | 94 |
\<forall>A[M]. is_field(M,r,A) --> |
13428 | 95 |
(\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *) |
13348 | 96 |
constdefs rtran_closure_fm :: "[i,i]=>i" |
13428 | 97 |
"rtran_closure_fm(r,s) == |
13348 | 98 |
Forall(Implies(field_fm(succ(r),0), |
99 |
Forall(Iff(Member(0,succ(succ(s))), |
|
100 |
rtran_closure_mem_fm(1,succ(succ(r)),0)))))" |
|
101 |
||
102 |
lemma rtran_closure_type [TC]: |
|
103 |
"[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula" |
|
13428 | 104 |
by (simp add: rtran_closure_fm_def) |
13348 | 105 |
|
106 |
lemma arity_rtran_closure_fm [simp]: |
|
13428 | 107 |
"[| x \<in> nat; y \<in> nat |] |
13348 | 108 |
==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)" |
109 |
by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
110 |
||
111 |
lemma sats_rtran_closure_fm [simp]: |
|
112 |
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
|
13428 | 113 |
==> sats(A, rtran_closure_fm(x,y), env) <-> |
13348 | 114 |
rtran_closure(**A, nth(x,env), nth(y,env))" |
115 |
by (simp add: rtran_closure_fm_def rtran_closure_def) |
|
116 |
||
117 |
lemma rtran_closure_iff_sats: |
|
13428 | 118 |
"[| nth(i,env) = x; nth(j,env) = y; |
13348 | 119 |
i \<in> nat; j \<in> nat; env \<in> list(A)|] |
120 |
==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)" |
|
121 |
by simp |
|
122 |
||
123 |
theorem rtran_closure_reflection: |
|
13428 | 124 |
"REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)), |
13348 | 125 |
\<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]" |
126 |
apply (simp only: rtran_closure_def setclass_simps) |
|
127 |
apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection) |
|
128 |
done |
|
129 |
||
130 |
||
131 |
subsubsection{*Transitive Closure of a Relation, Internalized*} |
|
132 |
||
133 |
(* "tran_closure(M,r,t) == |
|
134 |
\<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *) |
|
135 |
constdefs tran_closure_fm :: "[i,i]=>i" |
|
13428 | 136 |
"tran_closure_fm(r,s) == |
13348 | 137 |
Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" |
138 |
||
139 |
lemma tran_closure_type [TC]: |
|
140 |
"[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula" |
|
13428 | 141 |
by (simp add: tran_closure_fm_def) |
13348 | 142 |
|
143 |
lemma arity_tran_closure_fm [simp]: |
|
13428 | 144 |
"[| x \<in> nat; y \<in> nat |] |
13348 | 145 |
==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)" |
146 |
by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
147 |
||
148 |
lemma sats_tran_closure_fm [simp]: |
|
149 |
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
|
13428 | 150 |
==> sats(A, tran_closure_fm(x,y), env) <-> |
13348 | 151 |
tran_closure(**A, nth(x,env), nth(y,env))" |
152 |
by (simp add: tran_closure_fm_def tran_closure_def) |
|
153 |
||
154 |
lemma tran_closure_iff_sats: |
|
13428 | 155 |
"[| nth(i,env) = x; nth(j,env) = y; |
13348 | 156 |
i \<in> nat; j \<in> nat; env \<in> list(A)|] |
157 |
==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)" |
|
158 |
by simp |
|
159 |
||
160 |
theorem tran_closure_reflection: |
|
13428 | 161 |
"REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)), |
13348 | 162 |
\<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]" |
163 |
apply (simp only: tran_closure_def setclass_simps) |
|
13428 | 164 |
apply (intro FOL_reflections function_reflections |
13348 | 165 |
rtran_closure_reflection composition_reflection) |
166 |
done |
|
167 |
||
168 |
||
13506 | 169 |
subsubsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*} |
13348 | 170 |
|
171 |
lemma wellfounded_trancl_reflects: |
|
13428 | 172 |
"REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. |
173 |
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp, |
|
174 |
\<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i). |
|
13348 | 175 |
w \<in> Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) & |
176 |
wx \<in> rp]" |
|
13428 | 177 |
by (intro FOL_reflections function_reflections fun_plus_reflections |
13348 | 178 |
tran_closure_reflection) |
179 |
||
180 |
lemma wellfounded_trancl_separation: |
|
13428 | 181 |
"[| L(r); L(Z) |] ==> |
182 |
separation (L, \<lambda>x. |
|
183 |
\<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. |
|
184 |
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)" |
|
13566 | 185 |
apply (rule gen_separation [OF wellfounded_trancl_reflects, of "{r,Z}"], simp) |
186 |
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
|
187 |
apply (rule DPow_LsetI) |
13348 | 188 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 189 |
apply (rule_tac env = "[w,x,r,Z]" in mem_iff_sats) |
13348 | 190 |
apply (rule sep_rules tran_closure_iff_sats | simp)+ |
191 |
done |
|
192 |
||
13363 | 193 |
|
194 |
subsubsection{*Instantiating the locale @{text M_trancl}*} |
|
13428 | 195 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
196 |
lemma M_trancl_axioms_L: "M_trancl_axioms(L)" |
13428 | 197 |
apply (rule M_trancl_axioms.intro) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
198 |
apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+ |
13428 | 199 |
done |
13363 | 200 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
201 |
theorem M_trancl_L: "PROP M_trancl(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
202 |
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
|
203 |
[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
|
204 |
|
13428 | 205 |
lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L] |
206 |
and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L] |
|
207 |
and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L] |
|
208 |
and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L] |
|
209 |
and trancl_closed = M_trancl.trancl_closed [OF M_trancl_L] |
|
210 |
and trancl_abs = M_trancl.trancl_abs [OF M_trancl_L] |
|
211 |
and wellfounded_on_trancl = M_trancl.wellfounded_on_trancl [OF M_trancl_L] |
|
212 |
and wellfounded_trancl = M_trancl.wellfounded_trancl [OF M_trancl_L] |
|
213 |
and wfrec_relativize = M_trancl.wfrec_relativize [OF M_trancl_L] |
|
214 |
and trans_wfrec_relativize = M_trancl.trans_wfrec_relativize [OF M_trancl_L] |
|
215 |
and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L] |
|
216 |
and trans_eq_pair_wfrec_iff = M_trancl.trans_eq_pair_wfrec_iff [OF M_trancl_L] |
|
217 |
and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L] |
|
13363 | 218 |
|
219 |
declare rtrancl_closed [intro,simp] |
|
220 |
declare rtrancl_abs [simp] |
|
221 |
declare trancl_closed [intro,simp] |
|
222 |
declare trancl_abs [simp] |
|
223 |
||
224 |
||
13428 | 225 |
subsection{*@{term L} is Closed Under the Operator @{term list}*} |
13363 | 226 |
|
13386 | 227 |
subsubsection{*Instances of Replacement for Lists*} |
228 |
||
13363 | 229 |
lemma list_replacement1_Reflects: |
230 |
"REFLECTS |
|
231 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
|
232 |
is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)), |
|
233 |
\<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 | 234 |
is_wfrec(**Lset(i), |
235 |
iterates_MH(**Lset(i), |
|
13363 | 236 |
is_list_functor(**Lset(i), A), 0), memsn, u, y))]" |
13428 | 237 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
238 |
iterates_MH_reflection list_functor_reflection) |
|
13363 | 239 |
|
13441 | 240 |
|
13428 | 241 |
lemma list_replacement1: |
13363 | 242 |
"L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" |
243 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
13428 | 244 |
apply (rule strong_replacementI) |
245 |
apply (rename_tac B) |
|
13566 | 246 |
apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" |
247 |
in gen_separation [OF list_replacement1_Reflects], |
|
248 |
simp add: nonempty) |
|
249 |
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
|
250 |
apply (rule DPow_LsetI) |
13363 | 251 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 252 |
apply (rule_tac env = "[u,x,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 253 |
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
13441 | 254 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13363 | 255 |
done |
256 |
||
13441 | 257 |
|
13363 | 258 |
lemma list_replacement2_Reflects: |
259 |
"REFLECTS |
|
260 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and> |
|
261 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and> |
|
262 |
is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0), |
|
263 |
msn, u, x)), |
|
264 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
|
13428 | 265 |
(\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). |
13363 | 266 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 267 |
is_wfrec (**Lset(i), |
13363 | 268 |
iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0), |
269 |
msn, u, x))]" |
|
13428 | 270 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
271 |
iterates_MH_reflection list_functor_reflection) |
|
13363 | 272 |
|
273 |
||
13428 | 274 |
lemma list_replacement2: |
275 |
"L(A) ==> strong_replacement(L, |
|
276 |
\<lambda>n y. n\<in>nat & |
|
13363 | 277 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 278 |
is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), |
13363 | 279 |
msn, n, y)))" |
13428 | 280 |
apply (rule strong_replacementI) |
281 |
apply (rename_tac B) |
|
13566 | 282 |
apply (rule_tac u="{A,B,0,nat}" |
283 |
in gen_separation [OF list_replacement2_Reflects], |
|
284 |
simp add: L_nat nonempty) |
|
285 |
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
|
286 |
apply (rule DPow_LsetI) |
13363 | 287 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 288 |
apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats) |
13434 | 289 |
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
13441 | 290 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13363 | 291 |
done |
292 |
||
13386 | 293 |
|
13428 | 294 |
subsection{*@{term L} is Closed Under the Operator @{term formula}*} |
13386 | 295 |
|
296 |
subsubsection{*Instances of Replacement for Formulas*} |
|
297 |
||
298 |
lemma formula_replacement1_Reflects: |
|
299 |
"REFLECTS |
|
300 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
|
301 |
is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)), |
|
302 |
\<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 | 303 |
is_wfrec(**Lset(i), |
304 |
iterates_MH(**Lset(i), |
|
13386 | 305 |
is_formula_functor(**Lset(i)), 0), memsn, u, y))]" |
13428 | 306 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
307 |
iterates_MH_reflection formula_functor_reflection) |
|
13386 | 308 |
|
13428 | 309 |
lemma formula_replacement1: |
13386 | 310 |
"iterates_replacement(L, is_formula_functor(L), 0)" |
311 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
13428 | 312 |
apply (rule strong_replacementI) |
313 |
apply (rename_tac B) |
|
13566 | 314 |
apply (rule_tac u="{B,n,0,Memrel(succ(n))}" |
315 |
in gen_separation [OF formula_replacement1_Reflects], |
|
316 |
simp add: nonempty) |
|
317 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13386 | 318 |
apply (rule DPow_LsetI) |
319 |
apply (rule bex_iff_sats conj_iff_sats)+ |
|
13566 | 320 |
apply (rule_tac env = "[u,x,n,B,0,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 321 |
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
13441 | 322 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13386 | 323 |
done |
324 |
||
325 |
lemma formula_replacement2_Reflects: |
|
326 |
"REFLECTS |
|
327 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and> |
|
328 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and> |
|
329 |
is_wfrec (L, iterates_MH (L, is_formula_functor(L), 0), |
|
330 |
msn, u, x)), |
|
331 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
|
13428 | 332 |
(\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). |
13386 | 333 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 334 |
is_wfrec (**Lset(i), |
13386 | 335 |
iterates_MH (**Lset(i), is_formula_functor(**Lset(i)), 0), |
336 |
msn, u, x))]" |
|
13428 | 337 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
338 |
iterates_MH_reflection formula_functor_reflection) |
|
13386 | 339 |
|
340 |
||
13428 | 341 |
lemma formula_replacement2: |
342 |
"strong_replacement(L, |
|
343 |
\<lambda>n y. n\<in>nat & |
|
13386 | 344 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 345 |
is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0), |
13386 | 346 |
msn, n, y)))" |
13428 | 347 |
apply (rule strong_replacementI) |
348 |
apply (rename_tac B) |
|
13566 | 349 |
apply (rule_tac u="{B,0,nat}" |
350 |
in gen_separation [OF formula_replacement2_Reflects], |
|
351 |
simp add: nonempty L_nat) |
|
352 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13386 | 353 |
apply (rule DPow_LsetI) |
354 |
apply (rule bex_iff_sats conj_iff_sats)+ |
|
13566 | 355 |
apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats) |
13434 | 356 |
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
13441 | 357 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13386 | 358 |
done |
359 |
||
360 |
text{*NB The proofs for type @{term formula} are virtually identical to those |
|
361 |
for @{term "list(A)"}. It was a cut-and-paste job! *} |
|
362 |
||
13387 | 363 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
364 |
subsubsection{*The Formula @{term is_nth}, Internalized*} |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
365 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
366 |
(* "is_nth(M,n,l,Z) == |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
367 |
\<exists>X[M]. \<exists>sn[M]. \<exists>msn[M]. |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
368 |
2 1 0 |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
369 |
successor(M,n,sn) & membership(M,sn,msn) & |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
370 |
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
|
371 |
is_hd(M,X,Z)" *) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
372 |
constdefs nth_fm :: "[i,i,i]=>i" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
373 |
"nth_fm(n,l,Z) == |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
374 |
Exists(Exists(Exists( |
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
375 |
And(succ_fm(n#+3,1), |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
376 |
And(Memrel_fm(1,0), |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
377 |
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
|
378 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
379 |
lemma nth_fm_type [TC]: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
380 |
"[| 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
|
381 |
by (simp add: nth_fm_def) |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
382 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
383 |
lemma sats_nth_fm [simp]: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
384 |
"[| 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
|
385 |
==> sats(A, nth_fm(x,y,z), env) <-> |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
386 |
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
|
387 |
apply (frule lt_length_in_nat, assumption) |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
388 |
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
|
389 |
done |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
390 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
391 |
lemma nth_iff_sats: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
392 |
"[| 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
|
393 |
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
|
394 |
==> 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
|
395 |
by (simp add: sats_nth_fm) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
396 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
397 |
theorem nth_reflection: |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
398 |
"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
|
399 |
\<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
|
400 |
apply (simp only: is_nth_def setclass_simps) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
401 |
apply (intro FOL_reflections function_reflections is_wfrec_reflection |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
402 |
iterates_MH_reflection hd_reflection tl_reflection) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
403 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
404 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
405 |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
406 |
subsubsection{*An Instance of Replacement for @{term nth}*} |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
407 |
|
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
408 |
lemma nth_replacement_Reflects: |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
409 |
"REFLECTS |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
410 |
[\<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
|
411 |
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
|
412 |
\<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 | 413 |
is_wfrec(**Lset(i), |
414 |
iterates_MH(**Lset(i), |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
415 |
is_tl(**Lset(i)), z), memsn, u, y))]" |
13428 | 416 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
417 |
iterates_MH_reflection list_functor_reflection tl_reflection) |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
418 |
|
13428 | 419 |
lemma nth_replacement: |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
420 |
"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
|
421 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
13428 | 422 |
apply (rule strong_replacementI) |
13566 | 423 |
apply (rule_tac u="{A,n,w,Memrel(succ(n))}" |
424 |
in gen_separation [OF nth_replacement_Reflects], |
|
425 |
simp add: nonempty) |
|
426 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
427 |
apply (rule DPow_LsetI) |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
428 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 429 |
apply (rule_tac env = "[u,x,A,w,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 430 |
apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats |
13441 | 431 |
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
|
432 |
done |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
433 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
434 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
435 |
subsubsection{*Instantiating the locale @{text M_datatypes}*} |
13428 | 436 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
437 |
lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)" |
13428 | 438 |
apply (rule M_datatypes_axioms.intro) |
439 |
apply (assumption | rule |
|
440 |
list_replacement1 list_replacement2 |
|
441 |
formula_replacement1 formula_replacement2 |
|
442 |
nth_replacement)+ |
|
443 |
done |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
444 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
445 |
theorem M_datatypes_L: "PROP M_datatypes(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
446 |
apply (rule M_datatypes.intro) |
13634 | 447 |
apply (rule M_trancl.axioms [OF M_trancl_L])+ |
13441 | 448 |
apply (rule M_datatypes_axioms_L) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
449 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
450 |
|
13428 | 451 |
lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L] |
452 |
and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L] |
|
453 |
and list_abs = M_datatypes.list_abs [OF M_datatypes_L] |
|
454 |
and formula_abs = M_datatypes.formula_abs [OF M_datatypes_L] |
|
455 |
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
|
456 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
457 |
declare list_closed [intro,simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
458 |
declare formula_closed [intro,simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
459 |
declare list_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
460 |
declare formula_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
461 |
declare nth_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
462 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
463 |
|
13428 | 464 |
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
|
465 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
466 |
subsubsection{*Instances of Replacement for @{term eclose}*} |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
467 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
468 |
lemma eclose_replacement1_Reflects: |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
469 |
"REFLECTS |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
470 |
[\<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
|
471 |
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
|
472 |
\<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 | 473 |
is_wfrec(**Lset(i), |
474 |
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
|
475 |
memsn, u, y))]" |
13428 | 476 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
477 |
iterates_MH_reflection) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
478 |
|
13428 | 479 |
lemma eclose_replacement1: |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
480 |
"L(A) ==> iterates_replacement(L, big_union(L), A)" |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
481 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
13428 | 482 |
apply (rule strong_replacementI) |
483 |
apply (rename_tac B) |
|
13566 | 484 |
apply (rule_tac u="{B,A,n,Memrel(succ(n))}" |
485 |
in gen_separation [OF eclose_replacement1_Reflects], simp) |
|
486 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
487 |
apply (rule DPow_LsetI) |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
488 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 489 |
apply (rule_tac env = "[u,x,A,n,B,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 490 |
apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats |
13441 | 491 |
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
|
492 |
done |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
493 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
494 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
495 |
lemma eclose_replacement2_Reflects: |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
496 |
"REFLECTS |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
497 |
[\<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
|
498 |
(\<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
|
499 |
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
|
500 |
msn, u, x)), |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
501 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
13428 | 502 |
(\<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
|
503 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 504 |
is_wfrec (**Lset(i), |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
505 |
iterates_MH (**Lset(i), big_union(**Lset(i)), A), |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
506 |
msn, u, x))]" |
13428 | 507 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
508 |
iterates_MH_reflection) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
509 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
510 |
|
13428 | 511 |
lemma eclose_replacement2: |
512 |
"L(A) ==> strong_replacement(L, |
|
513 |
\<lambda>n y. n\<in>nat & |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
514 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 515 |
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
|
516 |
msn, n, y)))" |
13428 | 517 |
apply (rule strong_replacementI) |
518 |
apply (rename_tac B) |
|
13566 | 519 |
apply (rule_tac u="{A,B,nat}" |
520 |
in gen_separation [OF eclose_replacement2_Reflects], simp add: L_nat) |
|
521 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
522 |
apply (rule DPow_LsetI) |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
523 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 524 |
apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats) |
13434 | 525 |
apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats |
13441 | 526 |
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
|
527 |
done |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
528 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
529 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
530 |
subsubsection{*Instantiating the locale @{text M_eclose}*} |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
531 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
532 |
lemma M_eclose_axioms_L: "M_eclose_axioms(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
533 |
apply (rule M_eclose_axioms.intro) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
534 |
apply (assumption | rule eclose_replacement1 eclose_replacement2)+ |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
535 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
536 |
|
13428 | 537 |
theorem M_eclose_L: "PROP M_eclose(L)" |
538 |
apply (rule M_eclose.intro) |
|
13429 | 539 |
apply (rule M_datatypes.axioms [OF M_datatypes_L])+ |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
540 |
apply (rule M_eclose_axioms_L) |
13428 | 541 |
done |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
542 |
|
13428 | 543 |
lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L] |
544 |
and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L] |
|
13440 | 545 |
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
|
546 |
|
13348 | 547 |
end |