author  paulson 
Fri, 04 Oct 2002 15:57:32 +0200  
changeset 13628  87482b5e3f2e 
parent 13566  52a419210d5c 
child 13634  99a593b49b04 
permissions  rwrr 
13505  1 
(* Title: ZF/Constructible/L_axioms.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 2002 University of Cambridge 

5 
*) 

13429  6 

7 
header {* The ZF Axioms (Except Separation) in L *} 

13223  8 

13314  9 
theory L_axioms = Formula + Relative + Reflection + MetaExists: 
13223  10 

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

11 
text {* The class L satisfies the premises of locale @{text M_trivial} *} 
13223  12 

13 
lemma transL: "[ y\<in>x; L(x) ] ==> L(y)" 

13429  14 
apply (insert Transset_Lset) 
15 
apply (simp add: Transset_def L_def, blast) 

13223  16 
done 
17 

18 
lemma nonempty: "L(0)" 

13429  19 
apply (simp add: L_def) 
20 
apply (blast intro: zero_in_Lset) 

13223  21 
done 
22 

13563  23 
theorem upair_ax: "upair_ax(L)" 
13223  24 
apply (simp add: upair_ax_def upair_def, clarify) 
13429  25 
apply (rule_tac x="{x,y}" in rexI) 
26 
apply (simp_all add: doubleton_in_L) 

13223  27 
done 
28 

13563  29 
theorem Union_ax: "Union_ax(L)" 
13223  30 
apply (simp add: Union_ax_def big_union_def, clarify) 
13429  31 
apply (rule_tac x="Union(x)" in rexI) 
32 
apply (simp_all add: Union_in_L, auto) 

33 
apply (blast intro: transL) 

13223  34 
done 
35 

13563  36 
theorem power_ax: "power_ax(L)" 
13223  37 
apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify) 
13429  38 
apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI) 
13299  39 
apply (simp_all add: LPow_in_L, auto) 
13429  40 
apply (blast intro: transL) 
13223  41 
done 
42 

13563  43 
text{*We don't actually need @{term L} to satisfy the foundation axiom.*} 
44 
theorem foundation_ax: "foundation_ax(L)" 

45 
apply (simp add: foundation_ax_def) 

46 
apply (rule rallI) 

47 
apply (cut_tac A=x in foundation) 

48 
apply (blast intro: transL) 

49 
done 

50 

13506  51 
subsection{*For L to satisfy Replacement *} 
13223  52 

53 
(*Can't move these to Formula unless the definition of univalent is moved 

54 
there too!*) 

55 

56 
lemma LReplace_in_Lset: 

13429  57 
"[X \<in> Lset(i); univalent(L,X,Q); Ord(i)] 
13223  58 
==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)" 
13429  59 
apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))" 
13223  60 
in exI) 
61 
apply simp 

13429  62 
apply clarify 
63 
apply (rule_tac a=x in UN_I) 

64 
apply (simp_all add: Replace_iff univalent_def) 

65 
apply (blast dest: transL L_I) 

13223  66 
done 
67 

13429  68 
lemma LReplace_in_L: 
69 
"[L(X); univalent(L,X,Q)] 

13223  70 
==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y" 
13429  71 
apply (drule L_D, clarify) 
13223  72 
apply (drule LReplace_in_Lset, assumption+) 
73 
apply (blast intro: L_I Lset_in_Lset_succ) 

74 
done 

75 

13563  76 
theorem replacement: "replacement(L,P)" 
13223  77 
apply (simp add: replacement_def, clarify) 
13429  78 
apply (frule LReplace_in_L, assumption+, clarify) 
79 
apply (rule_tac x=Y in rexI) 

80 
apply (simp_all add: Replace_iff univalent_def, blast) 

13223  81 
done 
82 

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

83 
subsection{*Instantiating the locale @{text M_trivial}*} 
13363  84 
text{*No instances of Separation yet.*} 
13291  85 

86 
lemma Lset_mono_le: "mono_le_subset(Lset)" 

13429  87 
by (simp add: mono_le_subset_def le_imp_subset Lset_mono) 
13291  88 

89 
lemma Lset_cont: "cont_Ord(Lset)" 

13429  90 
by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord) 
13291  91 

13428  92 
lemmas Pair_in_Lset = Formula.Pair_in_LLimit 
13291  93 

13428  94 
lemmas L_nat = Ord_in_L [OF Ord_nat] 
13291  95 

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

96 
theorem M_trivial_L: "PROP M_trivial(L)" 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

97 
apply (rule M_trivial.intro) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13566
diff
changeset

98 
apply (erule (1) transL) 
13428  99 
apply (rule upair_ax) 
100 
apply (rule Union_ax) 

101 
apply (rule power_ax) 

102 
apply (rule replacement) 

103 
apply (rule L_nat) 

104 
done 

13291  105 

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

106 
lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

107 
and rex_abs = M_trivial.rex_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

