author  skalberg 
Thu, 28 Aug 2003 01:56:40 +0200  
changeset 14171  0cab06e3bbd0 
parent 13807  a28a8fbc76d4 
child 15696  1da4ce092c0b 
permissions  rwrr 
13505  1 
(* Title: ZF/Constructible/L_axioms.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
*) 

13429  5 

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

13223  7 

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

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

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

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

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

13223  15 
done 
16 

17 
lemma nonempty: "L(0)" 

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

13223  20 
done 
21 

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

13223  26 
done 
27 

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

32 
apply (blast intro: transL) 

13223  33 
done 
34 

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

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

44 
apply (simp add: foundation_ax_def) 

45 
apply (rule rallI) 

46 
apply (cut_tac A=x in foundation) 

47 
apply (blast intro: transL) 

48 
done 

49 

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

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

53 
there too!*) 

54 

55 
lemma LReplace_in_Lset: 

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

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

63 
apply (simp_all add: Replace_iff univalent_def) 

64 
apply (blast dest: transL L_I) 

13223  65 
done 
66 

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

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

73 
done 

74 

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

79 
apply (simp_all add: Replace_iff univalent_def, blast) 

13223  80 
done 
81 

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

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

85 
lemma Lset_mono_le: "mono_le_subset(Lset)" 

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

88 
lemma Lset_cont: "cont_Ord(Lset)" 

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

13428  91 
lemmas L_nat = Ord_in_L [OF Ord_nat] 
13291  92 

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

93 
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

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

95 
apply (erule (1) transL) 
13428  96 
apply (rule upair_ax) 
97 
apply (rule Union_ax) 

98 
apply (rule power_ax) 

99 
apply (rule replacement) 

100 
apply (rule L_nat) 

101 
done 

13291  102 

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

103 
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

104 
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

105 
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

106 
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

107 
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

108 
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

109 
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

110 
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

111 
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

112 
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

113 
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

114 
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

115 
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

116 
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

117 
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

118 
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

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

121 
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

122 
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

123 
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

124 
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

125 
and separation_closed = M_trivial.separation_closed [OF M_trivial_L] 
13566  126 
and strong_replacementI = 
127 
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

128 
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

129 
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

130 
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

131 
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

132 
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

133 
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

134 
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

135 
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

136 
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

137 
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

138 
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

139 
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

140 
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

141 
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

142 
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

143 
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

144 
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

145 
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

146 
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

147 
and number3_abs = M_trivial.number3_abs [OF M_trivial_L] 
13429  148 

149 
declare rall_abs [simp] 

150 
declare rex_abs [simp] 

151 
declare empty_abs [simp] 

152 
declare subset_abs [simp] 

153 
declare upair_abs [simp] 

154 
declare upair_in_M_iff [iff] 

155 
declare singleton_in_M_iff [iff] 

156 
declare pair_abs [simp] 

157 
declare pair_in_M_iff [iff] 

158 
declare cartprod_abs [simp] 

159 
declare union_abs [simp] 

160 
declare inter_abs [simp] 

161 
declare setdiff_abs [simp] 

162 
declare Union_abs [simp] 

163 
declare Union_closed [intro, simp] 

164 
declare Un_closed [intro, simp] 

165 
declare cons_closed [intro, simp] 

166 
declare successor_abs [simp] 

167 
declare succ_in_M_iff [iff] 

168 
declare separation_closed [intro, simp] 

169 
declare strong_replacement_closed [intro, simp] 

170 
declare RepFun_closed [intro, simp] 

171 
declare lam_closed [intro, simp] 

172 
declare image_abs [simp] 

173 
declare nat_into_M [intro] 

174 
declare Inl_in_M_iff [iff] 

175 
declare Inr_in_M_iff [iff] 

176 
declare transitive_set_abs [simp] 

177 
declare ordinal_abs [simp] 

178 
declare limit_ordinal_abs [simp] 

179 
declare successor_ordinal_abs [simp] 

180 
declare finite_ordinal_abs [simp] 

181 
declare omega_abs [simp] 

182 
declare number1_abs [simp] 

183 
declare number2_abs [simp] 

184 
declare number3_abs [simp] 

13291  185 

186 

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

188 

189 
text{*instances of locale constants*} 

190 
constdefs 

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

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13807
diff
changeset

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

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

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

196 

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

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

199 

200 

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

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

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

13291  207 

208 

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

13429  211 
apply (simp add: L_Reflects_def) 
212 
apply (rule meta_exI) 

213 
apply (rule Closed_Unbounded_Ord) 

13314  214 
done 
215 

216 
theorem Not_reflection: 

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

13429  218 
apply (unfold L_Reflects_def) 
219 
apply (erule meta_exE) 

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

13314  221 
done 
222 

223 
theorem And_reflection: 

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

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

