author | wenzelm |
Tue, 07 Nov 2006 19:40:13 +0100 | |
changeset 21233 | 5a5c8ea5f66a |
parent 19931 | fb32b43e7f80 |
child 21404 | eb85850d3eb7 |
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 |
|
16417 | 8 |
theory Rec_Separation imports Separation Internalize begin |
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)))"*) |
|
21233 | 33 |
definition 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 sats_rtran_closure_mem_fm [simp]: |
|
57 |
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
13428 | 58 |
==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
59 |
rtran_closure_mem(##A, nth(x,env), nth(y,env), nth(z,env))" |
13348 | 60 |
by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def) |
61 |
||
62 |
lemma rtran_closure_mem_iff_sats: |
|
13428 | 63 |
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
13348 | 64 |
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
65 |
==> rtran_closure_mem(##A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)" |
13348 | 66 |
by (simp add: sats_rtran_closure_mem_fm) |
67 |
||
13566 | 68 |
lemma rtran_closure_mem_reflection: |
13428 | 69 |
"REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)), |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
70 |
\<lambda>i x. rtran_closure_mem(##Lset(i),f(x),g(x),h(x))]" |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
71 |
apply (simp only: rtran_closure_mem_def) |
13428 | 72 |
apply (intro FOL_reflections function_reflections fun_plus_reflections) |
13348 | 73 |
done |
74 |
||
75 |
text{*Separation for @{term "rtrancl(r)"}.*} |
|
76 |
lemma rtrancl_separation: |
|
77 |
"[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))" |
|
13687 | 78 |
apply (rule gen_separation_multi [OF rtran_closure_mem_reflection, of "{r,A}"], |
79 |
auto) |
|
80 |
apply (rule_tac env="[r,A]" in DPow_LsetI) |
|
81 |
apply (rule rtran_closure_mem_iff_sats sep_rules | simp)+ |
|
13348 | 82 |
done |
83 |
||
84 |
||
85 |
subsubsection{*Reflexive/Transitive Closure, Internalized*} |
|
86 |
||
13428 | 87 |
(* "rtran_closure(M,r,s) == |
13348 | 88 |
\<forall>A[M]. is_field(M,r,A) --> |
13428 | 89 |
(\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *) |
21233 | 90 |
definition rtran_closure_fm :: "[i,i]=>i" |
13428 | 91 |
"rtran_closure_fm(r,s) == |
13348 | 92 |
Forall(Implies(field_fm(succ(r),0), |
93 |
Forall(Iff(Member(0,succ(succ(s))), |
|
94 |
rtran_closure_mem_fm(1,succ(succ(r)),0)))))" |
|
95 |
||
96 |
lemma rtran_closure_type [TC]: |
|
97 |
"[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula" |
|
13428 | 98 |
by (simp add: rtran_closure_fm_def) |
13348 | 99 |
|
100 |
lemma sats_rtran_closure_fm [simp]: |
|
101 |
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
|
13428 | 102 |
==> sats(A, rtran_closure_fm(x,y), env) <-> |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
103 |
rtran_closure(##A, nth(x,env), nth(y,env))" |
13348 | 104 |
by (simp add: rtran_closure_fm_def rtran_closure_def) |
105 |
||
106 |
lemma rtran_closure_iff_sats: |
|
13428 | 107 |
"[| nth(i,env) = x; nth(j,env) = y; |
13348 | 108 |
i \<in> nat; j \<in> nat; env \<in> list(A)|] |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
109 |
==> rtran_closure(##A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)" |
13348 | 110 |
by simp |
111 |
||
112 |
theorem rtran_closure_reflection: |
|
13428 | 113 |
"REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)), |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
114 |
\<lambda>i x. rtran_closure(##Lset(i),f(x),g(x))]" |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
115 |
apply (simp only: rtran_closure_def) |
13348 | 116 |
apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection) |
117 |
done |
|
118 |
||
119 |
||
120 |
subsubsection{*Transitive Closure of a Relation, Internalized*} |
|
121 |
||
122 |
(* "tran_closure(M,r,t) == |
|
123 |
\<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *) |
|
21233 | 124 |
definition tran_closure_fm :: "[i,i]=>i" |
13428 | 125 |
"tran_closure_fm(r,s) == |
13348 | 126 |
Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" |
127 |
||
128 |
lemma tran_closure_type [TC]: |
|
129 |
"[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula" |
|
13428 | 130 |
by (simp add: tran_closure_fm_def) |
13348 | 131 |
|
132 |
lemma sats_tran_closure_fm [simp]: |
|
133 |
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
|
13428 | 134 |
==> sats(A, tran_closure_fm(x,y), env) <-> |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
135 |
tran_closure(##A, nth(x,env), nth(y,env))" |
13348 | 136 |
by (simp add: tran_closure_fm_def tran_closure_def) |
137 |
||
138 |
lemma tran_closure_iff_sats: |
|
13428 | 139 |
"[| nth(i,env) = x; nth(j,env) = y; |
13348 | 140 |
i \<in> nat; j \<in> nat; env \<in> list(A)|] |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
141 |
==> tran_closure(##A, x, y) <-> sats(A, tran_closure_fm(i,j), env)" |
13348 | 142 |
by simp |
143 |
||
144 |
theorem tran_closure_reflection: |
|
13428 | 145 |
"REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)), |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
146 |
\<lambda>i x. tran_closure(##Lset(i),f(x),g(x))]" |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
147 |
apply (simp only: tran_closure_def) |
13428 | 148 |
apply (intro FOL_reflections function_reflections |
13348 | 149 |
rtran_closure_reflection composition_reflection) |
150 |
done |
|
151 |
||
152 |
||
13506 | 153 |
subsubsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*} |
13348 | 154 |
|
155 |
lemma wellfounded_trancl_reflects: |
|
13428 | 156 |
"REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. |
157 |
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp, |
|
158 |
\<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i). |
|
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
159 |
w \<in> Z & pair(##Lset(i),w,x,wx) & tran_closure(##Lset(i),r,rp) & |
13348 | 160 |
wx \<in> rp]" |
13428 | 161 |
by (intro FOL_reflections function_reflections fun_plus_reflections |
13348 | 162 |
tran_closure_reflection) |
163 |
||
164 |
lemma wellfounded_trancl_separation: |
|
13428 | 165 |
"[| L(r); L(Z) |] ==> |
166 |
separation (L, \<lambda>x. |
|
167 |
\<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. |
|
168 |
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)" |
|
13687 | 169 |
apply (rule gen_separation_multi [OF wellfounded_trancl_reflects, of "{r,Z}"], |
170 |
auto) |
|
171 |
apply (rule_tac env="[r,Z]" in DPow_LsetI) |
|
13348 | 172 |
apply (rule sep_rules tran_closure_iff_sats | simp)+ |
173 |
done |
|
174 |
||
13363 | 175 |
|
176 |
subsubsection{*Instantiating the locale @{text M_trancl}*} |
|
13428 | 177 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
178 |
lemma M_trancl_axioms_L: "M_trancl_axioms(L)" |
13428 | 179 |
apply (rule M_trancl_axioms.intro) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
180 |
apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+ |
13428 | 181 |
done |
13363 | 182 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
183 |
theorem M_trancl_L: "PROP M_trancl(L)" |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
184 |
by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L]) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
185 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
186 |
interpretation M_trancl [L] by (rule M_trancl_L) |
13363 | 187 |
|
188 |
||
13428 | 189 |
subsection{*@{term L} is Closed Under the Operator @{term list}*} |
13363 | 190 |
|
13386 | 191 |
subsubsection{*Instances of Replacement for Lists*} |
192 |
||
13363 | 193 |
lemma list_replacement1_Reflects: |
194 |
"REFLECTS |
|
195 |
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
|
196 |
is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)), |
|
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
197 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and> |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
198 |
is_wfrec(##Lset(i), |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
199 |
iterates_MH(##Lset(i), |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
200 |
is_list_functor(##Lset(i), A), 0), memsn, u, y))]" |
13428 | 201 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
202 |
iterates_MH_reflection list_functor_reflection) |
|
13363 | 203 |
|
13441 | 204 |
|
13428 | 205 |
lemma list_replacement1: |
13363 | 206 |
"L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" |
207 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
13428 | 208 |
apply (rule strong_replacementI) |
13566 | 209 |
apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" |
13687 | 210 |
in gen_separation_multi [OF list_replacement1_Reflects], |
211 |
auto simp add: nonempty) |
|
212 |
apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI) |
|
13434 | 213 |
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
13441 | 214 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13363 | 215 |
done |
216 |
||
13441 | 217 |
|
13363 | 218 |
lemma list_replacement2_Reflects: |
219 |
"REFLECTS |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
220 |
[\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat & |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
221 |
is_iterates(L, is_list_functor(L, A), 0, u, x), |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
222 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat & |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
223 |
is_iterates(##Lset(i), is_list_functor(##Lset(i), A), 0, u, x)]" |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
224 |
by (intro FOL_reflections |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
225 |
is_iterates_reflection list_functor_reflection) |
13363 | 226 |
|
13428 | 227 |
lemma list_replacement2: |
228 |
"L(A) ==> strong_replacement(L, |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
229 |
\<lambda>n y. n\<in>nat & is_iterates(L, is_list_functor(L,A), 0, n, y))" |
13428 | 230 |
apply (rule strong_replacementI) |
13566 | 231 |
apply (rule_tac u="{A,B,0,nat}" |
13687 | 232 |
in gen_separation_multi [OF list_replacement2_Reflects], |
233 |
auto simp add: L_nat nonempty) |
|
234 |
apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI) |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
235 |
apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+ |
13363 | 236 |
done |
237 |
||
13386 | 238 |
|
13428 | 239 |
subsection{*@{term L} is Closed Under the Operator @{term formula}*} |
13386 | 240 |
|
241 |
subsubsection{*Instances of Replacement for Formulas*} |
|
242 |
||
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
243 |
(*FIXME: could prove a lemma iterates_replacementI to eliminate the |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
244 |
need to expand iterates_replacement and wfrec_replacement*) |
13386 | 245 |
lemma formula_replacement1_Reflects: |
246 |
"REFLECTS |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
247 |
[\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) & |
13386 | 248 |
is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)), |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
249 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
250 |
is_wfrec(##Lset(i), |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
251 |
iterates_MH(##Lset(i), |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
252 |
is_formula_functor(##Lset(i)), 0), memsn, u, y))]" |
13428 | 253 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
254 |
iterates_MH_reflection formula_functor_reflection) |
|
13386 | 255 |
|
13428 | 256 |
lemma formula_replacement1: |
13386 | 257 |
"iterates_replacement(L, is_formula_functor(L), 0)" |
258 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
13428 | 259 |
apply (rule strong_replacementI) |
13566 | 260 |
apply (rule_tac u="{B,n,0,Memrel(succ(n))}" |
13687 | 261 |
in gen_separation_multi [OF formula_replacement1_Reflects], |
262 |
auto simp add: nonempty) |
|
263 |
apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI) |
|
13434 | 264 |
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
13441 | 265 |
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
13386 | 266 |
done |
267 |
||
268 |
lemma formula_replacement2_Reflects: |
|
269 |
"REFLECTS |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
270 |
[\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat & |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
271 |
is_iterates(L, is_formula_functor(L), 0, u, x), |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
272 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat & |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
273 |
is_iterates(##Lset(i), is_formula_functor(##Lset(i)), 0, u, x)]" |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
274 |
by (intro FOL_reflections |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
275 |
is_iterates_reflection formula_functor_reflection) |
13386 | 276 |
|
13428 | 277 |
lemma formula_replacement2: |
278 |
"strong_replacement(L, |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
279 |
\<lambda>n y. n\<in>nat & is_iterates(L, is_formula_functor(L), 0, n, y))" |
13428 | 280 |
apply (rule strong_replacementI) |
13566 | 281 |
apply (rule_tac u="{B,0,nat}" |
13687 | 282 |
in gen_separation_multi [OF formula_replacement2_Reflects], |
283 |
auto simp add: nonempty L_nat) |
|
284 |
apply (rule_tac env="[B,0,nat]" in DPow_LsetI) |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
285 |
apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+ |
13386 | 286 |
done |
287 |
||
288 |
text{*NB The proofs for type @{term formula} are virtually identical to those |
|
289 |
for @{term "list(A)"}. It was a cut-and-paste job! *} |
|
290 |
||
13387 | 291 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
292 |
subsubsection{*The Formula @{term is_nth}, Internalized*} |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
293 |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
294 |
(* "is_nth(M,n,l,Z) == |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
295 |
\<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *) |
21233 | 296 |
definition nth_fm :: "[i,i,i]=>i" |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
297 |
"nth_fm(n,l,Z) == |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
298 |
Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0), |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
299 |
hd_fm(0,succ(Z))))" |
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
300 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
301 |
lemma nth_fm_type [TC]: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
302 |
"[| 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
|
303 |
by (simp add: nth_fm_def) |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
304 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
305 |
lemma sats_nth_fm [simp]: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
306 |
"[| 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
|
307 |
==> sats(A, nth_fm(x,y,z), env) <-> |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
308 |
is_nth(##A, nth(x,env), nth(y,env), nth(z,env))" |
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
309 |
apply (frule lt_length_in_nat, assumption) |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
310 |
apply (simp add: nth_fm_def is_nth_def sats_is_iterates_fm) |
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
311 |
done |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
312 |
|
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
313 |
lemma nth_iff_sats: |
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
314 |
"[| 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
|
315 |
i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|] |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
316 |
==> is_nth(##A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)" |
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset
|
317 |
by (simp add: sats_nth_fm) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
318 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
319 |
theorem nth_reflection: |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
320 |
"REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)), |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
321 |
\<lambda>i x. is_nth(##Lset(i), f(x), g(x), h(x))]" |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
322 |
apply (simp only: is_nth_def) |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
323 |
apply (intro FOL_reflections is_iterates_reflection |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
324 |
hd_reflection tl_reflection) |
13437
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 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
327 |
|
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
328 |
subsubsection{*An Instance of Replacement for @{term nth}*} |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
329 |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
330 |
(*FIXME: could prove a lemma iterates_replacementI to eliminate the |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
331 |
need to expand iterates_replacement and wfrec_replacement*) |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
332 |
lemma nth_replacement_Reflects: |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
333 |
"REFLECTS |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
334 |
[\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) & |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
335 |
is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)), |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
336 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
337 |
is_wfrec(##Lset(i), |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
338 |
iterates_MH(##Lset(i), |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
339 |
is_tl(##Lset(i)), z), memsn, u, y))]" |
13428 | 340 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
341 |
iterates_MH_reflection tl_reflection) |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
342 |
|
13428 | 343 |
lemma nth_replacement: |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
344 |
"L(w) ==> iterates_replacement(L, is_tl(L), w)" |
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
345 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
13428 | 346 |
apply (rule strong_replacementI) |
13687 | 347 |
apply (rule_tac u="{B,w,Memrel(succ(n))}" |
348 |
in gen_separation_multi [OF nth_replacement_Reflects], |
|
349 |
auto) |
|
350 |
apply (rule_tac env="[B,w,Memrel(succ(n))]" in DPow_LsetI) |
|
13434 | 351 |
apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats |
13441 | 352 |
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
|
353 |
done |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
354 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
355 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
356 |
subsubsection{*Instantiating the locale @{text M_datatypes}*} |
13428 | 357 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
358 |
lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)" |
13428 | 359 |
apply (rule M_datatypes_axioms.intro) |
360 |
apply (assumption | rule |
|
361 |
list_replacement1 list_replacement2 |
|
362 |
formula_replacement1 formula_replacement2 |
|
363 |
nth_replacement)+ |
|
364 |
done |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
365 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
366 |
theorem M_datatypes_L: "PROP M_datatypes(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
367 |
apply (rule M_datatypes.intro) |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
368 |
apply (rule M_trancl_L) |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
369 |
apply (rule M_datatypes_axioms_L) |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
370 |
done |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
371 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
372 |
interpretation M_datatypes [L] by (rule M_datatypes_L) |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
373 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
374 |
|
13428 | 375 |
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
|
376 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
377 |
subsubsection{*Instances of Replacement for @{term eclose}*} |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
378 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
379 |
lemma eclose_replacement1_Reflects: |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
380 |
"REFLECTS |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
381 |
[\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) & |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
382 |
is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)), |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
383 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
384 |
is_wfrec(##Lset(i), |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
385 |
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
|
386 |
memsn, u, y))]" |
13428 | 387 |
by (intro FOL_reflections function_reflections is_wfrec_reflection |
388 |
iterates_MH_reflection) |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
389 |
|
13428 | 390 |
lemma eclose_replacement1: |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
391 |
"L(A) ==> iterates_replacement(L, big_union(L), A)" |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
392 |
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
13428 | 393 |
apply (rule strong_replacementI) |
13566 | 394 |
apply (rule_tac u="{B,A,n,Memrel(succ(n))}" |
13687 | 395 |
in gen_separation_multi [OF eclose_replacement1_Reflects], auto) |
396 |
apply (rule_tac env="[B,A,n,Memrel(succ(n))]" in DPow_LsetI) |
|
13434 | 397 |
apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats |
13441 | 398 |
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
|
399 |
done |
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset
|
400 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
401 |
|
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
402 |
lemma eclose_replacement2_Reflects: |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
403 |
"REFLECTS |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
404 |
[\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat & |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
405 |
is_iterates(L, big_union(L), A, u, x), |
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
406 |
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat & |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
407 |
is_iterates(##Lset(i), big_union(##Lset(i)), A, u, x)]" |
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
408 |
by (intro FOL_reflections function_reflections is_iterates_reflection) |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
409 |
|
13428 | 410 |
lemma eclose_replacement2: |
411 |
"L(A) ==> strong_replacement(L, |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
412 |
\<lambda>n y. n\<in>nat & is_iterates(L, big_union(L), A, n, y))" |
13428 | 413 |
apply (rule strong_replacementI) |
13566 | 414 |
apply (rule_tac u="{A,B,nat}" |
13687 | 415 |
in gen_separation_multi [OF eclose_replacement2_Reflects], |
416 |
auto simp add: L_nat) |
|
417 |
apply (rule_tac env="[A,B,nat]" in DPow_LsetI) |
|
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset
|
418 |
apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+ |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
419 |
done |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
420 |
|
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_eclose}*} |
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
423 |
|
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
424 |
lemma M_eclose_axioms_L: "M_eclose_axioms(L)" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
425 |
apply (rule M_eclose_axioms.intro) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
426 |
apply (assumption | rule eclose_replacement1 eclose_replacement2)+ |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
427 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
428 |
|
13428 | 429 |
theorem M_eclose_L: "PROP M_eclose(L)" |
430 |
apply (rule M_eclose.intro) |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
431 |
apply (rule M_datatypes_L) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset
|
432 |
apply (rule M_eclose_axioms_L) |
13428 | 433 |
done |
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
434 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
435 |
interpretation M_eclose [L] by (rule M_eclose_L) |
15766 | 436 |
|
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset
|
437 |
|
13348 | 438 |
end |