108 
and ball_iff_equiv = M_trivial.ball_iff_equiv [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

109 
and M_equalityI = M_trivial.M_equalityI [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

110 
and empty_abs = M_trivial.empty_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

111 
and subset_abs = M_trivial.subset_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

112 
and upair_abs = M_trivial.upair_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

113 
and upair_in_M_iff = M_trivial.upair_in_M_iff [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

114 
and singleton_in_M_iff = M_trivial.singleton_in_M_iff [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

115 
and pair_abs = M_trivial.pair_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

116 
and pair_in_M_iff = M_trivial.pair_in_M_iff [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

117 
and pair_components_in_M = M_trivial.pair_components_in_M [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

118 
and cartprod_abs = M_trivial.cartprod_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

119 
and union_abs = M_trivial.union_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

120 
and inter_abs = M_trivial.inter_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

121 
and setdiff_abs = M_trivial.setdiff_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

122 
and Union_abs = M_trivial.Union_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

123 
and Union_closed = M_trivial.Union_closed [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

124 
and Un_closed = M_trivial.Un_closed [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

125 
and cons_closed = M_trivial.cons_closed [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

126 
and successor_abs = M_trivial.successor_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

127 
and succ_in_M_iff = M_trivial.succ_in_M_iff [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

128 
and separation_closed = M_trivial.separation_closed [OF M_trivial_L] 
13566  129 
and strong_replacementI = 
130 
M_trivial.strong_replacementI [OF M_trivial_L, rule_format] 

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

131 
and strong_replacement_closed = M_trivial.strong_replacement_closed [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

132 
and RepFun_closed = M_trivial.RepFun_closed [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

133 
and lam_closed = M_trivial.lam_closed [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

134 
and image_abs = M_trivial.image_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

135 
and powerset_Pow = M_trivial.powerset_Pow [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

136 
and powerset_imp_subset_Pow = M_trivial.powerset_imp_subset_Pow [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

137 
and nat_into_M = M_trivial.nat_into_M [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

138 
and nat_case_closed = M_trivial.nat_case_closed [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

139 
and Inl_in_M_iff = M_trivial.Inl_in_M_iff [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

140 
and Inr_in_M_iff = M_trivial.Inr_in_M_iff [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

141 
and lt_closed = M_trivial.lt_closed [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

142 
and transitive_set_abs = M_trivial.transitive_set_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

143 
and ordinal_abs = M_trivial.ordinal_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

144 
and limit_ordinal_abs = M_trivial.limit_ordinal_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

145 
and successor_ordinal_abs = M_trivial.successor_ordinal_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

146 
and finite_ordinal_abs = M_trivial.finite_ordinal_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

147 
and omega_abs = M_trivial.omega_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

148 
and number1_abs = M_trivial.number1_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

149 
and number2_abs = M_trivial.number2_abs [OF M_trivial_L] 
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

150 
and number3_abs = M_trivial.number3_abs [OF M_trivial_L] 
13429  151 

152 
declare rall_abs [simp] 

153 
declare rex_abs [simp] 

154 
declare empty_abs [simp] 

155 
declare subset_abs [simp] 

156 
declare upair_abs [simp] 

157 
declare upair_in_M_iff [iff] 

158 
declare singleton_in_M_iff [iff] 

159 
declare pair_abs [simp] 

160 
declare pair_in_M_iff [iff] 

161 
declare cartprod_abs [simp] 

162 
declare union_abs [simp] 

163 
declare inter_abs [simp] 

164 
declare setdiff_abs [simp] 

165 
declare Union_abs [simp] 

166 
declare Union_closed [intro, simp] 

167 
declare Un_closed [intro, simp] 

168 
declare cons_closed [intro, simp] 

169 
declare successor_abs [simp] 

170 
declare succ_in_M_iff [iff] 

171 
declare separation_closed [intro, simp] 

172 
declare strong_replacement_closed [intro, simp] 

173 
declare RepFun_closed [intro, simp] 

174 
declare lam_closed [intro, simp] 

175 
declare image_abs [simp] 

176 
declare nat_into_M [intro] 

177 
declare Inl_in_M_iff [iff] 

178 
declare Inr_in_M_iff [iff] 

179 
declare transitive_set_abs [simp] 

180 
declare ordinal_abs [simp] 

181 
declare limit_ordinal_abs [simp] 

182 
declare successor_ordinal_abs [simp] 

183 
declare finite_ordinal_abs [simp] 

184 
declare omega_abs [simp] 

185 
declare number1_abs [simp] 

186 
declare number2_abs [simp] 

187 
declare number3_abs [simp] 

13291  188 

189 

190 
subsection{*Instantiation of the locale @{text reflection}*} 

191 

192 
text{*instances of locale constants*} 

193 
constdefs 

194 
L_F0 :: "[i=>o,i] => i" 

195 
"L_F0(P,y) == \<mu>b. (\<exists>z. L(z) \<and> P(<y,z>)) > (\<exists>z\<in>Lset(b). P(<y,z>))" 

196 

197 
L_FF :: "[i=>o,i] => i" 

198 
"L_FF(P) == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)" 

199 

200 
L_ClEx :: "[i=>o,i] => o" 

201 
"L_ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(L_FF(P),a) = a" 

202 

203 

13314  204 
text{*We must use the metaexistential quantifier; otherwise the reflection 
13429  205 
terms become enormous!*} 
13314  206 
constdefs 
207 
L_Reflects :: "[i=>o,[i,i]=>o] => prop" ("(3REFLECTS/ [_,/ _])") 

208 
"REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) & 

209 
(\<forall>a. Cl(a) > (\<forall>x \<in> Lset(a). P(x) <> Q(a,x))))" 

13291  210 

211 

13314  212 
theorem Triv_reflection: 
213 
"REFLECTS[P, \<lambda>a x. P(x)]" 

13429  214 
apply (simp add: L_Reflects_def) 
215 
apply (rule meta_exI) 

216 
apply (rule Closed_Unbounded_Ord) 

13314  217 
done 
218 

219 
theorem Not_reflection: 

220 
"REFLECTS[P,Q] ==> REFLECTS[\<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x)]" 

13429  221 
apply (unfold L_Reflects_def) 
222 
apply (erule meta_exE) 

223 
apply (rule_tac x=Cl in meta_exI, simp) 

13314  224 
done 
225 

226 
theorem And_reflection: 

13429  227 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
13314  228 
==> REFLECTS[\<lambda>x. P(x) \<and> P'(x), \<lambda>a x. Q(a,x) \<and> Q'(a,x)]" 
13429  229 
apply (unfold L_Reflects_def) 
230 
apply (elim meta_exE) 

231 
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI) 

232 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  233 
done 
234 

235 
theorem Or_reflection: 

13429  236 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
13314  237 
==> REFLECTS[\<lambda>x. P(x) \<or> P'(x), \<lambda>a x. Q(a,x) \<or> Q'(a,x)]" 
13429  238 
apply (unfold L_Reflects_def) 
239 
apply (elim meta_exE) 

240 
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI) 

241 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  242 
done 
243 

244 
theorem Imp_reflection: 

13429  245 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
13314  246 
==> REFLECTS[\<lambda>x. P(x) > P'(x), \<lambda>a x. Q(a,x) > Q'(a,x)]" 
13429  247 
apply (unfold L_Reflects_def) 
248 
apply (elim meta_exE) 

249 
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI) 

250 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  251 
done 
252 

253 
theorem Iff_reflection: 

13429  254 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
13314  255 
==> REFLECTS[\<lambda>x. P(x) <> P'(x), \<lambda>a x. Q(a,x) <> Q'(a,x)]" 
13429  256 
apply (unfold L_Reflects_def) 
257 
apply (elim meta_exE) 

258 
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI) 

259 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  260 
done 
261 

262 

13434  263 
lemma reflection_Lset: "reflection(Lset)" 
264 
apply (blast intro: reflection.intro Lset_mono_le Lset_cont Pair_in_Lset) + 

265 
done 

266 

13314  267 
theorem Ex_reflection: 
268 
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

269 
==> REFLECTS[\<lambda>x. \<exists>z. L(z) \<and> P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]" 

13429  270 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
271 
apply (elim meta_exE) 

13314  272 
apply (rule meta_exI) 
13434  273 
apply (erule reflection.Ex_reflection [OF reflection_Lset]) 
13291  274 
done 
275 

13314  276 
theorem All_reflection: 
277 
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

13429  278 
==> REFLECTS[\<lambda>x. \<forall>z. L(z) > P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]" 
279 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 

280 
apply (elim meta_exE) 

13314  281 
apply (rule meta_exI) 
13434  282 
apply (erule reflection.All_reflection [OF reflection_Lset]) 
13291  283 
done 
284 

13314  285 
theorem Rex_reflection: 
286 
"REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

287 
==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]" 

13429  288 
apply (unfold rex_def) 
13314  289 
apply (intro And_reflection Ex_reflection, assumption) 
290 
done 

13291  291 

13314  292 
theorem Rall_reflection: 
293 
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

13429  294 
==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]" 
295 
apply (unfold rall_def) 

13314  296 
apply (intro Imp_reflection All_reflection, assumption) 
297 
done 

298 

13440  299 
text{*This version handles an alternative form of the bounded quantifier 
300 
in the second argument of @{text REFLECTS}.*} 

301 
theorem Rex_reflection': 

302 
"REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

303 
==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[**Lset(a)]. Q(a,x,z)]" 

304 
apply (unfold setclass_def rex_def) 

305 
apply (erule Rex_reflection [unfolded rex_def Bex_def]) 

306 
done 

307 

308 
text{*As above.*} 

309 
theorem Rall_reflection': 

310 
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

311 
==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[**Lset(a)]. Q(a,x,z)]" 

312 
apply (unfold setclass_def rall_def) 

313 
apply (erule Rall_reflection [unfolded rall_def Ball_def]) 

314 
done 

315 

13429  316 
lemmas FOL_reflections = 
13314  317 
Triv_reflection Not_reflection And_reflection Or_reflection 
318 
Imp_reflection Iff_reflection Ex_reflection All_reflection 

13440  319 
Rex_reflection Rall_reflection Rex_reflection' Rall_reflection' 
13291  320 

321 
lemma ReflectsD: 

13429  322 
"[REFLECTS[P,Q]; Ord(i)] 
13291  323 
==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) <> Q(j,x))" 
13429  324 
apply (unfold L_Reflects_def Closed_Unbounded_def) 
325 
apply (elim meta_exE, clarify) 

326 
apply (blast dest!: UnboundedD) 

13291  327 
done 
328 

329 
lemma ReflectsE: 

13314  330 
"[ REFLECTS[P,Q]; Ord(i); 
13291  331 
!!j. [i<j; \<forall>x \<in> Lset(j). P(x) <> Q(j,x)] ==> R ] 
332 
==> R" 

13429  333 
apply (drule ReflectsD, assumption, blast) 
13314  334 
done 
13291  335 

13428  336 
lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B" 
13291  337 
by blast 
338 

339 

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

340 
subsection{*Internalized Formulas for some SetTheoretic Concepts*} 
13298  341 

13306  342 
lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex 
343 

344 
subsubsection{*Some numbers to help write de Bruijn indices*} 

345 

346 
syntax 

347 
"3" :: i ("3") 

348 
"4" :: i ("4") 

349 
"5" :: i ("5") 

350 
"6" :: i ("6") 

351 
"7" :: i ("7") 

352 
"8" :: i ("8") 

353 
"9" :: i ("9") 

354 

355 
translations 

356 
"3" == "succ(2)" 

357 
"4" == "succ(3)" 

358 
"5" == "succ(4)" 

359 
"6" == "succ(5)" 

360 
"7" == "succ(6)" 

361 
"8" == "succ(7)" 

362 
"9" == "succ(8)" 

363 

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

364 

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

365 
subsubsection{*The Empty Set, Internalized*} 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

366 

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

367 
constdefs empty_fm :: "i=>i" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

368 
"empty_fm(x) == Forall(Neg(Member(0,succ(x))))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

369 

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

370 
lemma empty_type [TC]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

371 
"x \<in> nat ==> empty_fm(x) \<in> formula" 
13429  372 
by (simp add: empty_fm_def) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

373 

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

374 
lemma arity_empty_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

375 
"x \<in> nat ==> arity(empty_fm(x)) = succ(x)" 
13429  376 
by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

377 

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

378 
lemma sats_empty_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

379 
"[ x \<in> nat; env \<in> list(A)] 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

380 
==> sats(A, empty_fm(x), env) <> empty(**A, nth(x,env))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

381 
by (simp add: empty_fm_def empty_def) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

382 

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

383 
lemma empty_iff_sats: 
13429  384 
"[ nth(i,env) = x; nth(j,env) = y; 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

385 
i \<in> nat; env \<in> list(A)] 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

386 
==> empty(**A, x) <> sats(A, empty_fm(i), env)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

387 
by simp 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

388 

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

389 
theorem empty_reflection: 
13429  390 
"REFLECTS[\<lambda>x. empty(L,f(x)), 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

391 
\<lambda>i x. empty(**Lset(i),f(x))]" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

392 
apply (simp only: empty_def setclass_simps) 
13429  393 
apply (intro FOL_reflections) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

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

395 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

396 
text{*Not used. But maybe useful?*} 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

397 
lemma Transset_sats_empty_fm_eq_0: 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

398 
"[ n \<in> nat; env \<in> list(A); Transset(A)] 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

399 
==> sats(A, empty_fm(n), env) <> nth(n,env) = 0" 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

400 
apply (simp add: empty_fm_def empty_def Transset_def, auto) 
13429  401 
apply (case_tac "n < length(env)") 
402 
apply (frule nth_type, assumption+, blast) 

403 
apply (simp_all add: not_lt_iff_le nth_eq_0) 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

404 
done 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

405 

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

406 

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

407 
subsubsection{*Unordered Pairs, Internalized*} 
13298  408 

409 
constdefs upair_fm :: "[i,i,i]=>i" 

13429  410 
"upair_fm(x,y,z) == 
411 
And(Member(x,z), 

13298  412 
And(Member(y,z), 
13429  413 
Forall(Implies(Member(0,succ(z)), 
13298  414 
Or(Equal(0,succ(x)), Equal(0,succ(y)))))))" 
415 

416 
lemma upair_type [TC]: 

417 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> upair_fm(x,y,z) \<in> formula" 

13429  418 
by (simp add: upair_fm_def) 
13298  419 

420 
lemma arity_upair_fm [simp]: 

13429  421 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13298  422 
==> arity(upair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  423 
by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac) 
13298  424 

425 
lemma sats_upair_fm [simp]: 

426 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  427 
==> sats(A, upair_fm(x,y,z), env) <> 
13298  428 
upair(**A, nth(x,env), nth(y,env), nth(z,env))" 
429 
by (simp add: upair_fm_def upair_def) 

430 

431 
lemma upair_iff_sats: 

13429  432 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13298  433 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
434 
==> upair(**A, x, y, z) <> sats(A, upair_fm(i,j,k), env)" 

435 
by (simp add: sats_upair_fm) 

436 

437 
text{*Useful? At least it refers to "real" unordered pairs*} 

438 
lemma sats_upair_fm2 [simp]: 

439 
"[ x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A); Transset(A)] 

13429  440 
==> sats(A, upair_fm(x,y,z), env) <> 
13298  441 
nth(z,env) = {nth(x,env), nth(y,env)}" 
13429  442 
apply (frule lt_length_in_nat, assumption) 
443 
apply (simp add: upair_fm_def Transset_def, auto) 

444 
apply (blast intro: nth_type) 

13298  445 
done 
446 

13314  447 
theorem upair_reflection: 
13429  448 
"REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)), 
449 
\<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]" 

13314  450 
apply (simp add: upair_def) 
13429  451 
apply (intro FOL_reflections) 
13314  452 
done 
13306  453 

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

454 
subsubsection{*Ordered pairs, Internalized*} 
13298  455 

456 
constdefs pair_fm :: "[i,i,i]=>i" 

13429  457 
"pair_fm(x,y,z) == 
13298  458 
Exists(And(upair_fm(succ(x),succ(x),0), 
459 
Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0), 

460 
upair_fm(1,0,succ(succ(z)))))))" 

461 

462 
lemma pair_type [TC]: 

463 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> pair_fm(x,y,z) \<in> formula" 

13429  464 
by (simp add: pair_fm_def) 
13298  465 

466 
lemma arity_pair_fm [simp]: 

13429  467 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13298  468 
==> arity(pair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  469 
by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac) 
13298  470 

471 
lemma sats_pair_fm [simp]: 

472 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  473 
==> sats(A, pair_fm(x,y,z), env) <> 
13298  474 
pair(**A, nth(x,env), nth(y,env), nth(z,env))" 
475 
by (simp add: pair_fm_def pair_def) 

476 

477 
lemma pair_iff_sats: 

13429  478 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13298  479 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
480 
==> pair(**A, x, y, z) <> sats(A, pair_fm(i,j,k), env)" 

481 
by (simp add: sats_pair_fm) 

482 

13314  483 
theorem pair_reflection: 
13429  484 
"REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)), 
13314  485 
\<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]" 
486 
apply (simp only: pair_def setclass_simps) 

13429  487 
apply (intro FOL_reflections upair_reflection) 
13314  488 
done 
13306  489 

490 

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

491 
subsubsection{*Binary Unions, Internalized*} 
13298  492 

13306  493 
constdefs union_fm :: "[i,i,i]=>i" 
13429  494 
"union_fm(x,y,z) == 
13306  495 
Forall(Iff(Member(0,succ(z)), 
496 
Or(Member(0,succ(x)),Member(0,succ(y)))))" 

497 

498 
lemma union_type [TC]: 

499 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> union_fm(x,y,z) \<in> formula" 

13429  500 
by (simp add: union_fm_def) 
13306  501 

502 
lemma arity_union_fm [simp]: 

13429  503 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13306  504 
==> arity(union_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  505 
by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac) 
13298  506 

13306  507 
lemma sats_union_fm [simp]: 
508 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  509 
==> sats(A, union_fm(x,y,z), env) <> 
13306  510 
union(**A, nth(x,env), nth(y,env), nth(z,env))" 
511 
by (simp add: union_fm_def union_def) 

512 

513 
lemma union_iff_sats: 

13429  514 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  515 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
516 
==> union(**A, x, y, z) <> sats(A, union_fm(i,j,k), env)" 

517 
by (simp add: sats_union_fm) 

13298  518 

13314  519 
theorem union_reflection: 
13429  520 
"REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)), 
13314  521 
\<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]" 
522 
apply (simp only: union_def setclass_simps) 

