tuned;
authorwenzelm
Mon Jul 29 18:07:53 2002 +0200 (2002-07-29)
changeset 134292232810416fc
parent 13428 99e52e78eb65
child 13430 ab814c7685a9
tuned;
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Separation.thy
     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.20 -apply (simp add: L_def) 
    1.21 -apply (blast intro: zero_in_Lset) 
    1.22 +apply (simp add: L_def)
    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.29 -apply (simp_all add: doubleton_in_L) 
    1.30 +apply (rule_tac x="{x,y}" in rexI)
    1.31 +apply (simp_all add: doubleton_in_L)
    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.246 -apply (simp add: L_Reflects_def) 
   1.247 -apply (rule meta_exI) 
   1.248 -apply (rule Closed_Unbounded_Ord) 
   1.249 +apply (simp add: L_Reflects_def)
   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.393 -by (simp add: empty_fm_def) 
   1.394 +by (simp add: empty_fm_def)
   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.450 -by (simp add: upair_fm_def) 
   1.451 +by (simp add: upair_fm_def)
   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.472  by (simp add: sats_upair_fm)
   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.493  apply (simp add: upair_def)
   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.509 -by (simp add: pair_fm_def) 
   1.510 +by (simp add: pair_fm_def)
   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.531  by (simp add: sats_pair_fm)
   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.553 -by (simp add: union_fm_def) 
   1.554 +by (simp add: union_fm_def)
   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.575  by (simp add: sats_union_fm)
   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.598 -by (simp add: cons_fm_def) 
   1.599 +by (simp add: cons_fm_def)
   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.636 -by (simp add: succ_fm_def) 
   1.637 +by (simp add: succ_fm_def)
   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.643  by (simp add: succ_fm_def)
   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.673 -by (simp add: number1_fm_def) 
   1.674 +by (simp add: number1_fm_def)
   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.710 -by (simp add: big_union_fm_def) 
   1.711 +by (simp add: big_union_fm_def)
   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.798 -by (simp add: Memrel_fm_def) 
   1.799 +by (simp add: Memrel_fm_def)
   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.846 -by (simp add: pred_set_fm_def) 
   1.847 +by (simp add: pred_set_fm_def)
   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.868  by (simp add: sats_pred_set_fm)
   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.897 -by (simp add: domain_fm_def) 
   1.898 +by (simp add: domain_fm_def)
   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.946 -by (simp add: range_fm_def) 
   1.947 +by (simp add: range_fm_def)
   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.999 -by (simp add: field_fm_def) 
  1.1000 +by (simp add: field_fm_def)
  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.1047 -by (simp add: image_fm_def) 
  1.1048 +by (simp add: image_fm_def)
  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.1069  by (simp add: sats_image_fm)
  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.1098 -by (simp add: pre_image_fm_def) 
  1.1099 +by (simp add: pre_image_fm_def)
  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.1120  by (simp add: sats_pre_image_fm)
  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.1149 -by (simp add: fun_apply_fm_def) 
  1.1150 +by (simp add: fun_apply_fm_def)
  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.1197 -by (simp add: relation_fm_def) 
  1.1198 +by (simp add: relation_fm_def)
  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.1244 -by (simp add: function_fm_def) 
  1.1245 +by (simp add: function_fm_def)
  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.1291 -by (simp add: typed_function_fm_def) 
  1.1292 +by (simp add: typed_function_fm_def)
  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.1382 -by (simp add: composition_fm_def) 
  1.1383 +by (simp add: composition_fm_def)
  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.1435 -by (simp add: injection_fm_def) 
  1.1436 +by (simp add: injection_fm_def)
  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.1486 -by (simp add: surjection_fm_def) 
  1.1487 +by (simp add: surjection_fm_def)
  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.1524 -by (simp add: bijection_fm_def) 
  1.1525 +by (simp add: bijection_fm_def)
  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.1575 -by (simp add: restriction_fm_def) 
  1.1576 +by (simp add: restriction_fm_def)
  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.1641 -by (simp add: order_isomorphism_fm_def) 
  1.1642 +by (simp add: order_isomorphism_fm_def)
  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.1706 -by (simp add: limit_ordinal_fm_def) 
  1.1707 +by (simp add: limit_ordinal_fm_def)
  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.1749 -by (simp add: omega_fm_def) 
  1.1750 +by (simp add: omega_fm_def)
  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.4 -header{*Separation for Facts About Recursion*}
     2.5 +
     2.6 +header {*Separation for Facts About Recursion*}
     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