author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
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 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

3 
*) 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

4 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13324
diff
changeset

5 
header{*Early Instances of Separation and Strong Replacement*} 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

6 

16417  7 
theory Separation imports L_axioms WF_absolute begin 
13306  8 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset

9 
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

10 

13306  11 
text{*Helps us solve for de Bruijn indices!*} 
12 
lemma nth_ConsI: "[nth(n,l) = x; n \<in> nat] ==> nth(succ(n), Cons(a,l)) = x" 

13 
by simp 

14 

13316  15 
lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI 
13428  16 
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

17 
fun_plus_iff_sats 
13306  18 

19 
lemma Collect_conj_in_DPow: 

13428  20 
"[ {x\<in>A. P(x)} \<in> DPow(A); {x\<in>A. Q(x)} \<in> DPow(A) ] 
13306  21 
==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)" 
13428  22 
by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric]) 
13306  23 

24 
lemma Collect_conj_in_DPow_Lset: 

25 
"[z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))] 

26 
==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> DPow(Lset(j))" 

27 
apply (frule mem_Lset_imp_subset_Lset) 

13428  28 
apply (simp add: Collect_conj_in_DPow Collect_mem_eq 
13306  29 
subset_Int_iff2 elem_subset_in_DPow) 
30 
done 

31 

32 
lemma separation_CollectI: 

33 
"(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))" 

13428  34 
apply (unfold separation_def, clarify) 
35 
apply (rule_tac x="{x\<in>z. P(x)}" in rexI) 

13306  36 
apply simp_all 
37 
done 

38 

39 
text{*Reduces the original comprehension to the reflected one*} 

40 
lemma reflection_imp_L_separation: 

46823  41 
"[ \<forall>x\<in>Lset(j). P(x) \<longleftrightarrow> Q(x); 
13428  42 
{x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j)); 
13306  43 
Ord(j); z \<in> Lset(j)] ==> L({x \<in> z . P(x)})" 
44 
apply (rule_tac i = "succ(j)" in L_I) 

45 
prefer 2 apply simp 

46 
apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> z & (Q(x))}") 

47 
prefer 2 

13428  48 
apply (blast dest: mem_Lset_imp_subset_Lset) 
13306  49 
apply (simp add: Lset_succ Collect_conj_in_DPow_Lset) 
50 
done 

51 

13566  52 
text{*Encapsulates the standard proof script for proving instances of 
13687  53 
Separation.*} 
13566  54 
lemma gen_separation: 
55 
assumes reflection: "REFLECTS [P,Q]" 

56 
and Lu: "L(u)" 

57 
and collI: "!!j. u \<in> Lset(j) 

58 
\<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))" 

59 
shows "separation(L,P)" 

60 
apply (rule separation_CollectI) 

61 
apply (rule_tac A="{u,z}" in subset_LsetE, blast intro: Lu) 

62 
apply (rule ReflectsE [OF reflection], assumption) 

63 
apply (drule subset_Lset_ltD, assumption) 

64 
apply (erule reflection_imp_L_separation) 

65 
apply (simp_all add: lt_Ord2, clarify) 

13691  66 
apply (rule collI, assumption) 
13687  67 
done 
68 

69 
text{*As above, but typically @{term u} is a finite enumeration such as 

70 
@{term "{a,b}"}; thus the new subgoal gets the assumption 

71 
@{term "{a,b} \<subseteq> Lset(i)"}, which is logically equivalent to 

72 
@{term "a \<in> Lset(i)"} and @{term "b \<in> Lset(i)"}.*} 

73 
lemma gen_separation_multi: 

74 
assumes reflection: "REFLECTS [P,Q]" 

75 
and Lu: "L(u)" 

76 
and collI: "!!j. u \<subseteq> Lset(j) 

77 
\<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))" 

78 
shows "separation(L,P)" 

79 
apply (rule gen_separation [OF reflection Lu]) 

80 
apply (drule mem_Lset_imp_subset_Lset) 

81 
apply (erule collI) 

13566  82 
done 
83 

13306  84 

13316  85 
subsection{*Separation for Intersection*} 
13306  86 

87 
lemma Inter_Reflects: 

46823  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]" 

13428  90 
by (intro FOL_reflections) 
13306  91 

92 
lemma Inter_separation: 