13429  523 
apply (intro FOL_reflections) 
13314  524 
done 
13306  525 

13298  526 

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

527 
subsubsection{*Set ``Cons,'' Internalized*} 
13306  528 

529 
constdefs cons_fm :: "[i,i,i]=>i" 

13429  530 
"cons_fm(x,y,z) == 
13306  531 
Exists(And(upair_fm(succ(x),succ(x),0), 
532 
union_fm(0,succ(y),succ(z))))" 

13298  533 

534 

13306  535 
lemma cons_type [TC]: 
536 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> cons_fm(x,y,z) \<in> formula" 

13429  537 
by (simp add: cons_fm_def) 
13306  538 

539 
lemma arity_cons_fm [simp]: 

13429  540 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13306  541 
==> arity(cons_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  542 
by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  543 

544 
lemma sats_cons_fm [simp]: 

545 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  546 
==> sats(A, cons_fm(x,y,z), env) <> 
13306  547 
is_cons(**A, nth(x,env), nth(y,env), nth(z,env))" 
548 
by (simp add: cons_fm_def is_cons_def) 

549 

550 
lemma cons_iff_sats: 

13429  551 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  552 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
553 
==> is_cons(**A, x, y, z) <> sats(A, cons_fm(i,j,k), env)" 

554 
by simp 

555 

13314  556 
theorem cons_reflection: 
13429  557 
"REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)), 
13314  558 
\<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]" 
559 
apply (simp only: is_cons_def setclass_simps) 

