author | paulson |
Mon, 14 Oct 2002 11:32:00 +0200 | |
changeset 13647 | 7f6f0ffc45c3 |
parent 13634 | 99a593b49b04 |
child 13651 | ac80e101306a |
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 trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L] |
|
208 |
and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L] |
|
13363 | 209 |
|
210 |
||
211 |
||
13428 | 212 |
subsection{*@{term L} is Closed Under the Operator @{term list}*} |
13363 | 213 |
|
13386 | 214 |
subsubsection{*Instances of Replacement for Lists*} |
215 |
||
13363 | 216 |
lemma list_replacement1_Reflects: |
217 |
"REFLECTS |
|
218 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
|
219 |
is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)), |
|
220 |
\<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 | 221 |
is_wfrec(**Lset(i), |
222 |
iterates_MH(**Lset(i), |
|
13363 | 223 |
is_list_functor(**Lset(i), A), 0), memsn, u, y))]" |
13428 | 224 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
225 |
iterates_MH_reflection list_functor_reflection) |
|
13363 | 226 |
|
13441 | 227 |
|
13428 | 228 |
lemma list_replacement1: |
13363 | 229 |
"L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" |
230 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
13428 | 231 |
apply (rule strong_replacementI) |
232 |
apply (rename_tac B) |
|
13566 | 233 |
apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" |
234 |
in gen_separation [OF list_replacement1_Reflects], |
|
235 |
simp add: nonempty) |
|
236 |
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
|
237 |
apply (rule DPow_LsetI) |
13363 | 238 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 239 |
apply (rule_tac env = "[u,x,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 240 |
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
13441 | 241 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13363 | 242 |
done |
243 |
||
13441 | 244 |
|
13363 | 245 |
lemma list_replacement2_Reflects: |
246 |
"REFLECTS |
|
247 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and> |
|
248 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and> |
|
249 |
is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0), |
|
250 |
msn, u, x)), |
|
251 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
|
13428 | 252 |
(\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). |
13363 | 253 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 254 |
is_wfrec (**Lset(i), |
13363 | 255 |
iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0), |
256 |
msn, u, x))]" |
|
13428 | 257 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
258 |
iterates_MH_reflection list_functor_reflection) |
|
13363 | 259 |
|
260 |
||
13428 | 261 |
lemma list_replacement2: |
262 |
"L(A) ==> strong_replacement(L, |
|
263 |
\<lambda>n y. n\<in>nat & |
|
13363 | 264 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 265 |
is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), |
13363 | 266 |
msn, n, y)))" |
13428 | 267 |
apply (rule strong_replacementI) |
268 |
apply (rename_tac B) |
|
13566 | 269 |
apply (rule_tac u="{A,B,0,nat}" |
270 |
in gen_separation [OF list_replacement2_Reflects], |
|
271 |
simp add: L_nat nonempty) |
|
272 |
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
|
273 |
apply (rule DPow_LsetI) |
13363 | 274 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 275 |
apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats) |
13434 | 276 |
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
13441 | 277 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13363 | 278 |
done |
279 |
||
13386 | 280 |
|
13428 | 281 |
subsection{*@{term L} is Closed Under the Operator @{term formula}*} |
13386 | 282 |
|
283 |
subsubsection{*Instances of Replacement for Formulas*} |
|
284 |
||
285 |
lemma formula_replacement1_Reflects: |
|
286 |
"REFLECTS |
|
287 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
|
288 |
is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)), |
|
289 |
\<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 | 290 |
is_wfrec(**Lset(i), |
291 |
iterates_MH(**Lset(i), |
|
13386 | 292 |
is_formula_functor(**Lset(i)), 0), memsn, u, y))]" |
13428 | 293 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
294 |
iterates_MH_reflection formula_functor_reflection) |
|
13386 | 295 |
|
13428 | 296 |
lemma formula_replacement1: |
13386 | 297 |
"iterates_replacement(L, is_formula_functor(L), 0)" |
298 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
13428 | 299 |
apply (rule strong_replacementI) |
300 |
apply (rename_tac B) |
|
13566 | 301 |
apply (rule_tac u="{B,n,0,Memrel(succ(n))}" |
302 |
in gen_separation [OF formula_replacement1_Reflects], |
|
303 |
simp add: nonempty) |
|
304 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13386 | 305 |
apply (rule DPow_LsetI) |
306 |
apply (rule bex_iff_sats conj_iff_sats)+ |
|
13566 | 307 |
apply (rule_tac env = "[u,x,n,B,0,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 308 |
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
13441 | 309 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13386 | 310 |
done |
311 |
||
312 |
lemma formula_replacement2_Reflects: |
|
313 |
"REFLECTS |
|
314 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and> |
|
315 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and> |
|
316 |
is_wfrec (L, iterates_MH (L, is_formula_functor(L), 0), |
|
317 |
msn, u, x)), |
|
318 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
|
13428 | 319 |
(\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). |
13386 | 320 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 321 |
is_wfrec (**Lset(i), |
13386 | 322 |
iterates_MH (**Lset(i), is_formula_functor(**Lset(i)), 0), |
323 |
msn, u, x))]" |
|
13428 | 324 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
325 |
iterates_MH_reflection formula_functor_reflection) |
|
13386 | 326 |
|
327 |
||
13428 | 328 |
lemma formula_replacement2: |
329 |
"strong_replacement(L, |
|
330 |
\<lambda>n y. n\<in>nat & |
|
13386 | 331 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 332 |
is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0), |
13386 | 333 |
msn, n, y)))" |
13428 | 334 |
apply (rule strong_replacementI) |
335 |
apply (rename_tac B) |
|
13566 | 336 |
apply (rule_tac u="{B,0,nat}" |
337 |
in gen_separation [OF formula_replacement2_Reflects], |
|
338 |
simp add: nonempty L_nat) |
|
339 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13386 | 340 |
apply (rule DPow_LsetI) |
341 |
apply (rule bex_iff_sats conj_iff_sats)+ |
|
13566 | 342 |
apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats) |
13434 | 343 |
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
13441 | 344 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13386 | 345 |
done |
346 |
||
347 |
text{*NB The proofs for type @{term formula} are virtually identical to those |
|
348 |
for @{term "list(A)"}. It was a cut-and-paste job! *} |
|
349 |
||
13387 | 350 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
351 |
subsubsection{*The Formula @{term is_nth}, Internalized*} |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
352 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
353 |
(* "is_nth(M,n,l,Z) == |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
354 |
\<exists>X[M]. \<exists>sn[M]. \<exists>msn[M]. |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
355 |
2 1 0 |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
356 |
successor(M,n,sn) & membership(M,sn,msn) & |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
357 |
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
|
358 |
is_hd(M,X,Z)" *) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
359 |
constdefs nth_fm :: "[i,i,i]=>i" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
360 |
"nth_fm(n,l,Z) == |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
361 |
Exists(Exists(Exists( |
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
362 |
And(succ_fm(n#+3,1), |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
363 |
And(Memrel_fm(1,0), |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
364 |
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
|
365 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
366 |
lemma nth_fm_type [TC]: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
367 |
"[| 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
|
368 |
by (simp add: nth_fm_def) |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
369 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
370 |
lemma sats_nth_fm [simp]: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
371 |
"[| 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
|
372 |
==> sats(A, nth_fm(x,y,z), env) <-> |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
373 |
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
|
374 |
apply (frule lt_length_in_nat, assumption) |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
375 |
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
|
376 |
done |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
377 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
378 |
lemma nth_iff_sats: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
379 |
"[| 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
|
380 |
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
|
381 |
==> 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
|
382 |
by (simp add: sats_nth_fm) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
383 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
384 |
theorem nth_reflection: |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
385 |
"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
|
386 |
\<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
|
387 |
apply (simp only: is_nth_def setclass_simps) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
388 |
apply (intro FOL_reflections function_reflections is_wfrec_reflection |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
389 |
iterates_MH_reflection hd_reflection tl_reflection) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
390 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
391 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
392 |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
393 |
subsubsection{*An Instance of Replacement for @{term nth}*} |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
394 |
|
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
395 |
lemma nth_replacement_Reflects: |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
396 |
"REFLECTS |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
397 |
[\<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
|
398 |
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
|
399 |
\<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 | 400 |
is_wfrec(**Lset(i), |
401 |
iterates_MH(**Lset(i), |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
402 |
is_tl(**Lset(i)), z), memsn, u, y))]" |
13428 | 403 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
404 |
iterates_MH_reflection list_functor_reflection tl_reflection) |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
405 |
|
13428 | 406 |
lemma nth_replacement: |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
407 |
"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
|
408 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
13428 | 409 |
apply (rule strong_replacementI) |
13566 | 410 |
apply (rule_tac u="{A,n,w,Memrel(succ(n))}" |
411 |
in gen_separation [OF nth_replacement_Reflects], |
|
412 |
simp add: nonempty) |
|
413 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
414 |
apply (rule DPow_LsetI) |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
415 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 416 |
apply (rule_tac env = "[u,x,A,w,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 417 |
apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats |
13441 | 418 |
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
|
419 |
done |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
420 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
421 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
422 |
subsubsection{*Instantiating the locale @{text M_datatypes}*} |
13428 | 423 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
424 |
lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)" |
13428 | 425 |
apply (rule M_datatypes_axioms.intro) |
426 |
apply (assumption | rule |
|
427 |
list_replacement1 list_replacement2 |
|
428 |
formula_replacement1 formula_replacement2 |
|
429 |
nth_replacement)+ |
|
430 |
done |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
431 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
432 |
theorem M_datatypes_L: "PROP M_datatypes(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
433 |
apply (rule M_datatypes.intro) |
13634 | 434 |
apply (rule M_trancl.axioms [OF M_trancl_L])+ |
13441 | 435 |
apply (rule M_datatypes_axioms_L) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
436 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
437 |
|
13428 | 438 |
lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L] |
439 |
and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L] |
|
440 |
and list_abs = M_datatypes.list_abs [OF M_datatypes_L] |
|
441 |
and formula_abs = M_datatypes.formula_abs [OF M_datatypes_L] |
|
442 |
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
|
443 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
444 |
declare list_closed [intro,simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
445 |
declare formula_closed [intro,simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
446 |
declare list_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
447 |
declare formula_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
448 |
declare nth_abs [simp] |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
449 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
450 |
|
13428 | 451 |
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
|
452 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
453 |
subsubsection{*Instances of Replacement for @{term eclose}*} |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
454 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
455 |
lemma eclose_replacement1_Reflects: |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
456 |
"REFLECTS |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
457 |
[\<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
|
458 |
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
|
459 |
\<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 | 460 |
is_wfrec(**Lset(i), |
461 |
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
|
462 |
memsn, u, y))]" |
13428 | 463 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
464 |
iterates_MH_reflection) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
465 |
|
13428 | 466 |
lemma eclose_replacement1: |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
467 |
"L(A) ==> iterates_replacement(L, big_union(L), A)" |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
468 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
13428 | 469 |
apply (rule strong_replacementI) |
470 |
apply (rename_tac B) |
|
13566 | 471 |
apply (rule_tac u="{B,A,n,Memrel(succ(n))}" |
472 |
in gen_separation [OF eclose_replacement1_Reflects], simp) |
|
473 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
474 |
apply (rule DPow_LsetI) |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
475 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 476 |
apply (rule_tac env = "[u,x,A,n,B,Memrel(succ(n))]" in mem_iff_sats) |
13434 | 477 |
apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats |
13441 | 478 |
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
|
479 |
done |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
480 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
481 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
482 |
lemma eclose_replacement2_Reflects: |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
483 |
"REFLECTS |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
484 |
[\<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
|
485 |
(\<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
|
486 |
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
|
487 |
msn, u, x)), |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
488 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
13428 | 489 |
(\<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
|
490 |
successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
13428 | 491 |
is_wfrec (**Lset(i), |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
492 |
iterates_MH (**Lset(i), big_union(**Lset(i)), A), |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
493 |
msn, u, x))]" |
13428 | 494 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
495 |
iterates_MH_reflection) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
496 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
497 |
|
13428 | 498 |
lemma eclose_replacement2: |
499 |
"L(A) ==> strong_replacement(L, |
|
500 |
\<lambda>n y. n\<in>nat & |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
501 |
(\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
13428 | 502 |
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
|
503 |
msn, n, y)))" |
13428 | 504 |
apply (rule strong_replacementI) |
505 |
apply (rename_tac B) |
|
13566 | 506 |
apply (rule_tac u="{A,B,nat}" |
507 |
in gen_separation [OF eclose_replacement2_Reflects], simp add: L_nat) |
|
508 |
apply (drule mem_Lset_imp_subset_Lset, clarsimp) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
509 |
apply (rule DPow_LsetI) |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
510 |
apply (rule bex_iff_sats conj_iff_sats)+ |
13566 | 511 |
apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats) |
13434 | 512 |
apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats |
13441 | 513 |
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
|
514 |
done |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
515 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
516 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
517 |
subsubsection{*Instantiating the locale @{text M_eclose}*} |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
518 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
519 |
lemma M_eclose_axioms_L: "M_eclose_axioms(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
520 |
apply (rule M_eclose_axioms.intro) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
521 |
apply (assumption | rule eclose_replacement1 eclose_replacement2)+ |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
522 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
523 |
|
13428 | 524 |
theorem M_eclose_L: "PROP M_eclose(L)" |
525 |
apply (rule M_eclose.intro) |
|
13429 | 526 |
apply (rule M_datatypes.axioms [OF M_datatypes_L])+ |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
527 |
apply (rule M_eclose_axioms_L) |
13428 | 528 |
done |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
529 |
|
13428 | 530 |
lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L] |
531 |
and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L] |
|
13440 | 532 |
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
|
533 |
|
13348 | 534 |
end |