46823  93 
"L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A \<longrightarrow> x\<in>y)" 
13566  94 
apply (rule gen_separation [OF Inter_Reflects], simp) 
13428  95 
apply (rule DPow_LsetI) 
13687  96 
txt{*I leave this one example of a manual proof. The tedium of manually 
97 
instantiating @{term i}, @{term j} and @{term env} is obvious. *} 

13428  98 
apply (rule ball_iff_sats) 
13306  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) 

101 
apply (rule_tac i=0 and j=2 in mem_iff_sats) 

102 
apply (simp_all add: succ_Un_distrib [symmetric]) 

103 
done 

104 

13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

105 
subsection{*Separation for Set Difference*} 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

106 

01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

107 
lemma Diff_Reflects: 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

108 
"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

109 
by (intro FOL_reflections) 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

110 

01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

111 
lemma Diff_separation: 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

112 
"L(B) ==> separation(L, \<lambda>x. x \<notin> B)" 
13566  113 
apply (rule gen_separation [OF Diff_Reflects], simp) 
13687  114 
apply (rule_tac env="[B]" in DPow_LsetI) 
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

115 
apply (rule sep_rules  simp)+ 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

116 
done 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

117 

13316  118 
subsection{*Separation for Cartesian Product*} 
13306  119 

13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

120 
lemma cartprod_Reflects: 
13314  121 
"REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)), 
13428  122 
\<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

123 
pair(##Lset(i),x,y,z))]" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

124 
by (intro FOL_reflections function_reflections) 
13306  125 

126 
lemma cartprod_separation: 

13428  127 
"[ L(A); L(B) ] 
13306  128 
==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))" 
13687  129 
apply (rule gen_separation_multi [OF cartprod_Reflects, of "{A,B}"], auto) 
130 
apply (rule_tac env="[A,B]" in DPow_LsetI) 

13316  131 
apply (rule sep_rules  simp)+ 
13306  132 
done 
133 

13316  134 
subsection{*Separation for Image*} 
13306  135 

136 
lemma image_Reflects: 

13314  137 
"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

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))]" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

139 
by (intro FOL_reflections function_reflections) 
13306  140 

141 
lemma image_separation: 

13428  142 
"[ L(A); L(r) ] 
13306  143 
==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))" 
13687  144 
apply (rule gen_separation_multi [OF image_Reflects, of "{A,r}"], auto) 
145 
apply (rule_tac env="[A,r]" in DPow_LsetI) 

13316  146 
apply (rule sep_rules  simp)+ 
13306  147 
done 
148 

149 

13316  150 
subsection{*Separation for Converse*} 
13306  151 

152 
lemma converse_Reflects: 

13314  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)), 
13428  154 
\<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

155 
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

156 
by (intro FOL_reflections function_reflections) 
13306  157 

158 
lemma converse_separation: 

13428  159 
"L(r) ==> separation(L, 
13306  160 
\<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  161 
apply (rule gen_separation [OF converse_Reflects], simp) 
13687  162 
apply (rule_tac env="[r]" in DPow_LsetI) 
13316  163 
apply (rule sep_rules  simp)+ 
13306  164 
done 
165 

166 

13316  167 
subsection{*Separation for Restriction*} 
13306  168 

169 
lemma restrict_Reflects: 

13314  170 
"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

171 
\<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

172 
by (intro FOL_reflections function_reflections) 
13306  173 

174 
lemma restrict_separation: 

175 
"L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))" 

13566  176 
apply (rule gen_separation [OF restrict_Reflects], simp) 
13687  177 
apply (rule_tac env="[A]" in DPow_LsetI) 
13316  178 
apply (rule sep_rules  simp)+ 
13306  179 
done 
180 

181 

13316  182 
subsection{*Separation for Composition*} 
13306  183 

184 
lemma comp_Reflects: 

13428  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) & 

13306  187 
xy\<in>s & yz\<in>r, 
13428  188 
\<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

189 
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

190 
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

191 
by (intro FOL_reflections function_reflections) 
13306  192 

193 
lemma comp_separation: 

194 
"[ L(r); L(s) ] 

13428  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) & 

13306  197 
xy\<in>s & yz\<in>r)" 
13687  198 
apply (rule gen_separation_multi [OF comp_Reflects, of "{r,s}"], auto) 
199 
txt{*Subgoals after applying general ``separation'' rule: 

200 
@{subgoals[display,indent=0,margin=65]}*} 