13429  560 
apply (intro FOL_reflections upair_reflection union_reflection) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

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

562 

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

563 

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

564 
subsubsection{*Successor Function, Internalized*} 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

565 

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

566 
constdefs succ_fm :: "[i,i]=>i" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

567 
"succ_fm(x,y) == cons_fm(x,x,y)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

568 

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

569 
lemma succ_type [TC]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

570 
"[ x \<in> nat; y \<in> nat ] ==> succ_fm(x,y) \<in> formula" 
13429  571 
by (simp add: succ_fm_def) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

572 

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

573 
lemma arity_succ_fm [simp]: 
13429  574 
"[ x \<in> nat; y \<in> nat ] 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

575 
==> arity(succ_fm(x,y)) = succ(x) \<union> succ(y)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

576 
by (simp add: succ_fm_def) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

577 

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

578 
lemma sats_succ_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

579 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 
13429  580 
==> sats(A, succ_fm(x,y), env) <> 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

581 
successor(**A, nth(x,env), nth(y,env))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

582 
by (simp add: succ_fm_def successor_def) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

583 

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

584 
lemma successor_iff_sats: 
13429  585 
"[ nth(i,env) = x; nth(j,env) = y; 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

586 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

587 
==> successor(**A, x, y) <> sats(A, succ_fm(i,j), env)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

588 
by simp 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

589 

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

590 
theorem successor_reflection: 
13429  591 
"REFLECTS[\<lambda>x. successor(L,f(x),g(x)), 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

592 
\<lambda>i x. successor(**Lset(i),f(x),g(x))]" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

593 
apply (simp only: successor_def setclass_simps) 
13429  594 
apply (intro cons_reflection) 
13314  595 
done 
13298  596 

597 

13363  598 
subsubsection{*The Number 1, Internalized*} 
599 

600 
(* "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))" *) 

601 
constdefs number1_fm :: "i=>i" 

602 
"number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))" 

603 

604 
lemma number1_type [TC]: 

605 
"x \<in> nat ==> number1_fm(x) \<in> formula" 

13429  606 
by (simp add: number1_fm_def) 
13363  607 

608 
lemma arity_number1_fm [simp]: 

609 
"x \<in> nat ==> arity(number1_fm(x)) = succ(x)" 

13429  610 
by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac) 
13363  611 

612 
lemma sats_number1_fm [simp]: 

613 
"[ x \<in> nat; env \<in> list(A)] 

614 
==> sats(A, number1_fm(x), env) <> number1(**A, nth(x,env))" 

615 
by (simp add: number1_fm_def number1_def) 

616 

617 
lemma number1_iff_sats: 

13429  618 
"[ nth(i,env) = x; nth(j,env) = y; 
13363  619 
i \<in> nat; env \<in> list(A)] 
620 
==> number1(**A, x) <> sats(A, number1_fm(i), env)" 

621 
by simp 

622 

623 
theorem number1_reflection: 

13429  624 
"REFLECTS[\<lambda>x. number1(L,f(x)), 
13363  625 
\<lambda>i x. number1(**Lset(i),f(x))]" 
626 
apply (simp only: number1_def setclass_simps) 

627 
apply (intro FOL_reflections empty_reflection successor_reflection) 

628 
done 

629 

630 

13352  631 
subsubsection{*Big Union, Internalized*} 
13306  632 

13352  633 
(* "big_union(M,A,z) == \<forall>x[M]. x \<in> z <> (\<exists>y[M]. y\<in>A & x \<in> y)" *) 
634 
constdefs big_union_fm :: "[i,i]=>i" 

