author wenzelm Mon Jul 29 18:07:53 2002 +0200 (2002-07-29) changeset 13429 2232810416fc parent 13428 99e52e78eb65 child 13430 ab814c7685a9
tuned;
```     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Jul 29 00:57:16 2002 +0200
1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Mon Jul 29 18:07:53 2002 +0200
1.3 @@ -1,37 +1,38 @@
1.4 -header {*The ZF Axioms (Except Separation) in L*}
1.5 +
1.6 +header {* The ZF Axioms (Except Separation) in L *}
1.7
1.8  theory L_axioms = Formula + Relative + Reflection + MetaExists:
1.9
1.10  text {* The class L satisfies the premises of locale @{text M_triv_axioms} *}
1.11
1.12  lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
1.13 -apply (insert Transset_Lset)
1.14 -apply (simp add: Transset_def L_def, blast)
1.15 +apply (insert Transset_Lset)
1.16 +apply (simp add: Transset_def L_def, blast)
1.17  done
1.18
1.19  lemma nonempty: "L(0)"
1.21 -apply (blast intro: zero_in_Lset)
1.23 +apply (blast intro: zero_in_Lset)
1.24  done
1.25
1.26  lemma upair_ax: "upair_ax(L)"
1.27  apply (simp add: upair_ax_def upair_def, clarify)
1.28 -apply (rule_tac x="{x,y}" in rexI)
1.30 +apply (rule_tac x="{x,y}" in rexI)
1.32  done
1.33
1.34  lemma Union_ax: "Union_ax(L)"
1.35  apply (simp add: Union_ax_def big_union_def, clarify)
1.36 -apply (rule_tac x="Union(x)" in rexI)
1.37 -apply (simp_all add: Union_in_L, auto)
1.38 -apply (blast intro: transL)
1.39 +apply (rule_tac x="Union(x)" in rexI)
1.40 +apply (simp_all add: Union_in_L, auto)
1.41 +apply (blast intro: transL)
1.42  done
1.43
1.44  lemma power_ax: "power_ax(L)"
1.45  apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
1.46 -apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI)
1.47 +apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI)
1.48  apply (simp_all add: LPow_in_L, auto)
1.49 -apply (blast intro: transL)
1.50 +apply (blast intro: transL)
1.51  done
1.52
1.53  subsubsection{*For L to satisfy Replacement *}
1.54 @@ -40,40 +41,40 @@
1.55  there too!*)
1.56
1.57  lemma LReplace_in_Lset:
1.58 -     "[|X \<in> Lset(i); univalent(L,X,Q); Ord(i)|]
1.59 +     "[|X \<in> Lset(i); univalent(L,X,Q); Ord(i)|]
1.60        ==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"
1.61 -apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))"
1.62 +apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))"
1.63         in exI)
1.64  apply simp
1.65 -apply clarify
1.66 -apply (rule_tac a=x in UN_I)
1.67 - apply (simp_all add: Replace_iff univalent_def)
1.68 -apply (blast dest: transL L_I)
1.69 +apply clarify
1.70 +apply (rule_tac a=x in UN_I)
1.71 + apply (simp_all add: Replace_iff univalent_def)
1.72 +apply (blast dest: transL L_I)
1.73  done
1.74
1.75 -lemma LReplace_in_L:
1.76 -     "[|L(X); univalent(L,X,Q)|]
1.77 +lemma LReplace_in_L:
1.78 +     "[|L(X); univalent(L,X,Q)|]
1.79        ==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y"
1.80 -apply (drule L_D, clarify)
1.81 +apply (drule L_D, clarify)
1.82  apply (drule LReplace_in_Lset, assumption+)
1.83  apply (blast intro: L_I Lset_in_Lset_succ)
1.84  done
1.85
1.86  lemma replacement: "replacement(L,P)"
1.87  apply (simp add: replacement_def, clarify)
1.88 -apply (frule LReplace_in_L, assumption+, clarify)
1.89 -apply (rule_tac x=Y in rexI)
1.90 -apply (simp_all add: Replace_iff univalent_def, blast)
1.91 +apply (frule LReplace_in_L, assumption+, clarify)
1.92 +apply (rule_tac x=Y in rexI)
1.93 +apply (simp_all add: Replace_iff univalent_def, blast)
1.94  done
1.95
1.96  subsection{*Instantiating the locale @{text M_triv_axioms}*}
1.97  text{*No instances of Separation yet.*}
1.98
1.99  lemma Lset_mono_le: "mono_le_subset(Lset)"
1.100 -by (simp add: mono_le_subset_def le_imp_subset Lset_mono)
1.101 +by (simp add: mono_le_subset_def le_imp_subset Lset_mono)
1.102
1.103  lemma Lset_cont: "cont_Ord(Lset)"
1.104 -by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord)
1.105 +by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord)
1.106
1.107  lemmas Pair_in_Lset = Formula.Pair_in_LLimit
1.108
1.109 @@ -90,50 +91,88 @@
1.110    apply (rule L_nat)
1.111    done
1.112
1.113 -lemmas rall_abs [simp] = M_triv_axioms.rall_abs [OF M_triv_axioms_L]
1.114 -  and rex_abs [simp] = M_triv_axioms.rex_abs [OF M_triv_axioms_L]
1.115 +lemmas rall_abs = M_triv_axioms.rall_abs [OF M_triv_axioms_L]
1.116 +  and rex_abs = M_triv_axioms.rex_abs [OF M_triv_axioms_L]
1.117    and ball_iff_equiv = M_triv_axioms.ball_iff_equiv [OF M_triv_axioms_L]
1.118    and M_equalityI = M_triv_axioms.M_equalityI [OF M_triv_axioms_L]
1.119 -  and empty_abs [simp] = M_triv_axioms.empty_abs [OF M_triv_axioms_L]
1.120 -  and subset_abs [simp] = M_triv_axioms.subset_abs [OF M_triv_axioms_L]
1.121 -  and upair_abs [simp] = M_triv_axioms.upair_abs [OF M_triv_axioms_L]
1.122 -  and upair_in_M_iff [iff] = M_triv_axioms.upair_in_M_iff [OF M_triv_axioms_L]
1.123 -  and singleton_in_M_iff [iff] = M_triv_axioms.singleton_in_M_iff [OF M_triv_axioms_L]
1.124 -  and pair_abs [simp] = M_triv_axioms.pair_abs [OF M_triv_axioms_L]
1.125 -  and pair_in_M_iff [iff] = M_triv_axioms.pair_in_M_iff [OF M_triv_axioms_L]
1.126 +  and empty_abs = M_triv_axioms.empty_abs [OF M_triv_axioms_L]
1.127 +  and subset_abs = M_triv_axioms.subset_abs [OF M_triv_axioms_L]
1.128 +  and upair_abs = M_triv_axioms.upair_abs [OF M_triv_axioms_L]
1.129 +  and upair_in_M_iff = M_triv_axioms.upair_in_M_iff [OF M_triv_axioms_L]
1.130 +  and singleton_in_M_iff = M_triv_axioms.singleton_in_M_iff [OF M_triv_axioms_L]
1.131 +  and pair_abs = M_triv_axioms.pair_abs [OF M_triv_axioms_L]
1.132 +  and pair_in_M_iff = M_triv_axioms.pair_in_M_iff [OF M_triv_axioms_L]
1.133    and pair_components_in_M = M_triv_axioms.pair_components_in_M [OF M_triv_axioms_L]
1.134 -  and cartprod_abs [simp] = M_triv_axioms.cartprod_abs [OF M_triv_axioms_L]
1.135 -  and union_abs [simp] = M_triv_axioms.union_abs [OF M_triv_axioms_L]
1.136 -  and inter_abs [simp] = M_triv_axioms.inter_abs [OF M_triv_axioms_L]
1.137 -  and setdiff_abs [simp] = M_triv_axioms.setdiff_abs [OF M_triv_axioms_L]
1.138 -  and Union_abs [simp] = M_triv_axioms.Union_abs [OF M_triv_axioms_L]
1.139 -  and Union_closed [intro, simp] = M_triv_axioms.Union_closed [OF M_triv_axioms_L]
1.140 -  and Un_closed [intro, simp] = M_triv_axioms.Un_closed [OF M_triv_axioms_L]
1.141 -  and cons_closed [intro, simp] = M_triv_axioms.cons_closed [OF M_triv_axioms_L]
1.142 -  and successor_abs [simp] = M_triv_axioms.successor_abs [OF M_triv_axioms_L]
1.143 -  and succ_in_M_iff [iff] = M_triv_axioms.succ_in_M_iff [OF M_triv_axioms_L]
1.144 -  and separation_closed [intro, simp] = M_triv_axioms.separation_closed [OF M_triv_axioms_L]
1.145 +  and cartprod_abs = M_triv_axioms.cartprod_abs [OF M_triv_axioms_L]
1.146 +  and union_abs = M_triv_axioms.union_abs [OF M_triv_axioms_L]
1.147 +  and inter_abs = M_triv_axioms.inter_abs [OF M_triv_axioms_L]
1.148 +  and setdiff_abs = M_triv_axioms.setdiff_abs [OF M_triv_axioms_L]
1.149 +  and Union_abs = M_triv_axioms.Union_abs [OF M_triv_axioms_L]
1.150 +  and Union_closed = M_triv_axioms.Union_closed [OF M_triv_axioms_L]
1.151 +  and Un_closed = M_triv_axioms.Un_closed [OF M_triv_axioms_L]
1.152 +  and cons_closed = M_triv_axioms.cons_closed [OF M_triv_axioms_L]
1.153 +  and successor_abs = M_triv_axioms.successor_abs [OF M_triv_axioms_L]
1.154 +  and succ_in_M_iff = M_triv_axioms.succ_in_M_iff [OF M_triv_axioms_L]
1.155 +  and separation_closed = M_triv_axioms.separation_closed [OF M_triv_axioms_L]
1.156    and strong_replacementI = M_triv_axioms.strong_replacementI [OF M_triv_axioms_L]
1.157 -  and strong_replacement_closed [intro, simp] = M_triv_axioms.strong_replacement_closed [OF M_triv_axioms_L]
1.158 -  and RepFun_closed [intro, simp] = M_triv_axioms.RepFun_closed [OF M_triv_axioms_L]
1.159 -  and lam_closed [intro, simp] = M_triv_axioms.lam_closed [OF M_triv_axioms_L]
1.160 -  and image_abs [simp] = M_triv_axioms.image_abs [OF M_triv_axioms_L]
1.161 +  and strong_replacement_closed = M_triv_axioms.strong_replacement_closed [OF M_triv_axioms_L]
1.162 +  and RepFun_closed = M_triv_axioms.RepFun_closed [OF M_triv_axioms_L]
1.163 +  and lam_closed = M_triv_axioms.lam_closed [OF M_triv_axioms_L]
1.164 +  and image_abs = M_triv_axioms.image_abs [OF M_triv_axioms_L]
1.165    and powerset_Pow = M_triv_axioms.powerset_Pow [OF M_triv_axioms_L]
1.166    and powerset_imp_subset_Pow = M_triv_axioms.powerset_imp_subset_Pow [OF M_triv_axioms_L]
1.167 -  and nat_into_M [intro] = M_triv_axioms.nat_into_M [OF M_triv_axioms_L]
1.168 +  and nat_into_M = M_triv_axioms.nat_into_M [OF M_triv_axioms_L]
1.169    and nat_case_closed = M_triv_axioms.nat_case_closed [OF M_triv_axioms_L]
1.170 -  and Inl_in_M_iff [iff] = M_triv_axioms.Inl_in_M_iff [OF M_triv_axioms_L]
1.171 -  and Inr_in_M_iff [iff] = M_triv_axioms.Inr_in_M_iff [OF M_triv_axioms_L]
1.172 +  and Inl_in_M_iff = M_triv_axioms.Inl_in_M_iff [OF M_triv_axioms_L]
1.173 +  and Inr_in_M_iff = M_triv_axioms.Inr_in_M_iff [OF M_triv_axioms_L]
1.174    and lt_closed = M_triv_axioms.lt_closed [OF M_triv_axioms_L]
1.175 -  and transitive_set_abs [simp] = M_triv_axioms.transitive_set_abs [OF M_triv_axioms_L]
1.176 -  and ordinal_abs [simp] = M_triv_axioms.ordinal_abs [OF M_triv_axioms_L]
1.177 -  and limit_ordinal_abs [simp] = M_triv_axioms.limit_ordinal_abs [OF M_triv_axioms_L]
1.178 -  and successor_ordinal_abs [simp] = M_triv_axioms.successor_ordinal_abs [OF M_triv_axioms_L]
1.179 +  and transitive_set_abs = M_triv_axioms.transitive_set_abs [OF M_triv_axioms_L]
1.180 +  and ordinal_abs = M_triv_axioms.ordinal_abs [OF M_triv_axioms_L]
1.181 +  and limit_ordinal_abs = M_triv_axioms.limit_ordinal_abs [OF M_triv_axioms_L]
1.182 +  and successor_ordinal_abs = M_triv_axioms.successor_ordinal_abs [OF M_triv_axioms_L]
1.183    and finite_ordinal_abs = M_triv_axioms.finite_ordinal_abs [OF M_triv_axioms_L]
1.184 -  and omega_abs [simp] = M_triv_axioms.omega_abs [OF M_triv_axioms_L]
1.185 -  and number1_abs [simp] = M_triv_axioms.number1_abs [OF M_triv_axioms_L]
1.186 -  and number2_abs [simp] = M_triv_axioms.number2_abs [OF M_triv_axioms_L]
1.187 -  and number3_abs [simp] = M_triv_axioms.number3_abs [OF M_triv_axioms_L]
1.188 +  and omega_abs = M_triv_axioms.omega_abs [OF M_triv_axioms_L]
1.189 +  and number1_abs = M_triv_axioms.number1_abs [OF M_triv_axioms_L]
1.190 +  and number2_abs = M_triv_axioms.number2_abs [OF M_triv_axioms_L]
1.191 +  and number3_abs = M_triv_axioms.number3_abs [OF M_triv_axioms_L]
1.192 +
1.193 +declare rall_abs [simp]
1.194 +declare rex_abs [simp]
1.195 +declare empty_abs [simp]
1.196 +declare subset_abs [simp]
1.197 +declare upair_abs [simp]
1.198 +declare upair_in_M_iff [iff]
1.199 +declare singleton_in_M_iff [iff]
1.200 +declare pair_abs [simp]
1.201 +declare pair_in_M_iff [iff]
1.202 +declare cartprod_abs [simp]
1.203 +declare union_abs [simp]
1.204 +declare inter_abs [simp]
1.205 +declare setdiff_abs [simp]
1.206 +declare Union_abs [simp]
1.207 +declare Union_closed [intro, simp]
1.208 +declare Un_closed [intro, simp]
1.209 +declare cons_closed [intro, simp]
1.210 +declare successor_abs [simp]
1.211 +declare succ_in_M_iff [iff]
1.212 +declare separation_closed [intro, simp]
1.213 +declare strong_replacementI
1.214 +declare strong_replacement_closed [intro, simp]
1.215 +declare RepFun_closed [intro, simp]
1.216 +declare lam_closed [intro, simp]
1.217 +declare image_abs [simp]
1.218 +declare nat_into_M [intro]
1.219 +declare Inl_in_M_iff [iff]
1.220 +declare Inr_in_M_iff [iff]
1.221 +declare transitive_set_abs [simp]
1.222 +declare ordinal_abs [simp]
1.223 +declare limit_ordinal_abs [simp]
1.224 +declare successor_ordinal_abs [simp]
1.225 +declare finite_ordinal_abs [simp]
1.226 +declare omega_abs [simp]
1.227 +declare number1_abs [simp]
1.228 +declare number2_abs [simp]
1.229 +declare number3_abs [simp]
1.230
1.231
1.232  subsection{*Instantiation of the locale @{text reflection}*}
1.233 @@ -151,7 +190,7 @@
1.234
1.235
1.236  text{*We must use the meta-existential quantifier; otherwise the reflection
1.237 -      terms become enormous!*}
1.238 +      terms become enormous!*}
1.239  constdefs
1.240    L_Reflects :: "[i=>o,[i,i]=>o] => prop"      ("(3REFLECTS/ [_,/ _])")
1.241      "REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) &
1.242 @@ -160,60 +199,60 @@
1.243
1.244  theorem Triv_reflection:
1.245       "REFLECTS[P, \<lambda>a x. P(x)]"
1.247 -apply (rule meta_exI)
1.248 -apply (rule Closed_Unbounded_Ord)
1.250 +apply (rule meta_exI)
1.251 +apply (rule Closed_Unbounded_Ord)
1.252  done
1.253
1.254  theorem Not_reflection:
1.255       "REFLECTS[P,Q] ==> REFLECTS[\<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x)]"
1.256 -apply (unfold L_Reflects_def)
1.257 -apply (erule meta_exE)
1.258 -apply (rule_tac x=Cl in meta_exI, simp)
1.259 +apply (unfold L_Reflects_def)
1.260 +apply (erule meta_exE)
1.261 +apply (rule_tac x=Cl in meta_exI, simp)
1.262  done
1.263
1.264  theorem And_reflection:
1.265 -     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
1.266 +     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
1.267        ==> REFLECTS[\<lambda>x. P(x) \<and> P'(x), \<lambda>a x. Q(a,x) \<and> Q'(a,x)]"
1.268 -apply (unfold L_Reflects_def)
1.269 -apply (elim meta_exE)
1.270 -apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
1.271 -apply (simp add: Closed_Unbounded_Int, blast)
1.272 +apply (unfold L_Reflects_def)
1.273 +apply (elim meta_exE)
1.274 +apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
1.275 +apply (simp add: Closed_Unbounded_Int, blast)
1.276  done
1.277
1.278  theorem Or_reflection:
1.279 -     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
1.280 +     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
1.281        ==> REFLECTS[\<lambda>x. P(x) \<or> P'(x), \<lambda>a x. Q(a,x) \<or> Q'(a,x)]"
1.282 -apply (unfold L_Reflects_def)
1.283 -apply (elim meta_exE)
1.284 -apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
1.285 -apply (simp add: Closed_Unbounded_Int, blast)
1.286 +apply (unfold L_Reflects_def)
1.287 +apply (elim meta_exE)
1.288 +apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
1.289 +apply (simp add: Closed_Unbounded_Int, blast)
1.290  done
1.291
1.292  theorem Imp_reflection:
1.293 -     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
1.294 +     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
1.295        ==> REFLECTS[\<lambda>x. P(x) --> P'(x), \<lambda>a x. Q(a,x) --> Q'(a,x)]"
1.296 -apply (unfold L_Reflects_def)
1.297 -apply (elim meta_exE)
1.298 -apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
1.299 -apply (simp add: Closed_Unbounded_Int, blast)
1.300 +apply (unfold L_Reflects_def)
1.301 +apply (elim meta_exE)
1.302 +apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
1.303 +apply (simp add: Closed_Unbounded_Int, blast)
1.304  done
1.305
1.306  theorem Iff_reflection:
1.307 -     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
1.308 +     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
1.309        ==> REFLECTS[\<lambda>x. P(x) <-> P'(x), \<lambda>a x. Q(a,x) <-> Q'(a,x)]"
1.310 -apply (unfold L_Reflects_def)
1.311 -apply (elim meta_exE)
1.312 -apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
1.313 -apply (simp add: Closed_Unbounded_Int, blast)
1.314 +apply (unfold L_Reflects_def)
1.315 +apply (elim meta_exE)
1.316 +apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
1.317 +apply (simp add: Closed_Unbounded_Int, blast)
1.318  done
1.319
1.320
1.321  theorem Ex_reflection:
1.322       "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
1.323        ==> REFLECTS[\<lambda>x. \<exists>z. L(z) \<and> P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
1.324 -apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
1.325 -apply (elim meta_exE)
1.326 +apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
1.327 +apply (elim meta_exE)
1.328  apply (rule meta_exI)
1.329  apply (rule reflection.Ex_reflection
1.330    [OF reflection.intro, OF Lset_mono_le Lset_cont Pair_in_Lset],
1.331 @@ -222,9 +261,9 @@
1.332
1.333  theorem All_reflection:
1.334       "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
1.335 -      ==> REFLECTS[\<lambda>x. \<forall>z. L(z) --> P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
1.336 -apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
1.337 -apply (elim meta_exE)
1.338 +      ==> REFLECTS[\<lambda>x. \<forall>z. L(z) --> P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
1.339 +apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
1.340 +apply (elim meta_exE)
1.341  apply (rule meta_exI)
1.342  apply (rule reflection.All_reflection
1.343    [OF reflection.intro, OF Lset_mono_le Lset_cont Pair_in_Lset],
1.344 @@ -234,35 +273,35 @@
1.345  theorem Rex_reflection:
1.346       "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
1.347        ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
1.348 -apply (unfold rex_def)
1.349 +apply (unfold rex_def)
1.350  apply (intro And_reflection Ex_reflection, assumption)
1.351  done
1.352
1.353  theorem Rall_reflection:
1.354       "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
1.355 -      ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
1.356 -apply (unfold rall_def)
1.357 +      ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
1.358 +apply (unfold rall_def)
1.359  apply (intro Imp_reflection All_reflection, assumption)
1.360  done
1.361
1.362 -lemmas FOL_reflections =
1.363 +lemmas FOL_reflections =
1.364          Triv_reflection Not_reflection And_reflection Or_reflection
1.365          Imp_reflection Iff_reflection Ex_reflection All_reflection
1.366          Rex_reflection Rall_reflection
1.367
1.368  lemma ReflectsD:
1.369 -     "[|REFLECTS[P,Q]; Ord(i)|]
1.370 +     "[|REFLECTS[P,Q]; Ord(i)|]
1.371        ==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) <-> Q(j,x))"
1.372 -apply (unfold L_Reflects_def Closed_Unbounded_def)
1.373 -apply (elim meta_exE, clarify)
1.374 -apply (blast dest!: UnboundedD)
1.375 +apply (unfold L_Reflects_def Closed_Unbounded_def)
1.376 +apply (elim meta_exE, clarify)
1.377 +apply (blast dest!: UnboundedD)
1.378  done
1.379
1.380  lemma ReflectsE:
1.381       "[| REFLECTS[P,Q]; Ord(i);
1.382           !!j. [|i<j;  \<forall>x \<in> Lset(j). P(x) <-> Q(j,x)|] ==> R |]
1.383        ==> R"
1.384 -apply (drule ReflectsD, assumption, blast)
1.385 +apply (drule ReflectsD, assumption, blast)
1.386  done
1.387
1.388  lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B"
1.389 @@ -301,11 +340,11 @@
1.390
1.391  lemma empty_type [TC]:
1.392       "x \<in> nat ==> empty_fm(x) \<in> formula"
1.395
1.396  lemma arity_empty_fm [simp]:
1.397       "x \<in> nat ==> arity(empty_fm(x)) = succ(x)"
1.398 -by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac)
1.399 +by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac)
1.400
1.401  lemma sats_empty_fm [simp]:
1.402     "[| x \<in> nat; env \<in> list(A)|]
1.403 @@ -313,16 +352,16 @@
1.404  by (simp add: empty_fm_def empty_def)
1.405
1.406  lemma empty_iff_sats:
1.407 -      "[| nth(i,env) = x; nth(j,env) = y;
1.408 +      "[| nth(i,env) = x; nth(j,env) = y;
1.409            i \<in> nat; env \<in> list(A)|]
1.410         ==> empty(**A, x) <-> sats(A, empty_fm(i), env)"
1.411  by simp
1.412
1.413  theorem empty_reflection:
1.414 -     "REFLECTS[\<lambda>x. empty(L,f(x)),
1.415 +     "REFLECTS[\<lambda>x. empty(L,f(x)),
1.416                 \<lambda>i x. empty(**Lset(i),f(x))]"
1.417  apply (simp only: empty_def setclass_simps)
1.418 -apply (intro FOL_reflections)
1.419 +apply (intro FOL_reflections)
1.420  done
1.421
1.422  text{*Not used.  But maybe useful?*}
1.423 @@ -330,38 +369,38 @@
1.424     "[| n \<in> nat; env \<in> list(A); Transset(A)|]
1.425      ==> sats(A, empty_fm(n), env) <-> nth(n,env) = 0"
1.426  apply (simp add: empty_fm_def empty_def Transset_def, auto)
1.427 -apply (case_tac "n < length(env)")
1.428 -apply (frule nth_type, assumption+, blast)
1.429 -apply (simp_all add: not_lt_iff_le nth_eq_0)
1.430 +apply (case_tac "n < length(env)")
1.431 +apply (frule nth_type, assumption+, blast)
1.432 +apply (simp_all add: not_lt_iff_le nth_eq_0)
1.433  done
1.434
1.435
1.436  subsubsection{*Unordered Pairs, Internalized*}
1.437
1.438  constdefs upair_fm :: "[i,i,i]=>i"
1.439 -    "upair_fm(x,y,z) ==
1.440 -       And(Member(x,z),
1.441 +    "upair_fm(x,y,z) ==
1.442 +       And(Member(x,z),
1.443             And(Member(y,z),
1.444 -               Forall(Implies(Member(0,succ(z)),
1.445 +               Forall(Implies(Member(0,succ(z)),
1.446                                Or(Equal(0,succ(x)), Equal(0,succ(y)))))))"
1.447
1.448  lemma upair_type [TC]:
1.449       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> upair_fm(x,y,z) \<in> formula"
1.452
1.453  lemma arity_upair_fm [simp]:
1.454 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.455 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.456        ==> arity(upair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.457 -by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac)
1.458 +by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac)
1.459
1.460  lemma sats_upair_fm [simp]:
1.461     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.462 -    ==> sats(A, upair_fm(x,y,z), env) <->
1.463 +    ==> sats(A, upair_fm(x,y,z), env) <->
1.464              upair(**A, nth(x,env), nth(y,env), nth(z,env))"
1.465  by (simp add: upair_fm_def upair_def)
1.466
1.467  lemma upair_iff_sats:
1.468 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.469 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.470            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.471         ==> upair(**A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)"
1.473 @@ -369,127 +408,127 @@
1.474  text{*Useful? At least it refers to "real" unordered pairs*}
1.475  lemma sats_upair_fm2 [simp]:
1.476     "[| x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A); Transset(A)|]
1.477 -    ==> sats(A, upair_fm(x,y,z), env) <->
1.478 +    ==> sats(A, upair_fm(x,y,z), env) <->
1.479          nth(z,env) = {nth(x,env), nth(y,env)}"
1.480 -apply (frule lt_length_in_nat, assumption)
1.481 -apply (simp add: upair_fm_def Transset_def, auto)
1.482 -apply (blast intro: nth_type)
1.483 +apply (frule lt_length_in_nat, assumption)
1.484 +apply (simp add: upair_fm_def Transset_def, auto)
1.485 +apply (blast intro: nth_type)
1.486  done
1.487
1.488  theorem upair_reflection:
1.489 -     "REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)),
1.490 -               \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]"
1.491 +     "REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)),
1.492 +               \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]"
1.494 -apply (intro FOL_reflections)
1.495 +apply (intro FOL_reflections)
1.496  done
1.497
1.498  subsubsection{*Ordered pairs, Internalized*}
1.499
1.500  constdefs pair_fm :: "[i,i,i]=>i"
1.501 -    "pair_fm(x,y,z) ==
1.502 +    "pair_fm(x,y,z) ==
1.503         Exists(And(upair_fm(succ(x),succ(x),0),
1.504                Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0),
1.505                           upair_fm(1,0,succ(succ(z)))))))"
1.506
1.507  lemma pair_type [TC]:
1.508       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pair_fm(x,y,z) \<in> formula"
1.511
1.512  lemma arity_pair_fm [simp]:
1.513 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.514 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.515        ==> arity(pair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.516 -by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac)
1.517 +by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac)
1.518
1.519  lemma sats_pair_fm [simp]:
1.520     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.521 -    ==> sats(A, pair_fm(x,y,z), env) <->
1.522 +    ==> sats(A, pair_fm(x,y,z), env) <->
1.523          pair(**A, nth(x,env), nth(y,env), nth(z,env))"
1.524  by (simp add: pair_fm_def pair_def)
1.525
1.526  lemma pair_iff_sats:
1.527 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.528 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.529            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.530         ==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)"
1.532
1.533  theorem pair_reflection:
1.534 -     "REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
1.535 +     "REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
1.536                 \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]"
1.537  apply (simp only: pair_def setclass_simps)
1.538 -apply (intro FOL_reflections upair_reflection)
1.539 +apply (intro FOL_reflections upair_reflection)
1.540  done
1.541
1.542
1.543  subsubsection{*Binary Unions, Internalized*}
1.544
1.545  constdefs union_fm :: "[i,i,i]=>i"
1.546 -    "union_fm(x,y,z) ==
1.547 +    "union_fm(x,y,z) ==
1.548         Forall(Iff(Member(0,succ(z)),
1.549                    Or(Member(0,succ(x)),Member(0,succ(y)))))"
1.550
1.551  lemma union_type [TC]:
1.552       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> union_fm(x,y,z) \<in> formula"
1.555
1.556  lemma arity_union_fm [simp]:
1.557 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.558 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.559        ==> arity(union_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.560 -by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac)
1.561 +by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac)
1.562
1.563  lemma sats_union_fm [simp]:
1.564     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.565 -    ==> sats(A, union_fm(x,y,z), env) <->
1.566 +    ==> sats(A, union_fm(x,y,z), env) <->
1.567          union(**A, nth(x,env), nth(y,env), nth(z,env))"
1.568  by (simp add: union_fm_def union_def)
1.569
1.570  lemma union_iff_sats:
1.571 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.572 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.573            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.574         ==> union(**A, x, y, z) <-> sats(A, union_fm(i,j,k), env)"
1.576
1.577  theorem union_reflection:
1.578 -     "REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
1.579 +     "REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
1.580                 \<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]"
1.581  apply (simp only: union_def setclass_simps)
1.582 -apply (intro FOL_reflections)
1.583 +apply (intro FOL_reflections)
1.584  done
1.585
1.586
1.587  subsubsection{*Set ``Cons,'' Internalized*}
1.588
1.589  constdefs cons_fm :: "[i,i,i]=>i"
1.590 -    "cons_fm(x,y,z) ==
1.591 +    "cons_fm(x,y,z) ==
1.592         Exists(And(upair_fm(succ(x),succ(x),0),
1.593                    union_fm(0,succ(y),succ(z))))"
1.594
1.595
1.596  lemma cons_type [TC]:
1.597       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cons_fm(x,y,z) \<in> formula"
1.600
1.601  lemma arity_cons_fm [simp]:
1.602 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.603 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.604        ==> arity(cons_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.605 -by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac)
1.606 +by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac)
1.607
1.608  lemma sats_cons_fm [simp]:
1.609     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.610 -    ==> sats(A, cons_fm(x,y,z), env) <->
1.611 +    ==> sats(A, cons_fm(x,y,z), env) <->
1.612          is_cons(**A, nth(x,env), nth(y,env), nth(z,env))"
1.613  by (simp add: cons_fm_def is_cons_def)
1.614
1.615  lemma cons_iff_sats:
1.616 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.617 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.618            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.619         ==> is_cons(**A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)"
1.620  by simp
1.621
1.622  theorem cons_reflection:
1.623 -     "REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)),
1.624 +     "REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)),
1.625                 \<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]"
1.626  apply (simp only: is_cons_def setclass_simps)
1.627 -apply (intro FOL_reflections upair_reflection union_reflection)
1.628 +apply (intro FOL_reflections upair_reflection union_reflection)
1.629  done
1.630
1.631
1.632 @@ -500,30 +539,30 @@
1.633
1.634  lemma succ_type [TC]:
1.635       "[| x \<in> nat; y \<in> nat |] ==> succ_fm(x,y) \<in> formula"
1.638
1.639  lemma arity_succ_fm [simp]:
1.640 -     "[| x \<in> nat; y \<in> nat |]
1.641 +     "[| x \<in> nat; y \<in> nat |]
1.642        ==> arity(succ_fm(x,y)) = succ(x) \<union> succ(y)"
1.644
1.645  lemma sats_succ_fm [simp]:
1.646     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.647 -    ==> sats(A, succ_fm(x,y), env) <->
1.648 +    ==> sats(A, succ_fm(x,y), env) <->
1.649          successor(**A, nth(x,env), nth(y,env))"
1.650  by (simp add: succ_fm_def successor_def)
1.651
1.652  lemma successor_iff_sats:
1.653 -      "[| nth(i,env) = x; nth(j,env) = y;
1.654 +      "[| nth(i,env) = x; nth(j,env) = y;
1.655            i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.656         ==> successor(**A, x, y) <-> sats(A, succ_fm(i,j), env)"
1.657  by simp
1.658
1.659  theorem successor_reflection:
1.660 -     "REFLECTS[\<lambda>x. successor(L,f(x),g(x)),
1.661 +     "REFLECTS[\<lambda>x. successor(L,f(x),g(x)),
1.662                 \<lambda>i x. successor(**Lset(i),f(x),g(x))]"
1.663  apply (simp only: successor_def setclass_simps)
1.664 -apply (intro cons_reflection)
1.665 +apply (intro cons_reflection)
1.666  done
1.667
1.668
1.669 @@ -535,11 +574,11 @@
1.670
1.671  lemma number1_type [TC]:
1.672       "x \<in> nat ==> number1_fm(x) \<in> formula"
1.675
1.676  lemma arity_number1_fm [simp]:
1.677       "x \<in> nat ==> arity(number1_fm(x)) = succ(x)"
1.678 -by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac)
1.679 +by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac)
1.680
1.681  lemma sats_number1_fm [simp]:
1.682     "[| x \<in> nat; env \<in> list(A)|]
1.683 @@ -547,13 +586,13 @@
1.684  by (simp add: number1_fm_def number1_def)
1.685
1.686  lemma number1_iff_sats:
1.687 -      "[| nth(i,env) = x; nth(j,env) = y;
1.688 +      "[| nth(i,env) = x; nth(j,env) = y;
1.689            i \<in> nat; env \<in> list(A)|]
1.690         ==> number1(**A, x) <-> sats(A, number1_fm(i), env)"
1.691  by simp
1.692
1.693  theorem number1_reflection:
1.694 -     "REFLECTS[\<lambda>x. number1(L,f(x)),
1.695 +     "REFLECTS[\<lambda>x. number1(L,f(x)),
1.696                 \<lambda>i x. number1(**Lset(i),f(x))]"
1.697  apply (simp only: number1_def setclass_simps)
1.698  apply (intro FOL_reflections empty_reflection successor_reflection)
1.699 @@ -564,36 +603,36 @@
1.700
1.701  (*  "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
1.702  constdefs big_union_fm :: "[i,i]=>i"
1.703 -    "big_union_fm(A,z) ==
1.704 +    "big_union_fm(A,z) ==
1.705         Forall(Iff(Member(0,succ(z)),
1.706                    Exists(And(Member(0,succ(succ(A))), Member(1,0)))))"
1.707
1.708  lemma big_union_type [TC]:
1.709       "[| x \<in> nat; y \<in> nat |] ==> big_union_fm(x,y) \<in> formula"
1.712
1.713  lemma arity_big_union_fm [simp]:
1.714 -     "[| x \<in> nat; y \<in> nat |]
1.715 +     "[| x \<in> nat; y \<in> nat |]
1.716        ==> arity(big_union_fm(x,y)) = succ(x) \<union> succ(y)"
1.717  by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac)
1.718
1.719  lemma sats_big_union_fm [simp]:
1.720     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.721 -    ==> sats(A, big_union_fm(x,y), env) <->
1.722 +    ==> sats(A, big_union_fm(x,y), env) <->
1.723          big_union(**A, nth(x,env), nth(y,env))"
1.724  by (simp add: big_union_fm_def big_union_def)
1.725
1.726  lemma big_union_iff_sats:
1.727 -      "[| nth(i,env) = x; nth(j,env) = y;
1.728 +      "[| nth(i,env) = x; nth(j,env) = y;
1.729            i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.730         ==> big_union(**A, x, y) <-> sats(A, big_union_fm(i,j), env)"
1.731  by simp
1.732
1.733  theorem big_union_reflection:
1.734 -     "REFLECTS[\<lambda>x. big_union(L,f(x),g(x)),
1.735 +     "REFLECTS[\<lambda>x. big_union(L,f(x),g(x)),
1.736                 \<lambda>i x. big_union(**Lset(i),f(x),g(x))]"
1.737  apply (simp only: big_union_def setclass_simps)
1.738 -apply (intro FOL_reflections)
1.739 +apply (intro FOL_reflections)
1.740  done
1.741
1.742
1.743 @@ -604,26 +643,26 @@
1.744
1.745  lemma sats_subset_fm':
1.746     "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.747 -    ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))"
1.748 -by (simp add: subset_fm_def Relative.subset_def)
1.749 +    ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))"
1.750 +by (simp add: subset_fm_def Relative.subset_def)
1.751
1.752  theorem subset_reflection:
1.753 -     "REFLECTS[\<lambda>x. subset(L,f(x),g(x)),
1.754 -               \<lambda>i x. subset(**Lset(i),f(x),g(x))]"
1.755 +     "REFLECTS[\<lambda>x. subset(L,f(x),g(x)),
1.756 +               \<lambda>i x. subset(**Lset(i),f(x),g(x))]"
1.757  apply (simp only: Relative.subset_def setclass_simps)
1.758 -apply (intro FOL_reflections)
1.759 +apply (intro FOL_reflections)
1.760  done
1.761
1.762  lemma sats_transset_fm':
1.763     "[|x \<in> nat; env \<in> list(A)|]
1.764      ==> sats(A, transset_fm(x), env) <-> transitive_set(**A, nth(x,env))"
1.765 -by (simp add: sats_subset_fm' transset_fm_def transitive_set_def)
1.766 +by (simp add: sats_subset_fm' transset_fm_def transitive_set_def)
1.767
1.768  theorem transitive_set_reflection:
1.769       "REFLECTS[\<lambda>x. transitive_set(L,f(x)),
1.770                 \<lambda>i x. transitive_set(**Lset(i),f(x))]"
1.771  apply (simp only: transitive_set_def setclass_simps)
1.772 -apply (intro FOL_reflections subset_reflection)
1.773 +apply (intro FOL_reflections subset_reflection)
1.774  done
1.775
1.776  lemma sats_ordinal_fm':
1.777 @@ -639,14 +678,14 @@
1.778  theorem ordinal_reflection:
1.779       "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]"
1.780  apply (simp only: ordinal_def setclass_simps)
1.781 -apply (intro FOL_reflections transitive_set_reflection)
1.782 +apply (intro FOL_reflections transitive_set_reflection)
1.783  done
1.784
1.785
1.786  subsubsection{*Membership Relation, Internalized*}
1.787
1.788  constdefs Memrel_fm :: "[i,i]=>i"
1.789 -    "Memrel_fm(A,r) ==
1.790 +    "Memrel_fm(A,r) ==
1.791         Forall(Iff(Member(0,succ(r)),
1.792                    Exists(And(Member(0,succ(succ(A))),
1.793                               Exists(And(Member(0,succ(succ(succ(A)))),
1.794 @@ -655,36 +694,36 @@
1.795
1.796  lemma Memrel_type [TC]:
1.797       "[| x \<in> nat; y \<in> nat |] ==> Memrel_fm(x,y) \<in> formula"
1.800
1.801  lemma arity_Memrel_fm [simp]:
1.802 -     "[| x \<in> nat; y \<in> nat |]
1.803 +     "[| x \<in> nat; y \<in> nat |]
1.804        ==> arity(Memrel_fm(x,y)) = succ(x) \<union> succ(y)"
1.805 -by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac)
1.806 +by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac)
1.807
1.808  lemma sats_Memrel_fm [simp]:
1.809     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.810 -    ==> sats(A, Memrel_fm(x,y), env) <->
1.811 +    ==> sats(A, Memrel_fm(x,y), env) <->
1.812          membership(**A, nth(x,env), nth(y,env))"
1.813  by (simp add: Memrel_fm_def membership_def)
1.814
1.815  lemma Memrel_iff_sats:
1.816 -      "[| nth(i,env) = x; nth(j,env) = y;
1.817 +      "[| nth(i,env) = x; nth(j,env) = y;
1.818            i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.819         ==> membership(**A, x, y) <-> sats(A, Memrel_fm(i,j), env)"
1.820  by simp
1.821
1.822  theorem membership_reflection:
1.823 -     "REFLECTS[\<lambda>x. membership(L,f(x),g(x)),
1.824 +     "REFLECTS[\<lambda>x. membership(L,f(x),g(x)),
1.825                 \<lambda>i x. membership(**Lset(i),f(x),g(x))]"
1.826  apply (simp only: membership_def setclass_simps)
1.827 -apply (intro FOL_reflections pair_reflection)
1.828 +apply (intro FOL_reflections pair_reflection)
1.829  done
1.830
1.831  subsubsection{*Predecessor Set, Internalized*}
1.832
1.833  constdefs pred_set_fm :: "[i,i,i,i]=>i"
1.834 -    "pred_set_fm(A,x,r,B) ==
1.835 +    "pred_set_fm(A,x,r,B) ==
1.836         Forall(Iff(Member(0,succ(B)),
1.837                    Exists(And(Member(0,succ(succ(r))),
1.838                               And(Member(1,succ(succ(A))),
1.839 @@ -692,148 +731,148 @@
1.840
1.841
1.842  lemma pred_set_type [TC]:
1.843 -     "[| A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
1.844 +     "[| A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
1.845        ==> pred_set_fm(A,x,r,B) \<in> formula"
1.848
1.849  lemma arity_pred_set_fm [simp]:
1.850 -   "[| A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
1.851 +   "[| A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
1.852      ==> arity(pred_set_fm(A,x,r,B)) = succ(A) \<union> succ(x) \<union> succ(r) \<union> succ(B)"
1.853 -by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac)
1.854 +by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac)
1.855
1.856  lemma sats_pred_set_fm [simp]:
1.857     "[| U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)|]
1.858 -    ==> sats(A, pred_set_fm(U,x,r,B), env) <->
1.859 +    ==> sats(A, pred_set_fm(U,x,r,B), env) <->
1.860          pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))"
1.861  by (simp add: pred_set_fm_def pred_set_def)
1.862
1.863  lemma pred_set_iff_sats:
1.864 -      "[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B;
1.865 +      "[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B;
1.866            i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)|]
1.867         ==> pred_set(**A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)"
1.869
1.870  theorem pred_set_reflection:
1.871 -     "REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
1.872 -               \<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]"
1.873 +     "REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
1.874 +               \<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]"
1.875  apply (simp only: pred_set_def setclass_simps)
1.876 -apply (intro FOL_reflections pair_reflection)
1.877 +apply (intro FOL_reflections pair_reflection)
1.878  done
1.879
1.880
1.881
1.882  subsubsection{*Domain of a Relation, Internalized*}
1.883
1.884 -(* "is_domain(M,r,z) ==
1.885 -	\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *)
1.886 +(* "is_domain(M,r,z) ==
1.887 +        \<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *)
1.888  constdefs domain_fm :: "[i,i]=>i"
1.889 -    "domain_fm(r,z) ==
1.890 +    "domain_fm(r,z) ==
1.891         Forall(Iff(Member(0,succ(z)),
1.892                    Exists(And(Member(0,succ(succ(r))),
1.893                               Exists(pair_fm(2,0,1))))))"
1.894
1.895  lemma domain_type [TC]:
1.896       "[| x \<in> nat; y \<in> nat |] ==> domain_fm(x,y) \<in> formula"
1.899
1.900  lemma arity_domain_fm [simp]:
1.901 -     "[| x \<in> nat; y \<in> nat |]
1.902 +     "[| x \<in> nat; y \<in> nat |]
1.903        ==> arity(domain_fm(x,y)) = succ(x) \<union> succ(y)"
1.904 -by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac)
1.905 +by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac)
1.906
1.907  lemma sats_domain_fm [simp]:
1.908     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.909 -    ==> sats(A, domain_fm(x,y), env) <->
1.910 +    ==> sats(A, domain_fm(x,y), env) <->
1.911          is_domain(**A, nth(x,env), nth(y,env))"
1.912  by (simp add: domain_fm_def is_domain_def)
1.913
1.914  lemma domain_iff_sats:
1.915 -      "[| nth(i,env) = x; nth(j,env) = y;
1.916 +      "[| nth(i,env) = x; nth(j,env) = y;
1.917            i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.918         ==> is_domain(**A, x, y) <-> sats(A, domain_fm(i,j), env)"
1.919  by simp
1.920
1.921  theorem domain_reflection:
1.922 -     "REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)),
1.923 +     "REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)),
1.924                 \<lambda>i x. is_domain(**Lset(i),f(x),g(x))]"
1.925  apply (simp only: is_domain_def setclass_simps)
1.926 -apply (intro FOL_reflections pair_reflection)
1.927 +apply (intro FOL_reflections pair_reflection)
1.928  done
1.929
1.930
1.931  subsubsection{*Range of a Relation, Internalized*}
1.932
1.933 -(* "is_range(M,r,z) ==
1.934 -	\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *)
1.935 +(* "is_range(M,r,z) ==
1.936 +        \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *)
1.937  constdefs range_fm :: "[i,i]=>i"
1.938 -    "range_fm(r,z) ==
1.939 +    "range_fm(r,z) ==
1.940         Forall(Iff(Member(0,succ(z)),
1.941                    Exists(And(Member(0,succ(succ(r))),
1.942                               Exists(pair_fm(0,2,1))))))"
1.943
1.944  lemma range_type [TC]:
1.945       "[| x \<in> nat; y \<in> nat |] ==> range_fm(x,y) \<in> formula"
1.948
1.949  lemma arity_range_fm [simp]:
1.950 -     "[| x \<in> nat; y \<in> nat |]
1.951 +     "[| x \<in> nat; y \<in> nat |]
1.952        ==> arity(range_fm(x,y)) = succ(x) \<union> succ(y)"
1.953 -by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac)
1.954 +by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac)
1.955
1.956  lemma sats_range_fm [simp]:
1.957     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.958 -    ==> sats(A, range_fm(x,y), env) <->
1.959 +    ==> sats(A, range_fm(x,y), env) <->
1.960          is_range(**A, nth(x,env), nth(y,env))"
1.961  by (simp add: range_fm_def is_range_def)
1.962
1.963  lemma range_iff_sats:
1.964 -      "[| nth(i,env) = x; nth(j,env) = y;
1.965 +      "[| nth(i,env) = x; nth(j,env) = y;
1.966            i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.967         ==> is_range(**A, x, y) <-> sats(A, range_fm(i,j), env)"
1.968  by simp
1.969
1.970  theorem range_reflection:
1.971 -     "REFLECTS[\<lambda>x. is_range(L,f(x),g(x)),
1.972 +     "REFLECTS[\<lambda>x. is_range(L,f(x),g(x)),
1.973                 \<lambda>i x. is_range(**Lset(i),f(x),g(x))]"
1.974  apply (simp only: is_range_def setclass_simps)
1.975 -apply (intro FOL_reflections pair_reflection)
1.976 +apply (intro FOL_reflections pair_reflection)
1.977  done
1.978
1.979 -
1.980 +
1.981  subsubsection{*Field of a Relation, Internalized*}
1.982
1.983 -(* "is_field(M,r,z) ==
1.984 -	\<exists>dr[M]. is_domain(M,r,dr) &
1.985 +(* "is_field(M,r,z) ==
1.986 +        \<exists>dr[M]. is_domain(M,r,dr) &
1.987              (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *)
1.988  constdefs field_fm :: "[i,i]=>i"
1.989 -    "field_fm(r,z) ==
1.990 -       Exists(And(domain_fm(succ(r),0),
1.991 -              Exists(And(range_fm(succ(succ(r)),0),
1.992 +    "field_fm(r,z) ==
1.993 +       Exists(And(domain_fm(succ(r),0),
1.994 +              Exists(And(range_fm(succ(succ(r)),0),
1.995                           union_fm(1,0,succ(succ(z)))))))"
1.996
1.997  lemma field_type [TC]:
1.998       "[| x \<in> nat; y \<in> nat |] ==> field_fm(x,y) \<in> formula"
1.1001
1.1002  lemma arity_field_fm [simp]:
1.1003 -     "[| x \<in> nat; y \<in> nat |]
1.1004 +     "[| x \<in> nat; y \<in> nat |]
1.1005        ==> arity(field_fm(x,y)) = succ(x) \<union> succ(y)"
1.1006 -by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1007 +by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1008
1.1009  lemma sats_field_fm [simp]:
1.1010     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.1011 -    ==> sats(A, field_fm(x,y), env) <->
1.1012 +    ==> sats(A, field_fm(x,y), env) <->
1.1013          is_field(**A, nth(x,env), nth(y,env))"
1.1014  by (simp add: field_fm_def is_field_def)
1.1015
1.1016  lemma field_iff_sats:
1.1017 -      "[| nth(i,env) = x; nth(j,env) = y;
1.1018 +      "[| nth(i,env) = x; nth(j,env) = y;
1.1019            i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.1020         ==> is_field(**A, x, y) <-> sats(A, field_fm(i,j), env)"
1.1021  by simp
1.1022
1.1023  theorem field_reflection:
1.1024 -     "REFLECTS[\<lambda>x. is_field(L,f(x),g(x)),
1.1025 +     "REFLECTS[\<lambda>x. is_field(L,f(x),g(x)),
1.1026                 \<lambda>i x. is_field(**Lset(i),f(x),g(x))]"
1.1027  apply (simp only: is_field_def setclass_simps)
1.1028  apply (intro FOL_reflections domain_reflection range_reflection
1.1029 @@ -843,140 +882,140 @@
1.1030
1.1031  subsubsection{*Image under a Relation, Internalized*}
1.1032
1.1033 -(* "image(M,r,A,z) ==
1.1034 +(* "image(M,r,A,z) ==
1.1035          \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *)
1.1036  constdefs image_fm :: "[i,i,i]=>i"
1.1037 -    "image_fm(r,A,z) ==
1.1038 +    "image_fm(r,A,z) ==
1.1039         Forall(Iff(Member(0,succ(z)),
1.1040                    Exists(And(Member(0,succ(succ(r))),
1.1041                               Exists(And(Member(0,succ(succ(succ(A)))),
1.1042 -	 			        pair_fm(0,2,1)))))))"
1.1043 +                                        pair_fm(0,2,1)))))))"
1.1044
1.1045  lemma image_type [TC]:
1.1046       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> image_fm(x,y,z) \<in> formula"
1.1049
1.1050  lemma arity_image_fm [simp]:
1.1051 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1052 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1053        ==> arity(image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.1054 -by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1055 +by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1056
1.1057  lemma sats_image_fm [simp]:
1.1058     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.1059 -    ==> sats(A, image_fm(x,y,z), env) <->
1.1060 +    ==> sats(A, image_fm(x,y,z), env) <->
1.1061          image(**A, nth(x,env), nth(y,env), nth(z,env))"
1.1062  by (simp add: image_fm_def Relative.image_def)
1.1063
1.1064  lemma image_iff_sats:
1.1065 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1066 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1067            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.1068         ==> image(**A, x, y, z) <-> sats(A, image_fm(i,j,k), env)"
1.1070
1.1071  theorem image_reflection:
1.1072 -     "REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
1.1073 +     "REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
1.1074                 \<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]"
1.1075  apply (simp only: Relative.image_def setclass_simps)
1.1076 -apply (intro FOL_reflections pair_reflection)
1.1077 +apply (intro FOL_reflections pair_reflection)
1.1078  done
1.1079
1.1080
1.1081  subsubsection{*Pre-Image under a Relation, Internalized*}
1.1082
1.1083 -(* "pre_image(M,r,A,z) ==
1.1084 -	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *)
1.1085 +(* "pre_image(M,r,A,z) ==
1.1086 +        \<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *)
1.1087  constdefs pre_image_fm :: "[i,i,i]=>i"
1.1088 -    "pre_image_fm(r,A,z) ==
1.1089 +    "pre_image_fm(r,A,z) ==
1.1090         Forall(Iff(Member(0,succ(z)),
1.1091                    Exists(And(Member(0,succ(succ(r))),
1.1092                               Exists(And(Member(0,succ(succ(succ(A)))),
1.1093 -	 			        pair_fm(2,0,1)))))))"
1.1094 +                                        pair_fm(2,0,1)))))))"
1.1095
1.1096  lemma pre_image_type [TC]:
1.1097       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pre_image_fm(x,y,z) \<in> formula"
1.1100
1.1101  lemma arity_pre_image_fm [simp]:
1.1102 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1103 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1104        ==> arity(pre_image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.1105 -by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1106 +by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1107
1.1108  lemma sats_pre_image_fm [simp]:
1.1109     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.1110 -    ==> sats(A, pre_image_fm(x,y,z), env) <->
1.1111 +    ==> sats(A, pre_image_fm(x,y,z), env) <->
1.1112          pre_image(**A, nth(x,env), nth(y,env), nth(z,env))"
1.1113  by (simp add: pre_image_fm_def Relative.pre_image_def)
1.1114
1.1115  lemma pre_image_iff_sats:
1.1116 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1117 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1118            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.1119         ==> pre_image(**A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)"
1.1121
1.1122  theorem pre_image_reflection:
1.1123 -     "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)),
1.1124 +     "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)),
1.1125                 \<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]"
1.1126  apply (simp only: Relative.pre_image_def setclass_simps)
1.1127 -apply (intro FOL_reflections pair_reflection)
1.1128 +apply (intro FOL_reflections pair_reflection)
1.1129  done
1.1130
1.1131
1.1132  subsubsection{*Function Application, Internalized*}
1.1133
1.1134 -(* "fun_apply(M,f,x,y) ==
1.1135 -        (\<exists>xs[M]. \<exists>fxs[M].
1.1136 +(* "fun_apply(M,f,x,y) ==
1.1137 +        (\<exists>xs[M]. \<exists>fxs[M].
1.1138           upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *)
1.1139  constdefs fun_apply_fm :: "[i,i,i]=>i"
1.1140 -    "fun_apply_fm(f,x,y) ==
1.1141 +    "fun_apply_fm(f,x,y) ==
1.1142         Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1),
1.1143 -                         And(image_fm(succ(succ(f)), 1, 0),
1.1144 +                         And(image_fm(succ(succ(f)), 1, 0),
1.1145                               big_union_fm(0,succ(succ(y)))))))"
1.1146
1.1147  lemma fun_apply_type [TC]:
1.1148       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
1.1151
1.1152  lemma arity_fun_apply_fm [simp]:
1.1153 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1154 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1155        ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.1156 -by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1157 +by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1158
1.1159  lemma sats_fun_apply_fm [simp]:
1.1160     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.1161 -    ==> sats(A, fun_apply_fm(x,y,z), env) <->
1.1162 +    ==> sats(A, fun_apply_fm(x,y,z), env) <->
1.1163          fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
1.1164  by (simp add: fun_apply_fm_def fun_apply_def)
1.1165
1.1166  lemma fun_apply_iff_sats:
1.1167 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1168 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1169            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.1170         ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
1.1171  by simp
1.1172
1.1173  theorem fun_apply_reflection:
1.1174 -     "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
1.1175 -               \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
1.1176 +     "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
1.1177 +               \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
1.1178  apply (simp only: fun_apply_def setclass_simps)
1.1179  apply (intro FOL_reflections upair_reflection image_reflection
1.1180 -             big_union_reflection)
1.1181 +             big_union_reflection)
1.1182  done
1.1183
1.1184
1.1185  subsubsection{*The Concept of Relation, Internalized*}
1.1186
1.1187 -(* "is_relation(M,r) ==
1.1188 +(* "is_relation(M,r) ==
1.1189          (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *)
1.1190  constdefs relation_fm :: "i=>i"
1.1191 -    "relation_fm(r) ==
1.1192 +    "relation_fm(r) ==
1.1193         Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))"
1.1194
1.1195  lemma relation_type [TC]:
1.1196       "[| x \<in> nat |] ==> relation_fm(x) \<in> formula"
1.1199
1.1200  lemma arity_relation_fm [simp]:
1.1201       "x \<in> nat ==> arity(relation_fm(x)) = succ(x)"
1.1202 -by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1203 +by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1204
1.1205  lemma sats_relation_fm [simp]:
1.1206     "[| x \<in> nat; env \<in> list(A)|]
1.1207 @@ -984,26 +1023,26 @@
1.1208  by (simp add: relation_fm_def is_relation_def)
1.1209
1.1210  lemma relation_iff_sats:
1.1211 -      "[| nth(i,env) = x; nth(j,env) = y;
1.1212 +      "[| nth(i,env) = x; nth(j,env) = y;
1.1213            i \<in> nat; env \<in> list(A)|]
1.1214         ==> is_relation(**A, x) <-> sats(A, relation_fm(i), env)"
1.1215  by simp
1.1216
1.1217  theorem is_relation_reflection:
1.1218 -     "REFLECTS[\<lambda>x. is_relation(L,f(x)),
1.1219 +     "REFLECTS[\<lambda>x. is_relation(L,f(x)),
1.1220                 \<lambda>i x. is_relation(**Lset(i),f(x))]"
1.1221  apply (simp only: is_relation_def setclass_simps)
1.1222 -apply (intro FOL_reflections pair_reflection)
1.1223 +apply (intro FOL_reflections pair_reflection)
1.1224  done
1.1225
1.1226
1.1227  subsubsection{*The Concept of Function, Internalized*}
1.1228
1.1229 -(* "is_function(M,r) ==
1.1230 -	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
1.1231 +(* "is_function(M,r) ==
1.1232 +        \<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
1.1233             pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'" *)
1.1234  constdefs function_fm :: "i=>i"
1.1235 -    "function_fm(r) ==
1.1236 +    "function_fm(r) ==
1.1237         Forall(Forall(Forall(Forall(Forall(
1.1238           Implies(pair_fm(4,3,1),
1.1239                   Implies(pair_fm(4,2,0),
1.1240 @@ -1012,11 +1051,11 @@
1.1241
1.1242  lemma function_type [TC]:
1.1243       "[| x \<in> nat |] ==> function_fm(x) \<in> formula"
1.1246
1.1247  lemma arity_function_fm [simp]:
1.1248       "x \<in> nat ==> arity(function_fm(x)) = succ(x)"
1.1249 -by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1250 +by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1251
1.1252  lemma sats_function_fm [simp]:
1.1253     "[| x \<in> nat; env \<in> list(A)|]
1.1254 @@ -1024,27 +1063,27 @@
1.1255  by (simp add: function_fm_def is_function_def)
1.1256
1.1257  lemma function_iff_sats:
1.1258 -      "[| nth(i,env) = x; nth(j,env) = y;
1.1259 +      "[| nth(i,env) = x; nth(j,env) = y;
1.1260            i \<in> nat; env \<in> list(A)|]
1.1261         ==> is_function(**A, x) <-> sats(A, function_fm(i), env)"
1.1262  by simp
1.1263
1.1264  theorem is_function_reflection:
1.1265 -     "REFLECTS[\<lambda>x. is_function(L,f(x)),
1.1266 +     "REFLECTS[\<lambda>x. is_function(L,f(x)),
1.1267                 \<lambda>i x. is_function(**Lset(i),f(x))]"
1.1268  apply (simp only: is_function_def setclass_simps)
1.1269 -apply (intro FOL_reflections pair_reflection)
1.1270 +apply (intro FOL_reflections pair_reflection)
1.1271  done
1.1272
1.1273
1.1274  subsubsection{*Typed Functions, Internalized*}
1.1275
1.1276 -(* "typed_function(M,A,B,r) ==
1.1277 +(* "typed_function(M,A,B,r) ==
1.1278          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
1.1279          (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))" *)
1.1280
1.1281  constdefs typed_function_fm :: "[i,i,i]=>i"
1.1282 -    "typed_function_fm(A,B,r) ==
1.1283 +    "typed_function_fm(A,B,r) ==
1.1284         And(function_fm(r),
1.1285           And(relation_fm(r),
1.1286             And(domain_fm(r,A),
1.1287 @@ -1053,64 +1092,64 @@
1.1288
1.1289  lemma typed_function_type [TC]:
1.1290       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> typed_function_fm(x,y,z) \<in> formula"
1.1293
1.1294  lemma arity_typed_function_fm [simp]:
1.1295 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1296 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1297        ==> arity(typed_function_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.1298 -by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1299 +by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1300
1.1301  lemma sats_typed_function_fm [simp]:
1.1302     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.1303 -    ==> sats(A, typed_function_fm(x,y,z), env) <->
1.1304 +    ==> sats(A, typed_function_fm(x,y,z), env) <->
1.1305          typed_function(**A, nth(x,env), nth(y,env), nth(z,env))"
1.1306  by (simp add: typed_function_fm_def typed_function_def)
1.1307
1.1308  lemma typed_function_iff_sats:
1.1309 -  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1310 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1311        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.1312     ==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)"
1.1313  by simp
1.1314
1.1315 -lemmas function_reflections =
1.1316 +lemmas function_reflections =
1.1317          empty_reflection number1_reflection
1.1318 -	upair_reflection pair_reflection union_reflection
1.1319 -	big_union_reflection cons_reflection successor_reflection
1.1320 +        upair_reflection pair_reflection union_reflection
1.1321 +        big_union_reflection cons_reflection successor_reflection
1.1322          fun_apply_reflection subset_reflection
1.1323 -	transitive_set_reflection membership_reflection
1.1324 -	pred_set_reflection domain_reflection range_reflection field_reflection
1.1325 +        transitive_set_reflection membership_reflection
1.1326 +        pred_set_reflection domain_reflection range_reflection field_reflection
1.1327          image_reflection pre_image_reflection
1.1328 -	is_relation_reflection is_function_reflection
1.1329 +        is_relation_reflection is_function_reflection
1.1330
1.1331 -lemmas function_iff_sats =
1.1332 -        empty_iff_sats number1_iff_sats
1.1333 -	upair_iff_sats pair_iff_sats union_iff_sats
1.1334 -	cons_iff_sats successor_iff_sats
1.1335 +lemmas function_iff_sats =
1.1336 +        empty_iff_sats number1_iff_sats
1.1337 +        upair_iff_sats pair_iff_sats union_iff_sats
1.1338 +        cons_iff_sats successor_iff_sats
1.1339          fun_apply_iff_sats  Memrel_iff_sats
1.1340 -	pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
1.1341 -        image_iff_sats pre_image_iff_sats
1.1342 -	relation_iff_sats function_iff_sats
1.1343 +        pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
1.1344 +        image_iff_sats pre_image_iff_sats
1.1345 +        relation_iff_sats function_iff_sats
1.1346
1.1347
1.1348  theorem typed_function_reflection:
1.1349 -     "REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)),
1.1350 +     "REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)),
1.1351                 \<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]"
1.1352  apply (simp only: typed_function_def setclass_simps)
1.1353 -apply (intro FOL_reflections function_reflections)
1.1354 +apply (intro FOL_reflections function_reflections)
1.1355  done
1.1356
1.1357
1.1358  subsubsection{*Composition of Relations, Internalized*}
1.1359
1.1360 -(* "composition(M,r,s,t) ==
1.1361 -        \<forall>p[M]. p \<in> t <->
1.1362 -               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
1.1363 -                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
1.1364 +(* "composition(M,r,s,t) ==
1.1365 +        \<forall>p[M]. p \<in> t <->
1.1366 +               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
1.1367 +                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
1.1368                  xy \<in> s & yz \<in> r)" *)
1.1369  constdefs composition_fm :: "[i,i,i]=>i"
1.1370 -  "composition_fm(r,s,t) ==
1.1371 +  "composition_fm(r,s,t) ==
1.1372       Forall(Iff(Member(0,succ(t)),
1.1373 -             Exists(Exists(Exists(Exists(Exists(
1.1374 +             Exists(Exists(Exists(Exists(Exists(
1.1375                And(pair_fm(4,2,5),
1.1376                 And(pair_fm(4,3,1),
1.1377                  And(pair_fm(3,2,0),
1.1378 @@ -1118,41 +1157,41 @@
1.1379
1.1380  lemma composition_type [TC]:
1.1381       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> composition_fm(x,y,z) \<in> formula"
1.1384
1.1385  lemma arity_composition_fm [simp]:
1.1386 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1387 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1388        ==> arity(composition_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.1389 -by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1390 +by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1391
1.1392  lemma sats_composition_fm [simp]:
1.1393     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.1394 -    ==> sats(A, composition_fm(x,y,z), env) <->
1.1395 +    ==> sats(A, composition_fm(x,y,z), env) <->
1.1396          composition(**A, nth(x,env), nth(y,env), nth(z,env))"
1.1397  by (simp add: composition_fm_def composition_def)
1.1398
1.1399  lemma composition_iff_sats:
1.1400 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1401 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1402            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.1403         ==> composition(**A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)"
1.1404  by simp
1.1405
1.1406  theorem composition_reflection:
1.1407 -     "REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)),
1.1408 +     "REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)),
1.1409                 \<lambda>i x. composition(**Lset(i),f(x),g(x),h(x))]"
1.1410  apply (simp only: composition_def setclass_simps)
1.1411 -apply (intro FOL_reflections pair_reflection)
1.1412 +apply (intro FOL_reflections pair_reflection)
1.1413  done
1.1414
1.1415
1.1416  subsubsection{*Injections, Internalized*}
1.1417
1.1418 -(* "injection(M,A,B,f) ==
1.1419 -	typed_function(M,A,B,f) &
1.1420 -        (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
1.1421 +(* "injection(M,A,B,f) ==
1.1422 +        typed_function(M,A,B,f) &
1.1423 +        (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
1.1424            pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')" *)
1.1425  constdefs injection_fm :: "[i,i,i]=>i"
1.1426 - "injection_fm(A,B,f) ==
1.1427 + "injection_fm(A,B,f) ==
1.1428      And(typed_function_fm(A,B,f),
1.1429         Forall(Forall(Forall(Forall(Forall(
1.1430           Implies(pair_fm(4,2,1),
1.1431 @@ -1163,41 +1202,41 @@
1.1432
1.1433  lemma injection_type [TC]:
1.1434       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> injection_fm(x,y,z) \<in> formula"
1.1437
1.1438  lemma arity_injection_fm [simp]:
1.1439 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1440 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1441        ==> arity(injection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.1442 -by (simp add: injection_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1443 +by (simp add: injection_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1444
1.1445  lemma sats_injection_fm [simp]:
1.1446     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.1447 -    ==> sats(A, injection_fm(x,y,z), env) <->
1.1448 +    ==> sats(A, injection_fm(x,y,z), env) <->
1.1449          injection(**A, nth(x,env), nth(y,env), nth(z,env))"
1.1450  by (simp add: injection_fm_def injection_def)
1.1451
1.1452  lemma injection_iff_sats:
1.1453 -  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1454 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1455        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.1456     ==> injection(**A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)"
1.1457  by simp
1.1458
1.1459  theorem injection_reflection:
1.1460 -     "REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)),
1.1461 +     "REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)),
1.1462                 \<lambda>i x. injection(**Lset(i),f(x),g(x),h(x))]"
1.1463  apply (simp only: injection_def setclass_simps)
1.1464 -apply (intro FOL_reflections function_reflections typed_function_reflection)
1.1465 +apply (intro FOL_reflections function_reflections typed_function_reflection)
1.1466  done
1.1467
1.1468
1.1469  subsubsection{*Surjections, Internalized*}
1.1470
1.1471  (*  surjection :: "[i=>o,i,i,i] => o"
1.1472 -    "surjection(M,A,B,f) ==
1.1473 +    "surjection(M,A,B,f) ==
1.1474          typed_function(M,A,B,f) &
1.1475          (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))" *)
1.1476  constdefs surjection_fm :: "[i,i,i]=>i"
1.1477 - "surjection_fm(A,B,f) ==
1.1478 + "surjection_fm(A,B,f) ==
1.1479      And(typed_function_fm(A,B,f),
1.1480         Forall(Implies(Member(0,succ(B)),
1.1481                        Exists(And(Member(0,succ(succ(A))),
1.1482 @@ -1205,30 +1244,30 @@
1.1483
1.1484  lemma surjection_type [TC]:
1.1485       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> surjection_fm(x,y,z) \<in> formula"
1.1488
1.1489  lemma arity_surjection_fm [simp]:
1.1490 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1491 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1492        ==> arity(surjection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.1493 -by (simp add: surjection_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1494 +by (simp add: surjection_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1495
1.1496  lemma sats_surjection_fm [simp]:
1.1497     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.1498 -    ==> sats(A, surjection_fm(x,y,z), env) <->
1.1499 +    ==> sats(A, surjection_fm(x,y,z), env) <->
1.1500          surjection(**A, nth(x,env), nth(y,env), nth(z,env))"
1.1501  by (simp add: surjection_fm_def surjection_def)
1.1502
1.1503  lemma surjection_iff_sats:
1.1504 -  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1505 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1506        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.1507     ==> surjection(**A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)"
1.1508  by simp
1.1509
1.1510  theorem surjection_reflection:
1.1511 -     "REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)),
1.1512 +     "REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)),
1.1513                 \<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x))]"
1.1514  apply (simp only: surjection_def setclass_simps)
1.1515 -apply (intro FOL_reflections function_reflections typed_function_reflection)
1.1516 +apply (intro FOL_reflections function_reflections typed_function_reflection)
1.1517  done
1.1518
1.1519
1.1520 @@ -1242,40 +1281,40 @@
1.1521
1.1522  lemma bijection_type [TC]:
1.1523       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> bijection_fm(x,y,z) \<in> formula"
1.1526
1.1527  lemma arity_bijection_fm [simp]:
1.1528 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1529 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1530        ==> arity(bijection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.1531 -by (simp add: bijection_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1532 +by (simp add: bijection_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1533
1.1534  lemma sats_bijection_fm [simp]:
1.1535     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.1536 -    ==> sats(A, bijection_fm(x,y,z), env) <->
1.1537 +    ==> sats(A, bijection_fm(x,y,z), env) <->
1.1538          bijection(**A, nth(x,env), nth(y,env), nth(z,env))"
1.1539  by (simp add: bijection_fm_def bijection_def)
1.1540
1.1541  lemma bijection_iff_sats:
1.1542 -  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1543 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1544        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.1545     ==> bijection(**A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)"
1.1546  by simp
1.1547
1.1548  theorem bijection_reflection:
1.1549 -     "REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)),
1.1550 +     "REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)),
1.1551                 \<lambda>i x. bijection(**Lset(i),f(x),g(x),h(x))]"
1.1552  apply (simp only: bijection_def setclass_simps)
1.1553 -apply (intro And_reflection injection_reflection surjection_reflection)
1.1554 +apply (intro And_reflection injection_reflection surjection_reflection)
1.1555  done
1.1556
1.1557
1.1558  subsubsection{*Restriction of a Relation, Internalized*}
1.1559
1.1560
1.1561 -(* "restriction(M,r,A,z) ==
1.1562 -	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" *)
1.1563 +(* "restriction(M,r,A,z) ==
1.1564 +        \<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" *)
1.1565  constdefs restriction_fm :: "[i,i,i]=>i"
1.1566 -    "restriction_fm(r,A,z) ==
1.1567 +    "restriction_fm(r,A,z) ==
1.1568         Forall(Iff(Member(0,succ(z)),
1.1569                    And(Member(0,succ(r)),
1.1570                        Exists(And(Member(0,succ(succ(A))),
1.1571 @@ -1283,111 +1322,111 @@
1.1572
1.1573  lemma restriction_type [TC]:
1.1574       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> restriction_fm(x,y,z) \<in> formula"
1.1577
1.1578  lemma arity_restriction_fm [simp]:
1.1579 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1580 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.1581        ==> arity(restriction_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.1582 -by (simp add: restriction_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1583 +by (simp add: restriction_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1584
1.1585  lemma sats_restriction_fm [simp]:
1.1586     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.1587 -    ==> sats(A, restriction_fm(x,y,z), env) <->
1.1588 +    ==> sats(A, restriction_fm(x,y,z), env) <->
1.1589          restriction(**A, nth(x,env), nth(y,env), nth(z,env))"
1.1590  by (simp add: restriction_fm_def restriction_def)
1.1591
1.1592  lemma restriction_iff_sats:
1.1593 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1594 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.1595            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.1596         ==> restriction(**A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)"
1.1597  by simp
1.1598
1.1599  theorem restriction_reflection:
1.1600 -     "REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)),
1.1601 +     "REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)),
1.1602                 \<lambda>i x. restriction(**Lset(i),f(x),g(x),h(x))]"
1.1603  apply (simp only: restriction_def setclass_simps)
1.1604 -apply (intro FOL_reflections pair_reflection)
1.1605 +apply (intro FOL_reflections pair_reflection)
1.1606  done
1.1607
1.1608  subsubsection{*Order-Isomorphisms, Internalized*}
1.1609
1.1610  (*  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
1.1611 -   "order_isomorphism(M,A,r,B,s,f) ==
1.1612 -        bijection(M,A,B,f) &
1.1613 +   "order_isomorphism(M,A,r,B,s,f) ==
1.1614 +        bijection(M,A,B,f) &
1.1615          (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
1.1616            (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
1.1617 -            pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->
1.1618 +            pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->
1.1619              pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
1.1620    *)
1.1621
1.1622  constdefs order_isomorphism_fm :: "[i,i,i,i,i]=>i"
1.1623 - "order_isomorphism_fm(A,r,B,s,f) ==
1.1624 -   And(bijection_fm(A,B,f),
1.1625 + "order_isomorphism_fm(A,r,B,s,f) ==
1.1626 +   And(bijection_fm(A,B,f),
1.1627       Forall(Implies(Member(0,succ(A)),
1.1628         Forall(Implies(Member(0,succ(succ(A))),
1.1629           Forall(Forall(Forall(Forall(
1.1630             Implies(pair_fm(5,4,3),
1.1631               Implies(fun_apply_fm(f#+6,5,2),
1.1632                 Implies(fun_apply_fm(f#+6,4,1),
1.1633 -                 Implies(pair_fm(2,1,0),
1.1634 +                 Implies(pair_fm(2,1,0),
1.1635                     Iff(Member(3,r#+6), Member(0,s#+6)))))))))))))))"
1.1636
1.1637  lemma order_isomorphism_type [TC]:
1.1638 -     "[| A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
1.1639 +     "[| A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
1.1640        ==> order_isomorphism_fm(A,r,B,s,f) \<in> formula"
1.1643
1.1644  lemma arity_order_isomorphism_fm [simp]:
1.1645 -     "[| A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
1.1646 -      ==> arity(order_isomorphism_fm(A,r,B,s,f)) =
1.1647 -          succ(A) \<union> succ(r) \<union> succ(B) \<union> succ(s) \<union> succ(f)"
1.1648 -by (simp add: order_isomorphism_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1649 +     "[| A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
1.1650 +      ==> arity(order_isomorphism_fm(A,r,B,s,f)) =
1.1651 +          succ(A) \<union> succ(r) \<union> succ(B) \<union> succ(s) \<union> succ(f)"
1.1652 +by (simp add: order_isomorphism_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1653
1.1654  lemma sats_order_isomorphism_fm [simp]:
1.1655     "[| U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)|]
1.1656 -    ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <->
1.1657 -        order_isomorphism(**A, nth(U,env), nth(r,env), nth(B,env),
1.1658 +    ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <->
1.1659 +        order_isomorphism(**A, nth(U,env), nth(r,env), nth(B,env),
1.1660                                 nth(s,env), nth(f,env))"
1.1661  by (simp add: order_isomorphism_fm_def order_isomorphism_def)
1.1662
1.1663  lemma order_isomorphism_iff_sats:
1.1664 -  "[| nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s;
1.1665 -      nth(k',env) = f;
1.1666 +  "[| nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s;
1.1667 +      nth(k',env) = f;
1.1668        i \<in> nat; j \<in> nat; k \<in> nat; j' \<in> nat; k' \<in> nat; env \<in> list(A)|]
1.1669 -   ==> order_isomorphism(**A,U,r,B,s,f) <->
1.1670 -       sats(A, order_isomorphism_fm(i,j,k,j',k'), env)"
1.1671 +   ==> order_isomorphism(**A,U,r,B,s,f) <->
1.1672 +       sats(A, order_isomorphism_fm(i,j,k,j',k'), env)"
1.1673  by simp
1.1674
1.1675  theorem order_isomorphism_reflection:
1.1676 -     "REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
1.1677 +     "REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
1.1678                 \<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
1.1679  apply (simp only: order_isomorphism_def setclass_simps)
1.1680 -apply (intro FOL_reflections function_reflections bijection_reflection)
1.1681 +apply (intro FOL_reflections function_reflections bijection_reflection)
1.1682  done
1.1683
1.1684  subsubsection{*Limit Ordinals, Internalized*}
1.1685
1.1686  text{*A limit ordinal is a non-empty, successor-closed ordinal*}
1.1687
1.1688 -(* "limit_ordinal(M,a) ==
1.1689 -	ordinal(M,a) & ~ empty(M,a) &
1.1690 +(* "limit_ordinal(M,a) ==
1.1691 +        ordinal(M,a) & ~ empty(M,a) &
1.1692          (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))" *)
1.1693
1.1694  constdefs limit_ordinal_fm :: "i=>i"
1.1695 -    "limit_ordinal_fm(x) ==
1.1696 +    "limit_ordinal_fm(x) ==
1.1697          And(ordinal_fm(x),
1.1698              And(Neg(empty_fm(x)),
1.1699 -	        Forall(Implies(Member(0,succ(x)),
1.1700 +                Forall(Implies(Member(0,succ(x)),
1.1701                                 Exists(And(Member(0,succ(succ(x))),
1.1702                                            succ_fm(1,0)))))))"
1.1703
1.1704  lemma limit_ordinal_type [TC]:
1.1705       "x \<in> nat ==> limit_ordinal_fm(x) \<in> formula"
1.1708
1.1709  lemma arity_limit_ordinal_fm [simp]:
1.1710       "x \<in> nat ==> arity(limit_ordinal_fm(x)) = succ(x)"
1.1711 -by (simp add: limit_ordinal_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1712 +by (simp add: limit_ordinal_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1713
1.1714  lemma sats_limit_ordinal_fm [simp]:
1.1715     "[| x \<in> nat; env \<in> list(A)|]
1.1716 @@ -1395,35 +1434,35 @@
1.1717  by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm')
1.1718
1.1719  lemma limit_ordinal_iff_sats:
1.1720 -      "[| nth(i,env) = x; nth(j,env) = y;
1.1721 +      "[| nth(i,env) = x; nth(j,env) = y;
1.1722            i \<in> nat; env \<in> list(A)|]
1.1723         ==> limit_ordinal(**A, x) <-> sats(A, limit_ordinal_fm(i), env)"
1.1724  by simp
1.1725
1.1726  theorem limit_ordinal_reflection:
1.1727 -     "REFLECTS[\<lambda>x. limit_ordinal(L,f(x)),
1.1728 +     "REFLECTS[\<lambda>x. limit_ordinal(L,f(x)),
1.1729                 \<lambda>i x. limit_ordinal(**Lset(i),f(x))]"
1.1730  apply (simp only: limit_ordinal_def setclass_simps)
1.1731 -apply (intro FOL_reflections ordinal_reflection
1.1732 -             empty_reflection successor_reflection)
1.1733 +apply (intro FOL_reflections ordinal_reflection
1.1734 +             empty_reflection successor_reflection)
1.1735  done
1.1736
1.1737  subsubsection{*Omega: The Set of Natural Numbers*}
1.1738
1.1739  (* omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x)) *)
1.1740  constdefs omega_fm :: "i=>i"
1.1741 -    "omega_fm(x) ==
1.1742 +    "omega_fm(x) ==
1.1743         And(limit_ordinal_fm(x),
1.1744             Forall(Implies(Member(0,succ(x)),
1.1745                            Neg(limit_ordinal_fm(0)))))"
1.1746
1.1747  lemma omega_type [TC]:
1.1748       "x \<in> nat ==> omega_fm(x) \<in> formula"
1.1751
1.1752  lemma arity_omega_fm [simp]:
1.1753       "x \<in> nat ==> arity(omega_fm(x)) = succ(x)"
1.1754 -by (simp add: omega_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1755 +by (simp add: omega_fm_def succ_Un_distrib [symmetric] Un_ac)
1.1756
1.1757  lemma sats_omega_fm [simp]:
1.1758     "[| x \<in> nat; env \<in> list(A)|]
1.1759 @@ -1431,16 +1470,16 @@
1.1760  by (simp add: omega_fm_def omega_def)
1.1761
1.1762  lemma omega_iff_sats:
1.1763 -      "[| nth(i,env) = x; nth(j,env) = y;
1.1764 +      "[| nth(i,env) = x; nth(j,env) = y;
1.1765            i \<in> nat; env \<in> list(A)|]
1.1766         ==> omega(**A, x) <-> sats(A, omega_fm(i), env)"
1.1767  by simp
1.1768
1.1769  theorem omega_reflection:
1.1770 -     "REFLECTS[\<lambda>x. omega(L,f(x)),
1.1771 +     "REFLECTS[\<lambda>x. omega(L,f(x)),
1.1772                 \<lambda>i x. omega(**Lset(i),f(x))]"
1.1773  apply (simp only: omega_def setclass_simps)
1.1774 -apply (intro FOL_reflections limit_ordinal_reflection)
1.1775 +apply (intro FOL_reflections limit_ordinal_reflection)
1.1776  done
1.1777
1.1778
1.1779 @@ -1451,10 +1490,10 @@
1.1780          order_isomorphism_reflection
1.1781          ordinal_reflection limit_ordinal_reflection omega_reflection
1.1782
1.1783 -lemmas fun_plus_iff_sats =
1.1784 -	typed_function_iff_sats composition_iff_sats
1.1785 -        injection_iff_sats surjection_iff_sats
1.1786 -        bijection_iff_sats restriction_iff_sats
1.1787 +lemmas fun_plus_iff_sats =
1.1788 +        typed_function_iff_sats composition_iff_sats
1.1789 +        injection_iff_sats surjection_iff_sats
1.1790 +        bijection_iff_sats restriction_iff_sats
1.1791          order_isomorphism_iff_sats
1.1792          ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats
1.1793
```
```     2.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Mon Jul 29 00:57:16 2002 +0200
2.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Jul 29 18:07:53 2002 +0200
2.3 @@ -1,4 +1,5 @@
2.5 +
2.7
2.8  theory Rec_Separation = Separation + Datatype_absolute:
2.9
2.10 @@ -198,19 +199,14 @@
2.11
2.12  subsubsection{*Instantiating the locale @{text M_trancl}*}
2.13
2.14 -theorem M_trancl_axioms_L: "M_trancl_axioms(L)"
2.15 +theorem M_trancl_L: "PROP M_trancl(L)"
2.16 +  apply (rule M_trancl.intro)
2.17 +    apply (rule M_axioms.axioms [OF M_axioms_L])+
2.18    apply (rule M_trancl_axioms.intro)
2.19     apply (assumption | rule
2.20       rtrancl_separation wellfounded_trancl_separation)+
2.21    done
2.22
2.23 -theorem M_trancl_L: "PROP M_trancl(L)"
2.24 -  apply (rule M_trancl.intro)
2.25 -    apply (rule M_triv_axioms_L)
2.26 -   apply (rule M_axioms_axioms_L)
2.27 -  apply (rule M_trancl_axioms_L)
2.28 -  done
2.29 -
2.30  lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
2.31    and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
2.32    and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L]
2.33 @@ -438,18 +434,12 @@
2.34
2.35  subsubsection{*Instantiating the locale @{text M_wfrank}*}
2.36
2.37 -theorem M_wfrank_axioms_L: "M_wfrank_axioms(L)"
2.38 -  apply (rule M_wfrank_axioms.intro)
2.39 -  apply (assumption | rule
2.40 -    wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
2.41 -  done
2.42 -
2.43  theorem M_wfrank_L: "PROP M_wfrank(L)"
2.44    apply (rule M_wfrank.intro)
2.45 -     apply (rule M_triv_axioms_L)
2.46 -    apply (rule M_axioms_axioms_L)
2.47 -   apply (rule M_trancl_axioms_L)
2.48 -  apply (rule M_wfrank_axioms_L)
2.49 +     apply (rule M_trancl.axioms [OF M_trancl_L])+
2.50 +  apply (rule M_wfrank_axioms.intro)
2.51 +   apply (assumption | rule
2.52 +     wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
2.53    done
2.54
2.55  lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L]
2.56 @@ -1224,7 +1214,9 @@
2.57
2.58  subsubsection{*Instantiating the locale @{text M_datatypes}*}
2.59
2.60 -theorem M_datatypes_axioms_L: "M_datatypes_axioms(L)"
2.61 +theorem M_datatypes_L: "PROP M_datatypes(L)"
2.62 +  apply (rule M_datatypes.intro)
2.63 +      apply (rule M_wfrank.axioms [OF M_wfrank_L])+
2.64    apply (rule M_datatypes_axioms.intro)
2.65        apply (assumption | rule
2.66          list_replacement1 list_replacement2
2.67 @@ -1232,15 +1224,6 @@
2.68          nth_replacement)+
2.69    done
2.70
2.71 -theorem M_datatypes_L: "PROP M_datatypes(L)"
2.72 -  apply (rule M_datatypes.intro)
2.73 -      apply (rule M_triv_axioms_L)
2.74 -     apply (rule M_axioms_axioms_L)
2.75 -    apply (rule M_trancl_axioms_L)
2.76 -   apply (rule M_wfrank_axioms_L)
2.77 -  apply (rule M_datatypes_axioms_L)
2.78 -  done
2.79 -
2.80  lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
2.81    and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L]
2.82    and list_abs = M_datatypes.list_abs [OF M_datatypes_L]
2.83 @@ -1338,19 +1321,11 @@
2.84
2.85  subsubsection{*Instantiating the locale @{text M_eclose}*}
2.86
2.87 -theorem M_eclose_axioms_L: "M_eclose_axioms(L)"
2.88 -  apply (rule M_eclose_axioms.intro)
2.89 -   apply (assumption | rule eclose_replacement1 eclose_replacement2)+
2.90 -  done
2.91 -
2.92  theorem M_eclose_L: "PROP M_eclose(L)"
2.93    apply (rule M_eclose.intro)
2.94 -       apply (rule M_triv_axioms_L)
2.95 -      apply (rule M_axioms_axioms_L)
2.96 -     apply (rule M_trancl_axioms_L)
2.97 -    apply (rule M_wfrank_axioms_L)
2.98 -   apply (rule M_datatypes_axioms_L)
2.99 -  apply (rule M_eclose_axioms_L)
2.100 +       apply (rule M_datatypes.axioms [OF M_datatypes_L])+
2.101 +  apply (rule M_eclose_axioms.intro)
2.102 +   apply (assumption | rule eclose_replacement1 eclose_replacement2)+
2.103    done
2.104
2.105  lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]
```
```     3.1 --- a/src/ZF/Constructible/Separation.thy	Mon Jul 29 00:57:16 2002 +0200
3.2 +++ b/src/ZF/Constructible/Separation.thy	Mon Jul 29 18:07:53 2002 +0200
3.3 @@ -448,7 +448,9 @@
3.4  text{*Separation (and Strong Replacement) for basic set-theoretic constructions
3.5  such as intersection, Cartesian Product and image.*}
3.6
3.7 -theorem M_axioms_axioms_L: "M_axioms_axioms(L)"
3.8 +theorem M_axioms_L: "PROP M_axioms(L)"
3.9 +  apply (rule M_axioms.intro)
3.10 +   apply (rule M_triv_axioms_L)
3.11    apply (rule M_axioms_axioms.intro)
3.12                 apply (assumption | rule
3.13                   Inter_separation cartprod_separation image_separation
3.14 @@ -458,12 +460,6 @@
3.15                   obase_separation obase_equals_separation
3.16                   omap_replacement is_recfun_separation)+
3.17    done
3.18 -
3.19 -theorem M_axioms_L: "PROP M_axioms(L)"
3.20 -  apply (rule M_axioms.intro)
3.21 -   apply (rule M_triv_axioms_L)
3.22 -  apply (rule M_axioms_axioms_L)
3.23 -  done
3.24
3.25  lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L]
3.26    and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L]
3.27 @@ -570,35 +566,34 @@
3.28    and relativized_imp_well_ord = M_axioms.relativized_imp_well_ord [OF M_axioms_L]
3.29    and well_ord_abs = M_axioms.well_ord_abs [OF M_axioms_L]
3.30
3.31 -
3.32 -declare cartprod_closed [intro,simp]
3.33 -declare sum_closed [intro,simp]
3.34 -declare converse_closed [intro,simp]
3.35 +declare cartprod_closed [intro, simp]
3.36 +declare sum_closed [intro, simp]
3.37 +declare converse_closed [intro, simp]
3.38  declare converse_abs [simp]
3.39 -declare image_closed [intro,simp]
3.40 +declare image_closed [intro, simp]
3.41  declare vimage_abs [simp]
3.42 -declare vimage_closed [intro,simp]
3.43 +declare vimage_closed [intro, simp]
3.44  declare domain_abs [simp]
3.45 -declare domain_closed [intro,simp]
3.46 +declare domain_closed [intro, simp]
3.47  declare range_abs [simp]
3.48 -declare range_closed [intro,simp]
3.49 +declare range_closed [intro, simp]
3.50  declare field_abs [simp]
3.51 -declare field_closed [intro,simp]
3.52 +declare field_closed [intro, simp]
3.53  declare relation_abs [simp]
3.54  declare function_abs [simp]
3.55 -declare apply_closed [intro,simp]
3.56 +declare apply_closed [intro, simp]
3.57  declare typed_function_abs [simp]
3.58  declare injection_abs [simp]
3.59  declare surjection_abs [simp]
3.60  declare bijection_abs [simp]
3.61 -declare comp_closed [intro,simp]
3.62 +declare comp_closed [intro, simp]
3.63  declare composition_abs [simp]
3.64  declare restriction_abs [simp]
3.65 -declare restrict_closed [intro,simp]
3.66 +declare restrict_closed [intro, simp]
3.67  declare Inter_abs [simp]
3.68 -declare Inter_closed [intro,simp]
3.69 -declare Int_closed [intro,simp]
3.70 +declare Inter_closed [intro, simp]
3.71 +declare Int_closed [intro, simp]
3.72  declare is_funspace_abs [simp]
3.73 -declare finite_funspace_closed [intro,simp]
3.74 +declare finite_funspace_closed [intro, simp]
3.75
3.76  end
```