author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
13505  1 
(* Title: ZF/Constructible/L_axioms.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
*) 

13429  4 

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

13223  6 

16417  7 
theory L_axioms imports Formula Relative Reflection MetaExists begin 
13223  8 

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

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

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

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

13223  14 
done 
15 

16 
lemma nonempty: "L(0)" 

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

13223  19 
done 
20 

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

13223  25 
done 
26 

13563  27 
theorem Union_ax: "Union_ax(L)" 
13223  28 
apply (simp add: Union_ax_def big_union_def, clarify) 
46823  29 
apply (rule_tac x="\<Union>(x)" in rexI) 
13429  30 
apply (simp_all add: Union_in_L, auto) 
31 
apply (blast intro: transL) 

13223  32 
done 
33 

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

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

43 
apply (simp add: foundation_ax_def) 

44 
apply (rule rallI) 

45 
apply (cut_tac A=x in foundation) 

46 
apply (blast intro: transL) 

47 
done 

48 

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

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

52 
there too!*) 

53 

54 
lemma LReplace_in_Lset: 

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

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

62 
apply (simp_all add: Replace_iff univalent_def) 

63 
apply (blast dest: transL L_I) 

13223  64 
done 
65 

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

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

72 
done 

73 

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

78 
apply (simp_all add: Replace_iff univalent_def, blast) 

13223  79 
done 
80 

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

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

84 
lemma Lset_mono_le: "mono_le_subset(Lset)" 

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

87 
lemma Lset_cont: "cont_Ord(Lset)" 

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

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

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

92 
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

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

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

97 
apply (rule power_ax) 

98 
apply (rule replacement) 

99 
apply (rule L_nat) 

100 
done 

13291  101 

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

102 
interpretation L?: M_trivial L by (rule M_trivial_L) 
15696  103 

15764  104 
(* Replaces the following declarations... 
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

105 
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

106 
and rex_abs = M_trivial.rex_abs [OF M_trivial_L] 
15764  107 
... 
13429  108 
declare rall_abs [simp] 
109 
declare rex_abs [simp] 

15764  110 
...and dozens of similar ones. 
15696  111 
*) 
13291  112 

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

114 

115 
text{*instances of locale constants*} 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

116 

21233  117 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

118 
L_F0 :: "[i=>o,i] => i" where 
46823  119 
"L_F0(P,y) == \<mu> b. (\<exists>z. L(z) \<and> P(<y,z>)) \<longrightarrow> (\<exists>z\<in>Lset(b). P(<y,z>))" 
13291  120 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

121 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

122 
L_FF :: "[i=>o,i] => i" where 
13291  123 
"L_FF(P) == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)" 
124 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

125 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

126 
L_ClEx :: "[i=>o,i] => o" where 
13291  127 
"L_ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(L_FF(P),a) = a" 
128 

129 

13314  130 
text{*We must use the metaexistential quantifier; otherwise the reflection 
13429  131 
terms become enormous!*} 
21233  132 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

133 
L_Reflects :: "[i=>o,[i,i]=>o] => prop" ("(3REFLECTS/ [_,/ _])") where 
13314  134 
"REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) & 
46823  135 
(\<forall>a. Cl(a) \<longrightarrow> (\<forall>x \<in> Lset(a). P(x) \<longleftrightarrow> Q(a,x))))" 
13291  136 

137 

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

13429  140 
apply (simp add: L_Reflects_def) 
141 
apply (rule meta_exI) 

142 
apply (rule Closed_Unbounded_Ord) 

13314  143 
done 
144 

145 
theorem Not_reflection: 

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

13429  147 
apply (unfold L_Reflects_def) 
148 
apply (erule meta_exE) 

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

13314  150 
done 
151 

152 
theorem And_reflection: 

13429  153 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
13314  154 
==> REFLECTS[\<lambda>x. P(x) \<and> P'(x), \<lambda>a x. Q(a,x) \<and> Q'(a,x)]" 
13429  155 
apply (unfold L_Reflects_def) 
156 
apply (elim meta_exE) 

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

158 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  159 
done 
160 

161 
theorem Or_reflection: 

13429  162 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
13314  163 
==> REFLECTS[\<lambda>x. P(x) \<or> P'(x), \<lambda>a x. Q(a,x) \<or> Q'(a,x)]" 
13429  164 
apply (unfold L_Reflects_def) 
165 
apply (elim meta_exE) 

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

167 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  168 
done 
169 

170 
theorem Imp_reflection: 

13429  171 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
46823  172 
==> REFLECTS[\<lambda>x. P(x) \<longrightarrow> P'(x), \<lambda>a x. Q(a,x) \<longrightarrow> Q'(a,x)]" 
13429  173 
apply (unfold L_Reflects_def) 
174 
apply (elim meta_exE) 

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

176 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  177 
done 
178 

179 
theorem Iff_reflection: 