13429  635 
"big_union_fm(A,z) == 
13352  636 
Forall(Iff(Member(0,succ(z)), 
637 
Exists(And(Member(0,succ(succ(A))), Member(1,0)))))" 

13298  638 

13352  639 
lemma big_union_type [TC]: 
640 
"[ x \<in> nat; y \<in> nat ] ==> big_union_fm(x,y) \<in> formula" 

13429  641 
by (simp add: big_union_fm_def) 
13306  642 

13352  643 
lemma arity_big_union_fm [simp]: 
13429  644 
"[ x \<in> nat; y \<in> nat ] 
13352  645 
==> arity(big_union_fm(x,y)) = succ(x) \<union> succ(y)" 
646 
by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac) 

13298  647 

13352  648 
lemma sats_big_union_fm [simp]: 
649 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  650 
==> sats(A, big_union_fm(x,y), env) <> 
13352  651 
big_union(**A, nth(x,env), nth(y,env))" 
652 
by (simp add: big_union_fm_def big_union_def) 

13306  653 

13352  654 
lemma big_union_iff_sats: 
13429  655 
"[ nth(i,env) = x; nth(j,env) = y; 
13352  656 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
657 
==> big_union(**A, x, y) <> sats(A, big_union_fm(i,j), env)" 

13306  658 
by simp 
659 

13352  660 
theorem big_union_reflection: 
13429  661 
"REFLECTS[\<lambda>x. big_union(L,f(x),g(x)), 
13352  662 
\<lambda>i x. big_union(**Lset(i),f(x),g(x))]" 
663 
apply (simp only: big_union_def setclass_simps) 

13429  664 
apply (intro FOL_reflections) 
13314  665 
done 
13298  666 

667 

13306  668 
subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*} 
669 

670 
text{*Differs from the one in Formula by using "ordinal" rather than "Ord"*} 

671 

672 

673 
lemma sats_subset_fm': 

674 
"[x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  675 
==> sats(A, subset_fm(x,y), env) <> subset(**A, nth(x,env), nth(y,env))" 
676 
by (simp add: subset_fm_def Relative.subset_def) 

13298  677 

13314  678 
theorem subset_reflection: 
13429  679 
"REFLECTS[\<lambda>x. subset(L,f(x),g(x)), 
680 
\<lambda>i x. subset(**Lset(i),f(x),g(x))]" 

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

681 
apply (simp only: Relative.subset_def setclass_simps) 
13429  682 
apply (intro FOL_reflections) 
13314  683 
done 
13306  684 

685 
lemma sats_transset_fm': 

686 
"[x \<in> nat; env \<in> list(A)] 

687 
==> sats(A, transset_fm(x), env) <> transitive_set(**A, nth(x,env))" 

13429  688 
by (simp add: sats_subset_fm' transset_fm_def transitive_set_def) 
13298  689 

13314  690 
theorem transitive_set_reflection: 
691 
"REFLECTS[\<lambda>x. transitive_set(L,f(x)), 

692 
\<lambda>i x. transitive_set(**Lset(i),f(x))]" 

693 
apply (simp only: transitive_set_def setclass_simps) 

13429  694 
apply (intro FOL_reflections subset_reflection) 
13314  695 
done 
13306  696 

697 
lemma sats_ordinal_fm': 

698 
"[x \<in> nat; env \<in> list(A)] 

699 
==> sats(A, ordinal_fm(x), env) <> ordinal(**A,nth(x,env))" 

700 
by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def) 

701 

702 
lemma ordinal_iff_sats: 

703 
"[ nth(i,env) = x; i \<in> nat; env \<in> list(A)] 

704 
==> ordinal(**A, x) <> sats(A, ordinal_fm(i), env)" 

705 
by (simp add: sats_ordinal_fm') 

706 

13314  707 
theorem ordinal_reflection: 
708 
"REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]" 

709 
apply (simp only: ordinal_def setclass_simps) 

13429  710 
apply (intro FOL_reflections transitive_set_reflection) 
13314  711 
done 
13298  712 

713 

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

714 
subsubsection{*Membership Relation, Internalized*} 
13298  715 

13306  716 
constdefs Memrel_fm :: "[i,i]=>i" 
13429  717 
"Memrel_fm(A,r) == 
13306  718 
Forall(Iff(Member(0,succ(r)), 
719 
Exists(And(Member(0,succ(succ(A))), 

720 
Exists(And(Member(0,succ(succ(succ(A)))), 

721 
And(Member(1,0), 

722 
pair_fm(1,0,2))))))))" 

723 

724 
lemma Memrel_type [TC]: 

725 
"[ x \<in> nat; y \<in> nat ] ==> Memrel_fm(x,y) \<in> formula" 

13429  726 
by (simp add: Memrel_fm_def) 
13298  727 

13306  728 
lemma arity_Memrel_fm [simp]: 
13429  729 
"[ x \<in> nat; y \<in> nat ] 
13306  730 
==> arity(Memrel_fm(x,y)) = succ(x) \<union> succ(y)" 
13429  731 
by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  732 

733 
lemma sats_Memrel_fm [simp]: 

734 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  735 
==> sats(A, Memrel_fm(x,y), env) <> 
13306  736 
membership(**A, nth(x,env), nth(y,env))" 
737 
by (simp add: Memrel_fm_def membership_def) 

13298  738 

13306  739 
lemma Memrel_iff_sats: 
13429  740 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  741 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
742 
==> membership(**A, x, y) <> sats(A, Memrel_fm(i,j), env)" 

743 
by simp 

13304  744 

13314  745 
theorem membership_reflection: 
13429  746 
"REFLECTS[\<lambda>x. membership(L,f(x),g(x)), 
13314  747 
\<lambda>i x. membership(**Lset(i),f(x),g(x))]" 
748 
apply (simp only: membership_def setclass_simps) 

13429  749 
apply (intro FOL_reflections pair_reflection) 
13314  750 
done 
13304  751 

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

752 
subsubsection{*Predecessor Set, Internalized*} 
13304  753 

13306  754 
constdefs pred_set_fm :: "[i,i,i,i]=>i" 
13429  755 
"pred_set_fm(A,x,r,B) == 
13306  756 
Forall(Iff(Member(0,succ(B)), 
757 
Exists(And(Member(0,succ(succ(r))), 

758 
And(Member(1,succ(succ(A))), 

759 
pair_fm(1,succ(succ(x)),0))))))" 

760 

761 

762 
lemma pred_set_type [TC]: 

13429  763 
"[ A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat ] 
13306  764 
==> pred_set_fm(A,x,r,B) \<in> formula" 
13429  765 
by (simp add: pred_set_fm_def) 
13304  766 

13306  767 
lemma arity_pred_set_fm [simp]: 
13429  768 
"[ A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat ] 
13306  769 
==> arity(pred_set_fm(A,x,r,B)) = succ(A) \<union> succ(x) \<union> succ(r) \<union> succ(B)" 
13429  770 
by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  771 

772 
lemma sats_pred_set_fm [simp]: 

773 
"[ U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)] 