229 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  230 
done 
231 

232 
theorem Or_reflection: 

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

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

238 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  239 
done 
240 

241 
theorem Imp_reflection: 

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

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

247 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  248 
done 
249 

250 
theorem Iff_reflection: 

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

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

256 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  257 
done 
258 

259 

13434  260 
lemma reflection_Lset: "reflection(Lset)" 
13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13634
diff
changeset

261 
by (blast intro: reflection.intro Lset_mono_le Lset_cont 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13634
diff
changeset

262 
Formula.Pair_in_LLimit)+ 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13634
diff
changeset

263 

13434  264 

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

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

13429  268 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
269 
apply (elim meta_exE) 

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

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

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

278 
apply (elim meta_exE) 

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

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

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

13429  286 
apply (unfold rex_def) 
13314  287 
apply (intro And_reflection Ex_reflection, assumption) 
288 
done 

13291  289 

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

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

13314  294 
apply (intro Imp_reflection All_reflection, assumption) 
295 
done 

296 

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

299 
theorem Rex_reflection': 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

300 
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

301 
==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[##Lset(a)]. Q(a,x,z)]" 
13440  302 
apply (unfold setclass_def rex_def) 
303 
apply (erule Rex_reflection [unfolded rex_def Bex_def]) 

304 
done 

305 

306 
text{*As above.*} 

307 
theorem Rall_reflection': 

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

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

309 
==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[##Lset(a)]. Q(a,x,z)]" 
13440  310 
apply (unfold setclass_def rall_def) 
311 
apply (erule Rall_reflection [unfolded rall_def Ball_def]) 

312 
done 

313 

13429  314 
lemmas FOL_reflections = 
13314  315 
Triv_reflection Not_reflection And_reflection Or_reflection 
316 
Imp_reflection Iff_reflection Ex_reflection All_reflection 

13440  317 
Rex_reflection Rall_reflection Rex_reflection' Rall_reflection' 
13291  318 

319 
lemma ReflectsD: 

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

324 
apply (blast dest!: UnboundedD) 

13291  325 
done 
326 

327 
lemma ReflectsE: 

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

13429  331 
apply (drule ReflectsD, assumption, blast) 
13314  332 
done 
13291  333 

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

337 

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

338 
subsection{*Internalized Formulas for some SetTheoretic Concepts*} 
13298  339 

13306  340 
subsubsection{*Some numbers to help write de Bruijn indices*} 
341 

342 
syntax 

343 
"3" :: i ("3") 

344 
"4" :: i ("4") 

345 
"5" :: i ("5") 

346 
"6" :: i ("6") 

347 
"7" :: i ("7") 

348 
"8" :: i ("8") 

349 
"9" :: i ("9") 

350 

351 
translations 

352 
"3" == "succ(2)" 

353 
"4" == "succ(3)" 

354 
"5" == "succ(4)" 

355 
"6" == "succ(5)" 

356 
"7" == "succ(6)" 

357 
"8" == "succ(7)" 

358 
"9" == "succ(8)" 

359 

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

360 

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

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

362 

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

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

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

365 

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

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

367 
"x \<in> nat ==> empty_fm(x) \<in> formula" 
13429  368 
by (simp add: empty_fm_def) 
13323
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 sats_empty_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

371 
"[ x \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

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

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

374 

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

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

377 
i \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

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

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

380 

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

381 
theorem empty_reflection: 
13429  382 
"REFLECTS[\<lambda>x. empty(L,f(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

383 
\<lambda>i x. empty(##Lset(i),f(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

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

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

387 

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

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

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

390 
"[ 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

391 
==> 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

392 
apply (simp add: empty_fm_def empty_def Transset_def, auto) 
13429  393 
apply (case_tac "n < length(env)") 
394 
apply (frule nth_type, assumption+, blast) 

395 
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

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

397 

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

398 

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

399 
subsubsection{*Unordered Pairs, Internalized*} 
13298  400 

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

13429  402 
"upair_fm(x,y,z) == 
403 
And(Member(x,z), 

13298  404 
And(Member(y,z), 
13429  405 
Forall(Implies(Member(0,succ(z)), 
13298  406 
Or(Equal(0,succ(x)), Equal(0,succ(y)))))))" 
407 

408 
lemma upair_type [TC]: 

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

13429  410 
by (simp add: upair_fm_def) 
13298  411 

412 
lemma sats_upair_fm [simp]: 

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

13429  414 
==> sats(A, upair_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

415 
upair(##A, nth(x,env), nth(y,env), nth(z,env))" 
13298  416 
by (simp add: upair_fm_def upair_def) 
417 

418 
lemma upair_iff_sats: 

13429  419 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13298  420 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

421 
==> upair(##A, x, y, z) <> sats(A, upair_fm(i,j,k), env)" 
13298  422 
by (simp add: sats_upair_fm) 
423 

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

425 
lemma sats_upair_fm2 [simp]: 

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

13429  427 
==> sats(A, upair_fm(x,y,z), env) <> 
13298  428 
nth(z,env) = {nth(x,env), nth(y,env)}" 
13429  429 
apply (frule lt_length_in_nat, assumption) 
430 
apply (simp add: upair_fm_def Transset_def, auto) 

431 
apply (blast intro: nth_type) 

13298  432 
done 
433 

13314  434 
theorem upair_reflection: 
13429  435 
"REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

436 
\<lambda>i x. upair(##Lset(i),f(x),g(x),h(x))]" 
13314  437 
apply (simp add: upair_def) 
13429  438 
apply (intro FOL_reflections) 
13314  439 
done 
13306  440 

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

441 
subsubsection{*Ordered pairs, Internalized*} 
13298  442 

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

13429  444 
"pair_fm(x,y,z) == 
13298  445 
Exists(And(upair_fm(succ(x),succ(x),0), 
446 
Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0), 

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

448 

449 
lemma pair_type [TC]: 

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

13429  451 
by (simp add: pair_fm_def) 
13298  452 

453 
lemma sats_pair_fm [simp]: 

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

13429  455 
==> sats(A, pair_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

456 
pair(##A, nth(x,env), nth(y,env), nth(z,env))" 
13298  457 
by (simp add: pair_fm_def pair_def) 
458 

459 
lemma pair_iff_sats: 

13429  460 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13298  461 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

462 
==> pair(##A, x, y, z) <> sats(A, pair_fm(i,j,k), env)" 
13298  463 
by (simp add: sats_pair_fm) 
464 

13314  465 
theorem pair_reflection: 
13429  466 
"REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

467 
\<lambda>i x. pair(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

468 
apply (simp only: pair_def) 
13429  469 
apply (intro FOL_reflections upair_reflection) 
13314  470 
done 
13306  471 

472 

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

473 
subsubsection{*Binary Unions, Internalized*} 
13298  474 

13306  475 
constdefs union_fm :: "[i,i,i]=>i" 
13429  476 
"union_fm(x,y,z) == 
13306  477 
Forall(Iff(Member(0,succ(z)), 
478 
Or(Member(0,succ(x)),Member(0,succ(y)))))" 

479 

480 
lemma union_type [TC]: 

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

13429  482 
by (simp add: union_fm_def) 
13306  483 

484 
lemma sats_union_fm [simp]: 

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

13429  486 
==> sats(A, union_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

487 
union(##A, nth(x,env), nth(y,env), nth(z,env))" 
13306  488 
by (simp add: union_fm_def union_def) 
489 

490 
lemma union_iff_sats: 

13429  491 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  492 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

493 
==> union(##A, x, y, z) <> sats(A, union_fm(i,j,k), env)" 
13306  494 
by (simp add: sats_union_fm) 
13298  495 

13314  496 
theorem union_reflection: 
13429  497 
"REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

498 
\<lambda>i x. union(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

499 
apply (simp only: union_def) 
13429  500 
apply (intro FOL_reflections) 
13314  501 
done 
13306  502 

13298  503 

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

504 
subsubsection{*Set ``Cons,'' Internalized*} 
13306  505 

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

13429  507 
"cons_fm(x,y,z) == 
13306  508 
Exists(And(upair_fm(succ(x),succ(x),0), 
509 
union_fm(0,succ(y),succ(z))))" 

13298  510 

511 

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

13429  514 
by (simp add: cons_fm_def) 
13306  515 

516 
lemma sats_cons_fm [simp]: 

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

13429  518 
==> sats(A, cons_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

519 
is_cons(##A, nth(x,env), nth(y,env), nth(z,env))" 
13306  520 
by (simp add: cons_fm_def is_cons_def) 
521 

522 
lemma cons_iff_sats: 

13429  523 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  524 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

525 
==> is_cons(##A, x, y, z) <> sats(A, cons_fm(i,j,k), env)" 
13306  526 
by simp 
527 

13314  528 
theorem cons_reflection: 
13429  529 
"REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

530 
\<lambda>i x. is_cons(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

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

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

534 

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

535 

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

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

537 

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

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

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

540 

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

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

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

544 

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

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

546 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 
13429  547 
==> sats(A, succ_fm(x,y), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

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

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

550 

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

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

553 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

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

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

556 

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

557 
theorem successor_reflection: 
13429  558 
"REFLECTS[\<lambda>x. successor(L,f(x),g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

559 
\<lambda>i x. successor(##Lset(i),f(x),g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

560 
apply (simp only: successor_def) 
13429  561 
apply (intro cons_reflection) 
13314  562 
done 
13298  563 

564 

13363  565 
subsubsection{*The Number 1, Internalized*} 
566 

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

568 
constdefs number1_fm :: "i=>i" 

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

570 

571 
lemma number1_type [TC]: 

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

13429  573 
by (simp add: number1_fm_def) 
13363  574 

575 
lemma sats_number1_fm [simp]: 

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

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

577 
==> sats(A, number1_fm(x), env) <> number1(##A, nth(x,env))" 
13363  578 
by (simp add: number1_fm_def number1_def) 
579 

580 
lemma number1_iff_sats: 

13429  581 
"[ nth(i,env) = x; nth(j,env) = y; 
13363  582 
i \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

583 
==> number1(##A, x) <> sats(A, number1_fm(i), env)" 
13363  584 
by simp 
585 

586 
theorem number1_reflection: 

13429  587 
"REFLECTS[\<lambda>x. number1(L,f(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

588 
\<lambda>i x. number1(##Lset(i),f(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

589 
apply (simp only: number1_def) 
13363  590 
apply (intro FOL_reflections empty_reflection successor_reflection) 
591 
done 

592 

593 

13352  594 
subsubsection{*Big Union, Internalized*} 
13306  595 

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

13429  598 
"big_union_fm(A,z) == 
13352  599 
Forall(Iff(Member(0,succ(z)), 
600 
Exists(And(Member(0,succ(succ(A))), Member(1,0)))))" 

13298  601 

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

13429  604 
by (simp add: big_union_fm_def) 
13306  605 

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

13429  608 
==> sats(A, big_union_fm(x,y), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

609 
big_union(##A, nth(x,env), nth(y,env))" 
13352  610 
by (simp add: big_union_fm_def big_union_def) 
13306  611 

13352  612 
lemma big_union_iff_sats: 
13429  613 
"[ nth(i,env) = x; nth(j,env) = y; 
13352  614 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

615 
==> big_union(##A, x, y) <> sats(A, big_union_fm(i,j), env)" 
13306  616 
by simp 
617 

13352  618 
theorem big_union_reflection: 
13429  619 
"REFLECTS[\<lambda>x. big_union(L,f(x),g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

620 
\<lambda>i x. big_union(##Lset(i),f(x),g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

621 
apply (simp only: big_union_def) 
13429  622 
apply (intro FOL_reflections) 
13314  623 
done 
13298  624 

625 

13306  626 
subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*} 
627 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13634
diff
changeset

628 
text{*The @{text sats} theorems below are standard versions of the ones proved 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13634
diff
changeset

629 
in theory @{text Formula}. They relate elements of type @{term formula} to 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13634
diff
changeset

630 
relativized concepts such as @{term subset} or @{term ordinal} rather than to 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13634
diff
changeset

631 
real concepts such as @{term Ord}. Now that we have instantiated the locale 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13634
diff
changeset

632 
@{text M_trivial}, we no longer require the earlier versions.*} 
13306  633 

634 
lemma sats_subset_fm': 

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

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

636 
==> sats(A, subset_fm(x,y), env) <> subset(##A, nth(x,env), nth(y,env))" 
13429  637 
by (simp add: subset_fm_def Relative.subset_def) 
13298  638 

13314  639 
theorem subset_reflection: 
13429  640 
"REFLECTS[\<lambda>x. subset(L,f(x),g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

641 
\<lambda>i x. subset(##Lset(i),f(x),g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

642 
apply (simp only: Relative.subset_def) 
13429  643 
apply (intro FOL_reflections) 
13314  644 
done 
13306  645 

646 
lemma sats_transset_fm': 

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

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

648 
==> sats(A, transset_fm(x), env) <> transitive_set(##A, nth(x,env))" 
13429  649 
by (simp add: sats_subset_fm' transset_fm_def transitive_set_def) 
13298  650 

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

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

653 
\<lambda>i x. transitive_set(##Lset(i),f(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

654 
apply (simp only: transitive_set_def) 
13429  655 
apply (intro FOL_reflections subset_reflection) 
13314  656 
done 
13306  657 

658 
lemma sats_ordinal_fm': 

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

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

660 
==> sats(A, ordinal_fm(x), env) <> ordinal(##A,nth(x,env))" 
13306  661 
by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def) 
662 

663 
lemma ordinal_iff_sats: 

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

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

665 
==> ordinal(##A, x) <> sats(A, ordinal_fm(i), env)" 
13306  666 
by (simp add: sats_ordinal_fm') 
667 

13314  668 
theorem ordinal_reflection: 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

669 
"REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(##Lset(i),f(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

670 
apply (simp only: ordinal_def) 
13429  671 
apply (intro FOL_reflections transitive_set_reflection) 
13314  672 
done 
13298  673 

674 

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

675 
subsubsection{*Membership Relation, Internalized*} 
13298  676 

13306  677 
constdefs Memrel_fm :: "[i,i]=>i" 
13429  678 
"Memrel_fm(A,r) == 
13306  679 
Forall(Iff(Member(0,succ(r)), 
680 
Exists(And(Member(0,succ(succ(A))), 

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

682 
And(Member(1,0), 

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

684 

685 
lemma Memrel_type [TC]: 

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

13429  687 
by (simp add: Memrel_fm_def) 
13298  688 

13306  689 
lemma sats_Memrel_fm [simp]: 
690 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  691 
==> sats(A, Memrel_fm(x,y), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

692 
membership(##A, nth(x,env), nth(y,env))" 
13306  693 
by (simp add: Memrel_fm_def membership_def) 
13298  694 

13306  695 
lemma Memrel_iff_sats: 
13429  696 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  697 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

698 
==> membership(##A, x, y) <> sats(A, Memrel_fm(i,j), env)" 
13306  699 
by simp 
13304  700 

13314  701 
theorem membership_reflection: 
13429  702 
"REFLECTS[\<lambda>x. membership(L,f(x),g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

703 
\<lambda>i x. membership(##Lset(i),f(x),g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

704 
apply (simp only: membership_def) 
13429  705 
apply (intro FOL_reflections pair_reflection) 
13314  706 
done 
13304  707 

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

708 
subsubsection{*Predecessor Set, Internalized*} 
13304  709 

13306  710 
constdefs pred_set_fm :: "[i,i,i,i]=>i" 
13429  711 
"pred_set_fm(A,x,r,B) == 
13306  712 
Forall(Iff(Member(0,succ(B)), 
713 
Exists(And(Member(0,succ(succ(r))), 

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

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

716 

717 

718 
lemma pred_set_type [TC]: 

13429  719 
"[ A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat ] 
13306  720 
==> pred_set_fm(A,x,r,B) \<in> formula" 
13429  721 
by (simp add: pred_set_fm_def) 
13304  722 

13306  723 
lemma sats_pred_set_fm [simp]: 
724 
"[ U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)] 

13429  725 
==> sats(A, pred_set_fm(U,x,r,B), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

726 
pred_set(##A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))" 
13306  727 
by (simp add: pred_set_fm_def pred_set_def) 
728 

729 
lemma pred_set_iff_sats: 

13429  730 
"[ nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B; 
13306  731 
i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

732 
==> pred_set(##A,U,x,r,B) <> sats(A, pred_set_fm(i,j,k,l), env)" 
13306  733 
by (simp add: sats_pred_set_fm) 
734 

13314  735 
theorem pred_set_reflection: 
13429  736 
"REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

737 
\<lambda>i x. pred_set(##Lset(i),f(x),g(x),h(x),b(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

738 
apply (simp only: pred_set_def) 
13429  739 
apply (intro FOL_reflections pair_reflection) 
13314  740 
done 
13304  741 

742 

13298  743 

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

744 
subsubsection{*Domain of a Relation, Internalized*} 
13306  745 

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

13306  748 
constdefs domain_fm :: "[i,i]=>i" 
13429  749 
"domain_fm(r,z) == 
13306  750 
Forall(Iff(Member(0,succ(z)), 
751 
Exists(And(Member(0,succ(succ(r))), 

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

753 

754 
lemma domain_type [TC]: 

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

13429  756 
by (simp add: domain_fm_def) 
13306  757 

758 
lemma sats_domain_fm [simp]: 

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

13429  760 
==> sats(A, domain_fm(x,y), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

761 
is_domain(##A, nth(x,env), nth(y,env))" 
13306  762 
by (simp add: domain_fm_def is_domain_def) 
763 

764 
lemma domain_iff_sats: 

13429  765 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  766 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

767 
==> is_domain(##A, x, y) <> sats(A, domain_fm(i,j), env)" 
13306  768 
by simp 
769 

13314  770 
theorem domain_reflection: 
13429  771 
"REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

772 
\<lambda>i x. is_domain(##Lset(i),f(x),g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

773 
apply (simp only: is_domain_def) 
13429  774 
apply (intro FOL_reflections pair_reflection) 
13314  775 
done 
13306  776 

777 

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

778 
subsubsection{*Range of a Relation, Internalized*} 
13306  779 

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

13306  782 
constdefs range_fm :: "[i,i]=>i" 
13429  783 
"range_fm(r,z) == 
13306  784 
Forall(Iff(Member(0,succ(z)), 
785 
Exists(And(Member(0,succ(succ(r))), 

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

787 

788 
lemma range_type [TC]: 

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

13429  790 
by (simp add: range_fm_def) 
13306  791 

792 
lemma sats_range_fm [simp]: 

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

13429  794 
==> sats(A, range_fm(x,y), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

795 
is_range(##A, nth(x,env), nth(y,env))" 
13306  796 
by (simp add: range_fm_def is_range_def) 
797 

798 
lemma range_iff_sats: 

13429  799 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  800 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

801 
==> is_range(##A, x, y) <> sats(A, range_fm(i,j), env)" 
13306  802 
by simp 
803 

13314  804 
theorem range_reflection: 
13429  805 
"REFLECTS[\<lambda>x. is_range(L,f(x),g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

806 
\<lambda>i x. is_range(##Lset(i),f(x),g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

807 
apply (simp only: is_range_def) 
13429  808 
apply (intro FOL_reflections pair_reflection) 
13314  809 
done 
13306  810 

13429  811 

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

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

813 

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

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

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

817 
constdefs field_fm :: "[i,i]=>i" 
13429  818 
"field_fm(r,z) == 
819 
Exists(And(domain_fm(succ(r),0), 

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

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

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

822 

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

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

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

826 

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

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

828 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 
13429  829 
==> sats(A, field_fm(x,y), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

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

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

832 

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

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

835 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

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

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

838 

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

839 
theorem field_reflection: 
13429  840 
"REFLECTS[\<lambda>x. is_field(L,f(x),g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

841 
\<lambda>i x. is_field(##Lset(i),f(x),g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

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

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

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

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

846 

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

847 

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

848 
subsubsection{*Image under a Relation, Internalized*} 
13306  849 

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

13429  853 
"image_fm(r,A,z) == 
13306  854 
Forall(Iff(Member(0,succ(z)), 
855 
Exists(And(Member(0,succ(succ(r))), 

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

13429  857 
pair_fm(0,2,1)))))))" 
13306  858 

859 
lemma image_type [TC]: 

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

13429  861 
by (simp add: image_fm_def) 
13306  862 

863 
lemma sats_image_fm [simp]: 

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

13429  865 
==> sats(A, image_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

866 
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

867 
by (simp add: image_fm_def Relative.image_def) 
13306  868 

869 
lemma image_iff_sats: 

13429  870 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  871 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

872 
==> image(##A, x, y, z) <> sats(A, image_fm(i,j,k), env)" 
13306  873 
by (simp add: sats_image_fm) 
874 

13314  875 
theorem image_reflection: 
13429  876 
"REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

877 
\<lambda>i x. image(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

878 
apply (simp only: Relative.image_def) 
13429  879 
apply (intro FOL_reflections pair_reflection) 
13314  880 
done 
13306  881 

882 

13348  883 
subsubsection{*PreImage under a Relation, Internalized*} 
884 

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

13348  887 
constdefs pre_image_fm :: "[i,i,i]=>i" 
13429  888 
"pre_image_fm(r,A,z) == 
13348  889 
Forall(Iff(Member(0,succ(z)), 
890 
Exists(And(Member(0,succ(succ(r))), 

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

13429  892 
pair_fm(2,0,1)))))))" 
13348  893 

894 
lemma pre_image_type [TC]: 

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

13429  896 
by (simp add: pre_image_fm_def) 
13348  897 

898 
lemma sats_pre_image_fm [simp]: 

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

13429  900 
==> sats(A, pre_image_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

901 
pre_image(##A, nth(x,env), nth(y,env), nth(z,env))" 
13348  902 
by (simp add: pre_image_fm_def Relative.pre_image_def) 
903 

904 
lemma pre_image_iff_sats: 

13429  905 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13348  906 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

907 
==> pre_image(##A, x, y, z) <> sats(A, pre_image_fm(i,j,k), env)" 
13348  908 
by (simp add: sats_pre_image_fm) 
909 

910 
theorem pre_image_reflection: 

13429  911 
"REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

912 
\<lambda>i x. pre_image(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

913 
apply (simp only: Relative.pre_image_def) 
13429  914 
apply (intro FOL_reflections pair_reflection) 
13348  915 
done 
916 

917 

13352  918 
subsubsection{*Function Application, Internalized*} 
919 

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

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

13429  924 
"fun_apply_fm(f,x,y) == 
13352  925 
Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1), 
13429  926 
And(image_fm(succ(succ(f)), 1, 0), 
13352  927 
big_union_fm(0,succ(succ(y)))))))" 
928 

929 
lemma fun_apply_type [TC]: 

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

13429  931 
by (simp add: fun_apply_fm_def) 
13352  932 

933 
lemma sats_fun_apply_fm [simp]: 

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

13429  935 
==> sats(A, fun_apply_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

936 
fun_apply(##A, nth(x,env), nth(y,env), nth(z,env))" 
13352  937 
by (simp add: fun_apply_fm_def fun_apply_def) 
938 

939 
lemma fun_apply_iff_sats: 

13429  940 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13352  941 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

942 
==> fun_apply(##A, x, y, z) <> sats(A, fun_apply_fm(i,j,k), env)" 
13352  943 
by simp 
944 

945 
theorem fun_apply_reflection: 

13429  946 
"REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

947 
\<lambda>i x. fun_apply(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

948 
apply (simp only: fun_apply_def) 
13352  949 
apply (intro FOL_reflections upair_reflection image_reflection 
13429  950 
big_union_reflection) 
13352  951 
done 
952 

953 

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

954 
subsubsection{*The Concept of Relation, Internalized*} 
13306  955 

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

13429  959 
"relation_fm(r) == 
13306  960 
Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))" 
961 

962 
lemma relation_type [TC]: 

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

13429  964 
by (simp add: relation_fm_def) 
13306  965 

966 
lemma sats_relation_fm [simp]: 

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

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

968 
==> sats(A, relation_fm(x), env) <> is_relation(##A, nth(x,env))" 
13306  969 
by (simp add: relation_fm_def is_relation_def) 
970 

971 
lemma relation_iff_sats: 

13429  972 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  973 
i \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

974 
==> is_relation(##A, x) <> sats(A, relation_fm(i), env)" 
13306  975 
by simp 
976 

13314  977 
theorem is_relation_reflection: 
13429  978 
"REFLECTS[\<lambda>x. is_relation(L,f(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

979 
\<lambda>i x. is_relation(##Lset(i),f(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

980 
apply (simp only: is_relation_def) 
13429  981 
apply (intro FOL_reflections pair_reflection) 
13314  982 
done 
13306  983 

984 

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

985 
subsubsection{*The Concept of Function, Internalized*} 
13306  986 

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

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

13429  991 
"function_fm(r) == 
13306  992 
Forall(Forall(Forall(Forall(Forall( 
993 
Implies(pair_fm(4,3,1), 

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

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

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

997 

998 
lemma function_type [TC]: 

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

13429  1000 
by (simp add: function_fm_def) 
13306  1001 

1002 
lemma sats_function_fm [simp]: 

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

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1004 
==> sats(A, function_fm(x), env) <> is_function(##A, nth(x,env))" 
13306  1005 
by (simp add: function_fm_def is_function_def) 
1006 

13505  1007 
lemma is_function_iff_sats: 
13429  1008 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  1009 
i \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1010 
==> is_function(##A, x) <> sats(A, function_fm(i), env)" 
13306  1011 
by simp 
1012 

13314  1013 
theorem is_function_reflection: 
13429  1014 
"REFLECTS[\<lambda>x. is_function(L,f(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1015 
\<lambda>i x. is_function(##Lset(i),f(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

1016 
apply (simp only: is_function_def) 
13429  1017 
apply (intro FOL_reflections pair_reflection) 
13314  1018 
done 
13298  1019 

1020 

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

1021 
subsubsection{*Typed Functions, Internalized*} 
13309  1022 

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

1026 

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

13429  1028 
"typed_function_fm(A,B,r) == 
13309  1029 
And(function_fm(r), 
1030 
And(relation_fm(r), 

1031 
And(domain_fm(r,A), 

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

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

1034 

1035 
lemma typed_function_type [TC]: 

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

13429  1037 
by (simp add: typed_function_fm_def) 
13309  1038 

1039 
lemma sats_typed_function_fm [simp]: 

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

13429  1041 
==> sats(A, typed_function_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1042 
typed_function(##A, nth(x,env), nth(y,env), nth(z,env))" 
13309  1043 
by (simp add: typed_function_fm_def typed_function_def) 
1044 

1045 
lemma typed_function_iff_sats: 

13429  1046 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13309  1047 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1048 
==> typed_function(##A, x, y, z) <> sats(A, typed_function_fm(i,j,k), env)" 
13309  1049 
by simp 
1050 

13429  1051 
lemmas function_reflections = 
13363  1052 
empty_reflection number1_reflection 
13429  1053 
upair_reflection pair_reflection union_reflection 
1054 
big_union_reflection cons_reflection successor_reflection 

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

1055 
fun_apply_reflection subset_reflection 
13429  1056 
transitive_set_reflection membership_reflection 
1057 
pred_set_reflection domain_reflection range_reflection field_reflection 

13348  1058 
image_reflection pre_image_reflection 
13429  1059 
is_relation_reflection is_function_reflection 
13309  1060 

13429  1061 
lemmas function_iff_sats = 
1062 
empty_iff_sats number1_iff_sats 

1063 
upair_iff_sats pair_iff_sats union_iff_sats 

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

1065 
fun_apply_iff_sats Memrel_iff_sats 
13429  1066 
pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats 
1067 
image_iff_sats pre_image_iff_sats 

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

1069 

13309  1070 

13314  1071 
theorem typed_function_reflection: 
13429  1072 
"REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1073 
\<lambda>i x. typed_function(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

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

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

1077 

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

1078 

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

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

1080 

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

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

1084 
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

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

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

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

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

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

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

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

1094 

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

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

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

1098 

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

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

1100 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
13429  1101 
==> sats(A, composition_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

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

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

1104 

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

1105 
lemma composition_iff_sats: 
13429  1106 
"[ 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

1107 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

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

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

1110 

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

1111 
theorem composition_reflection: 
13429  1112 
"REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1113 
\<lambda>i x. composition(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

1114 
apply (simp only: composition_def) 
13429  1115 
apply (intro FOL_reflections pair_reflection) 
13314  1116 
done 
1117 

13309  1118 

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

1119 
subsubsection{*Injections, Internalized*} 
13309  1120 

13429  1121 
(* "injection(M,A,B,f) == 
1122 
typed_function(M,A,B,f) & 

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

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

13429  1126 
"injection_fm(A,B,f) == 
13309  1127 
And(typed_function_fm(A,B,f), 
1128 
Forall(Forall(Forall(Forall(Forall( 

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

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

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

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

1133 

1134 

1135 
lemma injection_type [TC]: 

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

13429  1137 
by (simp add: injection_fm_def) 
13309  1138 

1139 
lemma sats_injection_fm [simp]: 

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

13429  1141 
==> sats(A, injection_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1142 
injection(##A, nth(x,env), nth(y,env), nth(z,env))" 
13309  1143 
by (simp add: injection_fm_def injection_def) 
1144 

1145 
lemma injection_iff_sats: 

13429  1146 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13309  1147 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1148 
==> injection(##A, x, y, z) <> sats(A, injection_fm(i,j,k), env)" 
13309  1149 
by simp 
1150 

13314  1151 
theorem injection_reflection: 
13429  1152 
"REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1153 
\<lambda>i x. injection(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

1154 
apply (simp only: injection_def) 
13429  1155 
apply (intro FOL_reflections function_reflections typed_function_reflection) 
13314  1156 
done 
13309  1157 

1158 

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

1159 
subsubsection{*Surjections, Internalized*} 
13309  1160 

1161 
(* surjection :: "[i=>o,i,i,i] => o" 

13429  1162 
"surjection(M,A,B,f) == 
13309  1163 
typed_function(M,A,B,f) & 
1164 
(\<forall>y[M]. y\<in>B > (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))" *) 

1165 
constdefs surjection_fm :: "[i,i,i]=>i" 

13429  1166 
"surjection_fm(A,B,f) == 
13309  1167 
And(typed_function_fm(A,B,f), 
1168 
Forall(Implies(Member(0,succ(B)), 

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

1170 
fun_apply_fm(succ(succ(f)),0,1))))))" 

1171 

1172 
lemma surjection_type [TC]: 

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

13429  1174 
by (simp add: surjection_fm_def) 
13309  1175 

1176 
lemma sats_surjection_fm [simp]: 

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

13429  1178 
==> sats(A, surjection_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1179 
surjection(##A, nth(x,env), nth(y,env), nth(z,env))" 
13309  1180 
by (simp add: surjection_fm_def surjection_def) 
1181 

1182 
lemma surjection_iff_sats: 

13429  1183 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13309  1184 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1185 
==> surjection(##A, x, y, z) <> sats(A, surjection_fm(i,j,k), env)" 
13309  1186 
by simp 
1187 

13314  1188 
theorem surjection_reflection: 
13429  1189 
"REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1190 
\<lambda>i x. surjection(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

1191 
apply (simp only: surjection_def) 
13429  1192 
apply (intro FOL_reflections function_reflections typed_function_reflection) 
13314  1193 
done 
13309  1194 

1195 

1196 

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

1197 
subsubsection{*Bijections, Internalized*} 
13309  1198 

1199 
(* bijection :: "[i=>o,i,i,i] => o" 

1200 
"bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *) 

1201 
constdefs bijection_fm :: "[i,i,i]=>i" 

1202 
"bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))" 

1203 

1204 
lemma bijection_type [TC]: 

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

13429  1206 
by (simp add: bijection_fm_def) 
13309  1207 

1208 
lemma sats_bijection_fm [simp]: 

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

13429  1210 
==> sats(A, bijection_fm(x,y,z), env) <> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1211 
bijection(##A, nth(x,env), nth(y,env), nth(z,env))" 
13309  1212 
by (simp add: bijection_fm_def bijection_def) 
1213 

1214 
lemma bijection_iff_sats: 

13429  1215 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13309  1216 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1217 
==> bijection(##A, x, y, z) <> sats(A, bijection_fm(i,j,k), env)" 
13309  1218 
by simp 
1219 

13314  1220 
theorem bijection_reflection: 
13429  1221 
"REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1222 
\<lambda>i x. bijection(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

1223 
apply (simp only: bijection_def) 
13429 