author | webertj |
Tue, 15 Jun 2004 00:06:40 +0200 | |
changeset 14942 | 78ddcbebace1 |
parent 13807 | a28a8fbc76d4 |
child 15766 | b08feb003f3c |
permissions | -rw-r--r-- |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
1 |
(* Title: ZF/Constructible/Separation.thy |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
2 |
ID: $Id$ |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
4 |
*) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
5 |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
6 |
header{*Early Instances of Separation and Strong Replacement*} |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
7 |
|
13324 | 8 |
theory Separation = L_axioms + WF_absolute: |
13306 | 9 |
|
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
10 |
text{*This theory proves all instances needed for locale @{text "M_basic"}*} |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset
|
11 |
|
13306 | 12 |
text{*Helps us solve for de Bruijn indices!*} |
13 |
lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x" |
|
14 |
by simp |
|
15 |
||
13316 | 16 |
lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI |
13428 | 17 |
lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
18 |
fun_plus_iff_sats |
13306 | 19 |
|
20 |
lemma Collect_conj_in_DPow: |
|
13428 | 21 |
"[| {x\<in>A. P(x)} \<in> DPow(A); {x\<in>A. Q(x)} \<in> DPow(A) |] |
13306 | 22 |
==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)" |
13428 | 23 |
by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric]) |
13306 | 24 |
|
25 |
lemma Collect_conj_in_DPow_Lset: |
|
26 |
"[|z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))|] |
|
27 |
==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> DPow(Lset(j))" |
|
28 |
apply (frule mem_Lset_imp_subset_Lset) |
|
13428 | 29 |
apply (simp add: Collect_conj_in_DPow Collect_mem_eq |
13306 | 30 |
subset_Int_iff2 elem_subset_in_DPow) |
31 |
done |
|
32 |
||
33 |
lemma separation_CollectI: |
|
34 |
"(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))" |
|
13428 | 35 |
apply (unfold separation_def, clarify) |
36 |
apply (rule_tac x="{x\<in>z. P(x)}" in rexI) |
|
13306 | 37 |
apply simp_all |
38 |
done |
|
39 |
||
40 |
text{*Reduces the original comprehension to the reflected one*} |
|
41 |
lemma reflection_imp_L_separation: |
|
42 |
"[| \<forall>x\<in>Lset(j). P(x) <-> Q(x); |
|
13428 | 43 |
{x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j)); |
13306 | 44 |
Ord(j); z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})" |
45 |
apply (rule_tac i = "succ(j)" in L_I) |
|
46 |
prefer 2 apply simp |
|
47 |
apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> z & (Q(x))}") |
|
48 |
prefer 2 |
|
13428 | 49 |
apply (blast dest: mem_Lset_imp_subset_Lset) |
13306 | 50 |
apply (simp add: Lset_succ Collect_conj_in_DPow_Lset) |
51 |
done |
|
52 |
||
13566 | 53 |
text{*Encapsulates the standard proof script for proving instances of |
13687 | 54 |
Separation.*} |
13566 | 55 |
lemma gen_separation: |
56 |
assumes reflection: "REFLECTS [P,Q]" |
|
57 |
and Lu: "L(u)" |
|
58 |
and collI: "!!j. u \<in> Lset(j) |
|
59 |
\<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))" |
|
60 |
shows "separation(L,P)" |
|
61 |
apply (rule separation_CollectI) |
|
62 |
apply (rule_tac A="{u,z}" in subset_LsetE, blast intro: Lu) |
|
63 |
apply (rule ReflectsE [OF reflection], assumption) |
|
64 |
apply (drule subset_Lset_ltD, assumption) |
|
65 |
apply (erule reflection_imp_L_separation) |
|
66 |
apply (simp_all add: lt_Ord2, clarify) |
|
13691 | 67 |
apply (rule collI, assumption) |
13687 | 68 |
done |
69 |
||
70 |
text{*As above, but typically @{term u} is a finite enumeration such as |
|
71 |
@{term "{a,b}"}; thus the new subgoal gets the assumption |
|
72 |
@{term "{a,b} \<subseteq> Lset(i)"}, which is logically equivalent to |
|
73 |
@{term "a \<in> Lset(i)"} and @{term "b \<in> Lset(i)"}.*} |
|
74 |
lemma gen_separation_multi: |
|
75 |
assumes reflection: "REFLECTS [P,Q]" |
|
76 |
and Lu: "L(u)" |
|
77 |
and collI: "!!j. u \<subseteq> Lset(j) |
|
78 |
\<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))" |
|
79 |
shows "separation(L,P)" |
|
80 |
apply (rule gen_separation [OF reflection Lu]) |
|
81 |
apply (drule mem_Lset_imp_subset_Lset) |
|
82 |
apply (erule collI) |
|
13566 | 83 |
done |
84 |
||
13306 | 85 |
|
13316 | 86 |
subsection{*Separation for Intersection*} |
13306 | 87 |
|
88 |
lemma Inter_Reflects: |
|
13428 | 89 |
"REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y, |
13314 | 90 |
\<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y]" |
13428 | 91 |
by (intro FOL_reflections) |
13306 | 92 |
|
93 |
lemma Inter_separation: |
|
94 |
"L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)" |
|
13566 | 95 |
apply (rule gen_separation [OF Inter_Reflects], simp) |
13428 | 96 |
apply (rule DPow_LsetI) |
13687 | 97 |
txt{*I leave this one example of a manual proof. The tedium of manually |
98 |
instantiating @{term i}, @{term j} and @{term env} is obvious. *} |
|
13428 | 99 |
apply (rule ball_iff_sats) |
13306 | 100 |
apply (rule imp_iff_sats) |
101 |
apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats) |
|
102 |
apply (rule_tac i=0 and j=2 in mem_iff_sats) |
|
103 |
apply (simp_all add: succ_Un_distrib [symmetric]) |
|
104 |
done |
|
105 |
||
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
106 |
subsection{*Separation for Set Difference*} |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
107 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
108 |
lemma Diff_Reflects: |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
109 |
"REFLECTS[\<lambda>x. x \<notin> B, \<lambda>i x. x \<notin> B]" |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
110 |
by (intro FOL_reflections) |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
111 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
112 |
lemma Diff_separation: |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
113 |
"L(B) ==> separation(L, \<lambda>x. x \<notin> B)" |
13566 | 114 |
apply (rule gen_separation [OF Diff_Reflects], simp) |
13687 | 115 |
apply (rule_tac env="[B]" in DPow_LsetI) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
116 |
apply (rule sep_rules | simp)+ |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
117 |
done |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
118 |
|
13316 | 119 |
subsection{*Separation for Cartesian Product*} |
13306 | 120 |
|
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
121 |
lemma cartprod_Reflects: |
13314 | 122 |
"REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)), |
13428 | 123 |
\<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B & |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
124 |
pair(##Lset(i),x,y,z))]" |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
125 |
by (intro FOL_reflections function_reflections) |
13306 | 126 |
|
127 |
lemma cartprod_separation: |
|
13428 | 128 |
"[| L(A); L(B) |] |
13306 | 129 |
==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))" |
13687 | 130 |
apply (rule gen_separation_multi [OF cartprod_Reflects, of "{A,B}"], auto) |
131 |
apply (rule_tac env="[A,B]" in DPow_LsetI) |
|
13316 | 132 |
apply (rule sep_rules | simp)+ |
13306 | 133 |
done |
134 |
||
13316 | 135 |
subsection{*Separation for Image*} |
13306 | 136 |
|
137 |
lemma image_Reflects: |
|
13314 | 138 |
"REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)), |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
139 |
\<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(##Lset(i),x,y,p))]" |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
140 |
by (intro FOL_reflections function_reflections) |
13306 | 141 |
|
142 |
lemma image_separation: |
|
13428 | 143 |
"[| L(A); L(r) |] |
13306 | 144 |
==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))" |
13687 | 145 |
apply (rule gen_separation_multi [OF image_Reflects, of "{A,r}"], auto) |
146 |
apply (rule_tac env="[A,r]" in DPow_LsetI) |
|
13316 | 147 |
apply (rule sep_rules | simp)+ |
13306 | 148 |
done |
149 |
||
150 |
||
13316 | 151 |
subsection{*Separation for Converse*} |
13306 | 152 |
|
153 |
lemma converse_Reflects: |
|
13314 | 154 |
"REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)), |
13428 | 155 |
\<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
156 |
pair(##Lset(i),x,y,p) & pair(##Lset(i),y,x,z))]" |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
157 |
by (intro FOL_reflections function_reflections) |
13306 | 158 |
|
159 |
lemma converse_separation: |
|
13428 | 160 |
"L(r) ==> separation(L, |
13306 | 161 |
\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))" |
13566 | 162 |
apply (rule gen_separation [OF converse_Reflects], simp) |
13687 | 163 |
apply (rule_tac env="[r]" in DPow_LsetI) |
13316 | 164 |
apply (rule sep_rules | simp)+ |
13306 | 165 |
done |
166 |
||
167 |
||
13316 | 168 |
subsection{*Separation for Restriction*} |
13306 | 169 |
|
170 |
lemma restrict_Reflects: |
|
13314 | 171 |
"REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)), |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
172 |
\<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(##Lset(i),x,y,z))]" |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
173 |
by (intro FOL_reflections function_reflections) |
13306 | 174 |
|
175 |
lemma restrict_separation: |
|
176 |
"L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))" |
|
13566 | 177 |
apply (rule gen_separation [OF restrict_Reflects], simp) |
13687 | 178 |
apply (rule_tac env="[A]" in DPow_LsetI) |
13316 | 179 |
apply (rule sep_rules | simp)+ |
13306 | 180 |
done |
181 |
||
182 |
||
13316 | 183 |
subsection{*Separation for Composition*} |
13306 | 184 |
|
185 |
lemma comp_Reflects: |
|
13428 | 186 |
"REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. |
187 |
pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & |
|
13306 | 188 |
xy\<in>s & yz\<in>r, |
13428 | 189 |
\<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i). |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
190 |
pair(##Lset(i),x,z,xz) & pair(##Lset(i),x,y,xy) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
191 |
pair(##Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]" |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
192 |
by (intro FOL_reflections function_reflections) |
13306 | 193 |
|
194 |
lemma comp_separation: |
|
195 |
"[| L(r); L(s) |] |
|
13428 | 196 |
==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. |
197 |
pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & |
|
13306 | 198 |
xy\<in>s & yz\<in>r)" |
13687 | 199 |
apply (rule gen_separation_multi [OF comp_Reflects, of "{r,s}"], auto) |
200 |
txt{*Subgoals after applying general ``separation'' rule: |
|
201 |
@{subgoals[display,indent=0,margin=65]}*} |
|
202 |
apply (rule_tac env="[r,s]" in DPow_LsetI) |
|
203 |
txt{*Subgoals ready for automatic synthesis of a formula: |
|
204 |
@{subgoals[display,indent=0,margin=65]}*} |
|
13316 | 205 |
apply (rule sep_rules | simp)+ |
13306 | 206 |
done |
207 |
||
13687 | 208 |
|
13316 | 209 |
subsection{*Separation for Predecessors in an Order*} |
13306 | 210 |
|
211 |
lemma pred_Reflects: |
|
13314 | 212 |
"REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p), |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
213 |
\<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(##Lset(i),y,x,p)]" |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
214 |
by (intro FOL_reflections function_reflections) |
13306 | 215 |
|
216 |
lemma pred_separation: |
|
217 |
"[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))" |
|
13687 | 218 |
apply (rule gen_separation_multi [OF pred_Reflects, of "{r,x}"], auto) |
219 |
apply (rule_tac env="[r,x]" in DPow_LsetI) |
|
13316 | 220 |
apply (rule sep_rules | simp)+ |
13306 | 221 |
done |
222 |
||
223 |
||
13316 | 224 |
subsection{*Separation for the Membership Relation*} |
13306 | 225 |
|
226 |
lemma Memrel_Reflects: |
|
13314 | 227 |
"REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y, |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
228 |
\<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(##Lset(i),x,y,z) & x \<in> y]" |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
229 |
by (intro FOL_reflections function_reflections) |
13306 | 230 |
|
231 |
lemma Memrel_separation: |
|
232 |
"separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)" |
|
13566 | 233 |
apply (rule gen_separation [OF Memrel_Reflects nonempty]) |
13687 | 234 |
apply (rule_tac env="[]" in DPow_LsetI) |
13316 | 235 |
apply (rule sep_rules | simp)+ |
13306 | 236 |
done |
237 |
||
238 |
||
13316 | 239 |
subsection{*Replacement for FunSpace*} |
13428 | 240 |
|
13306 | 241 |
lemma funspace_succ_Reflects: |
13428 | 242 |
"REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. |
243 |
pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & |
|
244 |
upair(L,cnbf,cnbf,z)), |
|
245 |
\<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i). |
|
246 |
\<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i). |
|
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
247 |
pair(##Lset(i),f,b,p) & pair(##Lset(i),n,b,nb) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
248 |
is_cons(##Lset(i),nb,f,cnbf) & upair(##Lset(i),cnbf,cnbf,z))]" |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
249 |
by (intro FOL_reflections function_reflections) |
13306 | 250 |
|
251 |
lemma funspace_succ_replacement: |
|
13428 | 252 |
"L(n) ==> |
253 |
strong_replacement(L, \<lambda>p z. \<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. |
|
13306 | 254 |
pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & |
255 |
upair(L,cnbf,cnbf,z))" |
|
13428 | 256 |
apply (rule strong_replacementI) |
13687 | 257 |
apply (rule_tac u="{n,B}" in gen_separation_multi [OF funspace_succ_Reflects], |
258 |
auto) |
|
259 |
apply (rule_tac env="[n,B]" in DPow_LsetI) |
|
13316 | 260 |
apply (rule sep_rules | simp)+ |
13306 | 261 |
done |
262 |
||
263 |
||
13634 | 264 |
subsection{*Separation for a Theorem about @{term "is_recfun"}*} |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
265 |
|
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
266 |
lemma is_recfun_reflects: |
13428 | 267 |
"REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L]. |
268 |
pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & |
|
269 |
(\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & |
|
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
270 |
fx \<noteq> gx), |
13428 | 271 |
\<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i). |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
272 |
pair(##Lset(i),x,a,xa) & xa \<in> r & pair(##Lset(i),x,b,xb) & xb \<in> r & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
273 |
(\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(##Lset(i),f,x,fx) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13691
diff
changeset
|
274 |
fun_apply(##Lset(i),g,x,gx) & fx \<noteq> gx)]" |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
275 |
by (intro FOL_reflections function_reflections fun_plus_reflections) |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
276 |
|
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
277 |
lemma is_recfun_separation: |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
278 |
--{*for well-founded recursion*} |
13428 | 279 |
"[| L(r); L(f); L(g); L(a); L(b) |] |
280 |
==> separation(L, |
|
281 |
\<lambda>x. \<exists>xa[L]. \<exists>xb[L]. |
|
282 |
pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & |
|
283 |
(\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & |
|
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
284 |
fx \<noteq> gx))" |
13687 | 285 |
apply (rule gen_separation_multi [OF is_recfun_reflects, of "{r,f,g,a,b}"], |
286 |
auto) |
|
287 |
apply (rule_tac env="[r,f,g,a,b]" in DPow_LsetI) |
|
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
288 |
apply (rule sep_rules | simp)+ |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
289 |
done |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
290 |
|
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
291 |
|
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
292 |
subsection{*Instantiating the locale @{text M_basic}*} |
13363 | 293 |
text{*Separation (and Strong Replacement) for basic set-theoretic constructions |
294 |
such as intersection, Cartesian Product and image.*} |
|
295 |
||
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
296 |
lemma M_basic_axioms_L: "M_basic_axioms(L)" |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
297 |
apply (rule M_basic_axioms.intro) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
298 |
apply (assumption | rule |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
299 |
Inter_separation Diff_separation cartprod_separation image_separation |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
300 |
converse_separation restrict_separation |
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
301 |
comp_separation pred_separation Memrel_separation |
13634 | 302 |
funspace_succ_replacement is_recfun_separation)+ |
13428 | 303 |
done |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
304 |
|
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
305 |
theorem M_basic_L: "PROP M_basic(L)" |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
306 |
by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L]) |
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
307 |
|
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset
|
308 |
|
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
309 |
lemmas cartprod_iff = M_basic.cartprod_iff [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
310 |
and cartprod_closed = M_basic.cartprod_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
311 |
and sum_closed = M_basic.sum_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
312 |
and M_converse_iff = M_basic.M_converse_iff [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
313 |
and converse_closed = M_basic.converse_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
314 |
and converse_abs = M_basic.converse_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
315 |
and image_closed = M_basic.image_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
316 |
and vimage_abs = M_basic.vimage_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
317 |
and vimage_closed = M_basic.vimage_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
318 |
and domain_abs = M_basic.domain_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
319 |
and domain_closed = M_basic.domain_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
320 |
and range_abs = M_basic.range_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
321 |
and range_closed = M_basic.range_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
322 |
and field_abs = M_basic.field_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
323 |
and field_closed = M_basic.field_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
324 |
and relation_abs = M_basic.relation_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
325 |
and function_abs = M_basic.function_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
326 |
and apply_closed = M_basic.apply_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
327 |
and apply_abs = M_basic.apply_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
328 |
and typed_function_abs = M_basic.typed_function_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
329 |
and injection_abs = M_basic.injection_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
330 |
and surjection_abs = M_basic.surjection_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
331 |
and bijection_abs = M_basic.bijection_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
332 |
and M_comp_iff = M_basic.M_comp_iff [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
333 |
and comp_closed = M_basic.comp_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
334 |
and composition_abs = M_basic.composition_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
335 |
and restriction_is_function = M_basic.restriction_is_function [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
336 |
and restriction_abs = M_basic.restriction_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
337 |
and M_restrict_iff = M_basic.M_restrict_iff [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
338 |
and restrict_closed = M_basic.restrict_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
339 |
and Inter_abs = M_basic.Inter_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
340 |
and Inter_closed = M_basic.Inter_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
341 |
and Int_closed = M_basic.Int_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
342 |
and is_funspace_abs = M_basic.is_funspace_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
343 |
and succ_fun_eq2 = M_basic.succ_fun_eq2 [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
344 |
and funspace_succ = M_basic.funspace_succ [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
345 |
and finite_funspace_closed = M_basic.finite_funspace_closed [OF M_basic_L] |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
346 |
|
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
347 |
lemmas is_recfun_equal = M_basic.is_recfun_equal [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
348 |
and is_recfun_cut = M_basic.is_recfun_cut [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
349 |
and is_recfun_functional = M_basic.is_recfun_functional [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
350 |
and is_recfun_relativize = M_basic.is_recfun_relativize [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
351 |
and is_recfun_restrict = M_basic.is_recfun_restrict [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
352 |
and univalent_is_recfun = M_basic.univalent_is_recfun [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
353 |
and wellfounded_exists_is_recfun = M_basic.wellfounded_exists_is_recfun [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
354 |
and wf_exists_is_recfun = M_basic.wf_exists_is_recfun [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
355 |
and is_recfun_abs = M_basic.is_recfun_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
356 |
and irreflexive_abs = M_basic.irreflexive_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
357 |
and transitive_rel_abs = M_basic.transitive_rel_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
358 |
and linear_rel_abs = M_basic.linear_rel_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
359 |
and wellordered_is_trans_on = M_basic.wellordered_is_trans_on [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
360 |
and wellordered_is_linear = M_basic.wellordered_is_linear [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
361 |
and wellordered_is_wellfounded_on = M_basic.wellordered_is_wellfounded_on [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
362 |
and wellfounded_imp_wellfounded_on = M_basic.wellfounded_imp_wellfounded_on [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
363 |
and wellfounded_on_subset_A = M_basic.wellfounded_on_subset_A [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
364 |
and wellfounded_on_iff_wellfounded = M_basic.wellfounded_on_iff_wellfounded [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
365 |
and wellfounded_on_imp_wellfounded = M_basic.wellfounded_on_imp_wellfounded [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
366 |
and wellfounded_on_field_imp_wellfounded = M_basic.wellfounded_on_field_imp_wellfounded [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
367 |
and wellfounded_iff_wellfounded_on_field = M_basic.wellfounded_iff_wellfounded_on_field [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
368 |
and wellfounded_induct = M_basic.wellfounded_induct [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
369 |
and wellfounded_on_induct = M_basic.wellfounded_on_induct [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
370 |
and linear_imp_relativized = M_basic.linear_imp_relativized [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
371 |
and trans_on_imp_relativized = M_basic.trans_on_imp_relativized [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
372 |
and wf_on_imp_relativized = M_basic.wf_on_imp_relativized [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
373 |
and wf_imp_relativized = M_basic.wf_imp_relativized [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
374 |
and well_ord_imp_relativized = M_basic.well_ord_imp_relativized [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
375 |
and order_isomorphism_abs = M_basic.order_isomorphism_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
376 |
and pred_set_abs = M_basic.pred_set_abs [OF M_basic_L] |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
377 |
|
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
378 |
lemmas pred_closed = M_basic.pred_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
379 |
and membership_abs = M_basic.membership_abs [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
380 |
and M_Memrel_iff = M_basic.M_Memrel_iff [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
381 |
and Memrel_closed = M_basic.Memrel_closed [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
382 |
and wellfounded_on_asym = M_basic.wellfounded_on_asym [OF M_basic_L] |
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset
|
383 |
and wellordered_asym = M_basic.wellordered_asym [OF M_basic_L] |
13428 | 384 |
|
13429 | 385 |
declare cartprod_closed [intro, simp] |
386 |
declare sum_closed [intro, simp] |
|
387 |
declare converse_closed [intro, simp] |
|
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
388 |
declare converse_abs [simp] |
13429 | 389 |
declare image_closed [intro, simp] |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
390 |
declare vimage_abs [simp] |
13429 | 391 |
declare vimage_closed [intro, simp] |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
392 |
declare domain_abs [simp] |
13429 | 393 |
declare domain_closed [intro, simp] |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
394 |
declare range_abs [simp] |
13429 | 395 |
declare range_closed [intro, simp] |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
396 |
declare field_abs [simp] |
13429 | 397 |
declare field_closed [intro, simp] |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
398 |
declare relation_abs [simp] |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
399 |
declare function_abs [simp] |
13429 | 400 |
declare apply_closed [intro, simp] |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
401 |
declare typed_function_abs [simp] |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
402 |
declare injection_abs [simp] |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
403 |
declare surjection_abs [simp] |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
404 |
declare bijection_abs [simp] |
13429 | 405 |
declare comp_closed [intro, simp] |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
406 |
declare composition_abs [simp] |
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
407 |
declare restriction_abs [simp] |
13429 | 408 |
declare restrict_closed [intro, simp] |
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
409 |
declare Inter_abs [simp] |
13429 | 410 |
declare Inter_closed [intro, simp] |
411 |
declare Int_closed [intro, simp] |
|
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
412 |
declare is_funspace_abs [simp] |
13429 | 413 |
declare finite_funspace_closed [intro, simp] |
13440 | 414 |
declare membership_abs [simp] |
415 |
declare Memrel_closed [intro,simp] |
|
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset
|
416 |
|
13306 | 417 |
end |