13429  774 
==> sats(A, pred_set_fm(U,x,r,B), env) <> 
13306  775 
pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))" 
776 
by (simp add: pred_set_fm_def pred_set_def) 

777 

778 
lemma pred_set_iff_sats: 

13429  779 
"[ nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B; 
13306  780 
i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)] 
781 
==> pred_set(**A,U,x,r,B) <> sats(A, pred_set_fm(i,j,k,l), env)" 

782 
by (simp add: sats_pred_set_fm) 

783 

13314  784 
theorem pred_set_reflection: 
13429  785 
"REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)), 
786 
\<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]" 

13314  787 
apply (simp only: pred_set_def setclass_simps) 
13429  788 
apply (intro FOL_reflections pair_reflection) 
13314  789 
done 
13304  790 

791 

13298  792 

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

793 
subsubsection{*Domain of a Relation, Internalized*} 
13306  794 

13429  795 
(* "is_domain(M,r,z) == 
796 
\<forall>x[M]. (x \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *) 

13306  797 
constdefs domain_fm :: "[i,i]=>i" 
13429  798 
"domain_fm(r,z) == 
13306  799 
Forall(Iff(Member(0,succ(z)), 
800 
Exists(And(Member(0,succ(succ(r))), 

801 
Exists(pair_fm(2,0,1))))))" 

802 

803 
lemma domain_type [TC]: 

804 
"[ x \<in> nat; y \<in> nat ] ==> domain_fm(x,y) \<in> formula" 

13429  805 
by (simp add: domain_fm_def) 
13306  806 

807 
lemma arity_domain_fm [simp]: 

13429  808 
"[ x \<in> nat; y \<in> nat ] 
13306  809 
==> arity(domain_fm(x,y)) = succ(x) \<union> succ(y)" 
13429  810 
by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  811 

812 
lemma sats_domain_fm [simp]: 

813 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  814 
==> sats(A, domain_fm(x,y), env) <> 
13306  815 
is_domain(**A, nth(x,env), nth(y,env))" 
816 
by (simp add: domain_fm_def is_domain_def) 

817 

818 
lemma domain_iff_sats: 

13429  819 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  820 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
821 
==> is_domain(**A, x, y) <> sats(A, domain_fm(i,j), env)" 

822 
by simp 

823 

13314  824 
theorem domain_reflection: 
13429  825 
"REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)), 
13314  826 
\<lambda>i x. is_domain(**Lset(i),f(x),g(x))]" 
827 
apply (simp only: is_domain_def setclass_simps) 

13429  828 
apply (intro FOL_reflections pair_reflection) 
13314  829 
done 
13306  830 

831 

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

832 
subsubsection{*Range of a Relation, Internalized*} 
13306  833 

13429  834 
(* "is_range(M,r,z) == 
835 
\<forall>y[M]. (y \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *) 

13306  836 
constdefs range_fm :: "[i,i]=>i" 
13429  837 
"range_fm(r,z) == 
13306  838 
Forall(Iff(Member(0,succ(z)), 
839 
Exists(And(Member(0,succ(succ(r))), 

840 
Exists(pair_fm(0,2,1))))))" 

841 

842 
lemma range_type [TC]: 

843 
"[ x \<in> nat; y \<in> nat ] ==> range_fm(x,y) \<in> formula" 

13429  844 
by (simp add: range_fm_def) 
13306  845 

846 
lemma arity_range_fm [simp]: 

13429  847 
"[ x \<in> nat; y \<in> nat ] 
13306  848 
==> arity(range_fm(x,y)) = succ(x) \<union> succ(y)" 
13429  849 
by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  850 

851 
lemma sats_range_fm [simp]: 

852 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  853 
==> sats(A, range_fm(x,y), env) <> 
13306  854 
is_range(**A, nth(x,env), nth(y,env))" 
855 
by (simp add: range_fm_def is_range_def) 

856 

857 
lemma range_iff_sats: 

13429  858 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  859 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
860 
==> is_range(**A, x, y) <> sats(A, range_fm(i,j), env)" 

861 
by simp 

862 

13314  863 
theorem range_reflection: 
13429  864 
"REFLECTS[\<lambda>x. is_range(L,f(x),g(x)), 
13314  865 
\<lambda>i x. is_range(**Lset(i),f(x),g(x))]" 
866 
apply (simp only: is_range_def setclass_simps) 

13429  867 
apply (intro FOL_reflections pair_reflection) 
13314  868 
done 
13306  869 

13429  870 

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

871 
subsubsection{*Field of a Relation, Internalized*} 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

872 