13429  180 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
46823  181 
==> REFLECTS[\<lambda>x. P(x) \<longleftrightarrow> P'(x), \<lambda>a x. Q(a,x) \<longleftrightarrow> Q'(a,x)]" 
13429  182 
apply (unfold L_Reflects_def) 
183 
apply (elim meta_exE) 

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

185 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  186 
done 
187 

188 

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

190 
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

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

192 

13434  193 

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

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

13429  197 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
198 
apply (elim meta_exE) 

13314  199 
apply (rule meta_exI) 
13434  200 
apply (erule reflection.Ex_reflection [OF reflection_Lset]) 
13291  201 
done 
202 

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

46823  205 
==> REFLECTS[\<lambda>x. \<forall>z. L(z) \<longrightarrow> P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]" 
13429  206 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
207 
apply (elim meta_exE) 

13314  208 
apply (rule meta_exI) 
13434  209 
apply (erule reflection.All_reflection [OF reflection_Lset]) 
13291  210 
done 
211 

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

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

13429  215 
apply (unfold rex_def) 
13314  216 
apply (intro And_reflection Ex_reflection, assumption) 
217 
done 

13291  218 

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

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

13314  223 
apply (intro Imp_reflection All_reflection, assumption) 
224 
done 

225 

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

228 
theorem Rex_reflection': 

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

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

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

233 
done 

234 

235 
text{*As above.*} 

236 
theorem Rall_reflection': 

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

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

241 
done 

242 

13429  243 
lemmas FOL_reflections = 
13314  244 
Triv_reflection Not_reflection And_reflection Or_reflection 
245 
Imp_reflection Iff_reflection Ex_reflection All_reflection 

13440  246 
Rex_reflection Rall_reflection Rex_reflection' Rall_reflection' 
13291  247 

248 
lemma ReflectsD: 

13429  249 
"[REFLECTS[P,Q]; Ord(i)] 
46823  250 
==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) \<longleftrightarrow> Q(j,x))" 
13429  251 
apply (unfold L_Reflects_def Closed_Unbounded_def) 
252 
apply (elim meta_exE, clarify) 

253 
apply (blast dest!: UnboundedD) 

13291  254 
done 
255 

256 
lemma ReflectsE: 

13314  257 
"[ REFLECTS[P,Q]; Ord(i); 
46823  258 
!!j. [i<j; \<forall>x \<in> Lset(j). P(x) \<longleftrightarrow> Q(j,x)] ==> R ] 
13291  259 
==> R" 
15764  260 
by (drule ReflectsD, assumption, blast) 
13291  261 

13428  262 
lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B" 
13291  263 
by blast 
264 

265 

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

266 
subsection{*Internalized Formulas for some SetTheoretic Concepts*} 
13298  267 

13306  268 
subsubsection{*Some numbers to help write de Bruijn indices*} 
269 

21233  270 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

271 
digit3 :: i ("3") where "3 == succ(2)" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

272 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

273 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

274 
digit4 :: i ("4") where "4 == succ(3)" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

275 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

276 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

277 
digit5 :: i ("5") where "5 == succ(4)" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

278 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

279 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

280 
digit6 :: i ("6") where "6 == succ(5)" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

281 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

282 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

283 
digit7 :: i ("7") where "7 == succ(6)" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

284 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

285 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

286 
digit8 :: i ("8") where "8 == succ(7)" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

287 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

288 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

289 
digit9 :: i ("9") where "9 == succ(8)" 
13306  290 

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

291 

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

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

293 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

294 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

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

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

297 

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

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

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

301 

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

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

