1 (* Title: ZF/Constructible/Separation.thy |
1 (* Title: ZF/Constructible/Separation.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 *) |
3 *) |
4 |
4 |
5 section{*Early Instances of Separation and Strong Replacement*} |
5 section\<open>Early Instances of Separation and Strong Replacement\<close> |
6 |
6 |
7 theory Separation imports L_axioms WF_absolute begin |
7 theory Separation imports L_axioms WF_absolute begin |
8 |
8 |
9 text{*This theory proves all instances needed for locale @{text "M_basic"}*} |
9 text\<open>This theory proves all instances needed for locale @{text "M_basic"}\<close> |
10 |
10 |
11 text{*Helps us solve for de Bruijn indices!*} |
11 text\<open>Helps us solve for de Bruijn indices!\<close> |
12 lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x" |
12 lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x" |
13 by simp |
13 by simp |
14 |
14 |
15 lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI |
15 lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI |
16 lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats |
16 lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats |
34 apply (unfold separation_def, clarify) |
34 apply (unfold separation_def, clarify) |
35 apply (rule_tac x="{x\<in>z. P(x)}" in rexI) |
35 apply (rule_tac x="{x\<in>z. P(x)}" in rexI) |
36 apply simp_all |
36 apply simp_all |
37 done |
37 done |
38 |
38 |
39 text{*Reduces the original comprehension to the reflected one*} |
39 text\<open>Reduces the original comprehension to the reflected one\<close> |
40 lemma reflection_imp_L_separation: |
40 lemma reflection_imp_L_separation: |
41 "[| \<forall>x\<in>Lset(j). P(x) \<longleftrightarrow> Q(x); |
41 "[| \<forall>x\<in>Lset(j). P(x) \<longleftrightarrow> Q(x); |
42 {x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j)); |
42 {x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j)); |
43 Ord(j); z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})" |
43 Ord(j); z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})" |
44 apply (rule_tac i = "succ(j)" in L_I) |
44 apply (rule_tac i = "succ(j)" in L_I) |
47 prefer 2 |
47 prefer 2 |
48 apply (blast dest: mem_Lset_imp_subset_Lset) |
48 apply (blast dest: mem_Lset_imp_subset_Lset) |
49 apply (simp add: Lset_succ Collect_conj_in_DPow_Lset) |
49 apply (simp add: Lset_succ Collect_conj_in_DPow_Lset) |
50 done |
50 done |
51 |
51 |
52 text{*Encapsulates the standard proof script for proving instances of |
52 text\<open>Encapsulates the standard proof script for proving instances of |
53 Separation.*} |
53 Separation.\<close> |
54 lemma gen_separation: |
54 lemma gen_separation: |
55 assumes reflection: "REFLECTS [P,Q]" |
55 assumes reflection: "REFLECTS [P,Q]" |
56 and Lu: "L(u)" |
56 and Lu: "L(u)" |
57 and collI: "!!j. u \<in> Lset(j) |
57 and collI: "!!j. u \<in> Lset(j) |
58 \<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))" |
58 \<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))" |
64 apply (erule reflection_imp_L_separation) |
64 apply (erule reflection_imp_L_separation) |
65 apply (simp_all add: lt_Ord2, clarify) |
65 apply (simp_all add: lt_Ord2, clarify) |
66 apply (rule collI, assumption) |
66 apply (rule collI, assumption) |
67 done |
67 done |
68 |
68 |
69 text{*As above, but typically @{term u} is a finite enumeration such as |
69 text\<open>As above, but typically @{term u} is a finite enumeration such as |
70 @{term "{a,b}"}; thus the new subgoal gets the assumption |
70 @{term "{a,b}"}; thus the new subgoal gets the assumption |
71 @{term "{a,b} \<subseteq> Lset(i)"}, which is logically equivalent to |
71 @{term "{a,b} \<subseteq> Lset(i)"}, which is logically equivalent to |
72 @{term "a \<in> Lset(i)"} and @{term "b \<in> Lset(i)"}.*} |
72 @{term "a \<in> Lset(i)"} and @{term "b \<in> Lset(i)"}.\<close> |
73 lemma gen_separation_multi: |
73 lemma gen_separation_multi: |
74 assumes reflection: "REFLECTS [P,Q]" |
74 assumes reflection: "REFLECTS [P,Q]" |
75 and Lu: "L(u)" |
75 and Lu: "L(u)" |
76 and collI: "!!j. u \<subseteq> Lset(j) |
76 and collI: "!!j. u \<subseteq> Lset(j) |
77 \<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))" |
77 \<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))" |
80 apply (drule mem_Lset_imp_subset_Lset) |
80 apply (drule mem_Lset_imp_subset_Lset) |
81 apply (erule collI) |
81 apply (erule collI) |
82 done |
82 done |
83 |
83 |
84 |
84 |
85 subsection{*Separation for Intersection*} |
85 subsection\<open>Separation for Intersection\<close> |
86 |
86 |
87 lemma Inter_Reflects: |
87 lemma Inter_Reflects: |
88 "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A \<longrightarrow> x \<in> y, |
88 "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A \<longrightarrow> x \<in> y, |
89 \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A \<longrightarrow> x \<in> y]" |
89 \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A \<longrightarrow> x \<in> y]" |
90 by (intro FOL_reflections) |
90 by (intro FOL_reflections) |
91 |
91 |
92 lemma Inter_separation: |
92 lemma Inter_separation: |
93 "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A \<longrightarrow> x\<in>y)" |
93 "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A \<longrightarrow> x\<in>y)" |
94 apply (rule gen_separation [OF Inter_Reflects], simp) |
94 apply (rule gen_separation [OF Inter_Reflects], simp) |
95 apply (rule DPow_LsetI) |
95 apply (rule DPow_LsetI) |
96 txt{*I leave this one example of a manual proof. The tedium of manually |
96 txt\<open>I leave this one example of a manual proof. The tedium of manually |
97 instantiating @{term i}, @{term j} and @{term env} is obvious. *} |
97 instantiating @{term i}, @{term j} and @{term env} is obvious.\<close> |
98 apply (rule ball_iff_sats) |
98 apply (rule ball_iff_sats) |
99 apply (rule imp_iff_sats) |
99 apply (rule imp_iff_sats) |
100 apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats) |
100 apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats) |
101 apply (rule_tac i=0 and j=2 in mem_iff_sats) |
101 apply (rule_tac i=0 and j=2 in mem_iff_sats) |
102 apply (simp_all add: succ_Un_distrib [symmetric]) |
102 apply (simp_all add: succ_Un_distrib [symmetric]) |
103 done |
103 done |
104 |
104 |
105 subsection{*Separation for Set Difference*} |
105 subsection\<open>Separation for Set Difference\<close> |
106 |
106 |
107 lemma Diff_Reflects: |
107 lemma Diff_Reflects: |
108 "REFLECTS[\<lambda>x. x \<notin> B, \<lambda>i x. x \<notin> B]" |
108 "REFLECTS[\<lambda>x. x \<notin> B, \<lambda>i x. x \<notin> B]" |
109 by (intro FOL_reflections) |
109 by (intro FOL_reflections) |
110 |
110 |
113 apply (rule gen_separation [OF Diff_Reflects], simp) |
113 apply (rule gen_separation [OF Diff_Reflects], simp) |
114 apply (rule_tac env="[B]" in DPow_LsetI) |
114 apply (rule_tac env="[B]" in DPow_LsetI) |
115 apply (rule sep_rules | simp)+ |
115 apply (rule sep_rules | simp)+ |
116 done |
116 done |
117 |
117 |
118 subsection{*Separation for Cartesian Product*} |
118 subsection\<open>Separation for Cartesian Product\<close> |
119 |
119 |
120 lemma cartprod_Reflects: |
120 lemma cartprod_Reflects: |
121 "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)), |
121 "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)), |
122 \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B & |
122 \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B & |
123 pair(##Lset(i),x,y,z))]" |
123 pair(##Lset(i),x,y,z))]" |
129 apply (rule gen_separation_multi [OF cartprod_Reflects, of "{A,B}"], auto) |
129 apply (rule gen_separation_multi [OF cartprod_Reflects, of "{A,B}"], auto) |
130 apply (rule_tac env="[A,B]" in DPow_LsetI) |
130 apply (rule_tac env="[A,B]" in DPow_LsetI) |
131 apply (rule sep_rules | simp)+ |
131 apply (rule sep_rules | simp)+ |
132 done |
132 done |
133 |
133 |
134 subsection{*Separation for Image*} |
134 subsection\<open>Separation for Image\<close> |
135 |
135 |
136 lemma image_Reflects: |
136 lemma image_Reflects: |
137 "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)), |
137 "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)), |
138 \<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))]" |
138 \<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))]" |
139 by (intro FOL_reflections function_reflections) |
139 by (intro FOL_reflections function_reflections) |
145 apply (rule_tac env="[A,r]" in DPow_LsetI) |
145 apply (rule_tac env="[A,r]" in DPow_LsetI) |
146 apply (rule sep_rules | simp)+ |
146 apply (rule sep_rules | simp)+ |
147 done |
147 done |
148 |
148 |
149 |
149 |
150 subsection{*Separation for Converse*} |
150 subsection\<open>Separation for Converse\<close> |
151 |
151 |
152 lemma converse_Reflects: |
152 lemma converse_Reflects: |
153 "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)), |
153 "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)), |
154 \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). |
154 \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). |
155 pair(##Lset(i),x,y,p) & pair(##Lset(i),y,x,z))]" |
155 pair(##Lset(i),x,y,p) & pair(##Lset(i),y,x,z))]" |
162 apply (rule_tac env="[r]" in DPow_LsetI) |
162 apply (rule_tac env="[r]" in DPow_LsetI) |
163 apply (rule sep_rules | simp)+ |
163 apply (rule sep_rules | simp)+ |
164 done |
164 done |
165 |
165 |
166 |
166 |
167 subsection{*Separation for Restriction*} |
167 subsection\<open>Separation for Restriction\<close> |
168 |
168 |
169 lemma restrict_Reflects: |
169 lemma restrict_Reflects: |
170 "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)), |
170 "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)), |
171 \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(##Lset(i),x,y,z))]" |
171 \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(##Lset(i),x,y,z))]" |
172 by (intro FOL_reflections function_reflections) |
172 by (intro FOL_reflections function_reflections) |
177 apply (rule_tac env="[A]" in DPow_LsetI) |
177 apply (rule_tac env="[A]" in DPow_LsetI) |
178 apply (rule sep_rules | simp)+ |
178 apply (rule sep_rules | simp)+ |
179 done |
179 done |
180 |
180 |
181 |
181 |
182 subsection{*Separation for Composition*} |
182 subsection\<open>Separation for Composition\<close> |
183 |
183 |
184 lemma comp_Reflects: |
184 lemma comp_Reflects: |
185 "REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. |
185 "REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. |
186 pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & |
186 pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & |
187 xy\<in>s & yz\<in>r, |
187 xy\<in>s & yz\<in>r, |
194 "[| L(r); L(s) |] |
194 "[| L(r); L(s) |] |
195 ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. |
195 ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. |
196 pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & |
196 pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & |
197 xy\<in>s & yz\<in>r)" |
197 xy\<in>s & yz\<in>r)" |
198 apply (rule gen_separation_multi [OF comp_Reflects, of "{r,s}"], auto) |
198 apply (rule gen_separation_multi [OF comp_Reflects, of "{r,s}"], auto) |
199 txt{*Subgoals after applying general ``separation'' rule: |
199 txt\<open>Subgoals after applying general ``separation'' rule: |
200 @{subgoals[display,indent=0,margin=65]}*} |
200 @{subgoals[display,indent=0,margin=65]}\<close> |
201 apply (rule_tac env="[r,s]" in DPow_LsetI) |
201 apply (rule_tac env="[r,s]" in DPow_LsetI) |
202 txt{*Subgoals ready for automatic synthesis of a formula: |
202 txt\<open>Subgoals ready for automatic synthesis of a formula: |
203 @{subgoals[display,indent=0,margin=65]}*} |
203 @{subgoals[display,indent=0,margin=65]}\<close> |
204 apply (rule sep_rules | simp)+ |
204 apply (rule sep_rules | simp)+ |
205 done |
205 done |
206 |
206 |
207 |
207 |
208 subsection{*Separation for Predecessors in an Order*} |
208 subsection\<open>Separation for Predecessors in an Order\<close> |
209 |
209 |
210 lemma pred_Reflects: |
210 lemma pred_Reflects: |
211 "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p), |
211 "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p), |
212 \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(##Lset(i),y,x,p)]" |
212 \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(##Lset(i),y,x,p)]" |
213 by (intro FOL_reflections function_reflections) |
213 by (intro FOL_reflections function_reflections) |
218 apply (rule_tac env="[r,x]" in DPow_LsetI) |
218 apply (rule_tac env="[r,x]" in DPow_LsetI) |
219 apply (rule sep_rules | simp)+ |
219 apply (rule sep_rules | simp)+ |
220 done |
220 done |
221 |
221 |
222 |
222 |
223 subsection{*Separation for the Membership Relation*} |
223 subsection\<open>Separation for the Membership Relation\<close> |
224 |
224 |
225 lemma Memrel_Reflects: |
225 lemma Memrel_Reflects: |
226 "REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y, |
226 "REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y, |
227 \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(##Lset(i),x,y,z) & x \<in> y]" |
227 \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(##Lset(i),x,y,z) & x \<in> y]" |
228 by (intro FOL_reflections function_reflections) |
228 by (intro FOL_reflections function_reflections) |
233 apply (rule_tac env="[]" in DPow_LsetI) |
233 apply (rule_tac env="[]" in DPow_LsetI) |
234 apply (rule sep_rules | simp)+ |
234 apply (rule sep_rules | simp)+ |
235 done |
235 done |
236 |
236 |
237 |
237 |
238 subsection{*Replacement for FunSpace*} |
238 subsection\<open>Replacement for FunSpace\<close> |
239 |
239 |
240 lemma funspace_succ_Reflects: |
240 lemma funspace_succ_Reflects: |
241 "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. |
241 "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. |
242 pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & |
242 pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & |
243 upair(L,cnbf,cnbf,z)), |
243 upair(L,cnbf,cnbf,z)), |
258 apply (rule_tac env="[n,B]" in DPow_LsetI) |
258 apply (rule_tac env="[n,B]" in DPow_LsetI) |
259 apply (rule sep_rules | simp)+ |
259 apply (rule sep_rules | simp)+ |
260 done |
260 done |
261 |
261 |
262 |
262 |
263 subsection{*Separation for a Theorem about @{term "is_recfun"}*} |
263 subsection\<open>Separation for a Theorem about @{term "is_recfun"}\<close> |
264 |
264 |
265 lemma is_recfun_reflects: |
265 lemma is_recfun_reflects: |
266 "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L]. |
266 "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L]. |
267 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & |
267 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & |
268 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & |
268 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & |
272 (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(##Lset(i),f,x,fx) & |
272 (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(##Lset(i),f,x,fx) & |
273 fun_apply(##Lset(i),g,x,gx) & fx \<noteq> gx)]" |
273 fun_apply(##Lset(i),g,x,gx) & fx \<noteq> gx)]" |
274 by (intro FOL_reflections function_reflections fun_plus_reflections) |
274 by (intro FOL_reflections function_reflections fun_plus_reflections) |
275 |
275 |
276 lemma is_recfun_separation: |
276 lemma is_recfun_separation: |
277 --{*for well-founded recursion*} |
277 --\<open>for well-founded recursion\<close> |
278 "[| L(r); L(f); L(g); L(a); L(b) |] |
278 "[| L(r); L(f); L(g); L(a); L(b) |] |
279 ==> separation(L, |
279 ==> separation(L, |
280 \<lambda>x. \<exists>xa[L]. \<exists>xb[L]. |
280 \<lambda>x. \<exists>xa[L]. \<exists>xb[L]. |
281 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & |
281 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & |
282 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & |
282 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & |
286 apply (rule_tac env="[r,f,g,a,b]" in DPow_LsetI) |
286 apply (rule_tac env="[r,f,g,a,b]" in DPow_LsetI) |
287 apply (rule sep_rules | simp)+ |
287 apply (rule sep_rules | simp)+ |
288 done |
288 done |
289 |
289 |
290 |
290 |
291 subsection{*Instantiating the locale @{text M_basic}*} |
291 subsection\<open>Instantiating the locale @{text M_basic}\<close> |
292 text{*Separation (and Strong Replacement) for basic set-theoretic constructions |
292 text\<open>Separation (and Strong Replacement) for basic set-theoretic constructions |
293 such as intersection, Cartesian Product and image.*} |
293 such as intersection, Cartesian Product and image.\<close> |
294 |
294 |
295 lemma M_basic_axioms_L: "M_basic_axioms(L)" |
295 lemma M_basic_axioms_L: "M_basic_axioms(L)" |
296 apply (rule M_basic_axioms.intro) |
296 apply (rule M_basic_axioms.intro) |
297 apply (assumption | rule |
297 apply (assumption | rule |
298 Inter_separation Diff_separation cartprod_separation image_separation |
298 Inter_separation Diff_separation cartprod_separation image_separation |