13429  873 
(* "is_field(M,r,z) == 
874 
\<exists>dr[M]. is_domain(M,r,dr) & 

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

875 
(\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

876 
constdefs field_fm :: "[i,i]=>i" 
13429  877 
"field_fm(r,z) == 
878 
Exists(And(domain_fm(succ(r),0), 

879 
Exists(And(range_fm(succ(succ(r)),0), 

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

880 
union_fm(1,0,succ(succ(z)))))))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

881 

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

882 
lemma field_type [TC]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

883 
"[ x \<in> nat; y \<in> nat ] ==> field_fm(x,y) \<in> formula" 
13429  884 
by (simp add: field_fm_def) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

885 

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

886 
lemma arity_field_fm [simp]: 
13429  887 
"[ x \<in> nat; y \<in> nat ] 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

888 
==> arity(field_fm(x,y)) = succ(x) \<union> succ(y)" 
13429  889 
by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

890 

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

891 
lemma sats_field_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

892 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 
13429  893 
==> sats(A, field_fm(x,y), env) <> 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

894 
is_field(**A, nth(x,env), nth(y,env))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

895 
by (simp add: field_fm_def is_field_def) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

896 

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

897 
lemma field_iff_sats: 
13429  898 
"[ nth(i,env) = x; nth(j,env) = y; 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

899 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

900 
==> is_field(**A, x, y) <> sats(A, field_fm(i,j), env)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

901 
by simp 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

902 

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

903 
theorem field_reflection: 
13429  904 
"REFLECTS[\<lambda>x. is_field(L,f(x),g(x)), 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

905 
\<lambda>i x. is_field(**Lset(i),f(x),g(x))]" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

906 
apply (simp only: is_field_def setclass_simps) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

907 
apply (intro FOL_reflections domain_reflection range_reflection 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

908 
union_reflection) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

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

910 

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

911 

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

912 
subsubsection{*Image under a Relation, Internalized*} 
13306  913 

13429  914 
(* "image(M,r,A,z) == 
13306  915 
\<forall>y[M]. (y \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *) 
916 
constdefs image_fm :: "[i,i,i]=>i" 

13429  917 
"image_fm(r,A,z) == 
13306  918 
Forall(Iff(Member(0,succ(z)), 
919 
Exists(And(Member(0,succ(succ(r))), 

920 
Exists(And(Member(0,succ(succ(succ(A)))), 

13429  921 
pair_fm(0,2,1)))))))" 
13306  922 

923 
lemma image_type [TC]: 

924 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> image_fm(x,y,z) \<in> formula" 

13429  925 
by (simp add: image_fm_def) 
13306  926 

927 
lemma arity_image_fm [simp]: 

13429  928 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13306  929 
==> arity(image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  930 
by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  931 

932 
lemma sats_image_fm [simp]: 

933 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  934 
==> sats(A, image_fm(x,y,z), env) <> 
13306  935 
image(**A, nth(x,env), nth(y,env), nth(z,env))" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

936 
by (simp add: image_fm_def Relative.image_def) 
13306  937 

938 
lemma image_iff_sats: 

13429  939 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  940 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
941 
==> image(**A, x, y, z) <> sats(A, image_fm(i,j,k), env)" 

942 
by (simp add: sats_image_fm) 

943 

13314  944 
theorem image_reflection: 
13429  945 
"REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)), 
13314  946 
\<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

947 
apply (simp only: Relative.image_def setclass_simps) 
13429  948 
apply (intro FOL_reflections pair_reflection) 
13314  949 
done 
13306  950 

951 

13348  952 
subsubsection{*PreImage under a Relation, Internalized*} 
953 

13429  954 
(* "pre_image(M,r,A,z) == 
955 
\<forall>x[M]. x \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *) 

13348  956 
constdefs pre_image_fm :: "[i,i,i]=>i" 
13429  957 
"pre_image_fm(r,A,z) == 
13348  958 
Forall(Iff(Member(0,succ(z)), 
959 
Exists(And(Member(0,succ(succ(r))), 

960 
Exists(And(Member(0,succ(succ(succ(A)))), 

13429  961 
pair_fm(2,0,1)))))))" 
13348  962 

963 
lemma pre_image_type [TC]: 

964 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> pre_image_fm(x,y,z) \<in> formula" 

13429  965 
by (simp add: pre_image_fm_def) 
13348  966 

967 
lemma arity_pre_image_fm [simp]: 

13429  968 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13348  969 
==> arity(pre_image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  970 
by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac) 
13348  971 

972 
lemma sats_pre_image_fm [simp]: 

973 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  974 
==> sats(A, pre_image_fm(x,y,z), env) <> 
13348  975 
pre_image(**A, nth(x,env), nth(y,env), nth(z,env))" 
976 
by (simp add: pre_image_fm_def Relative.pre_image_def) 

977 

978 
lemma pre_image_iff_sats: 

13429  979 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13348  980 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
981 
==> pre_image(**A, x, y, z) <> sats(A, pre_image_fm(i,j,k), env)" 

982 
by (simp add: sats_pre_image_fm) 

983 

984 
theorem pre_image_reflection: 

13429  985 
"REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)), 
13348  986 
\<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]" 
987 
apply (simp only: Relative.pre_image_def setclass_simps) 

13429  988 
apply (intro FOL_reflections pair_reflection) 
13348  989 
done 
990 

991 

13352  992 
subsubsection{*Function Application, Internalized*} 
993 

13429  994 
(* "fun_apply(M,f,x,y) == 
995 
(\<exists>xs[M]. \<exists>fxs[M]. 

13352  996 
upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *) 
997 
constdefs fun_apply_fm :: "[i,i,i]=>i" 

13429  998 
"fun_apply_fm(f,x,y) == 
13352  999 
Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1), 
13429  1000 
And(image_fm(succ(succ(f)), 1, 0), 
13352  1001 
big_union_fm(0,succ(succ(y)))))))" 
1002 

1003 
lemma fun_apply_type [TC]: 

1004 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> fun_apply_fm(x,y,z) \<in> formula" 

13429  1005 
by (simp add: fun_apply_fm_def) 
13352  1006 

1007 
lemma arity_fun_apply_fm [simp]: 

13429  1008 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13352  1009 
==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  1010 
by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac) 
13352  1011 

1012 
lemma sats_fun_apply_fm [simp]: 

1013 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  1014 
==> sats(A, fun_apply_fm(x,y,z), env) <> 
13352  1015 
fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))" 
1016 
by (simp add: fun_apply_fm_def fun_apply_def) 

1017 

1018 
lemma fun_apply_iff_sats: 

13429  1019 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13352  1020 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
1021 
==> fun_apply(**A, x, y, z) <> sats(A, fun_apply_fm(i,j,k), env)" 

1022 
by simp 

1023 

1024 
theorem fun_apply_reflection: 

13429  1025 
"REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)), 
1026 
\<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" 

13352  1027 
apply (simp only: fun_apply_def setclass_simps) 
1028 
apply (intro FOL_reflections upair_reflection image_reflection 

13429  1029 
big_union_reflection) 
13352  1030 
done 
1031 

1032 

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

1033 
subsubsection{*The Concept of Relation, Internalized*} 
13306  1034 

13429  1035 
(* "is_relation(M,r) == 
13306  1036 
(\<forall>z[M]. z\<in>r > (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *) 
1037 
constdefs relation_fm :: "i=>i" 

13429  1038 
"relation_fm(r) == 
13306  1039 
Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))" 
1040 

1041 
lemma relation_type [TC]: 

1042 
"[ x \<in> nat ] ==> relation_fm(x) \<in> formula" 

13429  1043 
by (simp add: relation_fm_def) 
13306  1044 

1045 
lemma arity_relation_fm [simp]: 

1046 
"x \<in> nat ==> arity(relation_fm(x)) = succ(x)" 

13429  1047 
by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  1048 

1049 
lemma sats_relation_fm [simp]: 

1050 
"[ x \<in> nat; env \<in> list(A)] 

1051 
==> sats(A, relation_fm(x), env) <> is_relation(**A, nth(x,env))" 

1052 
by (simp add: relation_fm_def is_relation_def) 

1053 

1054 
lemma relation_iff_sats: 

13429  1055 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  1056 
i \<in> nat; env \<in> list(A)] 
1057 
==> is_relation(**A, x) <> sats(A, relation_fm(i), env)" 

1058 
by simp 

1059 

13314  1060 
theorem is_relation_reflection: 
13429  1061 
"REFLECTS[\<lambda>x. is_relation(L,f(x)), 
13314  1062 
\<lambda>i x. is_relation(**Lset(i),f(x))]" 
1063 
apply (simp only: is_relation_def setclass_simps) 

13429  1064 
apply (intro FOL_reflections pair_reflection) 
13314  1065 
done 
13306  1066 

1067 

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

1068 
subsubsection{*The Concept of Function, Internalized*} 
13306  1069 