303 
"[ x \<in> nat; env \<in> list(A)] 
46823  304 
==> sats(A, empty_fm(x), env) \<longleftrightarrow> empty(##A, nth(x,env))" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

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

306 

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

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

309 
i \<in> nat; env \<in> list(A)] 
46823  310 
==> empty(##A, x) \<longleftrightarrow> sats(A, empty_fm(i), env)" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

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

312 

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

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

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

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

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

319 

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

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

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

322 
"[ n \<in> nat; env \<in> list(A); Transset(A)] 
46823  323 
==> sats(A, empty_fm(n), env) \<longleftrightarrow> nth(n,env) = 0" 
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

324 
apply (simp add: empty_fm_def empty_def Transset_def, auto) 
13429  325 
apply (case_tac "n < length(env)") 
326 
apply (frule nth_type, assumption+, blast) 

327 
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

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

329 

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

330 

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

331 
subsubsection{*Unordered Pairs, Internalized*} 
13298  332 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

333 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

334 
upair_fm :: "[i,i,i]=>i" where 
13429  335 
"upair_fm(x,y,z) == 
336 
And(Member(x,z), 

13298  337 
And(Member(y,z), 
13429  338 
Forall(Implies(Member(0,succ(z)), 
13298  339 
Or(Equal(0,succ(x)), Equal(0,succ(y)))))))" 
340 

341 
lemma upair_type [TC]: 

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

13429  343 
by (simp add: upair_fm_def) 
13298  344 

345 
lemma sats_upair_fm [simp]: 

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

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

348 
upair(##A, nth(x,env), nth(y,env), nth(z,env))" 
13298  349 
by (simp add: upair_fm_def upair_def) 
350 

351 
lemma upair_iff_sats: 

13429  352 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13298  353 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  354 
==> upair(##A, x, y, z) \<longleftrightarrow> sats(A, upair_fm(i,j,k), env)" 
13298  355 
by (simp add: sats_upair_fm) 
356 

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

358 
lemma sats_upair_fm2 [simp]: 

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

46823  360 
==> sats(A, upair_fm(x,y,z), env) \<longleftrightarrow> 
13298  361 
nth(z,env) = {nth(x,env), nth(y,env)}" 
13429  362 
apply (frule lt_length_in_nat, assumption) 
363 
apply (simp add: upair_fm_def Transset_def, auto) 

364 
apply (blast intro: nth_type) 

13298  365 
done 
366 

13314  367 
theorem upair_reflection: 
13429  368 
"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

369 
\<lambda>i x. upair(##Lset(i),f(x),g(x),h(x))]" 
13314  370 
apply (simp add: upair_def) 
13429  371 
apply (intro FOL_reflections) 
13314  372 
done 
13306  373 

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

374 
subsubsection{*Ordered pairs, Internalized*} 
13298  375 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

376 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

377 
pair_fm :: "[i,i,i]=>i" where 
13429  378 
"pair_fm(x,y,z) == 
13298  379 
Exists(And(upair_fm(succ(x),succ(x),0), 
380 
Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0), 

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

382 

383 
lemma pair_type [TC]: 

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

13429  385 
by (simp add: pair_fm_def) 
13298  386 

387 
lemma sats_pair_fm [simp]: 

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

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

390 
pair(##A, nth(x,env), nth(y,env), nth(z,env))" 
13298  391 
by (simp add: pair_fm_def pair_def) 
392 

393 
lemma pair_iff_sats: 

13429  394 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13298  395 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  396 
==> pair(##A, x, y, z) \<longleftrightarrow> sats(A, pair_fm(i,j,k), env)" 
13298  397 
by (simp add: sats_pair_fm) 
398 

13314  399 
theorem pair_reflection: 
13429  400 
"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

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

402 
apply (simp only: pair_def) 
13429  403 
apply (intro FOL_reflections upair_reflection) 
13314  404 
done 
13306  405 

406 

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

407 
subsubsection{*Binary Unions, Internalized*} 
13298  408 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

409 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

410 
union_fm :: "[i,i,i]=>i" where 
13429  411 
"union_fm(x,y,z) == 
13306  412 
Forall(Iff(Member(0,succ(z)), 
413 
Or(Member(0,succ(x)),Member(0,succ(y)))))" 

414 

415 
lemma union_type [TC]: 

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

13429  417 
by (simp add: union_fm_def) 
13306  418 

419 
lemma sats_union_fm [simp]: 

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

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

422 
union(##A, nth(x,env), nth(y,env), nth(z,env))" 
13306  423 
by (simp add: union_fm_def union_def) 
424 

425 
lemma union_iff_sats: 

13429  426 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  427 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  428 
==> union(##A, x, y, z) \<longleftrightarrow> sats(A, union_fm(i,j,k), env)" 
13306  429 
by (simp add: sats_union_fm) 
13298  430 

13314  431 
theorem union_reflection: 
13429  432 
"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

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

434 
apply (simp only: union_def) 
13429  435 
apply (intro FOL_reflections) 
13314  436 
done 
13306  437 

13298  438 

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

439 
subsubsection{*Set ``Cons,'' Internalized*} 
13306  440 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

441 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

442 
cons_fm :: "[i,i,i]=>i" where 
13429  443 
"cons_fm(x,y,z) == 
13306  444 
Exists(And(upair_fm(succ(x),succ(x),0), 
445 
union_fm(0,succ(y),succ(z))))" 

13298  446 

447 

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

13429  450 
by (simp add: cons_fm_def) 
13306  451 

452 
lemma sats_cons_fm [simp]: 

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

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

455 
is_cons(##A, nth(x,env), nth(y,env), nth(z,env))" 
13306  456 
by (simp add: cons_fm_def is_cons_def) 
457 

458 
lemma cons_iff_sats: 

13429  459 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  460 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  461 
==> is_cons(##A, x, y, z) \<longleftrightarrow> sats(A, cons_fm(i,j,k), env)" 
13306  462 
by simp 
463 

13314  464 
theorem cons_reflection: 
13429  465 
"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

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

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

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

470 

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

471 

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

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

473 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

474 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

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

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

477 

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

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

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

481 

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

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

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

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

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

487 

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

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

490 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
46823  491 
==> successor(##A, x, y) \<longleftrightarrow> sats(A, succ_fm(i,j), env)" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

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

493 

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

494 
theorem successor_reflection: 
13429  495 
"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

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

497 
apply (simp only: successor_def) 
13429  498 
apply (intro cons_reflection) 
13314  499 
done 
13298  500 

501 

13363  502 
subsubsection{*The Number 1, Internalized*} 
503 

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

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

505 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

506 
number1_fm :: "i=>i" where 
13363  507 
"number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))" 
508 

509 
lemma number1_type [TC]: 

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

13429  511 
by (simp add: number1_fm_def) 
13363  512 

513 
lemma sats_number1_fm [simp]: 

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

46823  515 
==> sats(A, number1_fm(x), env) \<longleftrightarrow> number1(##A, nth(x,env))" 
13363  516 
by (simp add: number1_fm_def number1_def) 
517 

518 
lemma number1_iff_sats: 

13429  519 
"[ nth(i,env) = x; nth(j,env) = y; 
13363  520 
i \<in> nat; env \<in> list(A)] 
46823  521 
==> number1(##A, x) \<longleftrightarrow> sats(A, number1_fm(i), env)" 
13363  522 
by simp 
523 

524 
theorem number1_reflection: 

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

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

527 
apply (simp only: number1_def) 
13363  528 
apply (intro FOL_reflections empty_reflection successor_reflection) 
529 
done 

530 

531 

13352  532 
subsubsection{*Big Union, Internalized*} 
13306  533 

46823  534 
(* "big_union(M,A,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>y[M]. y\<in>A & x \<in> y)" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

535 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

536 
big_union_fm :: "[i,i]=>i" where 
13429  537 
"big_union_fm(A,z) == 
13352  538 
Forall(Iff(Member(0,succ(z)), 
539 
Exists(And(Member(0,succ(succ(A))), Member(1,0)))))" 

13298  540 

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

13429  543 
by (simp add: big_union_fm_def) 
13306  544 

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

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

548 
big_union(##A, nth(x,env), nth(y,env))" 
13352  549 
by (simp add: big_union_fm_def big_union_def) 
13306  550 

13352  551 
lemma big_union_iff_sats: 
13429  552 
"[ nth(i,env) = x; nth(j,env) = y; 
13352  553 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
46823  554 
==> big_union(##A, x, y) \<longleftrightarrow> sats(A, big_union_fm(i,j), env)" 
13306  555 
by simp 
556 

13352  557 
theorem big_union_reflection: 
13429  558 
"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

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

560 
apply (simp only: big_union_def) 
13429  561 
apply (intro FOL_reflections) 
13314  562 
done 
13298  563 

564 

13306  565 
subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*} 
566 

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

567 
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

568 
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

569 
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

570 
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

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

573 
lemma sats_subset_fm': 

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

46823  575 
==> sats(A, subset_fm(x,y), env) \<longleftrightarrow> subset(##A, nth(x,env), nth(y,env))" 
13429  576 
by (simp add: subset_fm_def Relative.subset_def) 
13298  577 

13314  578 
theorem subset_reflection: 
13429  579 
"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

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

581 
apply (simp only: Relative.subset_def) 
13429  582 
apply (intro FOL_reflections) 
13314  583 
done 
13306  584 

585 
lemma sats_transset_fm': 

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

46823  587 
==> sats(A, transset_fm(x), env) \<longleftrightarrow> transitive_set(##A, nth(x,env))" 
13429  588 
by (simp add: sats_subset_fm' transset_fm_def transitive_set_def) 
13298  589 

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

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

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

593 
apply (simp only: transitive_set_def) 
13429  594 
apply (intro FOL_reflections subset_reflection) 
13314  595 
done 
13306  596 

597 
lemma sats_ordinal_fm': 

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

46823  599 
==> sats(A, ordinal_fm(x), env) \<longleftrightarrow> ordinal(##A,nth(x,env))" 
13306  600 
by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def) 
601 

602 
lemma ordinal_iff_sats: 

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

46823  604 
==> ordinal(##A, x) \<longleftrightarrow> sats(A, ordinal_fm(i), env)" 
13306  605 
by (simp add: sats_ordinal_fm') 
606 

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

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

609 
apply (simp only: ordinal_def) 
13429  610 
apply (intro FOL_reflections transitive_set_reflection) 
13314  611 
done 
13298  612 

613 

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

614 
subsubsection{*Membership Relation, Internalized*} 
13298  615 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

616 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

617 
Memrel_fm :: "[i,i]=>i" where 
13429  618 
"Memrel_fm(A,r) == 
13306  619 
Forall(Iff(Member(0,succ(r)), 
620 
Exists(And(Member(0,succ(succ(A))), 

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

622 
And(Member(1,0), 

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

624 

625 
lemma Memrel_type [TC]: 

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

13429  627 
by (simp add: Memrel_fm_def) 
13298  628 

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

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

632 
membership(##A, nth(x,env), nth(y,env))" 
13306  633 
by (simp add: Memrel_fm_def membership_def) 
13298  634 

13306  635 
lemma Memrel_iff_sats: 
13429  636 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  637 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
46823  638 
==> membership(##A, x, y) \<longleftrightarrow> sats(A, Memrel_fm(i,j), env)" 
13306  639 
by simp 
13304  640 

13314  641 
theorem membership_reflection: 
13429  642 
"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

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

644 
apply (simp only: membership_def) 
13429  645 
apply (intro FOL_reflections pair_reflection) 
13314  646 
done 
13304  647 

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

648 
subsubsection{*Predecessor Set, Internalized*} 
13304  649 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

650 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

651 
pred_set_fm :: "[i,i,i,i]=>i" where 
13429  652 
"pred_set_fm(A,x,r,B) == 
13306  653 
Forall(Iff(Member(0,succ(B)), 
654 
Exists(And(Member(0,succ(succ(r))), 

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

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

657 

658 

659 
lemma pred_set_type [TC]: 

13429  660 
"[ A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat ] 
13306  661 
==> pred_set_fm(A,x,r,B) \<in> formula" 
13429  662 
by (simp add: pred_set_fm_def) 
13304  663 

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

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

667 
pred_set(##A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))" 
13306  668 
by (simp add: pred_set_fm_def pred_set_def) 
669 

670 
lemma pred_set_iff_sats: 

13429  671 
"[ nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B; 
13306  672 
i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)] 
46823  673 
==> pred_set(##A,U,x,r,B) \<longleftrightarrow> sats(A, pred_set_fm(i,j,k,l), env)" 
13306  674 
by (simp add: sats_pred_set_fm) 
675 

13314  676 
theorem pred_set_reflection: 
13429  677 
"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

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

679 
apply (simp only: pred_set_def) 
13429  680 
apply (intro FOL_reflections pair_reflection) 
13314  681 
done 
13304  682 

683 

13298  684 

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

685 
subsubsection{*Domain of a Relation, Internalized*} 
13306  686 

13429  687 
(* "is_domain(M,r,z) == 
46823  688 
\<forall>x[M]. (x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

689 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

690 
domain_fm :: "[i,i]=>i" where 
13429  691 
"domain_fm(r,z) == 
13306  692 
Forall(Iff(Member(0,succ(z)), 
693 
Exists(And(Member(0,succ(succ(r))), 

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

695 

696 
lemma domain_type [TC]: 

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

13429  698 
by (simp add: domain_fm_def) 
13306  699 

700 
lemma sats_domain_fm [simp]: 

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

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

703 
is_domain(##A, nth(x,env), nth(y,env))" 
13306  704 
by (simp add: domain_fm_def is_domain_def) 
705 

706 
lemma domain_iff_sats: 

13429  707 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  708 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
46823  709 
==> is_domain(##A, x, y) \<longleftrightarrow> sats(A, domain_fm(i,j), env)" 
13306  710 
by simp 
711 

13314  712 
theorem domain_reflection: 
13429  713 
"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

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

715 
apply (simp only: is_domain_def) 
13429  716 
apply (intro FOL_reflections pair_reflection) 
13314  717 
done 
13306  718 

719 

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

720 
subsubsection{*Range of a Relation, Internalized*} 
13306  721 

13429  722 
(* "is_range(M,r,z) == 
46823  723 
\<forall>y[M]. (y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

724 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

725 
range_fm :: "[i,i]=>i" where 
13429  726 
"range_fm(r,z) == 
13306  727 
Forall(Iff(Member(0,succ(z)), 
728 
Exists(And(Member(0,succ(succ(r))), 

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

730 

731 
lemma range_type [TC]: 

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

13429  733 
by (simp add: range_fm_def) 
13306  734 

735 
lemma sats_range_fm [simp]: 

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

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

738 
is_range(##A, nth(x,env), nth(y,env))" 
13306  739 
by (simp add: range_fm_def is_range_def) 
740 

741 
lemma range_iff_sats: 

13429  742 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  743 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
46823  744 
==> is_range(##A, x, y) \<longleftrightarrow> sats(A, range_fm(i,j), env)" 
13306  745 
by simp 
746 

13314  747 
theorem range_reflection: 
13429  748 
"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

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

750 
apply (simp only: is_range_def) 
13429  751 
apply (intro FOL_reflections pair_reflection) 
13314  752 
done 
13306  753 

13429  754 

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

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

756 

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

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

759 
(\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

760 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

761 
field_fm :: "[i,i]=>i" where 
13429  762 
"field_fm(r,z) == 
763 
Exists(And(domain_fm(succ(r),0), 

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

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

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

766 

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

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

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

770 

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

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

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

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

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

776 

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

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

779 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
46823  780 
==> is_field(##A, x, y) \<longleftrightarrow> sats(A, field_fm(i,j), env)" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

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

782 

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

783 
theorem field_reflection: 
13429  784 
"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

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

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

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

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

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

790 

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

791 

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

792 
subsubsection{*Image under a Relation, Internalized*} 
13306  793 

13429  794 
(* "image(M,r,A,z) == 
46823  795 
\<forall>y[M]. (y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

796 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

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

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

13429  802 
pair_fm(0,2,1)))))))" 
13306  803 

804 
lemma image_type [TC]: 

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

13429  806 
by (simp add: image_fm_def) 
13306  807 

808 
lemma sats_image_fm [simp]: 

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

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

811 
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

812 
by (simp add: image_fm_def Relative.image_def) 
13306  813 

814 
lemma image_iff_sats: 

13429  815 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  816 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  817 
==> image(##A, x, y, z) \<longleftrightarrow> sats(A, image_fm(i,j,k), env)" 
13306  818 
by (simp add: sats_image_fm) 
819 

13314  820 
theorem image_reflection: 
13429  821 
"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

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

823 
apply (simp only: Relative.image_def) 
13429  824 
apply (intro FOL_reflections pair_reflection) 
13314  825 
done 
13306  826 

827 

13348  828 
subsubsection{*PreImage under a Relation, Internalized*} 
829 

13429  830 
(* "pre_image(M,r,A,z) == 
46823  831 
\<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

832 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

833 
pre_image_fm :: "[i,i,i]=>i" where 
13429  834 
"pre_image_fm(r,A,z) == 
13348  835 
Forall(Iff(Member(0,succ(z)), 
836 
Exists(And(Member(0,succ(succ(r))), 

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

13429  838 
pair_fm(2,0,1)))))))" 
13348  839 

840 
lemma pre_image_type [TC]: 

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

13429  842 
by (simp add: pre_image_fm_def) 
13348  843 

844 
lemma sats_pre_image_fm [simp]: 

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

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

847 
pre_image(##A, nth(x,env), nth(y,env), nth(z,env))" 
13348  848 
by (simp add: pre_image_fm_def Relative.pre_image_def) 
849 

850 
lemma pre_image_iff_sats: 

13429  851 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13348  852 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  853 
==> pre_image(##A, x, y, z) \<longleftrightarrow> sats(A, pre_image_fm(i,j,k), env)" 
13348  854 
by (simp add: sats_pre_image_fm) 
855 

856 
theorem pre_image_reflection: 

13429  857 
"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

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

859 
apply (simp only: Relative.pre_image_def) 
13429  860 
apply (intro FOL_reflections pair_reflection) 
13348  861 
done 
862 

863 

13352  864 
subsubsection{*Function Application, Internalized*} 
865 

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

13352  868 
upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

869 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

870 
fun_apply_fm :: "[i,i,i]=>i" where 
13429  871 
"fun_apply_fm(f,x,y) == 
13352  872 
Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1), 
13429  873 
And(image_fm(succ(succ(f)), 1, 0), 
13352  874 
big_union_fm(0,succ(succ(y)))))))" 
875 

876 
lemma fun_apply_type [TC]: 

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

13429  878 
by (simp add: fun_apply_fm_def) 
13352  879 

880 
lemma sats_fun_apply_fm [simp]: 

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

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

883 
fun_apply(##A, nth(x,env), nth(y,env), nth(z,env))" 
13352  884 
by (simp add: fun_apply_fm_def fun_apply_def) 
885 

886 
lemma fun_apply_iff_sats: 

13429  887 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13352  888 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  889 
==> fun_apply(##A, x, y, z) \<longleftrightarrow> sats(A, fun_apply_fm(i,j,k), env)" 
13352  890 
by simp 
891 

892 
theorem fun_apply_reflection: 

13429  893 
"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

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

895 
apply (simp only: fun_apply_def) 
13352  896 
apply (intro FOL_reflections upair_reflection image_reflection 
13429  897 
big_union_reflection) 
13352  898 
done 
899 

900 

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

901 
subsubsection{*The Concept of Relation, Internalized*} 
13306  902 

13429  903 
(* "is_relation(M,r) == 
46823  904 
(\<forall>z[M]. z\<in>r \<longrightarrow> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

905 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

906 
relation_fm :: "i=>i" where 
13429  907 
"relation_fm(r) == 
13306  908 
Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))" 
909 

910 
lemma relation_type [TC]: 

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

13429  912 
by (simp add: relation_fm_def) 
13306  913 

914 
lemma sats_relation_fm [simp]: 

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

46823  916 
==> sats(A, relation_fm(x), env) \<longleftrightarrow> is_relation(##A, nth(x,env))" 
13306  917 
by (simp add: relation_fm_def is_relation_def) 
918 

919 
lemma relation_iff_sats: 

13429  920 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  921 
i \<in> nat; env \<in> list(A)] 
46823  922 
==> is_relation(##A, x) \<longleftrightarrow> sats(A, relation_fm(i), env)" 
13306  923 
by simp 
924 

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

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

928 
apply (simp only: is_relation_def) 
13429  929 
apply (intro FOL_reflections pair_reflection) 
13314  930 
done 
13306  931 

932 

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

933 
subsubsection{*The Concept of Function, Internalized*} 
13306  934 

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

46823  937 
pair(M,x,y,p) \<longrightarrow> pair(M,x,y',p') \<longrightarrow> p\<in>r \<longrightarrow> p'\<in>r \<longrightarrow> y=y'" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

938 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

939 
function_fm :: "i=>i" where 
13429  940 
"function_fm(r) == 
13306  941 
Forall(Forall(Forall(Forall(Forall( 
942 
Implies(pair_fm(4,3,1), 

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

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

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

946 

947 
lemma function_type [TC]: 

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

13429  949 
by (simp add: function_fm_def) 
13306  950 

951 
lemma sats_function_fm [simp]: 

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

46823  953 
==> sats(A, function_fm(x), env) \<longleftrightarrow> is_function(##A, nth(x,env))" 
13306  954 
by (simp add: function_fm_def is_function_def) 
955 

13505  956 
lemma is_function_iff_sats: 
13429  957 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  958 
i \<in> nat; env \<in> list(A)] 
46823  959 
==> is_function(##A, x) \<longleftrightarrow> sats(A, function_fm(i), env)" 
13306  960 
by simp 
961 

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

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

965 
apply (simp only: is_function_def) 
13429  966 
apply (intro FOL_reflections pair_reflection) 
13314  967 
done 
13298  968 

969 

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

970 
subsubsection{*Typed Functions, Internalized*} 
13309  971 

13429  972 
(* "typed_function(M,A,B,r) == 
13309  973 
is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & 
46823  974 
(\<forall>u[M]. u\<in>r \<longrightarrow> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) \<longrightarrow> y\<in>B))" *) 
13309  975 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

976 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

977 
typed_function_fm :: "[i,i,i]=>i" where 
13429  978 
"typed_function_fm(A,B,r) == 
13309  979 
And(function_fm(r), 
980 
And(relation_fm(r), 

981 
And(domain_fm(r,A), 

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

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

984 

985 
lemma typed_function_type [TC]: 

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

13429  987 
by (simp add: typed_function_fm_def) 
13309  988 

989 
lemma sats_typed_function_fm [simp]: 

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

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

992 
typed_function(##A, nth(x,env), nth(y,env), nth(z,env))" 
13309  993 
by (simp add: typed_function_fm_def typed_function_def) 
994 

995 
lemma typed_function_iff_sats: 

13429  996 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13309  997 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  998 
==> typed_function(##A, x, y, z) \<longleftrightarrow> sats(A, typed_function_fm(i,j,k), env)" 
13309  999 
by simp 
1000 

13429  1001 
lemmas function_reflections = 
13363  1002 
empty_reflection number1_reflection 
13429  1003 
upair_reflection pair_reflection union_reflection 
1004 
big_union_reflection cons_reflection successor_reflection 

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

1005 
fun_apply_reflection subset_reflection 
13429  1006 
transitive_set_reflection membership_reflection 
1007 
pred_set_reflection domain_reflection range_reflection field_reflection 

13348  1008 
image_reflection pre_image_reflection 
13429  1009 
is_relation_reflection is_function_reflection 
13309  1010 

13429  1011 
lemmas function_iff_sats = 
1012 
empty_iff_sats number1_iff_sats 

1013 
upair_iff_sats pair_iff_sats union_iff_sats 

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

1015 
fun_apply_iff_sats Memrel_iff_sats 
13429  1016 
pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats 
1017 
image_iff_sats pre_image_iff_sats 

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

1019 

13309  1020 

13314  1021 
theorem typed_function_reflection: 
13429  1022 
"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

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

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

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

1027 

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

1028 

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

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

1030 

13429  1031 
(* "composition(M,r,s,t) == 
46823  1032 
\<forall>p[M]. p \<in> t \<longleftrightarrow> 
13429  1033 
(\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
1034 
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

1035 
xy \<in> s & yz \<in> r)" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1036 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

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

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

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

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

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

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

1045 

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

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

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

1049 

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

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

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

1053 
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

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

1055 

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

1056 
lemma composition_iff_sats: 
13429  1057 
"[ 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

1058 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  1059 
==> composition(##A, x, y, z) \<longleftrightarrow> sats(A, composition_fm(i,j,k), env)" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

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

1061 

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

1062 
theorem composition_reflection: 
13429  1063 
"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

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

1065 
apply (simp only: composition_def) 
13429  1066 
apply (intro FOL_reflections pair_reflection) 
13314  1067 
done 
1068 

13309  1069 

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

1070 
subsubsection{*Injections, Internalized*} 
13309  1071 

13429  1072 
(* "injection(M,A,B,f) == 
1073 
typed_function(M,A,B,f) & 

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

46823  1075 
pair(M,x,y,p) \<longrightarrow> pair(M,x',y,p') \<longrightarrow> p\<in>f \<longrightarrow> p'\<in>f \<longrightarrow> x=x')" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1076 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1077 
injection_fm :: "[i,i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1078 
"injection_fm(A,B,f) == 
13309  1079 
And(typed_function_fm(A,B,f), 
1080 
Forall(Forall(Forall(Forall(Forall( 

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

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

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

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

1085 

1086 

1087 
lemma injection_type [TC]: 

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

13429  1089 
by (simp add: injection_fm_def) 
13309  1090 

1091 
lemma sats_injection_fm [simp]: 

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

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

1094 
injection(##A, nth(x,env), nth(y,env), nth(z,env))" 
13309  1095 
by (simp add: injection_fm_def injection_def) 
1096 

1097 
lemma injection_iff_sats: 

13429  1098 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13309  1099 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  1100 
==> injection(##A, x, y, z) \<longleftrightarrow> sats(A, injection_fm(i,j,k), env)" 
13309  1101 
by simp 
1102 

13314  1103 
theorem injection_reflection: 
13429  1104 
"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

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

1106 
apply (simp only: injection_def) 
13429  1107 
apply (intro FOL_reflections function_reflections typed_function_reflection) 
13314  1108 
done 
13309  1109 

1110 

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

1111 
subsubsection{*Surjections, Internalized*} 
13309  1112 

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

13429  1114 
"surjection(M,A,B,f) == 
13309  1115 
typed_function(M,A,B,f) & 
46823  1116 
(\<forall>y[M]. y\<in>B \<longrightarrow> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1117 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1118 
surjection_fm :: "[i,i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1119 
"surjection_fm(A,B,f) == 
13309  1120 
And(typed_function_fm(A,B,f), 
1121 
Forall(Implies(Member(0,succ(B)), 

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

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

1124 

1125 
lemma surjection_type [TC]: 

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

13429  1127 
by (simp add: surjection_fm_def) 
13309  1128 

1129 
lemma sats_surjection_fm [simp]: 

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

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

1132 
surjection(##A, nth(x,env), nth(y,env), nth(z,env))" 
13309  1133 
by (simp add: surjection_fm_def surjection_def) 
1134 

1135 
lemma surjection_iff_sats: 

13429  1136 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13309  1137 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  1138 
==> surjection(##A, x, y, z) \<longleftrightarrow> sats(A, surjection_fm(i,j,k), env)" 
13309  1139 
by simp 
1140 

13314  1141 
theorem surjection_reflection: 
13429  1142 
"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

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

1144 
apply (simp only: surjection_def) 
13429  1145 
apply (intro FOL_reflections function_reflections typed_function_reflection) 
13314  1146 
done 
13309  1147 

1148 

1149 

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

1150 
subsubsection{*Bijections, Internalized*} 
13309  1151 

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

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

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1154 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1155 
bijection_fm :: "[i,i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1156 
"bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))" 
13309  1157 

1158 
lemma bijection_type [TC]: 

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

13429  1160 
by (simp add: bijection_fm_def) 
13309  1161 

1162 
lemma sats_bijection_fm [simp]: 

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

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

1165 
bijection(##A, nth(x,env), nth(y,env), nth(z,env))" 
13309  1166 
by (simp add: bijection_fm_def bijection_def) 
1167 

1168 
lemma bijection_iff_sats: 

13429  1169 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13309  1170 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  1171 
==> bijection(##A, x, y, z) \<longleftrightarrow> sats(A, bijection_fm(i,j,k), env)" 
13309  1172 
by simp 
1173 

13314  1174 
theorem bijection_reflection: 
13429  1175 
"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

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

1177 
apply (simp only: bijection_def) 
13429  1178 
apply (intro And_reflection injection_reflection surjection_reflection) 
13314  1179 
done 
13309  1180 

1181 

13348  1182 
subsubsection{*Restriction of a Relation, Internalized*} 
1183 

1184 

13429  1185 
(* "restriction(M,r,A,z) == 
46823  1186 
\<forall>x[M]. x \<in> z \<longleftrightarrow> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1187 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1188 
restriction_fm :: "[i,i,i]=>i" where 
13429  1189 
"restriction_fm(r,A,z) == 
13348  1190 
Forall(Iff(Member(0,succ(z)), 
1191 
And(Member(0,succ(r)), 

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

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

1194 

1195 
lemma restriction_type [TC]: 

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

13429  1197 
by (simp add: restriction_fm_def) 
13348  1198 

1199 
lemma sats_restriction_fm [simp]: 

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

46823  1201 
==> sats(A, restriction_fm(x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13655
diff
changeset

1202 
restriction(##A, nth(x,env), nth(y,env), nth(z,env))" 
13348  1203 
by (simp add: restriction_fm_def restriction_def) 
1204 

1205 
lemma restriction_iff_sats: 

13429  1206 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13348  1207 