201 
apply (rule_tac env="[r,s]" in DPow_LsetI) 

202 
txt{*Subgoals ready for automatic synthesis of a formula: 

203 
@{subgoals[display,indent=0,margin=65]}*} 

13316  204 
apply (rule sep_rules  simp)+ 
13306  205 
done 
206 

13687  207 

13316  208 
subsection{*Separation for Predecessors in an Order*} 
13306  209 

210 
lemma pred_Reflects: 

13314  211 
"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

212 
\<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

213 
by (intro FOL_reflections function_reflections) 
13306  214 

215 
lemma pred_separation: 

216 
"[ L(r); L(x) ] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))" 

13687  217 
apply (rule gen_separation_multi [OF pred_Reflects, of "{r,x}"], auto) 
218 
apply (rule_tac env="[r,x]" in DPow_LsetI) 

13316  219 
apply (rule sep_rules  simp)+ 
13306  220 
done 
221 

222 

13316  223 
subsection{*Separation for the Membership Relation*} 
13306  224 

225 
lemma Memrel_Reflects: 

13314  226 
"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

227 
\<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

228 
by (intro FOL_reflections function_reflections) 
13306  229 

230 
lemma Memrel_separation: 

231 
"separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)" 

13566  232 
apply (rule gen_separation [OF Memrel_Reflects nonempty]) 
13687  233 
apply (rule_tac env="[]" in DPow_LsetI) 
13316  234 
apply (rule sep_rules  simp)+ 
13306  235 
done 
236 

237 

13316  238 
subsection{*Replacement for FunSpace*} 
13428  239 

13306  240 
lemma funspace_succ_Reflects: 
13428  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) & 

243 
upair(L,cnbf,cnbf,z)), 

244 
\<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i). 

245 
\<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

246 
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

247 
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

248 
by (intro FOL_reflections function_reflections) 
13306  249 

250 
lemma funspace_succ_replacement: 

13428  251 
"L(n) ==> 
252 
strong_replacement(L, \<lambda>p z. \<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. 

13306  253 
pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & 
254 
upair(L,cnbf,cnbf,z))" 

13428  255 
apply (rule strong_replacementI) 
13687  256 
apply (rule_tac u="{n,B}" in gen_separation_multi [OF funspace_succ_Reflects], 
257 
auto) 

258 
apply (rule_tac env="[n,B]" in DPow_LsetI) 

13316  259 
apply (rule sep_rules  simp)+ 
13306  260 
done 
261 

262 

13634  263 
subsection{*Separation for a Theorem about @{term "is_recfun"}*} 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

264 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

265 
lemma is_recfun_reflects: 
13428  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 & 

268 
(\<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

269 
fx \<noteq> gx), 
13428  270 
\<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

271 
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

272 
(\<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

273 
fun_apply(##Lset(i),g,x,gx) & fx \<noteq> gx)]" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

274 
by (intro FOL_reflections function_reflections fun_plus_reflections) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

275 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

276 
lemma is_recfun_separation: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

277 
{*for wellfounded recursion*} 
13428  278 
"[ L(r); L(f); L(g); L(a); L(b) ] 
279 
==> separation(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 & 

282 
(\<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

283 
fx \<noteq> gx))" 
13687  284 
apply (rule gen_separation_multi [OF is_recfun_reflects, of "{r,f,g,a,b}"], 
285 
auto) 

286 
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

287 
apply (rule sep_rules  simp)+ 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

288 
done 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

289 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

290 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset

291 
subsection{*Instantiating the locale @{text M_basic}*} 
13363  292 
text{*Separation (and Strong Replacement) for basic settheoretic constructions 
293 
such as intersection, Cartesian Product and image.*} 

294 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset

295 
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

296 
apply (rule M_basic_axioms.intro) 
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13429
diff
changeset

297 
apply (assumption  rule 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30729
diff
changeset

298 
Inter_separation Diff_separation cartprod_separation image_separation 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30729
diff
changeset

299 
converse_separation restrict_separation 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30729
diff
changeset

300 
comp_separation pred_separation Memrel_separation 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30729
diff
changeset

301 
funspace_succ_replacement is_recfun_separation)+ 
13428  302 
done 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

303 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13505
diff
changeset

304 
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

305 
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

306 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29223
diff
changeset

307 
interpretation L?: M_basic L by (rule M_basic_L) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

308 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

309 

13306  310 
end 