13429  1070 
(* "is_function(M,r) == 
1071 
\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 

13306  1072 
pair(M,x,y,p) > pair(M,x,y',p') > p\<in>r > p'\<in>r > y=y'" *) 
1073 
constdefs function_fm :: "i=>i" 

13429  1074 
"function_fm(r) == 
13306  1075 
Forall(Forall(Forall(Forall(Forall( 
1076 
Implies(pair_fm(4,3,1), 

1077 
Implies(pair_fm(4,2,0), 

1078 
Implies(Member(1,r#+5), 

1079 
Implies(Member(0,r#+5), Equal(3,2))))))))))" 

1080 

1081 
lemma function_type [TC]: 

1082 
"[ x \<in> nat ] ==> function_fm(x) \<in> formula" 

13429  1083 
by (simp add: function_fm_def) 
13306  1084 

1085 
lemma arity_function_fm [simp]: 

1086 
"x \<in> nat ==> arity(function_fm(x)) = succ(x)" 

13429  1087 
by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  1088 

1089 
lemma sats_function_fm [simp]: 

1090 
"[ x \<in> nat; env \<in> list(A)] 

1091 
==> sats(A, function_fm(x), env) <> is_function(**A, nth(x,env))" 

1092 
by (simp add: function_fm_def is_function_def) 

1093 

13505  1094 
lemma is_function_iff_sats: 
13429  1095 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  1096 
i \<in> nat; env \<in> list(A)] 
1097 
==> is_function(**A, x) <> sats(A, function_fm(i), env)" 

1098 
by simp 

1099 

13314  1100 
theorem is_function_reflection: 
13429  1101 
"REFLECTS[\<lambda>x. is_function(L,f(x)), 
13314  1102 
\<lambda>i x. is_function(**Lset(i),f(x))]" 
1103 
apply (simp only: is_function_def setclass_simps) 

13429  1104 
apply (intro FOL_reflections pair_reflection) 
13314  1105 
done 
13298  1106 

1107 

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

1108 
subsubsection{*Typed Functions, Internalized*} 
13309  1109 

13429  1110 
(* "typed_function(M,A,B,r) == 
13309  1111 
is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & 
1112 
(\<forall>u[M]. u\<in>r > (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) > y\<in>B))" *) 

1113 

1114 
constdefs typed_function_fm :: "[i,i,i]=>i" 

13429  1115 
"typed_function_fm(A,B,r) == 
13309  1116 
And(function_fm(r), 
1117 
And(relation_fm(r), 

1118 
And(domain_fm(r,A), 

1119 
Forall(Implies(Member(0,succ(r)), 

1120 
Forall(Forall(Implies(pair_fm(1,0,2),Member(0,B#+3)))))))))" 

1121 

1122 
lemma typed_function_type [TC]: 

1123 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> typed_function_fm(x,y,z) \<in> formula" 

13429  1124 
by (simp add: typed_function_fm_def) 
13309  1125 

1126 
lemma arity_typed_function_fm [simp]: 

13429  1127 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13309  1128 
==> arity(typed_function_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  1129 
by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac) 
13309  1130 

1131 
lemma sats_typed_function_fm [simp]: 

1132 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  1133 
==> sats(A, typed_function_fm(x,y,z), env) <> 
13309  1134 
typed_function(**A, nth(x,env), nth(y,env), nth(z,env))" 
1135 
by (simp add: typed_function_fm_def typed_function_def) 

1136 

1137 
lemma typed_function_iff_sats: 

13429  1138 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13309  1139 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
1140 
==> typed_function(**A, x, y, z) <> sats(A, typed_function_fm(i,j,k), env)" 

1141 
by simp 

1142 

13429  1143 
lemmas function_reflections = 
13363  1144 
empty_reflection number1_reflection 
13429  1145 
upair_reflection pair_reflection union_reflection 
1146 
big_union_reflection cons_reflection successor_reflection 

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

1147 
fun_apply_reflection subset_reflection 
13429  1148 
transitive_set_reflection membership_reflection 
1149 
pred_set_reflection domain_reflection range_reflection field_reflection 

13348  1150 
image_reflection pre_image_reflection 
13429  1151 
is_relation_reflection is_function_reflection 
13309  1152 

13429  1153 
lemmas function_iff_sats = 
1154 
empty_iff_sats number1_iff_sats 

1155 
upair_iff_sats pair_iff_sats union_iff_sats 

13505  1156 
big_union_iff_sats cons_iff_sats successor_iff_sats 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1157 
fun_apply_iff_sats Memrel_iff_sats 
13429  1158 
pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats 
1159 
image_iff_sats pre_image_iff_sats 

13505  1160 
relation_iff_sats is_function_iff_sats 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1161 

13309  1162 

13314  1163 
theorem typed_function_reflection: 
13429  1164 
"REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)), 
13314  1165 
\<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]" 
1166 
apply (simp only: typed_function_def setclass_simps) 

13429  1167 
apply (intro FOL_reflections function_reflections) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

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

1169 

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

1170 

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

1171 
subsubsection{*Composition of Relations, Internalized*} 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1172 

13429  1173 
(* "composition(M,r,s,t) == 
1174 
\<forall>p[M]. p \<in> t <> 

1175 
(\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 

1176 
pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 

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

1177 
xy \<in> s & yz \<in> r)" *) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1178 
constdefs composition_fm :: "[i,i,i]=>i" 
13429  1179 
"composition_fm(r,s,t) == 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1180 
Forall(Iff(Member(0,succ(t)), 
13429  1181 
Exists(Exists(Exists(Exists(Exists( 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1182 
And(pair_fm(4,2,5), 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1183 
And(pair_fm(4,3,1), 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1184 
And(pair_fm(3,2,0), 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1185 
And(Member(1,s#+6), Member(0,r#+6))))))))))))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1186 

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

1187 
lemma composition_type [TC]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1188 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> composition_fm(x,y,z) \<in> formula" 
13429  1189 
by (simp add: composition_fm_def) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1190 

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

1191 
lemma arity_composition_fm [simp]: 
13429  1192 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1193 
==> arity(composition_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  1194 
by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1195 

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

1196 
lemma sats_composition_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1197 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
13429  1198 
==> sats(A, composition_fm(x,y,z), env) <> 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1199 
composition(**A, nth(x,env), nth(y,env), nth(z,env))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1200 
by (simp add: composition_fm_def composition_def) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1201 

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

1202 
lemma composition_iff_sats: 
13429  1203 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1204 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1205 
==> composition(**A, x, y, z) <> sats(A, composition_fm(i,j,k), env)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1206 
by simp 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1207 

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

1208 
theorem composition_reflection: 
13429  1209 
"REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)), 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1210 
\<lambda>i x. composition(**Lset(i),f(x),g(x),h(x))]" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1211 
apply (simp only: composition_def setclass_simps) 
13429  1212 
apply (intro FOL_reflections pair_reflection) 
13314  1213 
done 
1214 

13309  1215 

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

1216 
subsubsection{*Injections, Internalized*} 
13309  1217 

13429  1218 
(* "injection(M,A,B,f) == 
1219 
typed_function(M,A,B,f) & 

1220 
(\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M]. 

13309  1221 
pair(M,x,y,p) > pair(M,x',y,p') > p\<in>f > p'\<in>f > x=x')" *) 
1222 
constdefs injection_fm :: "[i,i,i]=>i" 

13429  1223 
"injection_fm(A,B,f) == 
13309  1224 
And(typed_function_fm(A,B,f), 
1225 
Forall(Forall(Forall(Forall(Forall( 

1226 
Implies(pair_fm(4,2,1), 

1227 
Implies(pair_fm(3,2,0), 

1228 
Implies(Member(1,f#+5), 

1229 
Implies(Member(0,f#+5), Equal(4,3)))))))))))" 

1230 

1231 

1232 
lemma injection_type [TC]: 

1233 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> injection_fm(x,y,z) \<in> formula" 

13429  1234 
by (simp add: injection_fm_def) 
13309  1235 

a6adee8ea75a
reflection for more internal formulas
pauls 