eliminate open locales and special ML code;
authorwenzelm
Mon Jul 29 00:57:16 2002 +0200 (2002-07-29)
changeset 1342899e52e78eb65
parent 13427 b429fd98549c
child 13429 2232810416fc
eliminate open locales and special ML code;
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Reflection.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Sun Jul 28 21:09:37 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Mon Jul 29 00:57:16 2002 +0200
     1.3 @@ -362,7 +362,7 @@
     1.4    is_formula :: "[i=>o,i] => o"
     1.5      "is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
     1.6  
     1.7 -locale (open) M_datatypes = M_wfrank +
     1.8 +locale M_datatypes = M_wfrank +
     1.9   assumes list_replacement1: 
    1.10     "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    1.11    and list_replacement2: 
    1.12 @@ -506,7 +506,7 @@
    1.13      "is_eclose(M,A,Z) == \<forall>u[M]. u \<in> Z <-> mem_eclose(M,A,u)"
    1.14  
    1.15  
    1.16 -locale (open) M_eclose = M_datatypes +
    1.17 +locale M_eclose = M_datatypes +
    1.18   assumes eclose_replacement1: 
    1.19     "M(A) ==> iterates_replacement(M, big_union(M), A)"
    1.20    and eclose_replacement2: 
     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Sun Jul 28 21:09:37 2002 +0200
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Mon Jul 29 00:57:16 2002 +0200
     2.3 @@ -75,110 +75,65 @@
     2.4  lemma Lset_cont: "cont_Ord(Lset)"
     2.5  by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord) 
     2.6  
     2.7 -lemmas Pair_in_Lset = Formula.Pair_in_LLimit;
     2.8 +lemmas Pair_in_Lset = Formula.Pair_in_LLimit
     2.9  
    2.10 -lemmas L_nat = Ord_in_L [OF Ord_nat];
    2.11 +lemmas L_nat = Ord_in_L [OF Ord_nat]
    2.12  
    2.13 -ML
    2.14 -{*
    2.15 -val transL = thm "transL";
    2.16 -val nonempty = thm "nonempty";
    2.17 -val upair_ax = thm "upair_ax";
    2.18 -val Union_ax = thm "Union_ax";
    2.19 -val power_ax = thm "power_ax";
    2.20 -val replacement = thm "replacement";
    2.21 -val L_nat = thm "L_nat";
    2.22 -
    2.23 -fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st);
    2.24 -
    2.25 -fun triv_axioms_L th =
    2.26 -    kill_flex_triv_prems 
    2.27 -       ([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat] 
    2.28 -        MRS (inst "M" "L" th));
    2.29 +theorem M_triv_axioms_L: "PROP M_triv_axioms(L)"
    2.30 +  apply (rule M_triv_axioms.intro)
    2.31 +        apply (erule (1) transL)
    2.32 +       apply (rule nonempty)
    2.33 +      apply (rule upair_ax)
    2.34 +     apply (rule Union_ax)
    2.35 +    apply (rule power_ax)
    2.36 +   apply (rule replacement)
    2.37 +  apply (rule L_nat)
    2.38 +  done
    2.39  
    2.40 -bind_thm ("rall_abs", triv_axioms_L (thm "M_triv_axioms.rall_abs"));
    2.41 -bind_thm ("rex_abs", triv_axioms_L (thm "M_triv_axioms.rex_abs"));
    2.42 -bind_thm ("ball_iff_equiv", triv_axioms_L (thm "M_triv_axioms.ball_iff_equiv"));
    2.43 -bind_thm ("M_equalityI", triv_axioms_L (thm "M_triv_axioms.M_equalityI"));
    2.44 -bind_thm ("empty_abs", triv_axioms_L (thm "M_triv_axioms.empty_abs"));
    2.45 -bind_thm ("subset_abs", triv_axioms_L (thm "M_triv_axioms.subset_abs"));
    2.46 -bind_thm ("upair_abs", triv_axioms_L (thm "M_triv_axioms.upair_abs"));
    2.47 -bind_thm ("upair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.upair_in_M_iff"));
    2.48 -bind_thm ("singleton_in_M_iff", triv_axioms_L (thm "M_triv_axioms.singleton_in_M_iff"));
    2.49 -bind_thm ("pair_abs", triv_axioms_L (thm "M_triv_axioms.pair_abs"));
    2.50 -bind_thm ("pair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.pair_in_M_iff"));
    2.51 -bind_thm ("pair_components_in_M", triv_axioms_L (thm "M_triv_axioms.pair_components_in_M"));
    2.52 -bind_thm ("cartprod_abs", triv_axioms_L (thm "M_triv_axioms.cartprod_abs"));
    2.53 -bind_thm ("union_abs", triv_axioms_L (thm "M_triv_axioms.union_abs"));
    2.54 -bind_thm ("inter_abs", triv_axioms_L (thm "M_triv_axioms.inter_abs"));
    2.55 -bind_thm ("setdiff_abs", triv_axioms_L (thm "M_triv_axioms.setdiff_abs"));
    2.56 -bind_thm ("Union_abs", triv_axioms_L (thm "M_triv_axioms.Union_abs"));
    2.57 -bind_thm ("Union_closed", triv_axioms_L (thm "M_triv_axioms.Union_closed"));
    2.58 -bind_thm ("Un_closed", triv_axioms_L (thm "M_triv_axioms.Un_closed"));
    2.59 -bind_thm ("cons_closed", triv_axioms_L (thm "M_triv_axioms.cons_closed"));
    2.60 -bind_thm ("successor_abs", triv_axioms_L (thm "M_triv_axioms.successor_abs"));
    2.61 -bind_thm ("succ_in_M_iff", triv_axioms_L (thm "M_triv_axioms.succ_in_M_iff"));
    2.62 -bind_thm ("separation_closed", triv_axioms_L (thm "M_triv_axioms.separation_closed"));
    2.63 -bind_thm ("strong_replacementI", triv_axioms_L (thm "M_triv_axioms.strong_replacementI"));
    2.64 -bind_thm ("strong_replacement_closed", triv_axioms_L (thm "M_triv_axioms.strong_replacement_closed"));
    2.65 -bind_thm ("RepFun_closed", triv_axioms_L (thm "M_triv_axioms.RepFun_closed"));
    2.66 -bind_thm ("lam_closed", triv_axioms_L (thm "M_triv_axioms.lam_closed"));
    2.67 -bind_thm ("image_abs", triv_axioms_L (thm "M_triv_axioms.image_abs"));
    2.68 -bind_thm ("powerset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_Pow"));
    2.69 -bind_thm ("powerset_imp_subset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_imp_subset_Pow"));
    2.70 -bind_thm ("nat_into_M", triv_axioms_L (thm "M_triv_axioms.nat_into_M"));
    2.71 -bind_thm ("nat_case_closed", triv_axioms_L (thm "M_triv_axioms.nat_case_closed"));
    2.72 -bind_thm ("Inl_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inl_in_M_iff"));
    2.73 -bind_thm ("Inr_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inr_in_M_iff"));
    2.74 -bind_thm ("lt_closed", triv_axioms_L (thm "M_triv_axioms.lt_closed"));
    2.75 -bind_thm ("transitive_set_abs", triv_axioms_L (thm "M_triv_axioms.transitive_set_abs"));
    2.76 -bind_thm ("ordinal_abs", triv_axioms_L (thm "M_triv_axioms.ordinal_abs"));
    2.77 -bind_thm ("limit_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.limit_ordinal_abs"));
    2.78 -bind_thm ("successor_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.successor_ordinal_abs"));
    2.79 -bind_thm ("finite_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.finite_ordinal_abs"));
    2.80 -bind_thm ("omega_abs", triv_axioms_L (thm "M_triv_axioms.omega_abs"));
    2.81 -bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs"));
    2.82 -bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs"));
    2.83 -bind_thm ("number3_abs", triv_axioms_L (thm "M_triv_axioms.number3_abs"));
    2.84 -*}
    2.85 -
    2.86 -declare rall_abs [simp] 
    2.87 -declare rex_abs [simp] 
    2.88 -declare empty_abs [simp] 
    2.89 -declare subset_abs [simp] 
    2.90 -declare upair_abs [simp] 
    2.91 -declare upair_in_M_iff [iff]
    2.92 -declare singleton_in_M_iff [iff]
    2.93 -declare pair_abs [simp] 
    2.94 -declare pair_in_M_iff [iff]
    2.95 -declare cartprod_abs [simp] 
    2.96 -declare union_abs [simp] 
    2.97 -declare inter_abs [simp] 
    2.98 -declare setdiff_abs [simp] 
    2.99 -declare Union_abs [simp] 
   2.100 -declare Union_closed [intro,simp]
   2.101 -declare Un_closed [intro,simp]
   2.102 -declare cons_closed [intro,simp]
   2.103 -declare successor_abs [simp] 
   2.104 -declare succ_in_M_iff [iff]
   2.105 -declare separation_closed [intro,simp]
   2.106 -declare strong_replacementI
   2.107 -declare strong_replacement_closed [intro,simp]
   2.108 -declare RepFun_closed [intro,simp]
   2.109 -declare lam_closed [intro,simp]
   2.110 -declare image_abs [simp] 
   2.111 -declare nat_into_M [intro]
   2.112 -declare Inl_in_M_iff [iff]
   2.113 -declare Inr_in_M_iff [iff]
   2.114 -declare transitive_set_abs [simp] 
   2.115 -declare ordinal_abs [simp] 
   2.116 -declare limit_ordinal_abs [simp] 
   2.117 -declare successor_ordinal_abs [simp] 
   2.118 -declare finite_ordinal_abs [simp] 
   2.119 -declare omega_abs [simp] 
   2.120 -declare number1_abs [simp] 
   2.121 -declare number1_abs [simp] 
   2.122 -declare number3_abs [simp]
   2.123 +lemmas rall_abs [simp] = M_triv_axioms.rall_abs [OF M_triv_axioms_L]
   2.124 +  and rex_abs [simp] = M_triv_axioms.rex_abs [OF M_triv_axioms_L]
   2.125 +  and ball_iff_equiv = M_triv_axioms.ball_iff_equiv [OF M_triv_axioms_L]
   2.126 +  and M_equalityI = M_triv_axioms.M_equalityI [OF M_triv_axioms_L]
   2.127 +  and empty_abs [simp] = M_triv_axioms.empty_abs [OF M_triv_axioms_L]
   2.128 +  and subset_abs [simp] = M_triv_axioms.subset_abs [OF M_triv_axioms_L]
   2.129 +  and upair_abs [simp] = M_triv_axioms.upair_abs [OF M_triv_axioms_L]
   2.130 +  and upair_in_M_iff [iff] = M_triv_axioms.upair_in_M_iff [OF M_triv_axioms_L]
   2.131 +  and singleton_in_M_iff [iff] = M_triv_axioms.singleton_in_M_iff [OF M_triv_axioms_L]
   2.132 +  and pair_abs [simp] = M_triv_axioms.pair_abs [OF M_triv_axioms_L]
   2.133 +  and pair_in_M_iff [iff] = M_triv_axioms.pair_in_M_iff [OF M_triv_axioms_L]
   2.134 +  and pair_components_in_M = M_triv_axioms.pair_components_in_M [OF M_triv_axioms_L]
   2.135 +  and cartprod_abs [simp] = M_triv_axioms.cartprod_abs [OF M_triv_axioms_L]
   2.136 +  and union_abs [simp] = M_triv_axioms.union_abs [OF M_triv_axioms_L]
   2.137 +  and inter_abs [simp] = M_triv_axioms.inter_abs [OF M_triv_axioms_L]
   2.138 +  and setdiff_abs [simp] = M_triv_axioms.setdiff_abs [OF M_triv_axioms_L]
   2.139 +  and Union_abs [simp] = M_triv_axioms.Union_abs [OF M_triv_axioms_L]
   2.140 +  and Union_closed [intro, simp] = M_triv_axioms.Union_closed [OF M_triv_axioms_L]
   2.141 +  and Un_closed [intro, simp] = M_triv_axioms.Un_closed [OF M_triv_axioms_L]
   2.142 +  and cons_closed [intro, simp] = M_triv_axioms.cons_closed [OF M_triv_axioms_L]
   2.143 +  and successor_abs [simp] = M_triv_axioms.successor_abs [OF M_triv_axioms_L]
   2.144 +  and succ_in_M_iff [iff] = M_triv_axioms.succ_in_M_iff [OF M_triv_axioms_L]
   2.145 +  and separation_closed [intro, simp] = M_triv_axioms.separation_closed [OF M_triv_axioms_L]
   2.146 +  and strong_replacementI = M_triv_axioms.strong_replacementI [OF M_triv_axioms_L]
   2.147 +  and strong_replacement_closed [intro, simp] = M_triv_axioms.strong_replacement_closed [OF M_triv_axioms_L]
   2.148 +  and RepFun_closed [intro, simp] = M_triv_axioms.RepFun_closed [OF M_triv_axioms_L]
   2.149 +  and lam_closed [intro, simp] = M_triv_axioms.lam_closed [OF M_triv_axioms_L]
   2.150 +  and image_abs [simp] = M_triv_axioms.image_abs [OF M_triv_axioms_L]
   2.151 +  and powerset_Pow = M_triv_axioms.powerset_Pow [OF M_triv_axioms_L]
   2.152 +  and powerset_imp_subset_Pow = M_triv_axioms.powerset_imp_subset_Pow [OF M_triv_axioms_L]
   2.153 +  and nat_into_M [intro] = M_triv_axioms.nat_into_M [OF M_triv_axioms_L]
   2.154 +  and nat_case_closed = M_triv_axioms.nat_case_closed [OF M_triv_axioms_L]
   2.155 +  and Inl_in_M_iff [iff] = M_triv_axioms.Inl_in_M_iff [OF M_triv_axioms_L]
   2.156 +  and Inr_in_M_iff [iff] = M_triv_axioms.Inr_in_M_iff [OF M_triv_axioms_L]
   2.157 +  and lt_closed = M_triv_axioms.lt_closed [OF M_triv_axioms_L]
   2.158 +  and transitive_set_abs [simp] = M_triv_axioms.transitive_set_abs [OF M_triv_axioms_L]
   2.159 +  and ordinal_abs [simp] = M_triv_axioms.ordinal_abs [OF M_triv_axioms_L]
   2.160 +  and limit_ordinal_abs [simp] = M_triv_axioms.limit_ordinal_abs [OF M_triv_axioms_L]
   2.161 +  and successor_ordinal_abs [simp] = M_triv_axioms.successor_ordinal_abs [OF M_triv_axioms_L]
   2.162 +  and finite_ordinal_abs = M_triv_axioms.finite_ordinal_abs [OF M_triv_axioms_L]
   2.163 +  and omega_abs [simp] = M_triv_axioms.omega_abs [OF M_triv_axioms_L]
   2.164 +  and number1_abs [simp] = M_triv_axioms.number1_abs [OF M_triv_axioms_L]
   2.165 +  and number2_abs [simp] = M_triv_axioms.number2_abs [OF M_triv_axioms_L]
   2.166 +  and number3_abs [simp] = M_triv_axioms.number3_abs [OF M_triv_axioms_L]
   2.167  
   2.168  
   2.169  subsection{*Instantiation of the locale @{text reflection}*}
   2.170 @@ -260,8 +215,9 @@
   2.171  apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
   2.172  apply (elim meta_exE) 
   2.173  apply (rule meta_exI)
   2.174 -apply (rule reflection.Ex_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],
   2.175 -       assumption+)
   2.176 +apply (rule reflection.Ex_reflection
   2.177 +  [OF reflection.intro, OF Lset_mono_le Lset_cont Pair_in_Lset],
   2.178 +  assumption+)
   2.179  done
   2.180  
   2.181  theorem All_reflection:
   2.182 @@ -270,7 +226,8 @@
   2.183  apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
   2.184  apply (elim meta_exE) 
   2.185  apply (rule meta_exI)
   2.186 -apply (rule reflection.All_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],
   2.187 +apply (rule reflection.All_reflection
   2.188 +  [OF reflection.intro, OF Lset_mono_le Lset_cont Pair_in_Lset],
   2.189         assumption+)
   2.190  done
   2.191  
   2.192 @@ -308,7 +265,7 @@
   2.193  apply (drule ReflectsD, assumption, blast) 
   2.194  done
   2.195  
   2.196 -lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B";
   2.197 +lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B"
   2.198  by blast
   2.199  
   2.200  
     3.1 --- a/src/ZF/Constructible/Normal.thy	Sun Jul 28 21:09:37 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Normal.thy	Mon Jul 29 00:57:16 2002 +0200
     3.3 @@ -72,7 +72,7 @@
     3.4        c.u.*}
     3.5  
     3.6  text{*The constructions below come from Kunen, \emph{Set Theory}, page 78.*}
     3.7 -locale (open) cub_family =
     3.8 +locale cub_family =
     3.9    fixes P and A
    3.10    fixes next_greater -- "the next ordinal satisfying class @{term A}"
    3.11    fixes sup_greater  -- "sup of those ordinals over all @{term A}"
    3.12 @@ -177,7 +177,7 @@
    3.13      "(!!a. a\<in>A ==> Closed_Unbounded(P(a)))
    3.14       ==> Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a, x))"
    3.15  apply (case_tac "A=0", simp)
    3.16 -apply (rule cub_family.Closed_Unbounded_INT)
    3.17 +apply (rule cub_family.Closed_Unbounded_INT [OF cub_family.intro])
    3.18  apply (simp_all add: Closed_Unbounded_def)
    3.19  done
    3.20  
     4.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Sun Jul 28 21:09:37 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Jul 29 00:57:16 2002 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  "M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}
     4.5  
     4.6  lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
     4.7 -by simp 
     4.8 +by simp
     4.9  
    4.10  subsection{*The Locale @{text "M_trancl"}*}
    4.11  
    4.12 @@ -15,69 +15,69 @@
    4.13  text{*First, The Defining Formula*}
    4.14  
    4.15  (* "rtran_closure_mem(M,A,r,p) ==
    4.16 -      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
    4.17 +      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
    4.18         omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
    4.19         (\<exists>f[M]. typed_function(M,n',A,f) &
    4.20 -	(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
    4.21 -	  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
    4.22 -	(\<forall>j[M]. j\<in>n --> 
    4.23 -	  (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. 
    4.24 -	    fun_apply(M,f,j,fj) & successor(M,j,sj) &
    4.25 -	    fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
    4.26 +        (\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
    4.27 +          fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
    4.28 +        (\<forall>j[M]. j\<in>n -->
    4.29 +          (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
    4.30 +            fun_apply(M,f,j,fj) & successor(M,j,sj) &
    4.31 +            fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
    4.32  constdefs rtran_closure_mem_fm :: "[i,i,i]=>i"
    4.33 - "rtran_closure_mem_fm(A,r,p) == 
    4.34 + "rtran_closure_mem_fm(A,r,p) ==
    4.35     Exists(Exists(Exists(
    4.36      And(omega_fm(2),
    4.37       And(Member(1,2),
    4.38        And(succ_fm(1,0),
    4.39         Exists(And(typed_function_fm(1, A#+4, 0),
    4.40 -	And(Exists(Exists(Exists(
    4.41 -	      And(pair_fm(2,1,p#+7), 
    4.42 -	       And(empty_fm(0),
    4.43 -		And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))),
    4.44 -	    Forall(Implies(Member(0,3),
    4.45 -	     Exists(Exists(Exists(Exists(
    4.46 -	      And(fun_apply_fm(5,4,3),
    4.47 -	       And(succ_fm(4,2),
    4.48 -		And(fun_apply_fm(5,2,1),
    4.49 -		 And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))"
    4.50 +        And(Exists(Exists(Exists(
    4.51 +              And(pair_fm(2,1,p#+7),
    4.52 +               And(empty_fm(0),
    4.53 +                And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))),
    4.54 +            Forall(Implies(Member(0,3),
    4.55 +             Exists(Exists(Exists(Exists(
    4.56 +              And(fun_apply_fm(5,4,3),
    4.57 +               And(succ_fm(4,2),
    4.58 +                And(fun_apply_fm(5,2,1),
    4.59 +                 And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))"
    4.60  
    4.61  
    4.62  lemma rtran_closure_mem_type [TC]:
    4.63   "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
    4.64 -by (simp add: rtran_closure_mem_fm_def) 
    4.65 +by (simp add: rtran_closure_mem_fm_def)
    4.66  
    4.67  lemma arity_rtran_closure_mem_fm [simp]:
    4.68 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
    4.69 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
    4.70        ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    4.71 -by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac) 
    4.72 +by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac)
    4.73  
    4.74  lemma sats_rtran_closure_mem_fm [simp]:
    4.75     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    4.76 -    ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> 
    4.77 +    ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
    4.78          rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))"
    4.79  by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def)
    4.80  
    4.81  lemma rtran_closure_mem_iff_sats:
    4.82 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    4.83 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
    4.84            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    4.85         ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
    4.86  by (simp add: sats_rtran_closure_mem_fm)
    4.87  
    4.88  theorem rtran_closure_mem_reflection:
    4.89 -     "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)), 
    4.90 +     "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
    4.91                 \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
    4.92  apply (simp only: rtran_closure_mem_def setclass_simps)
    4.93 -apply (intro FOL_reflections function_reflections fun_plus_reflections)  
    4.94 +apply (intro FOL_reflections function_reflections fun_plus_reflections)
    4.95  done
    4.96  
    4.97  text{*Separation for @{term "rtrancl(r)"}.*}
    4.98  lemma rtrancl_separation:
    4.99       "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
   4.100 -apply (rule separation_CollectI) 
   4.101 -apply (rule_tac A="{r,A,z}" in subset_LsetE, blast ) 
   4.102 +apply (rule separation_CollectI)
   4.103 +apply (rule_tac A="{r,A,z}" in subset_LsetE, blast )
   4.104  apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
   4.105 -apply (drule subset_Lset_ltD, assumption) 
   4.106 +apply (drule subset_Lset_ltD, assumption)
   4.107  apply (erule reflection_imp_L_separation)
   4.108    apply (simp_all add: lt_Ord2)
   4.109  apply (rule DPow_LsetI)
   4.110 @@ -89,38 +89,38 @@
   4.111  
   4.112  subsubsection{*Reflexive/Transitive Closure, Internalized*}
   4.113  
   4.114 -(*  "rtran_closure(M,r,s) == 
   4.115 +(*  "rtran_closure(M,r,s) ==
   4.116          \<forall>A[M]. is_field(M,r,A) -->
   4.117 - 	 (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *)
   4.118 +         (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *)
   4.119  constdefs rtran_closure_fm :: "[i,i]=>i"
   4.120 - "rtran_closure_fm(r,s) == 
   4.121 + "rtran_closure_fm(r,s) ==
   4.122     Forall(Implies(field_fm(succ(r),0),
   4.123                    Forall(Iff(Member(0,succ(succ(s))),
   4.124                               rtran_closure_mem_fm(1,succ(succ(r)),0)))))"
   4.125  
   4.126  lemma rtran_closure_type [TC]:
   4.127       "[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula"
   4.128 -by (simp add: rtran_closure_fm_def) 
   4.129 +by (simp add: rtran_closure_fm_def)
   4.130  
   4.131  lemma arity_rtran_closure_fm [simp]:
   4.132 -     "[| x \<in> nat; y \<in> nat |] 
   4.133 +     "[| x \<in> nat; y \<in> nat |]
   4.134        ==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
   4.135  by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
   4.136  
   4.137  lemma sats_rtran_closure_fm [simp]:
   4.138     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   4.139 -    ==> sats(A, rtran_closure_fm(x,y), env) <-> 
   4.140 +    ==> sats(A, rtran_closure_fm(x,y), env) <->
   4.141          rtran_closure(**A, nth(x,env), nth(y,env))"
   4.142  by (simp add: rtran_closure_fm_def rtran_closure_def)
   4.143  
   4.144  lemma rtran_closure_iff_sats:
   4.145 -      "[| nth(i,env) = x; nth(j,env) = y; 
   4.146 +      "[| nth(i,env) = x; nth(j,env) = y;
   4.147            i \<in> nat; j \<in> nat; env \<in> list(A)|]
   4.148         ==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)"
   4.149  by simp
   4.150  
   4.151  theorem rtran_closure_reflection:
   4.152 -     "REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)), 
   4.153 +     "REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)),
   4.154                 \<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]"
   4.155  apply (simp only: rtran_closure_def setclass_simps)
   4.156  apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection)
   4.157 @@ -132,35 +132,35 @@
   4.158  (*  "tran_closure(M,r,t) ==
   4.159           \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *)
   4.160  constdefs tran_closure_fm :: "[i,i]=>i"
   4.161 - "tran_closure_fm(r,s) == 
   4.162 + "tran_closure_fm(r,s) ==
   4.163     Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))"
   4.164  
   4.165  lemma tran_closure_type [TC]:
   4.166       "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula"
   4.167 -by (simp add: tran_closure_fm_def) 
   4.168 +by (simp add: tran_closure_fm_def)
   4.169  
   4.170  lemma arity_tran_closure_fm [simp]:
   4.171 -     "[| x \<in> nat; y \<in> nat |] 
   4.172 +     "[| x \<in> nat; y \<in> nat |]
   4.173        ==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
   4.174  by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
   4.175  
   4.176  lemma sats_tran_closure_fm [simp]:
   4.177     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   4.178 -    ==> sats(A, tran_closure_fm(x,y), env) <-> 
   4.179 +    ==> sats(A, tran_closure_fm(x,y), env) <->
   4.180          tran_closure(**A, nth(x,env), nth(y,env))"
   4.181  by (simp add: tran_closure_fm_def tran_closure_def)
   4.182  
   4.183  lemma tran_closure_iff_sats:
   4.184 -      "[| nth(i,env) = x; nth(j,env) = y; 
   4.185 +      "[| nth(i,env) = x; nth(j,env) = y;
   4.186            i \<in> nat; j \<in> nat; env \<in> list(A)|]
   4.187         ==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)"
   4.188  by simp
   4.189  
   4.190  theorem tran_closure_reflection:
   4.191 -     "REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)), 
   4.192 +     "REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)),
   4.193                 \<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]"
   4.194  apply (simp only: tran_closure_def setclass_simps)
   4.195 -apply (intro FOL_reflections function_reflections 
   4.196 +apply (intro FOL_reflections function_reflections
   4.197               rtran_closure_reflection composition_reflection)
   4.198  done
   4.199  
   4.200 @@ -168,60 +168,62 @@
   4.201  subsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
   4.202  
   4.203  lemma wellfounded_trancl_reflects:
   4.204 -  "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. 
   4.205 -	         w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
   4.206 -   \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i). 
   4.207 +  "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
   4.208 +                 w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
   4.209 +   \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i).
   4.210         w \<in> Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) &
   4.211         wx \<in> rp]"
   4.212 -by (intro FOL_reflections function_reflections fun_plus_reflections 
   4.213 +by (intro FOL_reflections function_reflections fun_plus_reflections
   4.214            tran_closure_reflection)
   4.215  
   4.216  
   4.217  lemma wellfounded_trancl_separation:
   4.218 -	 "[| L(r); L(Z) |] ==> 
   4.219 -	  separation (L, \<lambda>x. 
   4.220 -	      \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. 
   4.221 -	       w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
   4.222 -apply (rule separation_CollectI) 
   4.223 -apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast ) 
   4.224 +         "[| L(r); L(Z) |] ==>
   4.225 +          separation (L, \<lambda>x.
   4.226 +              \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
   4.227 +               w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
   4.228 +apply (rule separation_CollectI)
   4.229 +apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast )
   4.230  apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption)
   4.231 -apply (drule subset_Lset_ltD, assumption) 
   4.232 +apply (drule subset_Lset_ltD, assumption)
   4.233  apply (erule reflection_imp_L_separation)
   4.234    apply (simp_all add: lt_Ord2)
   4.235  apply (rule DPow_LsetI)
   4.236 -apply (rename_tac u) 
   4.237 +apply (rename_tac u)
   4.238  apply (rule bex_iff_sats conj_iff_sats)+
   4.239 -apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats) 
   4.240 +apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats)
   4.241  apply (rule sep_rules tran_closure_iff_sats | simp)+
   4.242  done
   4.243  
   4.244  
   4.245  subsubsection{*Instantiating the locale @{text M_trancl}*}
   4.246 -ML
   4.247 -{*
   4.248 -val rtrancl_separation = thm "rtrancl_separation";
   4.249 -val wellfounded_trancl_separation = thm "wellfounded_trancl_separation";
   4.250 +
   4.251 +theorem M_trancl_axioms_L: "M_trancl_axioms(L)"
   4.252 +  apply (rule M_trancl_axioms.intro)
   4.253 +   apply (assumption | rule
   4.254 +     rtrancl_separation wellfounded_trancl_separation)+
   4.255 +  done
   4.256  
   4.257 -
   4.258 -val m_trancl = [rtrancl_separation, wellfounded_trancl_separation];
   4.259 -
   4.260 -fun trancl_L th =
   4.261 -    kill_flex_triv_prems (m_trancl MRS (axioms_L th));
   4.262 +theorem M_trancl_L: "PROP M_trancl(L)"
   4.263 +  apply (rule M_trancl.intro)
   4.264 +    apply (rule M_triv_axioms_L)
   4.265 +   apply (rule M_axioms_axioms_L)
   4.266 +  apply (rule M_trancl_axioms_L)
   4.267 +  done
   4.268  
   4.269 -bind_thm ("iterates_abs", trancl_L (thm "M_trancl.iterates_abs"));
   4.270 -bind_thm ("rtran_closure_rtrancl", trancl_L (thm "M_trancl.rtran_closure_rtrancl"));
   4.271 -bind_thm ("rtrancl_closed", trancl_L (thm "M_trancl.rtrancl_closed"));
   4.272 -bind_thm ("rtrancl_abs", trancl_L (thm "M_trancl.rtrancl_abs"));
   4.273 -bind_thm ("trancl_closed", trancl_L (thm "M_trancl.trancl_closed"));
   4.274 -bind_thm ("trancl_abs", trancl_L (thm "M_trancl.trancl_abs"));
   4.275 -bind_thm ("wellfounded_on_trancl", trancl_L (thm "M_trancl.wellfounded_on_trancl"));
   4.276 -bind_thm ("wellfounded_trancl", trancl_L (thm "M_trancl.wellfounded_trancl"));
   4.277 -bind_thm ("wfrec_relativize", trancl_L (thm "M_trancl.wfrec_relativize"));
   4.278 -bind_thm ("trans_wfrec_relativize", trancl_L (thm "M_trancl.trans_wfrec_relativize"));
   4.279 -bind_thm ("trans_wfrec_abs", trancl_L (thm "M_trancl.trans_wfrec_abs"));
   4.280 -bind_thm ("trans_eq_pair_wfrec_iff", trancl_L (thm "M_trancl.trans_eq_pair_wfrec_iff"));
   4.281 -bind_thm ("eq_pair_wfrec_iff", trancl_L (thm "M_trancl.eq_pair_wfrec_iff"));
   4.282 -*}
   4.283 +lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
   4.284 +  and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
   4.285 +  and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L]
   4.286 +  and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L]
   4.287 +  and trancl_closed = M_trancl.trancl_closed [OF M_trancl_L]
   4.288 +  and trancl_abs = M_trancl.trancl_abs [OF M_trancl_L]
   4.289 +  and wellfounded_on_trancl = M_trancl.wellfounded_on_trancl [OF M_trancl_L]
   4.290 +  and wellfounded_trancl = M_trancl.wellfounded_trancl [OF M_trancl_L]
   4.291 +  and wfrec_relativize = M_trancl.wfrec_relativize [OF M_trancl_L]
   4.292 +  and trans_wfrec_relativize = M_trancl.trans_wfrec_relativize [OF M_trancl_L]
   4.293 +  and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L]
   4.294 +  and trans_eq_pair_wfrec_iff = M_trancl.trans_eq_pair_wfrec_iff [OF M_trancl_L]
   4.295 +  and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L]
   4.296  
   4.297  declare rtrancl_closed [intro,simp]
   4.298  declare rtrancl_abs [simp]
   4.299 @@ -232,17 +234,17 @@
   4.300  subsection{*Well-Founded Recursion!*}
   4.301  
   4.302  (* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
   4.303 -   "M_is_recfun(M,MH,r,a,f) == 
   4.304 -     \<forall>z[M]. z \<in> f <-> 
   4.305 +   "M_is_recfun(M,MH,r,a,f) ==
   4.306 +     \<forall>z[M]. z \<in> f <->
   4.307              5      4       3       2       1           0
   4.308 -            (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. 
   4.309 -	       pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
   4.310 +            (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M].
   4.311 +               pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
   4.312                 pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
   4.313                 xa \<in> r & MH(x, f_r_sx, y))"
   4.314  *)
   4.315  
   4.316  constdefs is_recfun_fm :: "[[i,i,i]=>i, i, i, i]=>i"
   4.317 - "is_recfun_fm(p,r,a,f) == 
   4.318 + "is_recfun_fm(p,r,a,f) ==
   4.319     Forall(Iff(Member(0,succ(f)),
   4.320      Exists(Exists(Exists(Exists(Exists(Exists(
   4.321       And(pair_fm(5,4,6),
   4.322 @@ -254,39 +256,39 @@
   4.323  
   4.324  
   4.325  lemma is_recfun_type_0:
   4.326 -     "[| !!x y z. [| x \<in> nat; y \<in> nat; z \<in> nat |] ==> p(x,y,z) \<in> formula;  
   4.327 -         x \<in> nat; y \<in> nat; z \<in> nat |] 
   4.328 +     "[| !!x y z. [| x \<in> nat; y \<in> nat; z \<in> nat |] ==> p(x,y,z) \<in> formula;
   4.329 +         x \<in> nat; y \<in> nat; z \<in> nat |]
   4.330        ==> is_recfun_fm(p,x,y,z) \<in> formula"
   4.331  apply (unfold is_recfun_fm_def)
   4.332  (*FIXME: FIND OUT why simp loops!*)
   4.333  apply typecheck
   4.334 -by simp 
   4.335 +by simp
   4.336  
   4.337  lemma is_recfun_type [TC]:
   4.338 -     "[| p(5,0,4) \<in> formula;  
   4.339 -         x \<in> nat; y \<in> nat; z \<in> nat |] 
   4.340 +     "[| p(5,0,4) \<in> formula;
   4.341 +         x \<in> nat; y \<in> nat; z \<in> nat |]
   4.342        ==> is_recfun_fm(p,x,y,z) \<in> formula"
   4.343 -by (simp add: is_recfun_fm_def) 
   4.344 +by (simp add: is_recfun_fm_def)
   4.345  
   4.346  lemma arity_is_recfun_fm [simp]:
   4.347 -     "[| arity(p(5,0,4)) le 8; x \<in> nat; y \<in> nat; z \<in> nat |] 
   4.348 +     "[| arity(p(5,0,4)) le 8; x \<in> nat; y \<in> nat; z \<in> nat |]
   4.349        ==> arity(is_recfun_fm(p,x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   4.350 -apply (frule lt_nat_in_nat, simp) 
   4.351 -apply (simp add: is_recfun_fm_def succ_Un_distrib [symmetric] ) 
   4.352 -apply (subst subset_Un_iff2 [of "arity(p(5,0,4))", THEN iffD1]) 
   4.353 -apply (rule le_imp_subset) 
   4.354 -apply (erule le_trans, simp) 
   4.355 -apply (simp add: succ_Un_distrib [symmetric] Un_ac) 
   4.356 +apply (frule lt_nat_in_nat, simp)
   4.357 +apply (simp add: is_recfun_fm_def succ_Un_distrib [symmetric] )
   4.358 +apply (subst subset_Un_iff2 [of "arity(p(5,0,4))", THEN iffD1])
   4.359 +apply (rule le_imp_subset)
   4.360 +apply (erule le_trans, simp)
   4.361 +apply (simp add: succ_Un_distrib [symmetric] Un_ac)
   4.362  done
   4.363  
   4.364  lemma sats_is_recfun_fm:
   4.365 -  assumes MH_iff_sats: 
   4.366 -      "!!x y z env. 
   4.367 -	 [| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   4.368 -	 ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> sats(A, p(x,y,z), env)"
   4.369 -  shows 
   4.370 +  assumes MH_iff_sats:
   4.371 +      "!!x y z env.
   4.372 +         [| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   4.373 +         ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> sats(A, p(x,y,z), env)"
   4.374 +  shows
   4.375        "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   4.376 -       ==> sats(A, is_recfun_fm(p,x,y,z), env) <-> 
   4.377 +       ==> sats(A, is_recfun_fm(p,x,y,z), env) <->
   4.378             M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
   4.379  by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym])
   4.380  
   4.381 @@ -294,20 +296,20 @@
   4.382    "[| (!!x y z env. [| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   4.383                      ==> MH(nth(x,env), nth(y,env), nth(z,env)) <->
   4.384                          sats(A, p(x,y,z), env));
   4.385 -      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   4.386 +      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   4.387        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   4.388 -   ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" 
   4.389 +   ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
   4.390  by (simp add: sats_is_recfun_fm [of A MH])
   4.391  
   4.392  theorem is_recfun_reflection:
   4.393    assumes MH_reflection:
   4.394 -    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)), 
   4.395 +    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)),
   4.396                       \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
   4.397 -  shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L), f(x), g(x), h(x)), 
   4.398 +  shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L), f(x), g(x), h(x)),
   4.399                 \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
   4.400  apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps)
   4.401 -apply (intro FOL_reflections function_reflections 
   4.402 -             restriction_reflection MH_reflection)  
   4.403 +apply (intro FOL_reflections function_reflections
   4.404 +             restriction_reflection MH_reflection)
   4.405  done
   4.406  
   4.407  text{*Currently, @{text sats}-theorems for higher-order operators don't seem
   4.408 @@ -315,12 +317,12 @@
   4.409  of the @{text MH}-term.*}
   4.410  theorem is_wfrec_reflection:
   4.411    assumes MH_reflection:
   4.412 -    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)), 
   4.413 +    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)),
   4.414                       \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
   4.415 -  shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L), f(x), g(x), h(x)), 
   4.416 +  shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L), f(x), g(x), h(x)),
   4.417                 \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
   4.418  apply (simp (no_asm_use) only: is_wfrec_def setclass_simps)
   4.419 -apply (intro FOL_reflections MH_reflection is_recfun_reflection)  
   4.420 +apply (intro FOL_reflections MH_reflection is_recfun_reflection)
   4.421  done
   4.422  
   4.423  subsection{*The Locale @{text "M_wfrank"}*}
   4.424 @@ -331,23 +333,23 @@
   4.425   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   4.426                ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
   4.427        \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
   4.428 -         ~ (\<exists>f \<in> Lset(i). 
   4.429 -            M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), 
   4.430 +         ~ (\<exists>f \<in> Lset(i).
   4.431 +            M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y),
   4.432                          rplus, x, f))]"
   4.433 -by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)  
   4.434 +by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)
   4.435  
   4.436  lemma wfrank_separation:
   4.437       "L(r) ==>
   4.438        separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   4.439           ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
   4.440 -apply (rule separation_CollectI) 
   4.441 -apply (rule_tac A="{r,z}" in subset_LsetE, blast ) 
   4.442 +apply (rule separation_CollectI)
   4.443 +apply (rule_tac A="{r,z}" in subset_LsetE, blast )
   4.444  apply (rule ReflectsE [OF wfrank_Reflects], assumption)
   4.445 -apply (drule subset_Lset_ltD, assumption) 
   4.446 +apply (drule subset_Lset_ltD, assumption)
   4.447  apply (erule reflection_imp_L_separation)
   4.448    apply (simp_all add: lt_Ord2, clarify)
   4.449  apply (rule DPow_LsetI)
   4.450 -apply (rename_tac u)  
   4.451 +apply (rename_tac u)
   4.452  apply (rule ball_iff_sats imp_iff_sats)+
   4.453  apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
   4.454  apply (rule sep_rules is_recfun_iff_sats | simp)+
   4.455 @@ -357,14 +359,14 @@
   4.456  subsubsection{*Replacement for @{term "wfrank"}*}
   4.457  
   4.458  lemma wfrank_replacement_Reflects:
   4.459 - "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A & 
   4.460 + "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A &
   4.461          (\<forall>rplus[L]. tran_closure(L,r,rplus) -->
   4.462 -         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  & 
   4.463 +         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
   4.464                          M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
   4.465                          is_range(L,f,y))),
   4.466 - \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A & 
   4.467 + \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A &
   4.468        (\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
   4.469 -       (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  & 
   4.470 +       (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  &
   4.471           M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) &
   4.472           is_range(**Lset(i),f,y)))]"
   4.473  by (intro FOL_reflections function_reflections fun_plus_reflections
   4.474 @@ -373,24 +375,24 @@
   4.475  
   4.476  lemma wfrank_strong_replacement:
   4.477       "L(r) ==>
   4.478 -      strong_replacement(L, \<lambda>x z. 
   4.479 +      strong_replacement(L, \<lambda>x z.
   4.480           \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   4.481 -         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  & 
   4.482 +         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
   4.483                          M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
   4.484                          is_range(L,f,y)))"
   4.485 -apply (rule strong_replacementI) 
   4.486 +apply (rule strong_replacementI)
   4.487  apply (rule rallI)
   4.488 -apply (rename_tac B)  
   4.489 -apply (rule separation_CollectI) 
   4.490 -apply (rule_tac A="{B,r,z}" in subset_LsetE, blast ) 
   4.491 +apply (rename_tac B)
   4.492 +apply (rule separation_CollectI)
   4.493 +apply (rule_tac A="{B,r,z}" in subset_LsetE, blast )
   4.494  apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption)
   4.495 -apply (drule subset_Lset_ltD, assumption) 
   4.496 +apply (drule subset_Lset_ltD, assumption)
   4.497  apply (erule reflection_imp_L_separation)
   4.498    apply (simp_all add: lt_Ord2)
   4.499  apply (rule DPow_LsetI)
   4.500 -apply (rename_tac u) 
   4.501 +apply (rename_tac u)
   4.502  apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
   4.503 -apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats) 
   4.504 +apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats)
   4.505  apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
   4.506  done
   4.507  
   4.508 @@ -398,36 +400,36 @@
   4.509  subsubsection{*Separation for Proving @{text Ord_wfrank_range}*}
   4.510  
   4.511  lemma Ord_wfrank_Reflects:
   4.512 - "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> 
   4.513 -          ~ (\<forall>f[L]. \<forall>rangef[L]. 
   4.514 + "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   4.515 +          ~ (\<forall>f[L]. \<forall>rangef[L].
   4.516               is_range(L,f,rangef) -->
   4.517               M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
   4.518               ordinal(L,rangef)),
   4.519 -      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) --> 
   4.520 -          ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i). 
   4.521 +      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
   4.522 +          ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
   4.523               is_range(**Lset(i),f,rangef) -->
   4.524 -             M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y), 
   4.525 +             M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y),
   4.526                           rplus, x, f) -->
   4.527               ordinal(**Lset(i),rangef))]"
   4.528 -by (intro FOL_reflections function_reflections is_recfun_reflection 
   4.529 +by (intro FOL_reflections function_reflections is_recfun_reflection
   4.530            tran_closure_reflection ordinal_reflection)
   4.531  
   4.532  lemma  Ord_wfrank_separation:
   4.533       "L(r) ==>
   4.534        separation (L, \<lambda>x.
   4.535 -         \<forall>rplus[L]. tran_closure(L,r,rplus) --> 
   4.536 -          ~ (\<forall>f[L]. \<forall>rangef[L]. 
   4.537 +         \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   4.538 +          ~ (\<forall>f[L]. \<forall>rangef[L].
   4.539               is_range(L,f,rangef) -->
   4.540               M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
   4.541 -             ordinal(L,rangef)))" 
   4.542 -apply (rule separation_CollectI) 
   4.543 -apply (rule_tac A="{r,z}" in subset_LsetE, blast ) 
   4.544 +             ordinal(L,rangef)))"
   4.545 +apply (rule separation_CollectI)
   4.546 +apply (rule_tac A="{r,z}" in subset_LsetE, blast )
   4.547  apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption)
   4.548 -apply (drule subset_Lset_ltD, assumption) 
   4.549 +apply (drule subset_Lset_ltD, assumption)
   4.550  apply (erule reflection_imp_L_separation)
   4.551    apply (simp_all add: lt_Ord2, clarify)
   4.552  apply (rule DPow_LsetI)
   4.553 -apply (rename_tac u)  
   4.554 +apply (rename_tac u)
   4.555  apply (rule ball_iff_sats imp_iff_sats)+
   4.556  apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
   4.557  apply (rule sep_rules is_recfun_iff_sats | simp)+
   4.558 @@ -435,40 +437,40 @@
   4.559  
   4.560  
   4.561  subsubsection{*Instantiating the locale @{text M_wfrank}*}
   4.562 -ML
   4.563 -{*
   4.564 -val wfrank_separation = thm "wfrank_separation";
   4.565 -val wfrank_strong_replacement = thm "wfrank_strong_replacement";
   4.566 -val Ord_wfrank_separation = thm "Ord_wfrank_separation";
   4.567 +
   4.568 +theorem M_wfrank_axioms_L: "M_wfrank_axioms(L)"
   4.569 +  apply (rule M_wfrank_axioms.intro)
   4.570 +  apply (assumption | rule
   4.571 +    wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
   4.572 +  done
   4.573  
   4.574 -val m_wfrank = 
   4.575 -    [wfrank_separation, wfrank_strong_replacement, Ord_wfrank_separation];
   4.576 -
   4.577 -fun wfrank_L th =
   4.578 -    kill_flex_triv_prems (m_wfrank MRS (trancl_L th));
   4.579 -
   4.580 -
   4.581 +theorem M_wfrank_L: "PROP M_wfrank(L)"
   4.582 +  apply (rule M_wfrank.intro)
   4.583 +     apply (rule M_triv_axioms_L)
   4.584 +    apply (rule M_axioms_axioms_L)
   4.585 +   apply (rule M_trancl_axioms_L)
   4.586 +  apply (rule M_wfrank_axioms_L)
   4.587 +  done
   4.588  
   4.589 -bind_thm ("iterates_closed", wfrank_L (thm "M_wfrank.iterates_closed"));
   4.590 -bind_thm ("exists_wfrank", wfrank_L (thm "M_wfrank.exists_wfrank"));
   4.591 -bind_thm ("M_wellfoundedrank", wfrank_L (thm "M_wfrank.M_wellfoundedrank"));
   4.592 -bind_thm ("Ord_wfrank_range", wfrank_L (thm "M_wfrank.Ord_wfrank_range"));
   4.593 -bind_thm ("Ord_range_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_range_wellfoundedrank"));
   4.594 -bind_thm ("function_wellfoundedrank", wfrank_L (thm "M_wfrank.function_wellfoundedrank"));
   4.595 -bind_thm ("domain_wellfoundedrank", wfrank_L (thm "M_wfrank.domain_wellfoundedrank"));
   4.596 -bind_thm ("wellfoundedrank_type", wfrank_L (thm "M_wfrank.wellfoundedrank_type"));
   4.597 -bind_thm ("Ord_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_wellfoundedrank"));
   4.598 -bind_thm ("wellfoundedrank_eq", wfrank_L (thm "M_wfrank.wellfoundedrank_eq"));
   4.599 -bind_thm ("wellfoundedrank_lt", wfrank_L (thm "M_wfrank.wellfoundedrank_lt"));
   4.600 -bind_thm ("wellfounded_imp_subset_rvimage", wfrank_L (thm "M_wfrank.wellfounded_imp_subset_rvimage"));
   4.601 -bind_thm ("wellfounded_imp_wf", wfrank_L (thm "M_wfrank.wellfounded_imp_wf"));
   4.602 -bind_thm ("wellfounded_on_imp_wf_on", wfrank_L (thm "M_wfrank.wellfounded_on_imp_wf_on"));
   4.603 -bind_thm ("wf_abs", wfrank_L (thm "M_wfrank.wf_abs"));
   4.604 -bind_thm ("wf_on_abs", wfrank_L (thm "M_wfrank.wf_on_abs"));
   4.605 -bind_thm ("wfrec_replacement_iff", wfrank_L (thm "M_wfrank.wfrec_replacement_iff"));
   4.606 -bind_thm ("trans_wfrec_closed", wfrank_L (thm "M_wfrank.trans_wfrec_closed"));
   4.607 -bind_thm ("wfrec_closed", wfrank_L (thm "M_wfrank.wfrec_closed"));
   4.608 -*}
   4.609 +lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L]
   4.610 +  and exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L]
   4.611 +  and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L]
   4.612 +  and Ord_wfrank_range = M_wfrank.Ord_wfrank_range [OF M_wfrank_L]
   4.613 +  and Ord_range_wellfoundedrank = M_wfrank.Ord_range_wellfoundedrank [OF M_wfrank_L]
   4.614 +  and function_wellfoundedrank = M_wfrank.function_wellfoundedrank [OF M_wfrank_L]
   4.615 +  and domain_wellfoundedrank = M_wfrank.domain_wellfoundedrank [OF M_wfrank_L]
   4.616 +  and wellfoundedrank_type = M_wfrank.wellfoundedrank_type [OF M_wfrank_L]
   4.617 +  and Ord_wellfoundedrank = M_wfrank.Ord_wellfoundedrank [OF M_wfrank_L]
   4.618 +  and wellfoundedrank_eq = M_wfrank.wellfoundedrank_eq [OF M_wfrank_L]
   4.619 +  and wellfoundedrank_lt = M_wfrank.wellfoundedrank_lt [OF M_wfrank_L]
   4.620 +  and wellfounded_imp_subset_rvimage = M_wfrank.wellfounded_imp_subset_rvimage [OF M_wfrank_L]
   4.621 +  and wellfounded_imp_wf = M_wfrank.wellfounded_imp_wf [OF M_wfrank_L]
   4.622 +  and wellfounded_on_imp_wf_on = M_wfrank.wellfounded_on_imp_wf_on [OF M_wfrank_L]
   4.623 +  and wf_abs = M_wfrank.wf_abs [OF M_wfrank_L]
   4.624 +  and wf_on_abs = M_wfrank.wf_on_abs [OF M_wfrank_L]
   4.625 +  and wfrec_replacement_iff = M_wfrank.wfrec_replacement_iff [OF M_wfrank_L]
   4.626 +  and trans_wfrec_closed = M_wfrank.trans_wfrec_closed [OF M_wfrank_L]
   4.627 +  and wfrec_closed = M_wfrank.wfrec_closed [OF M_wfrank_L]
   4.628  
   4.629  declare iterates_closed [intro,simp]
   4.630  declare Ord_wfrank_range [rule_format]
   4.631 @@ -481,9 +483,9 @@
   4.632  subsubsection{*Binary Products, Internalized*}
   4.633  
   4.634  constdefs cartprod_fm :: "[i,i,i]=>i"
   4.635 -(* "cartprod(M,A,B,z) == 
   4.636 -	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
   4.637 -    "cartprod_fm(A,B,z) == 
   4.638 +(* "cartprod(M,A,B,z) ==
   4.639 +        \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
   4.640 +    "cartprod_fm(A,B,z) ==
   4.641         Forall(Iff(Member(0,succ(z)),
   4.642                    Exists(And(Member(0,succ(succ(A))),
   4.643                           Exists(And(Member(0,succ(succ(succ(B)))),
   4.644 @@ -491,74 +493,74 @@
   4.645  
   4.646  lemma cartprod_type [TC]:
   4.647       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
   4.648 -by (simp add: cartprod_fm_def) 
   4.649 +by (simp add: cartprod_fm_def)
   4.650  
   4.651  lemma arity_cartprod_fm [simp]:
   4.652 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   4.653 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   4.654        ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   4.655 -by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac) 
   4.656 +by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac)
   4.657  
   4.658  lemma sats_cartprod_fm [simp]:
   4.659     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   4.660 -    ==> sats(A, cartprod_fm(x,y,z), env) <-> 
   4.661 +    ==> sats(A, cartprod_fm(x,y,z), env) <->
   4.662          cartprod(**A, nth(x,env), nth(y,env), nth(z,env))"
   4.663  by (simp add: cartprod_fm_def cartprod_def)
   4.664  
   4.665  lemma cartprod_iff_sats:
   4.666 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   4.667 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   4.668            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   4.669         ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
   4.670  by (simp add: sats_cartprod_fm)
   4.671  
   4.672  theorem cartprod_reflection:
   4.673 -     "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)), 
   4.674 +     "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
   4.675                 \<lambda>i x. cartprod(**Lset(i),f(x),g(x),h(x))]"
   4.676  apply (simp only: cartprod_def setclass_simps)
   4.677 -apply (intro FOL_reflections pair_reflection)  
   4.678 +apply (intro FOL_reflections pair_reflection)
   4.679  done
   4.680  
   4.681  
   4.682  subsubsection{*Binary Sums, Internalized*}
   4.683  
   4.684 -(* "is_sum(M,A,B,Z) == 
   4.685 -       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
   4.686 +(* "is_sum(M,A,B,Z) ==
   4.687 +       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
   4.688           3      2       1        0
   4.689         number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
   4.690         cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"  *)
   4.691  constdefs sum_fm :: "[i,i,i]=>i"
   4.692 -    "sum_fm(A,B,Z) == 
   4.693 +    "sum_fm(A,B,Z) ==
   4.694         Exists(Exists(Exists(Exists(
   4.695 -	And(number1_fm(2),
   4.696 +        And(number1_fm(2),
   4.697              And(cartprod_fm(2,A#+4,3),
   4.698                  And(upair_fm(2,2,1),
   4.699                      And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))"
   4.700  
   4.701  lemma sum_type [TC]:
   4.702       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
   4.703 -by (simp add: sum_fm_def) 
   4.704 +by (simp add: sum_fm_def)
   4.705  
   4.706  lemma arity_sum_fm [simp]:
   4.707 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   4.708 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   4.709        ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   4.710 -by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac) 
   4.711 +by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac)
   4.712  
   4.713  lemma sats_sum_fm [simp]:
   4.714     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   4.715 -    ==> sats(A, sum_fm(x,y,z), env) <-> 
   4.716 +    ==> sats(A, sum_fm(x,y,z), env) <->
   4.717          is_sum(**A, nth(x,env), nth(y,env), nth(z,env))"
   4.718  by (simp add: sum_fm_def is_sum_def)
   4.719  
   4.720  lemma sum_iff_sats:
   4.721 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   4.722 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   4.723            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   4.724         ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
   4.725  by simp
   4.726  
   4.727  theorem sum_reflection:
   4.728 -     "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)), 
   4.729 +     "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)),
   4.730                 \<lambda>i x. is_sum(**Lset(i),f(x),g(x),h(x))]"
   4.731  apply (simp only: is_sum_def setclass_simps)
   4.732 -apply (intro FOL_reflections function_reflections cartprod_reflection)  
   4.733 +apply (intro FOL_reflections function_reflections cartprod_reflection)
   4.734  done
   4.735  
   4.736  
   4.737 @@ -570,11 +572,11 @@
   4.738  
   4.739  lemma quasinat_type [TC]:
   4.740       "x \<in> nat ==> quasinat_fm(x) \<in> formula"
   4.741 -by (simp add: quasinat_fm_def) 
   4.742 +by (simp add: quasinat_fm_def)
   4.743  
   4.744  lemma arity_quasinat_fm [simp]:
   4.745       "x \<in> nat ==> arity(quasinat_fm(x)) = succ(x)"
   4.746 -by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac) 
   4.747 +by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac)
   4.748  
   4.749  lemma sats_quasinat_fm [simp]:
   4.750     "[| x \<in> nat; env \<in> list(A)|]
   4.751 @@ -582,85 +584,85 @@
   4.752  by (simp add: quasinat_fm_def is_quasinat_def)
   4.753  
   4.754  lemma quasinat_iff_sats:
   4.755 -      "[| nth(i,env) = x; nth(j,env) = y; 
   4.756 +      "[| nth(i,env) = x; nth(j,env) = y;
   4.757            i \<in> nat; env \<in> list(A)|]
   4.758         ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)"
   4.759  by simp
   4.760  
   4.761  theorem quasinat_reflection:
   4.762 -     "REFLECTS[\<lambda>x. is_quasinat(L,f(x)), 
   4.763 +     "REFLECTS[\<lambda>x. is_quasinat(L,f(x)),
   4.764                 \<lambda>i x. is_quasinat(**Lset(i),f(x))]"
   4.765  apply (simp only: is_quasinat_def setclass_simps)
   4.766 -apply (intro FOL_reflections function_reflections)  
   4.767 +apply (intro FOL_reflections function_reflections)
   4.768  done
   4.769  
   4.770  
   4.771  subsubsection{*The Operator @{term is_nat_case}*}
   4.772  
   4.773  (* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
   4.774 -    "is_nat_case(M, a, is_b, k, z) == 
   4.775 +    "is_nat_case(M, a, is_b, k, z) ==
   4.776         (empty(M,k) --> z=a) &
   4.777         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   4.778         (is_quasinat(M,k) | empty(M,z))" *)
   4.779  text{*The formula @{term is_b} has free variables 1 and 0.*}
   4.780  constdefs is_nat_case_fm :: "[i, [i,i]=>i, i, i]=>i"
   4.781 - "is_nat_case_fm(a,is_b,k,z) == 
   4.782 + "is_nat_case_fm(a,is_b,k,z) ==
   4.783      And(Implies(empty_fm(k), Equal(z,a)),
   4.784 -        And(Forall(Implies(succ_fm(0,succ(k)), 
   4.785 +        And(Forall(Implies(succ_fm(0,succ(k)),
   4.786                     Forall(Implies(Equal(0,succ(succ(z))), is_b(1,0))))),
   4.787              Or(quasinat_fm(k), empty_fm(z))))"
   4.788  
   4.789  lemma is_nat_case_type [TC]:
   4.790 -     "[| is_b(1,0) \<in> formula;  
   4.791 -         x \<in> nat; y \<in> nat; z \<in> nat |] 
   4.792 +     "[| is_b(1,0) \<in> formula;
   4.793 +         x \<in> nat; y \<in> nat; z \<in> nat |]
   4.794        ==> is_nat_case_fm(x,is_b,y,z) \<in> formula"
   4.795 -by (simp add: is_nat_case_fm_def) 
   4.796 +by (simp add: is_nat_case_fm_def)
   4.797  
   4.798  lemma arity_is_nat_case_fm [simp]:
   4.799 -     "[| is_b(1,0) \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
   4.800 -      ==> arity(is_nat_case_fm(x,is_b,y,z)) = 
   4.801 -          succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(is_b(1,0)) #- 2)" 
   4.802 -apply (subgoal_tac "arity(is_b(1,0)) \<in> nat")  
   4.803 +     "[| is_b(1,0) \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
   4.804 +      ==> arity(is_nat_case_fm(x,is_b,y,z)) =
   4.805 +          succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(is_b(1,0)) #- 2)"
   4.806 +apply (subgoal_tac "arity(is_b(1,0)) \<in> nat")
   4.807  apply typecheck
   4.808  (*FIXME: could nat_diff_split work?*)
   4.809  apply (auto simp add: diff_def raw_diff_succ is_nat_case_fm_def nat_imp_quasinat
   4.810                   succ_Un_distrib [symmetric] Un_ac
   4.811 -                 split: split_nat_case) 
   4.812 +                 split: split_nat_case)
   4.813  done
   4.814  
   4.815  lemma sats_is_nat_case_fm:
   4.816 -  assumes is_b_iff_sats: 
   4.817 -      "!!a b. [| a \<in> A; b \<in> A|] 
   4.818 +  assumes is_b_iff_sats:
   4.819 +      "!!a b. [| a \<in> A; b \<in> A|]
   4.820                ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))"
   4.821 -  shows 
   4.822 +  shows
   4.823        "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   4.824 -       ==> sats(A, is_nat_case_fm(x,p,y,z), env) <-> 
   4.825 +       ==> sats(A, is_nat_case_fm(x,p,y,z), env) <->
   4.826             is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))"
   4.827 -apply (frule lt_length_in_nat, assumption)  
   4.828 +apply (frule lt_length_in_nat, assumption)
   4.829  apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym])
   4.830  done
   4.831  
   4.832  lemma is_nat_case_iff_sats:
   4.833 -  "[| (!!a b. [| a \<in> A; b \<in> A|] 
   4.834 +  "[| (!!a b. [| a \<in> A; b \<in> A|]
   4.835                ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env))));
   4.836 -      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   4.837 +      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   4.838        i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   4.839 -   ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)" 
   4.840 +   ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)"
   4.841  by (simp add: sats_is_nat_case_fm [of A is_b])
   4.842  
   4.843  
   4.844  text{*The second argument of @{term is_b} gives it direct access to @{term x},
   4.845 -  which is essential for handling free variable references.  Without this 
   4.846 +  which is essential for handling free variable references.  Without this
   4.847    argument, we cannot prove reflection for @{term iterates_MH}.*}
   4.848  theorem is_nat_case_reflection:
   4.849    assumes is_b_reflection:
   4.850 -    "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)), 
   4.851 +    "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)),
   4.852                       \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
   4.853 -  shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)), 
   4.854 +  shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),
   4.855                 \<lambda>i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]"
   4.856  apply (simp (no_asm_use) only: is_nat_case_def setclass_simps)
   4.857 -apply (intro FOL_reflections function_reflections 
   4.858 -             restriction_reflection is_b_reflection quasinat_reflection)  
   4.859 +apply (intro FOL_reflections function_reflections
   4.860 +             restriction_reflection is_b_reflection quasinat_reflection)
   4.861  done
   4.862  
   4.863  
   4.864 @@ -672,117 +674,117 @@
   4.865          is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
   4.866                      n, z)" *)
   4.867  constdefs iterates_MH_fm :: "[[i,i]=>i, i, i, i, i]=>i"
   4.868 - "iterates_MH_fm(isF,v,n,g,z) == 
   4.869 -    is_nat_case_fm(v, 
   4.870 -      \<lambda>m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0), 
   4.871 -                     Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))), 
   4.872 + "iterates_MH_fm(isF,v,n,g,z) ==
   4.873 +    is_nat_case_fm(v,
   4.874 +      \<lambda>m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0),
   4.875 +                     Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))),
   4.876        n, z)"
   4.877  
   4.878  lemma iterates_MH_type [TC]:
   4.879 -     "[| p(1,0) \<in> formula;  
   4.880 -         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] 
   4.881 +     "[| p(1,0) \<in> formula;
   4.882 +         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
   4.883        ==> iterates_MH_fm(p,v,x,y,z) \<in> formula"
   4.884 -by (simp add: iterates_MH_fm_def) 
   4.885 +by (simp add: iterates_MH_fm_def)
   4.886  
   4.887  
   4.888  lemma arity_iterates_MH_fm [simp]:
   4.889 -     "[| p(1,0) \<in> formula; 
   4.890 -         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] 
   4.891 -      ==> arity(iterates_MH_fm(p,v,x,y,z)) = 
   4.892 +     "[| p(1,0) \<in> formula;
   4.893 +         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
   4.894 +      ==> arity(iterates_MH_fm(p,v,x,y,z)) =
   4.895            succ(v) \<union> succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(p(1,0)) #- 4)"
   4.896  apply (subgoal_tac "arity(p(1,0)) \<in> nat")
   4.897  apply typecheck
   4.898  apply (simp add: nat_imp_quasinat iterates_MH_fm_def Un_ac
   4.899              split: split_nat_case, clarify)
   4.900  apply (rename_tac i j)
   4.901 -apply (drule eq_succ_imp_eq_m1, simp) 
   4.902 +apply (drule eq_succ_imp_eq_m1, simp)
   4.903  apply (drule eq_succ_imp_eq_m1, simp)
   4.904  apply (simp add: diff_Un_distrib succ_Un_distrib Un_ac diff_diff_left)
   4.905  done
   4.906  
   4.907  lemma sats_iterates_MH_fm:
   4.908 -  assumes is_F_iff_sats: 
   4.909 -      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|] 
   4.910 +  assumes is_F_iff_sats:
   4.911 +      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
   4.912                ==> is_F(a,b) <->
   4.913                    sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
   4.914 -  shows 
   4.915 +  shows
   4.916        "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   4.917 -       ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <-> 
   4.918 +       ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <->
   4.919             iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
   4.920 -by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm 
   4.921 +by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm
   4.922                is_F_iff_sats [symmetric])
   4.923  
   4.924  lemma iterates_MH_iff_sats:
   4.925 -  "[| (!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|] 
   4.926 +  "[| (!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
   4.927                ==> is_F(a,b) <->
   4.928                    sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env))))));
   4.929 -      nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   4.930 +      nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   4.931        i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   4.932 -   ==> iterates_MH(**A, is_F, v, x, y, z) <-> 
   4.933 +   ==> iterates_MH(**A, is_F, v, x, y, z) <->
   4.934         sats(A, iterates_MH_fm(p,i',i,j,k), env)"
   4.935 -apply (rule iff_sym) 
   4.936 -apply (rule iff_trans) 
   4.937 -apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all) 
   4.938 +apply (rule iff_sym)
   4.939 +apply (rule iff_trans)
   4.940 +apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all)
   4.941  done
   4.942  
   4.943  theorem iterates_MH_reflection:
   4.944    assumes p_reflection:
   4.945 -    "!!f g h. REFLECTS[\<lambda>x. p(L, f(x), g(x)), 
   4.946 +    "!!f g h. REFLECTS[\<lambda>x. p(L, f(x), g(x)),
   4.947                       \<lambda>i x. p(**Lset(i), f(x), g(x))]"
   4.948 - shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)), 
   4.949 + shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)),
   4.950                 \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i)), e(x), f(x), g(x), h(x))]"
   4.951  apply (simp (no_asm_use) only: iterates_MH_def)
   4.952  txt{*Must be careful: simplifying with @{text setclass_simps} above would
   4.953       change @{text "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> Lset(i)"}, when
   4.954       it would no longer match rule @{text is_nat_case_reflection}. *}
   4.955 -apply (rule is_nat_case_reflection) 
   4.956 +apply (rule is_nat_case_reflection)
   4.957  apply (simp (no_asm_use) only: setclass_simps)
   4.958  apply (intro FOL_reflections function_reflections is_nat_case_reflection
   4.959 -             restriction_reflection p_reflection)  
   4.960 +             restriction_reflection p_reflection)
   4.961  done
   4.962  
   4.963  
   4.964  
   4.965 -subsection{*@{term L} is Closed Under the Operator @{term list}*} 
   4.966 +subsection{*@{term L} is Closed Under the Operator @{term list}*}
   4.967  
   4.968  subsubsection{*The List Functor, Internalized*}
   4.969  
   4.970  constdefs list_functor_fm :: "[i,i,i]=>i"
   4.971 -(* "is_list_functor(M,A,X,Z) == 
   4.972 -        \<exists>n1[M]. \<exists>AX[M]. 
   4.973 +(* "is_list_functor(M,A,X,Z) ==
   4.974 +        \<exists>n1[M]. \<exists>AX[M].
   4.975           number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
   4.976 -    "list_functor_fm(A,X,Z) == 
   4.977 +    "list_functor_fm(A,X,Z) ==
   4.978         Exists(Exists(
   4.979 -	And(number1_fm(1),
   4.980 +        And(number1_fm(1),
   4.981              And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))"
   4.982  
   4.983  lemma list_functor_type [TC]:
   4.984       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
   4.985 -by (simp add: list_functor_fm_def) 
   4.986 +by (simp add: list_functor_fm_def)
   4.987  
   4.988  lemma arity_list_functor_fm [simp]:
   4.989 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   4.990 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   4.991        ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   4.992 -by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac) 
   4.993 +by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac)
   4.994  
   4.995  lemma sats_list_functor_fm [simp]:
   4.996     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   4.997 -    ==> sats(A, list_functor_fm(x,y,z), env) <-> 
   4.998 +    ==> sats(A, list_functor_fm(x,y,z), env) <->
   4.999          is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))"
  4.1000  by (simp add: list_functor_fm_def is_list_functor_def)
  4.1001  
  4.1002  lemma list_functor_iff_sats:
  4.1003 -  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
  4.1004 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  4.1005        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  4.1006     ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
  4.1007  by simp
  4.1008  
  4.1009  theorem list_functor_reflection:
  4.1010 -     "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)), 
  4.1011 +     "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)),
  4.1012                 \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
  4.1013  apply (simp only: is_list_functor_def setclass_simps)
  4.1014  apply (intro FOL_reflections number1_reflection
  4.1015 -             cartprod_reflection sum_reflection)  
  4.1016 +             cartprod_reflection sum_reflection)
  4.1017  done
  4.1018  
  4.1019  
  4.1020 @@ -793,29 +795,29 @@
  4.1021     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
  4.1022           is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)),
  4.1023      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
  4.1024 -         is_wfrec(**Lset(i), 
  4.1025 -                  iterates_MH(**Lset(i), 
  4.1026 +         is_wfrec(**Lset(i),
  4.1027 +                  iterates_MH(**Lset(i),
  4.1028                            is_list_functor(**Lset(i), A), 0), memsn, u, y))]"
  4.1029 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  4.1030 -          iterates_MH_reflection list_functor_reflection) 
  4.1031 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  4.1032 +          iterates_MH_reflection list_functor_reflection)
  4.1033  
  4.1034 -lemma list_replacement1: 
  4.1035 +lemma list_replacement1:
  4.1036     "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
  4.1037  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
  4.1038 -apply (rule strong_replacementI) 
  4.1039 +apply (rule strong_replacementI)
  4.1040  apply (rule rallI)
  4.1041 -apply (rename_tac B)   
  4.1042 -apply (rule separation_CollectI) 
  4.1043 -apply (insert nonempty) 
  4.1044 -apply (subgoal_tac "L(Memrel(succ(n)))") 
  4.1045 -apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast ) 
  4.1046 +apply (rename_tac B)
  4.1047 +apply (rule separation_CollectI)
  4.1048 +apply (insert nonempty)
  4.1049 +apply (subgoal_tac "L(Memrel(succ(n)))")
  4.1050 +apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
  4.1051  apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
  4.1052 -apply (drule subset_Lset_ltD, assumption) 
  4.1053 +apply (drule subset_Lset_ltD, assumption)
  4.1054  apply (erule reflection_imp_L_separation)
  4.1055    apply (simp_all add: lt_Ord2 Memrel_closed)
  4.1056 -apply (elim conjE) 
  4.1057 +apply (elim conjE)
  4.1058  apply (rule DPow_LsetI)
  4.1059 -apply (rename_tac v) 
  4.1060 +apply (rename_tac v)
  4.1061  apply (rule bex_iff_sats conj_iff_sats)+
  4.1062  apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
  4.1063  apply (rule sep_rules | simp)+
  4.1064 @@ -832,34 +834,34 @@
  4.1065             is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0),
  4.1066                                msn, u, x)),
  4.1067      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
  4.1068 -         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
  4.1069 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
  4.1070            successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
  4.1071 -           is_wfrec (**Lset(i), 
  4.1072 +           is_wfrec (**Lset(i),
  4.1073                   iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0),
  4.1074                       msn, u, x))]"
  4.1075 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  4.1076 -          iterates_MH_reflection list_functor_reflection) 
  4.1077 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  4.1078 +          iterates_MH_reflection list_functor_reflection)
  4.1079  
  4.1080  
  4.1081 -lemma list_replacement2: 
  4.1082 -   "L(A) ==> strong_replacement(L, 
  4.1083 -         \<lambda>n y. n\<in>nat & 
  4.1084 +lemma list_replacement2:
  4.1085 +   "L(A) ==> strong_replacement(L,
  4.1086 +         \<lambda>n y. n\<in>nat &
  4.1087                 (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
  4.1088 -               is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), 
  4.1089 +               is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0),
  4.1090                          msn, n, y)))"
  4.1091 -apply (rule strong_replacementI) 
  4.1092 +apply (rule strong_replacementI)
  4.1093  apply (rule rallI)
  4.1094 -apply (rename_tac B)   
  4.1095 -apply (rule separation_CollectI) 
  4.1096 -apply (insert nonempty) 
  4.1097 -apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE) 
  4.1098 -apply (blast intro: L_nat) 
  4.1099 +apply (rename_tac B)
  4.1100 +apply (rule separation_CollectI)
  4.1101 +apply (insert nonempty)
  4.1102 +apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE)
  4.1103 +apply (blast intro: L_nat)
  4.1104  apply (rule ReflectsE [OF list_replacement2_Reflects], assumption)
  4.1105 -apply (drule subset_Lset_ltD, assumption) 
  4.1106 +apply (drule subset_Lset_ltD, assumption)
  4.1107  apply (erule reflection_imp_L_separation)
  4.1108    apply (simp_all add: lt_Ord2)
  4.1109  apply (rule DPow_LsetI)
  4.1110 -apply (rename_tac v) 
  4.1111 +apply (rename_tac v)
  4.1112  apply (rule bex_iff_sats conj_iff_sats)+
  4.1113  apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
  4.1114  apply (rule sep_rules | simp)+
  4.1115 @@ -868,21 +870,21 @@
  4.1116  done
  4.1117  
  4.1118  
  4.1119 -subsection{*@{term L} is Closed Under the Operator @{term formula}*} 
  4.1120 +subsection{*@{term L} is Closed Under the Operator @{term formula}*}
  4.1121  
  4.1122  subsubsection{*The Formula Functor, Internalized*}
  4.1123  
  4.1124  constdefs formula_functor_fm :: "[i,i]=>i"
  4.1125 -(*     "is_formula_functor(M,X,Z) == 
  4.1126 -        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. 
  4.1127 +(*     "is_formula_functor(M,X,Z) ==
  4.1128 +        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M].
  4.1129             4           3               2       1       0
  4.1130 -          omega(M,nat') & cartprod(M,nat',nat',natnat) & 
  4.1131 +          omega(M,nat') & cartprod(M,nat',nat',natnat) &
  4.1132            is_sum(M,natnat,natnat,natnatsum) &
  4.1133 -          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & 
  4.1134 -          is_sum(M,natnatsum,X3,Z)" *) 
  4.1135 -    "formula_functor_fm(X,Z) == 
  4.1136 +          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) &
  4.1137 +          is_sum(M,natnatsum,X3,Z)" *)
  4.1138 +    "formula_functor_fm(X,Z) ==
  4.1139         Exists(Exists(Exists(Exists(Exists(
  4.1140 -	And(omega_fm(4),
  4.1141 +        And(omega_fm(4),
  4.1142           And(cartprod_fm(4,4,3),
  4.1143            And(sum_fm(3,3,2),
  4.1144             And(cartprod_fm(X#+5,X#+5,1),
  4.1145 @@ -890,26 +892,26 @@
  4.1146  
  4.1147  lemma formula_functor_type [TC]:
  4.1148       "[| x \<in> nat; y \<in> nat |] ==> formula_functor_fm(x,y) \<in> formula"
  4.1149 -by (simp add: formula_functor_fm_def) 
  4.1150 +by (simp add: formula_functor_fm_def)
  4.1151  
  4.1152  lemma sats_formula_functor_fm [simp]:
  4.1153     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
  4.1154 -    ==> sats(A, formula_functor_fm(x,y), env) <-> 
  4.1155 +    ==> sats(A, formula_functor_fm(x,y), env) <->
  4.1156          is_formula_functor(**A, nth(x,env), nth(y,env))"
  4.1157  by (simp add: formula_functor_fm_def is_formula_functor_def)
  4.1158  
  4.1159  lemma formula_functor_iff_sats:
  4.1160 -  "[| nth(i,env) = x; nth(j,env) = y; 
  4.1161 +  "[| nth(i,env) = x; nth(j,env) = y;
  4.1162        i \<in> nat; j \<in> nat; env \<in> list(A)|]
  4.1163     ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
  4.1164  by simp
  4.1165  
  4.1166  theorem formula_functor_reflection:
  4.1167 -     "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)), 
  4.1168 +     "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)),
  4.1169                 \<lambda>i x. is_formula_functor(**Lset(i),f(x),g(x))]"
  4.1170  apply (simp only: is_formula_functor_def setclass_simps)
  4.1171  apply (intro FOL_reflections omega_reflection
  4.1172 -             cartprod_reflection sum_reflection)  
  4.1173 +             cartprod_reflection sum_reflection)
  4.1174  done
  4.1175  
  4.1176  subsubsection{*Instances of Replacement for Formulas*}
  4.1177 @@ -919,28 +921,28 @@
  4.1178     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
  4.1179           is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)),
  4.1180      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
  4.1181 -         is_wfrec(**Lset(i), 
  4.1182 -                  iterates_MH(**Lset(i), 
  4.1183 +         is_wfrec(**Lset(i),
  4.1184 +                  iterates_MH(**Lset(i),
  4.1185                            is_formula_functor(**Lset(i)), 0), memsn, u, y))]"
  4.1186 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  4.1187 -          iterates_MH_reflection formula_functor_reflection) 
  4.1188 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  4.1189 +          iterates_MH_reflection formula_functor_reflection)
  4.1190  
  4.1191 -lemma formula_replacement1: 
  4.1192 +lemma formula_replacement1:
  4.1193     "iterates_replacement(L, is_formula_functor(L), 0)"
  4.1194  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
  4.1195 -apply (rule strong_replacementI) 
  4.1196 +apply (rule strong_replacementI)
  4.1197  apply (rule rallI)
  4.1198 -apply (rename_tac B)   
  4.1199 -apply (rule separation_CollectI) 
  4.1200 -apply (insert nonempty) 
  4.1201 -apply (subgoal_tac "L(Memrel(succ(n)))") 
  4.1202 -apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast ) 
  4.1203 +apply (rename_tac B)
  4.1204 +apply (rule separation_CollectI)
  4.1205 +apply (insert nonempty)
  4.1206 +apply (subgoal_tac "L(Memrel(succ(n)))")
  4.1207 +apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
  4.1208  apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption)
  4.1209 -apply (drule subset_Lset_ltD, assumption) 
  4.1210 +apply (drule subset_Lset_ltD, assumption)
  4.1211  apply (erule reflection_imp_L_separation)
  4.1212    apply (simp_all add: lt_Ord2 Memrel_closed)
  4.1213  apply (rule DPow_LsetI)
  4.1214 -apply (rename_tac v) 
  4.1215 +apply (rename_tac v)
  4.1216  apply (rule bex_iff_sats conj_iff_sats)+
  4.1217  apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
  4.1218  apply (rule sep_rules | simp)+
  4.1219 @@ -957,34 +959,34 @@
  4.1220             is_wfrec (L, iterates_MH (L, is_formula_functor(L), 0),
  4.1221                                msn, u, x)),
  4.1222      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
  4.1223 -         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
  4.1224 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
  4.1225            successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
  4.1226 -           is_wfrec (**Lset(i), 
  4.1227 +           is_wfrec (**Lset(i),
  4.1228                   iterates_MH (**Lset(i), is_formula_functor(**Lset(i)), 0),
  4.1229                       msn, u, x))]"
  4.1230 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  4.1231 -          iterates_MH_reflection formula_functor_reflection) 
  4.1232 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  4.1233 +          iterates_MH_reflection formula_functor_reflection)
  4.1234  
  4.1235  
  4.1236 -lemma formula_replacement2: 
  4.1237 -   "strong_replacement(L, 
  4.1238 -         \<lambda>n y. n\<in>nat & 
  4.1239 +lemma formula_replacement2:
  4.1240 +   "strong_replacement(L,
  4.1241 +         \<lambda>n y. n\<in>nat &
  4.1242                 (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
  4.1243 -               is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0), 
  4.1244 +               is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0),
  4.1245                          msn, n, y)))"
  4.1246 -apply (rule strong_replacementI) 
  4.1247 +apply (rule strong_replacementI)
  4.1248  apply (rule rallI)
  4.1249 -apply (rename_tac B)   
  4.1250 -apply (rule separation_CollectI) 
  4.1251 -apply (insert nonempty) 
  4.1252 -apply (rule_tac A="{B,z,0,nat}" in subset_LsetE) 
  4.1253 -apply (blast intro: L_nat) 
  4.1254 +apply (rename_tac B)
  4.1255 +apply (rule separation_CollectI)
  4.1256 +apply (insert nonempty)
  4.1257 +apply (rule_tac A="{B,z,0,nat}" in subset_LsetE)
  4.1258 +apply (blast intro: L_nat)
  4.1259  apply (rule ReflectsE [OF formula_replacement2_Reflects], assumption)
  4.1260 -apply (drule subset_Lset_ltD, assumption) 
  4.1261 +apply (drule subset_Lset_ltD, assumption)
  4.1262  apply (erule reflection_imp_L_separation)
  4.1263    apply (simp_all add: lt_Ord2)
  4.1264  apply (rule DPow_LsetI)
  4.1265 -apply (rename_tac v) 
  4.1266 +apply (rename_tac v)
  4.1267  apply (rule bex_iff_sats conj_iff_sats)+
  4.1268  apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats)
  4.1269  apply (rule sep_rules | simp)+
  4.1270 @@ -1006,7 +1008,7 @@
  4.1271  
  4.1272  lemma Inl_type [TC]:
  4.1273       "[| x \<in> nat; z \<in> nat |] ==> Inl_fm(x,z) \<in> formula"
  4.1274 -by (simp add: Inl_fm_def) 
  4.1275 +by (simp add: Inl_fm_def)
  4.1276  
  4.1277  lemma sats_Inl_fm [simp]:
  4.1278     "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
  4.1279 @@ -1014,16 +1016,16 @@
  4.1280  by (simp add: Inl_fm_def is_Inl_def)
  4.1281  
  4.1282  lemma Inl_iff_sats:
  4.1283 -      "[| nth(i,env) = x; nth(k,env) = z; 
  4.1284 +      "[| nth(i,env) = x; nth(k,env) = z;
  4.1285            i \<in> nat; k \<in> nat; env \<in> list(A)|]
  4.1286         ==> is_Inl(**A, x, z) <-> sats(A, Inl_fm(i,k), env)"
  4.1287  by simp
  4.1288  
  4.1289  theorem Inl_reflection:
  4.1290 -     "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)), 
  4.1291 +     "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)),
  4.1292                 \<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
  4.1293  apply (simp only: is_Inl_def setclass_simps)
  4.1294 -apply (intro FOL_reflections function_reflections)  
  4.1295 +apply (intro FOL_reflections function_reflections)
  4.1296  done
  4.1297  
  4.1298  
  4.1299 @@ -1035,7 +1037,7 @@
  4.1300  
  4.1301  lemma Inr_type [TC]:
  4.1302       "[| x \<in> nat; z \<in> nat |] ==> Inr_fm(x,z) \<in> formula"
  4.1303 -by (simp add: Inr_fm_def) 
  4.1304 +by (simp add: Inr_fm_def)
  4.1305  
  4.1306  lemma sats_Inr_fm [simp]:
  4.1307     "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
  4.1308 @@ -1043,16 +1045,16 @@
  4.1309  by (simp add: Inr_fm_def is_Inr_def)
  4.1310  
  4.1311  lemma Inr_iff_sats:
  4.1312 -      "[| nth(i,env) = x; nth(k,env) = z; 
  4.1313 +      "[| nth(i,env) = x; nth(k,env) = z;
  4.1314            i \<in> nat; k \<in> nat; env \<in> list(A)|]
  4.1315         ==> is_Inr(**A, x, z) <-> sats(A, Inr_fm(i,k), env)"
  4.1316  by simp
  4.1317  
  4.1318  theorem Inr_reflection:
  4.1319 -     "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)), 
  4.1320 +     "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)),
  4.1321                 \<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
  4.1322  apply (simp only: is_Inr_def setclass_simps)
  4.1323 -apply (intro FOL_reflections function_reflections)  
  4.1324 +apply (intro FOL_reflections function_reflections)
  4.1325  done
  4.1326  
  4.1327  
  4.1328 @@ -1062,9 +1064,9 @@
  4.1329  
  4.1330  constdefs Nil_fm :: "i=>i"
  4.1331      "Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
  4.1332 - 
  4.1333 +
  4.1334  lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
  4.1335 -by (simp add: Nil_fm_def) 
  4.1336 +by (simp add: Nil_fm_def)
  4.1337  
  4.1338  lemma sats_Nil_fm [simp]:
  4.1339     "[| x \<in> nat; env \<in> list(A)|]
  4.1340 @@ -1077,10 +1079,10 @@
  4.1341  by simp
  4.1342  
  4.1343  theorem Nil_reflection:
  4.1344 -     "REFLECTS[\<lambda>x. is_Nil(L,f(x)), 
  4.1345 +     "REFLECTS[\<lambda>x. is_Nil(L,f(x)),
  4.1346                 \<lambda>i x. is_Nil(**Lset(i),f(x))]"
  4.1347  apply (simp only: is_Nil_def setclass_simps)
  4.1348 -apply (intro FOL_reflections function_reflections Inl_reflection)  
  4.1349 +apply (intro FOL_reflections function_reflections Inl_reflection)
  4.1350  done
  4.1351  
  4.1352  
  4.1353 @@ -1089,30 +1091,30 @@
  4.1354  
  4.1355  (*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
  4.1356  constdefs Cons_fm :: "[i,i,i]=>i"
  4.1357 -    "Cons_fm(a,l,Z) == 
  4.1358 +    "Cons_fm(a,l,Z) ==
  4.1359         Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
  4.1360  
  4.1361  lemma Cons_type [TC]:
  4.1362       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Cons_fm(x,y,z) \<in> formula"
  4.1363 -by (simp add: Cons_fm_def) 
  4.1364 +by (simp add: Cons_fm_def)
  4.1365  
  4.1366  lemma sats_Cons_fm [simp]:
  4.1367     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  4.1368 -    ==> sats(A, Cons_fm(x,y,z), env) <-> 
  4.1369 +    ==> sats(A, Cons_fm(x,y,z), env) <->
  4.1370         is_Cons(**A, nth(x,env), nth(y,env), nth(z,env))"
  4.1371  by (simp add: Cons_fm_def is_Cons_def)
  4.1372  
  4.1373  lemma Cons_iff_sats:
  4.1374 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
  4.1375 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  4.1376            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  4.1377         ==>is_Cons(**A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
  4.1378  by simp
  4.1379  
  4.1380  theorem Cons_reflection:
  4.1381 -     "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)), 
  4.1382 +     "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)),
  4.1383                 \<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
  4.1384  apply (simp only: is_Cons_def setclass_simps)
  4.1385 -apply (intro FOL_reflections pair_reflection Inr_reflection)  
  4.1386 +apply (intro FOL_reflections pair_reflection Inr_reflection)
  4.1387  done
  4.1388  
  4.1389  subsubsection{*The Formula @{term is_quasilist}, Internalized*}
  4.1390 @@ -1120,11 +1122,11 @@
  4.1391  (* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
  4.1392  
  4.1393  constdefs quasilist_fm :: "i=>i"
  4.1394 -    "quasilist_fm(x) == 
  4.1395 +    "quasilist_fm(x) ==
  4.1396         Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
  4.1397 - 
  4.1398 +
  4.1399  lemma quasilist_type [TC]: "x \<in> nat ==> quasilist_fm(x) \<in> formula"
  4.1400 -by (simp add: quasilist_fm_def) 
  4.1401 +by (simp add: quasilist_fm_def)
  4.1402  
  4.1403  lemma sats_quasilist_fm [simp]:
  4.1404     "[| x \<in> nat; env \<in> list(A)|]
  4.1405 @@ -1137,10 +1139,10 @@
  4.1406  by simp
  4.1407  
  4.1408  theorem quasilist_reflection:
  4.1409 -     "REFLECTS[\<lambda>x. is_quasilist(L,f(x)), 
  4.1410 +     "REFLECTS[\<lambda>x. is_quasilist(L,f(x)),
  4.1411                 \<lambda>i x. is_quasilist(**Lset(i),f(x))]"
  4.1412  apply (simp only: is_quasilist_def setclass_simps)
  4.1413 -apply (intro FOL_reflections Nil_reflection Cons_reflection)  
  4.1414 +apply (intro FOL_reflections Nil_reflection Cons_reflection)
  4.1415  done
  4.1416  
  4.1417  
  4.1418 @@ -1149,19 +1151,19 @@
  4.1419  
  4.1420  subsubsection{*The Formula @{term is_tl}, Internalized*}
  4.1421  
  4.1422 -(*     "is_tl(M,xs,T) == 
  4.1423 +(*     "is_tl(M,xs,T) ==
  4.1424         (is_Nil(M,xs) --> T=xs) &
  4.1425         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
  4.1426         (is_quasilist(M,xs) | empty(M,T))" *)
  4.1427  constdefs tl_fm :: "[i,i]=>i"
  4.1428 -    "tl_fm(xs,T) == 
  4.1429 +    "tl_fm(xs,T) ==
  4.1430         And(Implies(Nil_fm(xs), Equal(T,xs)),
  4.1431             And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
  4.1432                 Or(quasilist_fm(xs), empty_fm(T))))"
  4.1433  
  4.1434  lemma tl_type [TC]:
  4.1435       "[| x \<in> nat; y \<in> nat |] ==> tl_fm(x,y) \<in> formula"
  4.1436 -by (simp add: tl_fm_def) 
  4.1437 +by (simp add: tl_fm_def)
  4.1438  
  4.1439  lemma sats_tl_fm [simp]:
  4.1440     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
  4.1441 @@ -1175,11 +1177,11 @@
  4.1442  by simp
  4.1443  
  4.1444  theorem tl_reflection:
  4.1445 -     "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)), 
  4.1446 +     "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)),
  4.1447                 \<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
  4.1448  apply (simp only: is_tl_def setclass_simps)
  4.1449  apply (intro FOL_reflections Nil_reflection Cons_reflection
  4.1450 -             quasilist_reflection empty_reflection)  
  4.1451 +             quasilist_reflection empty_reflection)
  4.1452  done
  4.1453  
  4.1454  
  4.1455 @@ -1190,27 +1192,27 @@
  4.1456     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
  4.1457           is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
  4.1458      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
  4.1459 -         is_wfrec(**Lset(i), 
  4.1460 -                  iterates_MH(**Lset(i), 
  4.1461 +         is_wfrec(**Lset(i),
  4.1462 +                  iterates_MH(**Lset(i),
  4.1463                            is_tl(**Lset(i)), z), memsn, u, y))]"
  4.1464 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  4.1465 -          iterates_MH_reflection list_functor_reflection tl_reflection) 
  4.1466 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  4.1467 +          iterates_MH_reflection list_functor_reflection tl_reflection)
  4.1468  
  4.1469 -lemma nth_replacement: 
  4.1470 +lemma nth_replacement:
  4.1471     "L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)"
  4.1472  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
  4.1473 -apply (rule strong_replacementI) 
  4.1474 -apply (rule rallI)   
  4.1475 -apply (rule separation_CollectI) 
  4.1476 -apply (subgoal_tac "L(Memrel(succ(n)))") 
  4.1477 -apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
  4.1478 +apply (rule strong_replacementI)
  4.1479 +apply (rule rallI)
  4.1480 +apply (rule separation_CollectI)
  4.1481 +apply (subgoal_tac "L(Memrel(succ(n)))")
  4.1482 +apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast )
  4.1483  apply (rule ReflectsE [OF nth_replacement_Reflects], assumption)
  4.1484 -apply (drule subset_Lset_ltD, assumption) 
  4.1485 +apply (drule subset_Lset_ltD, assumption)
  4.1486  apply (erule reflection_imp_L_separation)
  4.1487    apply (simp_all add: lt_Ord2 Memrel_closed)
  4.1488 -apply (elim conjE) 
  4.1489 +apply (elim conjE)
  4.1490  apply (rule DPow_LsetI)
  4.1491 -apply (rename_tac v) 
  4.1492 +apply (rename_tac v)
  4.1493  apply (rule bex_iff_sats conj_iff_sats)+
  4.1494  apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats)
  4.1495  apply (rule sep_rules | simp)+
  4.1496 @@ -1221,27 +1223,29 @@
  4.1497  
  4.1498  
  4.1499  subsubsection{*Instantiating the locale @{text M_datatypes}*}
  4.1500 -ML
  4.1501 -{*
  4.1502 -val list_replacement1 = thm "list_replacement1"; 
  4.1503 -val list_replacement2 = thm "list_replacement2";
  4.1504 -val formula_replacement1 = thm "formula_replacement1";
  4.1505 -val formula_replacement2 = thm "formula_replacement2";
  4.1506 -val nth_replacement = thm "nth_replacement";
  4.1507 +
  4.1508 +theorem M_datatypes_axioms_L: "M_datatypes_axioms(L)"
  4.1509 +  apply (rule M_datatypes_axioms.intro)
  4.1510 +      apply (assumption | rule
  4.1511 +        list_replacement1 list_replacement2
  4.1512 +        formula_replacement1 formula_replacement2
  4.1513 +        nth_replacement)+
  4.1514 +  done
  4.1515  
  4.1516 -val m_datatypes = [list_replacement1, list_replacement2, 
  4.1517 -                   formula_replacement1, formula_replacement2, 
  4.1518 -                   nth_replacement];
  4.1519 -
  4.1520 -fun datatypes_L th =
  4.1521 -    kill_flex_triv_prems (m_datatypes MRS (wfrank_L th));
  4.1522 +theorem M_datatypes_L: "PROP M_datatypes(L)"
  4.1523 +  apply (rule M_datatypes.intro)
  4.1524 +      apply (rule M_triv_axioms_L)
  4.1525 +     apply (rule M_axioms_axioms_L)
  4.1526 +    apply (rule M_trancl_axioms_L)
  4.1527 +   apply (rule M_wfrank_axioms_L)
  4.1528 +  apply (rule M_datatypes_axioms_L)
  4.1529 +  done
  4.1530  
  4.1531 -bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
  4.1532 -bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
  4.1533 -bind_thm ("list_abs", datatypes_L (thm "M_datatypes.list_abs"));
  4.1534 -bind_thm ("formula_abs", datatypes_L (thm "M_datatypes.formula_abs"));
  4.1535 -bind_thm ("nth_abs", datatypes_L (thm "M_datatypes.nth_abs"));
  4.1536 -*}
  4.1537 +lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
  4.1538 +  and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L]
  4.1539 +  and list_abs = M_datatypes.list_abs [OF M_datatypes_L]
  4.1540 +  and formula_abs = M_datatypes.formula_abs [OF M_datatypes_L]
  4.1541 +  and nth_abs = M_datatypes.nth_abs [OF M_datatypes_L]
  4.1542  
  4.1543  declare list_closed [intro,simp]
  4.1544  declare formula_closed [intro,simp]
  4.1545 @@ -1250,8 +1254,7 @@
  4.1546  declare nth_abs [simp]
  4.1547  
  4.1548  
  4.1549 -
  4.1550 -subsection{*@{term L} is Closed Under the Operator @{term eclose}*} 
  4.1551 +subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
  4.1552  
  4.1553  subsubsection{*Instances of Replacement for @{term eclose}*}
  4.1554  
  4.1555 @@ -1260,28 +1263,28 @@
  4.1556     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
  4.1557           is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
  4.1558      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
  4.1559 -         is_wfrec(**Lset(i), 
  4.1560 -                  iterates_MH(**Lset(i), big_union(**Lset(i)), A), 
  4.1561 +         is_wfrec(**Lset(i),
  4.1562 +                  iterates_MH(**Lset(i), big_union(**Lset(i)), A),
  4.1563                    memsn, u, y))]"
  4.1564 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  4.1565 -          iterates_MH_reflection) 
  4.1566 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  4.1567 +          iterates_MH_reflection)
  4.1568  
  4.1569 -lemma eclose_replacement1: 
  4.1570 +lemma eclose_replacement1:
  4.1571     "L(A) ==> iterates_replacement(L, big_union(L), A)"
  4.1572  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
  4.1573 -apply (rule strong_replacementI) 
  4.1574 +apply (rule strong_replacementI)
  4.1575  apply (rule rallI)
  4.1576 -apply (rename_tac B)   
  4.1577 -apply (rule separation_CollectI) 
  4.1578 -apply (subgoal_tac "L(Memrel(succ(n)))") 
  4.1579 -apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
  4.1580 +apply (rename_tac B)
  4.1581 +apply (rule separation_CollectI)
  4.1582 +apply (subgoal_tac "L(Memrel(succ(n)))")
  4.1583 +apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast )
  4.1584  apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
  4.1585 -apply (drule subset_Lset_ltD, assumption) 
  4.1586 +apply (drule subset_Lset_ltD, assumption)
  4.1587  apply (erule reflection_imp_L_separation)
  4.1588    apply (simp_all add: lt_Ord2 Memrel_closed)
  4.1589 -apply (elim conjE) 
  4.1590 +apply (elim conjE)
  4.1591  apply (rule DPow_LsetI)
  4.1592 -apply (rename_tac v) 
  4.1593 +apply (rename_tac v)
  4.1594  apply (rule bex_iff_sats conj_iff_sats)+
  4.1595  apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
  4.1596  apply (rule sep_rules | simp)+
  4.1597 @@ -1298,33 +1301,33 @@
  4.1598             is_wfrec (L, iterates_MH (L, big_union(L), A),
  4.1599                                msn, u, x)),
  4.1600      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
  4.1601 -         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
  4.1602 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
  4.1603            successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
  4.1604 -           is_wfrec (**Lset(i), 
  4.1605 +           is_wfrec (**Lset(i),
  4.1606                   iterates_MH (**Lset(i), big_union(**Lset(i)), A),
  4.1607                       msn, u, x))]"
  4.1608 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  4.1609 -          iterates_MH_reflection) 
  4.1610 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  4.1611 +          iterates_MH_reflection)
  4.1612  
  4.1613  
  4.1614 -lemma eclose_replacement2: 
  4.1615 -   "L(A) ==> strong_replacement(L, 
  4.1616 -         \<lambda>n y. n\<in>nat & 
  4.1617 +lemma eclose_replacement2:
  4.1618 +   "L(A) ==> strong_replacement(L,
  4.1619 +         \<lambda>n y. n\<in>nat &
  4.1620                 (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
  4.1621 -               is_wfrec(L, iterates_MH(L,big_union(L), A), 
  4.1622 +               is_wfrec(L, iterates_MH(L,big_union(L), A),
  4.1623                          msn, n, y)))"
  4.1624 -apply (rule strong_replacementI) 
  4.1625 +apply (rule strong_replacementI)
  4.1626  apply (rule rallI)
  4.1627 -apply (rename_tac B)   
  4.1628 -apply (rule separation_CollectI) 
  4.1629 -apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) 
  4.1630 -apply (blast intro: L_nat) 
  4.1631 +apply (rename_tac B)
  4.1632 +apply (rule separation_CollectI)
  4.1633 +apply (rule_tac A="{A,B,z,nat}" in subset_LsetE)
  4.1634 +apply (blast intro: L_nat)
  4.1635  apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
  4.1636 -apply (drule subset_Lset_ltD, assumption) 
  4.1637 +apply (drule subset_Lset_ltD, assumption)
  4.1638  apply (erule reflection_imp_L_separation)
  4.1639    apply (simp_all add: lt_Ord2)
  4.1640  apply (rule DPow_LsetI)
  4.1641 -apply (rename_tac v) 
  4.1642 +apply (rename_tac v)
  4.1643  apply (rule bex_iff_sats conj_iff_sats)+
  4.1644  apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
  4.1645  apply (rule sep_rules | simp)+
  4.1646 @@ -1334,22 +1337,23 @@
  4.1647  
  4.1648  
  4.1649  subsubsection{*Instantiating the locale @{text M_eclose}*}
  4.1650 -ML
  4.1651 -{*
  4.1652 -val eclose_replacement1 = thm "eclose_replacement1"; 
  4.1653 -val eclose_replacement2 = thm "eclose_replacement2";
  4.1654  
  4.1655 -val m_eclose = [eclose_replacement1, eclose_replacement2];
  4.1656 +theorem M_eclose_axioms_L: "M_eclose_axioms(L)"
  4.1657 +  apply (rule M_eclose_axioms.intro)
  4.1658 +   apply (assumption | rule eclose_replacement1 eclose_replacement2)+
  4.1659 +  done
  4.1660  
  4.1661 -fun eclose_L th =
  4.1662 -    kill_flex_triv_prems (m_eclose MRS (datatypes_L th));
  4.1663 +theorem M_eclose_L: "PROP M_eclose(L)"
  4.1664 +  apply (rule M_eclose.intro)
  4.1665 +       apply (rule M_triv_axioms_L)
  4.1666 +      apply (rule M_axioms_axioms_L)
  4.1667 +     apply (rule M_trancl_axioms_L)
  4.1668 +    apply (rule M_wfrank_axioms_L)
  4.1669 +   apply (rule M_datatypes_axioms_L)
  4.1670 +  apply (rule M_eclose_axioms_L)
  4.1671 +  done
  4.1672  
  4.1673 -bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed"));
  4.1674 -bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs"));
  4.1675 -*}
  4.1676 -
  4.1677 -declare eclose_closed [intro,simp]
  4.1678 -declare eclose_abs [intro,simp]
  4.1679 -
  4.1680 +lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]
  4.1681 +  and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L]
  4.1682  
  4.1683  end
     5.1 --- a/src/ZF/Constructible/Reflection.thy	Sun Jul 28 21:09:37 2002 +0200
     5.2 +++ b/src/ZF/Constructible/Reflection.thy	Mon Jul 29 00:57:16 2002 +0200
     5.3 @@ -25,7 +25,7 @@
     5.4  ultimately the @{text ex_reflection} proof is packaged up using the
     5.5  predicate @{text Reflects}.
     5.6  *}
     5.7 -locale (open) reflection =
     5.8 +locale reflection =
     5.9    fixes Mset and M and Reflects
    5.10    assumes Mset_mono_le : "mono_le_subset(Mset)"
    5.11        and Mset_cont    : "cont_Ord(Mset)"
    5.12 @@ -124,7 +124,7 @@
    5.13  
    5.14  text{*Locale for the induction hypothesis*}
    5.15  
    5.16 -locale (open) ex_reflection = reflection +
    5.17 +locale ex_reflection = reflection +
    5.18    fixes P  --"the original formula"
    5.19    fixes Q  --"the reflected formula"
    5.20    fixes Cl --"the class of reflecting ordinals"
    5.21 @@ -170,16 +170,19 @@
    5.22          !!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x) |] 
    5.23        ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
    5.24  apply (unfold ClEx_def FF_def F0_def M_def)
    5.25 -apply (rule Reflection.ZF_ClEx_iff [of Mset Cl], 
    5.26 -       simp_all add: Mset_mono_le Mset_cont Pair_in_Mset)
    5.27 +apply (rule ex_reflection.ZF_ClEx_iff
    5.28 +  [OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro,
    5.29 +    of Mset Cl])
    5.30 +apply (simp_all add: Mset_mono_le Mset_cont Pair_in_Mset)
    5.31  done
    5.32  
    5.33  lemma (in reflection) Closed_Unbounded_ClEx:
    5.34       "(!!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x))
    5.35        ==> Closed_Unbounded(ClEx(P))"
    5.36  apply (unfold ClEx_def FF_def F0_def M_def)
    5.37 -apply (rule Reflection.ZF_Closed_Unbounded_ClEx, 
    5.38 -       simp_all add: Mset_mono_le Mset_cont Pair_in_Mset) 
    5.39 +apply (rule ex_reflection.ZF_Closed_Unbounded_ClEx
    5.40 +  [OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro])
    5.41 +apply (simp_all add: Mset_mono_le Mset_cont Pair_in_Mset) 
    5.42  done
    5.43  
    5.44  subsection{*Packaging the Quantifier Reflection Rules*}
     6.1 --- a/src/ZF/Constructible/Relative.thy	Sun Jul 28 21:09:37 2002 +0200
     6.2 +++ b/src/ZF/Constructible/Relative.thy	Mon Jul 29 00:57:16 2002 +0200
     6.3 @@ -448,7 +448,7 @@
     6.4  
     6.5  text{*The class M is assumed to be transitive and to satisfy some
     6.6        relativized ZF axioms*}
     6.7 -locale (open) M_triv_axioms =
     6.8 +locale M_triv_axioms =
     6.9    fixes M
    6.10    assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
    6.11        and nonempty [simp]:  "M(0)"
    6.12 @@ -821,7 +821,7 @@
    6.13       "M(a) ==> number1(M,a) <-> a = 1"
    6.14  by (simp add: number1_def) 
    6.15  
    6.16 -lemma (in M_triv_axioms) number1_abs [simp]: 
    6.17 +lemma (in M_triv_axioms) number2_abs [simp]: 
    6.18       "M(a) ==> number2(M,a) <-> a = succ(1)"
    6.19  by (simp add: number2_def) 
    6.20  
    6.21 @@ -854,7 +854,7 @@
    6.22  
    6.23  subsection{*Some instances of separation and strong replacement*}
    6.24  
    6.25 -locale (open) M_axioms = M_triv_axioms +
    6.26 +locale M_axioms = M_triv_axioms +
    6.27  assumes Inter_separation:
    6.28       "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
    6.29    and cartprod_separation:
     7.1 --- a/src/ZF/Constructible/Separation.thy	Sun Jul 28 21:09:37 2002 +0200
     7.2 +++ b/src/ZF/Constructible/Separation.thy	Mon Jul 29 00:57:16 2002 +0200
     7.3 @@ -9,39 +9,39 @@
     7.4  by simp
     7.5  
     7.6  lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI
     7.7 -lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats 
     7.8 +lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats
     7.9                     fun_plus_iff_sats
    7.10  
    7.11  lemma Collect_conj_in_DPow:
    7.12 -     "[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |] 
    7.13 +     "[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |]
    7.14        ==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)"
    7.15 -by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric]) 
    7.16 +by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric])
    7.17  
    7.18  lemma Collect_conj_in_DPow_Lset:
    7.19       "[|z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))|]
    7.20        ==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> DPow(Lset(j))"
    7.21  apply (frule mem_Lset_imp_subset_Lset)
    7.22 -apply (simp add: Collect_conj_in_DPow Collect_mem_eq 
    7.23 +apply (simp add: Collect_conj_in_DPow Collect_mem_eq
    7.24                   subset_Int_iff2 elem_subset_in_DPow)
    7.25  done
    7.26  
    7.27  lemma separation_CollectI:
    7.28       "(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))"
    7.29 -apply (unfold separation_def, clarify) 
    7.30 -apply (rule_tac x="{x\<in>z. P(x)}" in rexI) 
    7.31 +apply (unfold separation_def, clarify)
    7.32 +apply (rule_tac x="{x\<in>z. P(x)}" in rexI)
    7.33  apply simp_all
    7.34  done
    7.35  
    7.36  text{*Reduces the original comprehension to the reflected one*}
    7.37  lemma reflection_imp_L_separation:
    7.38        "[| \<forall>x\<in>Lset(j). P(x) <-> Q(x);
    7.39 -          {x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j)); 
    7.40 +          {x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j));
    7.41            Ord(j);  z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})"
    7.42  apply (rule_tac i = "succ(j)" in L_I)
    7.43   prefer 2 apply simp
    7.44  apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> z & (Q(x))}")
    7.45   prefer 2
    7.46 - apply (blast dest: mem_Lset_imp_subset_Lset) 
    7.47 + apply (blast dest: mem_Lset_imp_subset_Lset)
    7.48  apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)
    7.49  done
    7.50  
    7.51 @@ -49,20 +49,20 @@
    7.52  subsection{*Separation for Intersection*}
    7.53  
    7.54  lemma Inter_Reflects:
    7.55 -     "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y, 
    7.56 +     "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y,
    7.57                 \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y]"
    7.58 -by (intro FOL_reflections)  
    7.59 +by (intro FOL_reflections)
    7.60  
    7.61  lemma Inter_separation:
    7.62       "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
    7.63 -apply (rule separation_CollectI) 
    7.64 -apply (rule_tac A="{A,z}" in subset_LsetE, blast ) 
    7.65 +apply (rule separation_CollectI)
    7.66 +apply (rule_tac A="{A,z}" in subset_LsetE, blast )
    7.67  apply (rule ReflectsE [OF Inter_Reflects], assumption)
    7.68 -apply (drule subset_Lset_ltD, assumption) 
    7.69 +apply (drule subset_Lset_ltD, assumption)
    7.70  apply (erule reflection_imp_L_separation)
    7.71    apply (simp_all add: lt_Ord2, clarify)
    7.72 -apply (rule DPow_LsetI) 
    7.73 -apply (rule ball_iff_sats) 
    7.74 +apply (rule DPow_LsetI)
    7.75 +apply (rule ball_iff_sats)
    7.76  apply (rule imp_iff_sats)
    7.77  apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)
    7.78  apply (rule_tac i=0 and j=2 in mem_iff_sats)
    7.79 @@ -73,22 +73,22 @@
    7.80  
    7.81  lemma cartprod_Reflects:
    7.82       "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
    7.83 -                \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B & 
    7.84 +                \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &
    7.85                                     pair(**Lset(i),x,y,z))]"
    7.86  by (intro FOL_reflections function_reflections)
    7.87  
    7.88  lemma cartprod_separation:
    7.89 -     "[| L(A); L(B) |] 
    7.90 +     "[| L(A); L(B) |]
    7.91        ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
    7.92 -apply (rule separation_CollectI) 
    7.93 -apply (rule_tac A="{A,B,z}" in subset_LsetE, blast ) 
    7.94 +apply (rule separation_CollectI)
    7.95 +apply (rule_tac A="{A,B,z}" in subset_LsetE, blast )
    7.96  apply (rule ReflectsE [OF cartprod_Reflects], assumption)
    7.97 -apply (drule subset_Lset_ltD, assumption) 
    7.98 +apply (drule subset_Lset_ltD, assumption)
    7.99  apply (erule reflection_imp_L_separation)
   7.100 -  apply (simp_all add: lt_Ord2, clarify) 
   7.101 +  apply (simp_all add: lt_Ord2, clarify)
   7.102  apply (rule DPow_LsetI)
   7.103 -apply (rename_tac u)  
   7.104 -apply (rule bex_iff_sats) 
   7.105 +apply (rename_tac u)
   7.106 +apply (rule bex_iff_sats)
   7.107  apply (rule conj_iff_sats)
   7.108  apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
   7.109  apply (rule sep_rules | simp)+
   7.110 @@ -102,16 +102,16 @@
   7.111  by (intro FOL_reflections function_reflections)
   7.112  
   7.113  lemma image_separation:
   7.114 -     "[| L(A); L(r) |] 
   7.115 +     "[| L(A); L(r) |]
   7.116        ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
   7.117 -apply (rule separation_CollectI) 
   7.118 -apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) 
   7.119 +apply (rule separation_CollectI)
   7.120 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
   7.121  apply (rule ReflectsE [OF image_Reflects], assumption)
   7.122 -apply (drule subset_Lset_ltD, assumption) 
   7.123 +apply (drule subset_Lset_ltD, assumption)
   7.124  apply (erule reflection_imp_L_separation)
   7.125    apply (simp_all add: lt_Ord2, clarify)
   7.126  apply (rule DPow_LsetI)
   7.127 -apply (rule bex_iff_sats) 
   7.128 +apply (rule bex_iff_sats)
   7.129  apply (rule conj_iff_sats)
   7.130  apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
   7.131  apply (rule sep_rules | simp)+
   7.132 @@ -122,22 +122,22 @@
   7.133  
   7.134  lemma converse_Reflects:
   7.135    "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
   7.136 -     \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). 
   7.137 +     \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i).
   7.138                       pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]"
   7.139  by (intro FOL_reflections function_reflections)
   7.140  
   7.141  lemma converse_separation:
   7.142 -     "L(r) ==> separation(L, 
   7.143 +     "L(r) ==> separation(L,
   7.144           \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
   7.145 -apply (rule separation_CollectI) 
   7.146 -apply (rule_tac A="{r,z}" in subset_LsetE, blast ) 
   7.147 +apply (rule separation_CollectI)
   7.148 +apply (rule_tac A="{r,z}" in subset_LsetE, blast )
   7.149  apply (rule ReflectsE [OF converse_Reflects], assumption)
   7.150 -apply (drule subset_Lset_ltD, assumption) 
   7.151 +apply (drule subset_Lset_ltD, assumption)
   7.152  apply (erule reflection_imp_L_separation)
   7.153    apply (simp_all add: lt_Ord2, clarify)
   7.154  apply (rule DPow_LsetI)
   7.155 -apply (rename_tac u) 
   7.156 -apply (rule bex_iff_sats) 
   7.157 +apply (rename_tac u)
   7.158 +apply (rule bex_iff_sats)
   7.159  apply (rule conj_iff_sats)
   7.160  apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all)
   7.161  apply (rule sep_rules | simp)+
   7.162 @@ -153,15 +153,15 @@
   7.163  
   7.164  lemma restrict_separation:
   7.165     "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
   7.166 -apply (rule separation_CollectI) 
   7.167 -apply (rule_tac A="{A,z}" in subset_LsetE, blast ) 
   7.168 +apply (rule separation_CollectI)
   7.169 +apply (rule_tac A="{A,z}" in subset_LsetE, blast )
   7.170  apply (rule ReflectsE [OF restrict_Reflects], assumption)
   7.171 -apply (drule subset_Lset_ltD, assumption) 
   7.172 +apply (drule subset_Lset_ltD, assumption)
   7.173  apply (erule reflection_imp_L_separation)
   7.174    apply (simp_all add: lt_Ord2, clarify)
   7.175  apply (rule DPow_LsetI)
   7.176 -apply (rename_tac u) 
   7.177 -apply (rule bex_iff_sats) 
   7.178 +apply (rename_tac u)
   7.179 +apply (rule bex_iff_sats)
   7.180  apply (rule conj_iff_sats)
   7.181  apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all)
   7.182  apply (rule sep_rules | simp)+
   7.183 @@ -171,29 +171,29 @@
   7.184  subsection{*Separation for Composition*}
   7.185  
   7.186  lemma comp_Reflects:
   7.187 -     "REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. 
   7.188 -		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & 
   7.189 +     "REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
   7.190 +                  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
   7.191                    xy\<in>s & yz\<in>r,
   7.192 -        \<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i). 
   7.193 -		  pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) & 
   7.194 +        \<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i).
   7.195 +                  pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) &
   7.196                    pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
   7.197  by (intro FOL_reflections function_reflections)
   7.198  
   7.199  lemma comp_separation:
   7.200       "[| L(r); L(s) |]
   7.201 -      ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. 
   7.202 -		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & 
   7.203 +      ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
   7.204 +                  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
   7.205                    xy\<in>s & yz\<in>r)"
   7.206 -apply (rule separation_CollectI) 
   7.207 -apply (rule_tac A="{r,s,z}" in subset_LsetE, blast ) 
   7.208 +apply (rule separation_CollectI)
   7.209 +apply (rule_tac A="{r,s,z}" in subset_LsetE, blast )
   7.210  apply (rule ReflectsE [OF comp_Reflects], assumption)
   7.211 -apply (drule subset_Lset_ltD, assumption) 
   7.212 +apply (drule subset_Lset_ltD, assumption)
   7.213  apply (erule reflection_imp_L_separation)
   7.214    apply (simp_all add: lt_Ord2, clarify)
   7.215  apply (rule DPow_LsetI)
   7.216 -apply (rename_tac u) 
   7.217 +apply (rename_tac u)
   7.218  apply (rule bex_iff_sats)+
   7.219 -apply (rename_tac x y z)  
   7.220 +apply (rename_tac x y z)
   7.221  apply (rule conj_iff_sats)
   7.222  apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
   7.223  apply (rule sep_rules | simp)+
   7.224 @@ -208,17 +208,17 @@
   7.225  
   7.226  lemma pred_separation:
   7.227       "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
   7.228 -apply (rule separation_CollectI) 
   7.229 -apply (rule_tac A="{r,x,z}" in subset_LsetE, blast ) 
   7.230 +apply (rule separation_CollectI)
   7.231 +apply (rule_tac A="{r,x,z}" in subset_LsetE, blast )
   7.232  apply (rule ReflectsE [OF pred_Reflects], assumption)
   7.233 -apply (drule subset_Lset_ltD, assumption) 
   7.234 +apply (drule subset_Lset_ltD, assumption)
   7.235  apply (erule reflection_imp_L_separation)
   7.236    apply (simp_all add: lt_Ord2, clarify)
   7.237  apply (rule DPow_LsetI)
   7.238 -apply (rename_tac u) 
   7.239 +apply (rename_tac u)
   7.240  apply (rule bex_iff_sats)
   7.241  apply (rule conj_iff_sats)
   7.242 -apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats) 
   7.243 +apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats)
   7.244  apply (rule sep_rules | simp)+
   7.245  done
   7.246  
   7.247 @@ -232,50 +232,50 @@
   7.248  
   7.249  lemma Memrel_separation:
   7.250       "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
   7.251 -apply (rule separation_CollectI) 
   7.252 -apply (rule_tac A="{z}" in subset_LsetE, blast ) 
   7.253 +apply (rule separation_CollectI)
   7.254 +apply (rule_tac A="{z}" in subset_LsetE, blast )
   7.255  apply (rule ReflectsE [OF Memrel_Reflects], assumption)
   7.256 -apply (drule subset_Lset_ltD, assumption) 
   7.257 +apply (drule subset_Lset_ltD, assumption)
   7.258  apply (erule reflection_imp_L_separation)
   7.259    apply (simp_all add: lt_Ord2)
   7.260  apply (rule DPow_LsetI)
   7.261 -apply (rename_tac u) 
   7.262 +apply (rename_tac u)
   7.263  apply (rule bex_iff_sats conj_iff_sats)+
   7.264 -apply (rule_tac env = "[y,x,u]" in pair_iff_sats) 
   7.265 +apply (rule_tac env = "[y,x,u]" in pair_iff_sats)
   7.266  apply (rule sep_rules | simp)+
   7.267  done
   7.268  
   7.269  
   7.270  subsection{*Replacement for FunSpace*}
   7.271 -		
   7.272 +
   7.273  lemma funspace_succ_Reflects:
   7.274 - "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. 
   7.275 -	    pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
   7.276 -	    upair(L,cnbf,cnbf,z)),
   7.277 -	\<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i). 
   7.278 -	      \<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i). 
   7.279 -		pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) & 
   7.280 -		is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]"
   7.281 + "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L].
   7.282 +            pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
   7.283 +            upair(L,cnbf,cnbf,z)),
   7.284 +        \<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i).
   7.285 +              \<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i).
   7.286 +                pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) &
   7.287 +                is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]"
   7.288  by (intro FOL_reflections function_reflections)
   7.289  
   7.290  lemma funspace_succ_replacement:
   7.291 -     "L(n) ==> 
   7.292 -      strong_replacement(L, \<lambda>p z. \<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. 
   7.293 +     "L(n) ==>
   7.294 +      strong_replacement(L, \<lambda>p z. \<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L].
   7.295                  pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
   7.296                  upair(L,cnbf,cnbf,z))"
   7.297 -apply (rule strong_replacementI) 
   7.298 -apply (rule rallI) 
   7.299 -apply (rule separation_CollectI) 
   7.300 -apply (rule_tac A="{n,A,z}" in subset_LsetE, blast ) 
   7.301 +apply (rule strong_replacementI)
   7.302 +apply (rule rallI)
   7.303 +apply (rule separation_CollectI)
   7.304 +apply (rule_tac A="{n,A,z}" in subset_LsetE, blast )
   7.305  apply (rule ReflectsE [OF funspace_succ_Reflects], assumption)
   7.306 -apply (drule subset_Lset_ltD, assumption) 
   7.307 +apply (drule subset_Lset_ltD, assumption)
   7.308  apply (erule reflection_imp_L_separation)
   7.309    apply (simp_all add: lt_Ord2)
   7.310  apply (rule DPow_LsetI)
   7.311 -apply (rename_tac u) 
   7.312 +apply (rename_tac u)
   7.313  apply (rule bex_iff_sats)
   7.314  apply (rule conj_iff_sats)
   7.315 -apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats) 
   7.316 +apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats)
   7.317  apply (rule sep_rules | simp)+
   7.318  done
   7.319  
   7.320 @@ -283,26 +283,26 @@
   7.321  subsection{*Separation for Order-Isomorphisms*}
   7.322  
   7.323  lemma well_ord_iso_Reflects:
   7.324 -  "REFLECTS[\<lambda>x. x\<in>A --> 
   7.325 +  "REFLECTS[\<lambda>x. x\<in>A -->
   7.326                  (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
   7.327 -        \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i). 
   7.328 +        \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i).
   7.329                  fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]"
   7.330  by (intro FOL_reflections function_reflections)
   7.331  
   7.332  lemma well_ord_iso_separation:
   7.333 -     "[| L(A); L(f); L(r) |] 
   7.334 -      ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L]. 
   7.335 -		     fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
   7.336 -apply (rule separation_CollectI) 
   7.337 -apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast ) 
   7.338 +     "[| L(A); L(f); L(r) |]
   7.339 +      ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L].
   7.340 +                     fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
   7.341 +apply (rule separation_CollectI)
   7.342 +apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast )
   7.343  apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption)
   7.344 -apply (drule subset_Lset_ltD, assumption) 
   7.345 +apply (drule subset_Lset_ltD, assumption)
   7.346  apply (erule reflection_imp_L_separation)
   7.347    apply (simp_all add: lt_Ord2)
   7.348  apply (rule DPow_LsetI)
   7.349 -apply (rename_tac u) 
   7.350 +apply (rename_tac u)
   7.351  apply (rule imp_iff_sats)
   7.352 -apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats) 
   7.353 +apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats)
   7.354  apply (rule sep_rules | simp)+
   7.355  done
   7.356  
   7.357 @@ -310,31 +310,31 @@
   7.358  subsection{*Separation for @{term "obase"}*}
   7.359  
   7.360  lemma obase_reflects:
   7.361 -  "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. 
   7.362 -	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   7.363 -	     order_isomorphism(L,par,r,x,mx,g),
   7.364 -        \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i). 
   7.365 -	     ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
   7.366 -	     order_isomorphism(**Lset(i),par,r,x,mx,g)]"
   7.367 +  "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   7.368 +             ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   7.369 +             order_isomorphism(L,par,r,x,mx,g),
   7.370 +        \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i).
   7.371 +             ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
   7.372 +             order_isomorphism(**Lset(i),par,r,x,mx,g)]"
   7.373  by (intro FOL_reflections function_reflections fun_plus_reflections)
   7.374  
   7.375  lemma obase_separation:
   7.376       --{*part of the order type formalization*}
   7.377 -     "[| L(A); L(r) |] 
   7.378 -      ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. 
   7.379 -	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   7.380 -	     order_isomorphism(L,par,r,x,mx,g))"
   7.381 -apply (rule separation_CollectI) 
   7.382 -apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) 
   7.383 +     "[| L(A); L(r) |]
   7.384 +      ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   7.385 +             ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   7.386 +             order_isomorphism(L,par,r,x,mx,g))"
   7.387 +apply (rule separation_CollectI)
   7.388 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
   7.389  apply (rule ReflectsE [OF obase_reflects], assumption)
   7.390 -apply (drule subset_Lset_ltD, assumption) 
   7.391 +apply (drule subset_Lset_ltD, assumption)
   7.392  apply (erule reflection_imp_L_separation)
   7.393    apply (simp_all add: lt_Ord2)
   7.394  apply (rule DPow_LsetI)
   7.395 -apply (rename_tac u) 
   7.396 +apply (rename_tac u)
   7.397  apply (rule bex_iff_sats)
   7.398  apply (rule conj_iff_sats)
   7.399 -apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats) 
   7.400 +apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats)
   7.401  apply (rule sep_rules | simp)+
   7.402  done
   7.403  
   7.404 @@ -342,33 +342,33 @@
   7.405  subsection{*Separation for a Theorem about @{term "obase"}*}
   7.406  
   7.407  lemma obase_equals_reflects:
   7.408 -  "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L]. 
   7.409 -		ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. 
   7.410 -		membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   7.411 -		order_isomorphism(L,pxr,r,y,my,g))),
   7.412 -	\<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i). 
   7.413 -		ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i). 
   7.414 -		membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
   7.415 -		order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
   7.416 +  "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
   7.417 +                ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
   7.418 +                membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   7.419 +                order_isomorphism(L,pxr,r,y,my,g))),
   7.420 +        \<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i).
   7.421 +                ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
   7.422 +                membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
   7.423 +                order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
   7.424  by (intro FOL_reflections function_reflections fun_plus_reflections)
   7.425  
   7.426  
   7.427  lemma obase_equals_separation:
   7.428 -     "[| L(A); L(r) |] 
   7.429 -      ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L]. 
   7.430 -			      ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. 
   7.431 -			      membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   7.432 -			      order_isomorphism(L,pxr,r,y,my,g))))"
   7.433 -apply (rule separation_CollectI) 
   7.434 -apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) 
   7.435 +     "[| L(A); L(r) |]
   7.436 +      ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
   7.437 +                              ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
   7.438 +                              membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   7.439 +                              order_isomorphism(L,pxr,r,y,my,g))))"
   7.440 +apply (rule separation_CollectI)
   7.441 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
   7.442  apply (rule ReflectsE [OF obase_equals_reflects], assumption)
   7.443 -apply (drule subset_Lset_ltD, assumption) 
   7.444 +apply (drule subset_Lset_ltD, assumption)
   7.445  apply (erule reflection_imp_L_separation)
   7.446    apply (simp_all add: lt_Ord2)
   7.447  apply (rule DPow_LsetI)
   7.448 -apply (rename_tac u) 
   7.449 +apply (rename_tac u)
   7.450  apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
   7.451 -apply (rule_tac env = "[u,A,r]" in mem_iff_sats) 
   7.452 +apply (rule_tac env = "[u,A,r]" in mem_iff_sats)
   7.453  apply (rule sep_rules | simp)+
   7.454  done
   7.455  
   7.456 @@ -376,35 +376,35 @@
   7.457  subsection{*Replacement for @{term "omap"}*}
   7.458  
   7.459  lemma omap_reflects:
   7.460 - "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. 
   7.461 -     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & 
   7.462 + "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   7.463 +     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
   7.464       pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)),
   7.465 - \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). 
   7.466 -        \<exists>par \<in> Lset(i). 
   7.467 -	 ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) & 
   7.468 -         membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & 
   7.469 + \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i).
   7.470 +        \<exists>par \<in> Lset(i).
   7.471 +         ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) &
   7.472 +         membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
   7.473           order_isomorphism(**Lset(i),par,r,x,mx,g))]"
   7.474  by (intro FOL_reflections function_reflections fun_plus_reflections)
   7.475  
   7.476  lemma omap_replacement:
   7.477 -     "[| L(A); L(r) |] 
   7.478 +     "[| L(A); L(r) |]
   7.479        ==> strong_replacement(L,
   7.480 -             \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. 
   7.481 -	     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & 
   7.482 -	     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
   7.483 -apply (rule strong_replacementI) 
   7.484 +             \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   7.485 +             ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
   7.486 +             pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
   7.487 +apply (rule strong_replacementI)
   7.488  apply (rule rallI)
   7.489 -apply (rename_tac B)  
   7.490 -apply (rule separation_CollectI) 
   7.491 -apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast ) 
   7.492 +apply (rename_tac B)
   7.493 +apply (rule separation_CollectI)
   7.494 +apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast )
   7.495  apply (rule ReflectsE [OF omap_reflects], assumption)
   7.496 -apply (drule subset_Lset_ltD, assumption) 
   7.497 +apply (drule subset_Lset_ltD, assumption)
   7.498  apply (erule reflection_imp_L_separation)
   7.499    apply (simp_all add: lt_Ord2)
   7.500  apply (rule DPow_LsetI)
   7.501 -apply (rename_tac u) 
   7.502 +apply (rename_tac u)
   7.503  apply (rule bex_iff_sats conj_iff_sats)+
   7.504 -apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats) 
   7.505 +apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats)
   7.506  apply (rule sep_rules | simp)+
   7.507  done
   7.508  
   7.509 @@ -412,34 +412,34 @@
   7.510  subsection{*Separation for a Theorem about @{term "obase"}*}
   7.511  
   7.512  lemma is_recfun_reflects:
   7.513 -  "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L]. 
   7.514 -                pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & 
   7.515 -                (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & 
   7.516 +  "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L].
   7.517 +                pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
   7.518 +                (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
   7.519                                     fx \<noteq> gx),
   7.520 -   \<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i). 
   7.521 +   \<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i).
   7.522            pair(**Lset(i),x,a,xa) & xa \<in> r & pair(**Lset(i),x,b,xb) & xb \<in> r &
   7.523 -                (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(**Lset(i),f,x,fx) & 
   7.524 +                (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(**Lset(i),f,x,fx) &
   7.525                    fun_apply(**Lset(i),g,x,gx) & fx \<noteq> gx)]"
   7.526  by (intro FOL_reflections function_reflections fun_plus_reflections)
   7.527  
   7.528  lemma is_recfun_separation:
   7.529       --{*for well-founded recursion*}
   7.530 -     "[| L(r); L(f); L(g); L(a); L(b) |] 
   7.531 -     ==> separation(L, 
   7.532 -            \<lambda>x. \<exists>xa[L]. \<exists>xb[L]. 
   7.533 -                pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & 
   7.534 -                (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & 
   7.535 +     "[| L(r); L(f); L(g); L(a); L(b) |]
   7.536 +     ==> separation(L,
   7.537 +            \<lambda>x. \<exists>xa[L]. \<exists>xb[L].
   7.538 +                pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
   7.539 +                (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
   7.540                                     fx \<noteq> gx))"
   7.541 -apply (rule separation_CollectI) 
   7.542 -apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast ) 
   7.543 +apply (rule separation_CollectI)
   7.544 +apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast )
   7.545  apply (rule ReflectsE [OF is_recfun_reflects], assumption)
   7.546 -apply (drule subset_Lset_ltD, assumption) 
   7.547 +apply (drule subset_Lset_ltD, assumption)
   7.548  apply (erule reflection_imp_L_separation)
   7.549    apply (simp_all add: lt_Ord2)
   7.550  apply (rule DPow_LsetI)
   7.551 -apply (rename_tac u) 
   7.552 +apply (rename_tac u)
   7.553  apply (rule bex_iff_sats conj_iff_sats)+
   7.554 -apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats) 
   7.555 +apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats)
   7.556  apply (rule sep_rules | simp)+
   7.557  done
   7.558  
   7.559 @@ -448,144 +448,128 @@
   7.560  text{*Separation (and Strong Replacement) for basic set-theoretic constructions
   7.561  such as intersection, Cartesian Product and image.*}
   7.562  
   7.563 -ML
   7.564 -{*
   7.565 -val Inter_separation = thm "Inter_separation";
   7.566 -val cartprod_separation = thm "cartprod_separation";
   7.567 -val image_separation = thm "image_separation";
   7.568 -val converse_separation = thm "converse_separation";
   7.569 -val restrict_separation = thm "restrict_separation";
   7.570 -val comp_separation = thm "comp_separation";
   7.571 -val pred_separation = thm "pred_separation";
   7.572 -val Memrel_separation = thm "Memrel_separation";
   7.573 -val funspace_succ_replacement = thm "funspace_succ_replacement";
   7.574 -val well_ord_iso_separation = thm "well_ord_iso_separation";
   7.575 -val obase_separation = thm "obase_separation";
   7.576 -val obase_equals_separation = thm "obase_equals_separation";
   7.577 -val omap_replacement = thm "omap_replacement";
   7.578 -val is_recfun_separation = thm "is_recfun_separation";
   7.579 -
   7.580 -val m_axioms = 
   7.581 -    [Inter_separation, cartprod_separation, image_separation, 
   7.582 -     converse_separation, restrict_separation, comp_separation, 
   7.583 -     pred_separation, Memrel_separation, funspace_succ_replacement, 
   7.584 -     well_ord_iso_separation, obase_separation,
   7.585 -     obase_equals_separation, omap_replacement, is_recfun_separation]
   7.586 -
   7.587 -fun axioms_L th =
   7.588 -    kill_flex_triv_prems (m_axioms MRS (triv_axioms_L th));
   7.589 +theorem M_axioms_axioms_L: "M_axioms_axioms(L)"
   7.590 +  apply (rule M_axioms_axioms.intro)
   7.591 +               apply (assumption | rule
   7.592 +                 Inter_separation cartprod_separation image_separation
   7.593 +                 converse_separation restrict_separation
   7.594 +                 comp_separation pred_separation Memrel_separation
   7.595 +                 funspace_succ_replacement well_ord_iso_separation
   7.596 +                 obase_separation obase_equals_separation
   7.597 +                 omap_replacement is_recfun_separation)+
   7.598 +  done
   7.599 +  
   7.600 +theorem M_axioms_L: "PROP M_axioms(L)"
   7.601 +  apply (rule M_axioms.intro)
   7.602 +   apply (rule M_triv_axioms_L)
   7.603 +  apply (rule M_axioms_axioms_L)
   7.604 +  done
   7.605  
   7.606 -bind_thm ("cartprod_iff", axioms_L (thm "M_axioms.cartprod_iff"));
   7.607 -bind_thm ("cartprod_closed", axioms_L (thm "M_axioms.cartprod_closed"));
   7.608 -bind_thm ("sum_closed", axioms_L (thm "M_axioms.sum_closed"));
   7.609 -bind_thm ("M_converse_iff", axioms_L (thm "M_axioms.M_converse_iff"));
   7.610 -bind_thm ("converse_closed", axioms_L (thm "M_axioms.converse_closed"));
   7.611 -bind_thm ("converse_abs", axioms_L (thm "M_axioms.converse_abs"));
   7.612 -bind_thm ("image_closed", axioms_L (thm "M_axioms.image_closed"));
   7.613 -bind_thm ("vimage_abs", axioms_L (thm "M_axioms.vimage_abs"));
   7.614 -bind_thm ("vimage_closed", axioms_L (thm "M_axioms.vimage_closed"));
   7.615 -bind_thm ("domain_abs", axioms_L (thm "M_axioms.domain_abs"));
   7.616 -bind_thm ("domain_closed", axioms_L (thm "M_axioms.domain_closed"));
   7.617 -bind_thm ("range_abs", axioms_L (thm "M_axioms.range_abs"));
   7.618 -bind_thm ("range_closed", axioms_L (thm "M_axioms.range_closed"));
   7.619 -bind_thm ("field_abs", axioms_L (thm "M_axioms.field_abs"));
   7.620 -bind_thm ("field_closed", axioms_L (thm "M_axioms.field_closed"));
   7.621 -bind_thm ("relation_abs", axioms_L (thm "M_axioms.relation_abs"));
   7.622 -bind_thm ("function_abs", axioms_L (thm "M_axioms.function_abs"));
   7.623 -bind_thm ("apply_closed", axioms_L (thm "M_axioms.apply_closed"));
   7.624 -bind_thm ("apply_abs", axioms_L (thm "M_axioms.apply_abs"));
   7.625 -bind_thm ("typed_function_abs", axioms_L (thm "M_axioms.typed_function_abs"));
   7.626 -bind_thm ("injection_abs", axioms_L (thm "M_axioms.injection_abs"));
   7.627 -bind_thm ("surjection_abs", axioms_L (thm "M_axioms.surjection_abs"));
   7.628 -bind_thm ("bijection_abs", axioms_L (thm "M_axioms.bijection_abs"));
   7.629 -bind_thm ("M_comp_iff", axioms_L (thm "M_axioms.M_comp_iff"));
   7.630 -bind_thm ("comp_closed", axioms_L (thm "M_axioms.comp_closed"));
   7.631 -bind_thm ("composition_abs", axioms_L (thm "M_axioms.composition_abs"));
   7.632 -bind_thm ("restriction_is_function", axioms_L (thm "M_axioms.restriction_is_function"));
   7.633 -bind_thm ("restriction_abs", axioms_L (thm "M_axioms.restriction_abs"));
   7.634 -bind_thm ("M_restrict_iff", axioms_L (thm "M_axioms.M_restrict_iff"));
   7.635 -bind_thm ("restrict_closed", axioms_L (thm "M_axioms.restrict_closed"));
   7.636 -bind_thm ("Inter_abs", axioms_L (thm "M_axioms.Inter_abs"));
   7.637 -bind_thm ("Inter_closed", axioms_L (thm "M_axioms.Inter_closed"));
   7.638 -bind_thm ("Int_closed", axioms_L (thm "M_axioms.Int_closed"));
   7.639 -bind_thm ("finite_fun_closed", axioms_L (thm "M_axioms.finite_fun_closed"));
   7.640 -bind_thm ("is_funspace_abs", axioms_L (thm "M_axioms.is_funspace_abs"));
   7.641 -bind_thm ("succ_fun_eq2", axioms_L (thm "M_axioms.succ_fun_eq2"));
   7.642 -bind_thm ("funspace_succ", axioms_L (thm "M_axioms.funspace_succ"));
   7.643 -bind_thm ("finite_funspace_closed", axioms_L (thm "M_axioms.finite_funspace_closed"));
   7.644 -*}
   7.645 +lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L]
   7.646 +  and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L]
   7.647 +  and sum_closed = M_axioms.sum_closed [OF M_axioms_L]
   7.648 +  and M_converse_iff = M_axioms.M_converse_iff [OF M_axioms_L]
   7.649 +  and converse_closed = M_axioms.converse_closed [OF M_axioms_L]
   7.650 +  and converse_abs = M_axioms.converse_abs [OF M_axioms_L]
   7.651 +  and image_closed = M_axioms.image_closed [OF M_axioms_L]
   7.652 +  and vimage_abs = M_axioms.vimage_abs [OF M_axioms_L]
   7.653 +  and vimage_closed = M_axioms.vimage_closed [OF M_axioms_L]
   7.654 +  and domain_abs = M_axioms.domain_abs [OF M_axioms_L]
   7.655 +  and domain_closed = M_axioms.domain_closed [OF M_axioms_L]
   7.656 +  and range_abs = M_axioms.range_abs [OF M_axioms_L]
   7.657 +  and range_closed = M_axioms.range_closed [OF M_axioms_L]
   7.658 +  and field_abs = M_axioms.field_abs [OF M_axioms_L]
   7.659 +  and field_closed = M_axioms.field_closed [OF M_axioms_L]
   7.660 +  and relation_abs = M_axioms.relation_abs [OF M_axioms_L]
   7.661 +  and function_abs = M_axioms.function_abs [OF M_axioms_L]
   7.662 +  and apply_closed = M_axioms.apply_closed [OF M_axioms_L]
   7.663 +  and apply_abs = M_axioms.apply_abs [OF M_axioms_L]
   7.664 +  and typed_function_abs = M_axioms.typed_function_abs [OF M_axioms_L]
   7.665 +  and injection_abs = M_axioms.injection_abs [OF M_axioms_L]
   7.666 +  and surjection_abs = M_axioms.surjection_abs [OF M_axioms_L]
   7.667 +  and bijection_abs = M_axioms.bijection_abs [OF M_axioms_L]
   7.668 +  and M_comp_iff = M_axioms.M_comp_iff [OF M_axioms_L]
   7.669 +  and comp_closed = M_axioms.comp_closed [OF M_axioms_L]
   7.670 +  and composition_abs = M_axioms.composition_abs [OF M_axioms_L]
   7.671 +  and restriction_is_function = M_axioms.restriction_is_function [OF M_axioms_L]
   7.672 +  and restriction_abs = M_axioms.restriction_abs [OF M_axioms_L]
   7.673 +  and M_restrict_iff = M_axioms.M_restrict_iff [OF M_axioms_L]
   7.674 +  and restrict_closed = M_axioms.restrict_closed [OF M_axioms_L]
   7.675 +  and Inter_abs = M_axioms.Inter_abs [OF M_axioms_L]
   7.676 +  and Inter_closed = M_axioms.Inter_closed [OF M_axioms_L]
   7.677 +  and Int_closed = M_axioms.Int_closed [OF M_axioms_L]
   7.678 +  and finite_fun_closed = M_axioms.finite_fun_closed [OF M_axioms_L]
   7.679 +  and is_funspace_abs = M_axioms.is_funspace_abs [OF M_axioms_L]
   7.680 +  and succ_fun_eq2 = M_axioms.succ_fun_eq2 [OF M_axioms_L]
   7.681 +  and funspace_succ = M_axioms.funspace_succ [OF M_axioms_L]
   7.682 +  and finite_funspace_closed = M_axioms.finite_funspace_closed [OF M_axioms_L]
   7.683  
   7.684 -ML
   7.685 -{*
   7.686 -bind_thm ("is_recfun_equal", axioms_L (thm "M_axioms.is_recfun_equal"));  
   7.687 -bind_thm ("is_recfun_cut", axioms_L (thm "M_axioms.is_recfun_cut")); 
   7.688 -bind_thm ("is_recfun_functional", axioms_L (thm "M_axioms.is_recfun_functional"));
   7.689 -bind_thm ("is_recfun_relativize", axioms_L (thm "M_axioms.is_recfun_relativize"));
   7.690 -bind_thm ("is_recfun_restrict", axioms_L (thm "M_axioms.is_recfun_restrict"));
   7.691 -bind_thm ("univalent_is_recfun", axioms_L (thm "M_axioms.univalent_is_recfun"));
   7.692 -bind_thm ("exists_is_recfun_indstep", axioms_L (thm "M_axioms.exists_is_recfun_indstep"));
   7.693 -bind_thm ("wellfounded_exists_is_recfun", axioms_L (thm "M_axioms.wellfounded_exists_is_recfun"));
   7.694 -bind_thm ("wf_exists_is_recfun", axioms_L (thm "M_axioms.wf_exists_is_recfun")); 
   7.695 -bind_thm ("is_recfun_abs", axioms_L (thm "M_axioms.is_recfun_abs"));
   7.696 -bind_thm ("irreflexive_abs", axioms_L (thm "M_axioms.irreflexive_abs"));  
   7.697 -bind_thm ("transitive_rel_abs", axioms_L (thm "M_axioms.transitive_rel_abs"));  
   7.698 -bind_thm ("linear_rel_abs", axioms_L (thm "M_axioms.linear_rel_abs"));  
   7.699 -bind_thm ("wellordered_is_trans_on", axioms_L (thm "M_axioms.wellordered_is_trans_on")); 
   7.700 -bind_thm ("wellordered_is_linear", axioms_L (thm "M_axioms.wellordered_is_linear")); 
   7.701 -bind_thm ("wellordered_is_wellfounded_on", axioms_L (thm "M_axioms.wellordered_is_wellfounded_on")); 
   7.702 -bind_thm ("wellfounded_imp_wellfounded_on", axioms_L (thm "M_axioms.wellfounded_imp_wellfounded_on")); 
   7.703 -bind_thm ("wellfounded_on_subset_A", axioms_L (thm "M_axioms.wellfounded_on_subset_A"));
   7.704 -bind_thm ("wellfounded_on_iff_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_iff_wellfounded"));
   7.705 -bind_thm ("wellfounded_on_imp_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_imp_wellfounded"));
   7.706 -bind_thm ("wellfounded_on_field_imp_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_field_imp_wellfounded"));
   7.707 -bind_thm ("wellfounded_iff_wellfounded_on_field", axioms_L (thm "M_axioms.wellfounded_iff_wellfounded_on_field"));
   7.708 -bind_thm ("wellfounded_induct", axioms_L (thm "M_axioms.wellfounded_induct")); 
   7.709 -bind_thm ("wellfounded_on_induct", axioms_L (thm "M_axioms.wellfounded_on_induct")); 
   7.710 -bind_thm ("wellfounded_on_induct2", axioms_L (thm "M_axioms.wellfounded_on_induct2")); 
   7.711 -bind_thm ("linear_imp_relativized", axioms_L (thm "M_axioms.linear_imp_relativized")); 
   7.712 -bind_thm ("trans_on_imp_relativized", axioms_L (thm "M_axioms.trans_on_imp_relativized")); 
   7.713 -bind_thm ("wf_on_imp_relativized", axioms_L (thm "M_axioms.wf_on_imp_relativized")); 
   7.714 -bind_thm ("wf_imp_relativized", axioms_L (thm "M_axioms.wf_imp_relativized")); 
   7.715 -bind_thm ("well_ord_imp_relativized", axioms_L (thm "M_axioms.well_ord_imp_relativized")); 
   7.716 -bind_thm ("order_isomorphism_abs", axioms_L (thm "M_axioms.order_isomorphism_abs"));  
   7.717 -bind_thm ("pred_set_abs", axioms_L (thm "M_axioms.pred_set_abs"));  
   7.718 -*}
   7.719 +lemmas is_recfun_equal = M_axioms.is_recfun_equal [OF M_axioms_L]
   7.720 +  and is_recfun_cut = M_axioms.is_recfun_cut [OF M_axioms_L]
   7.721 +  and is_recfun_functional = M_axioms.is_recfun_functional [OF M_axioms_L]
   7.722 +  and is_recfun_relativize = M_axioms.is_recfun_relativize [OF M_axioms_L]
   7.723 +  and is_recfun_restrict = M_axioms.is_recfun_restrict [OF M_axioms_L]
   7.724 +  and univalent_is_recfun = M_axioms.univalent_is_recfun [OF M_axioms_L]
   7.725 +  and exists_is_recfun_indstep = M_axioms.exists_is_recfun_indstep [OF M_axioms_L]
   7.726 +  and wellfounded_exists_is_recfun = M_axioms.wellfounded_exists_is_recfun [OF M_axioms_L]
   7.727 +  and wf_exists_is_recfun = M_axioms.wf_exists_is_recfun [OF M_axioms_L]
   7.728 +  and is_recfun_abs = M_axioms.is_recfun_abs [OF M_axioms_L]
   7.729 +  and irreflexive_abs = M_axioms.irreflexive_abs [OF M_axioms_L]
   7.730 +  and transitive_rel_abs = M_axioms.transitive_rel_abs [OF M_axioms_L]
   7.731 +  and linear_rel_abs = M_axioms.linear_rel_abs [OF M_axioms_L]
   7.732 +  and wellordered_is_trans_on = M_axioms.wellordered_is_trans_on [OF M_axioms_L]
   7.733 +  and wellordered_is_linear = M_axioms.wellordered_is_linear [OF M_axioms_L]
   7.734 +  and wellordered_is_wellfounded_on = M_axioms.wellordered_is_wellfounded_on [OF M_axioms_L]
   7.735 +  and wellfounded_imp_wellfounded_on = M_axioms.wellfounded_imp_wellfounded_on [OF M_axioms_L]
   7.736 +  and wellfounded_on_subset_A = M_axioms.wellfounded_on_subset_A [OF M_axioms_L]
   7.737 +  and wellfounded_on_iff_wellfounded = M_axioms.wellfounded_on_iff_wellfounded [OF M_axioms_L]
   7.738 +  and wellfounded_on_imp_wellfounded = M_axioms.wellfounded_on_imp_wellfounded [OF M_axioms_L]
   7.739 +  and wellfounded_on_field_imp_wellfounded = M_axioms.wellfounded_on_field_imp_wellfounded [OF M_axioms_L]
   7.740 +  and wellfounded_iff_wellfounded_on_field = M_axioms.wellfounded_iff_wellfounded_on_field [OF M_axioms_L]
   7.741 +  and wellfounded_induct = M_axioms.wellfounded_induct [OF M_axioms_L]
   7.742 +  and wellfounded_on_induct = M_axioms.wellfounded_on_induct [OF M_axioms_L]
   7.743 +  and wellfounded_on_induct2 = M_axioms.wellfounded_on_induct2 [OF M_axioms_L]
   7.744 +  and linear_imp_relativized = M_axioms.linear_imp_relativized [OF M_axioms_L]
   7.745 +  and trans_on_imp_relativized = M_axioms.trans_on_imp_relativized [OF M_axioms_L]
   7.746 +  and wf_on_imp_relativized = M_axioms.wf_on_imp_relativized [OF M_axioms_L]
   7.747 +  and wf_imp_relativized = M_axioms.wf_imp_relativized [OF M_axioms_L]
   7.748 +  and well_ord_imp_relativized = M_axioms.well_ord_imp_relativized [OF M_axioms_L]
   7.749 +  and order_isomorphism_abs = M_axioms.order_isomorphism_abs [OF M_axioms_L]
   7.750 +  and pred_set_abs = M_axioms.pred_set_abs [OF M_axioms_L]
   7.751  
   7.752 -ML
   7.753 -{*
   7.754 -bind_thm ("pred_closed", axioms_L (thm "M_axioms.pred_closed"));  
   7.755 -bind_thm ("membership_abs", axioms_L (thm "M_axioms.membership_abs"));  
   7.756 -bind_thm ("M_Memrel_iff", axioms_L (thm "M_axioms.M_Memrel_iff"));
   7.757 -bind_thm ("Memrel_closed", axioms_L (thm "M_axioms.Memrel_closed"));  
   7.758 -bind_thm ("wellordered_iso_predD", axioms_L (thm "M_axioms.wellordered_iso_predD"));
   7.759 -bind_thm ("wellordered_iso_pred_eq", axioms_L (thm "M_axioms.wellordered_iso_pred_eq"));
   7.760 -bind_thm ("wellfounded_on_asym", axioms_L (thm "M_axioms.wellfounded_on_asym"));
   7.761 -bind_thm ("wellordered_asym", axioms_L (thm "M_axioms.wellordered_asym"));
   7.762 -bind_thm ("ord_iso_pred_imp_lt", axioms_L (thm "M_axioms.ord_iso_pred_imp_lt"));
   7.763 -bind_thm ("obase_iff", axioms_L (thm "M_axioms.obase_iff"));
   7.764 -bind_thm ("omap_iff", axioms_L (thm "M_axioms.omap_iff"));
   7.765 -bind_thm ("omap_unique", axioms_L (thm "M_axioms.omap_unique"));
   7.766 -bind_thm ("omap_yields_Ord", axioms_L (thm "M_axioms.omap_yields_Ord"));
   7.767 -bind_thm ("otype_iff", axioms_L (thm "M_axioms.otype_iff"));
   7.768 -bind_thm ("otype_eq_range", axioms_L (thm "M_axioms.otype_eq_range"));
   7.769 -bind_thm ("Ord_otype", axioms_L (thm "M_axioms.Ord_otype"));
   7.770 -bind_thm ("domain_omap", axioms_L (thm "M_axioms.domain_omap"));
   7.771 -bind_thm ("omap_subset", axioms_L (thm "M_axioms.omap_subset")); 
   7.772 -bind_thm ("omap_funtype", axioms_L (thm "M_axioms.omap_funtype")); 
   7.773 -bind_thm ("wellordered_omap_bij", axioms_L (thm "M_axioms.wellordered_omap_bij"));
   7.774 -bind_thm ("omap_ord_iso", axioms_L (thm "M_axioms.omap_ord_iso"));
   7.775 -bind_thm ("Ord_omap_image_pred", axioms_L (thm "M_axioms.Ord_omap_image_pred"));
   7.776 -bind_thm ("restrict_omap_ord_iso", axioms_L (thm "M_axioms.restrict_omap_ord_iso"));
   7.777 -bind_thm ("obase_equals", axioms_L (thm "M_axioms.obase_equals")); 
   7.778 -bind_thm ("omap_ord_iso_otype", axioms_L (thm "M_axioms.omap_ord_iso_otype"));
   7.779 -bind_thm ("obase_exists", axioms_L (thm "M_axioms.obase_exists"));
   7.780 -bind_thm ("omap_exists", axioms_L (thm "M_axioms.omap_exists"));
   7.781 -bind_thm ("otype_exists", axioms_L (thm "M_axioms.otype_exists"));
   7.782 -bind_thm ("omap_ord_iso_otype", axioms_L (thm "M_axioms.omap_ord_iso_otype"));
   7.783 -bind_thm ("ordertype_exists", axioms_L (thm "M_axioms.ordertype_exists"));
   7.784 -bind_thm ("relativized_imp_well_ord", axioms_L (thm "M_axioms.relativized_imp_well_ord")); 
   7.785 -bind_thm ("well_ord_abs", axioms_L (thm "M_axioms.well_ord_abs"));  
   7.786 -*}
   7.787 +lemmas pred_closed = M_axioms.pred_closed [OF M_axioms_L]
   7.788 +  and membership_abs = M_axioms.membership_abs [OF M_axioms_L]
   7.789 +  and M_Memrel_iff = M_axioms.M_Memrel_iff [OF M_axioms_L]
   7.790 +  and Memrel_closed = M_axioms.Memrel_closed [OF M_axioms_L]
   7.791 +  and wellordered_iso_predD = M_axioms.wellordered_iso_predD [OF M_axioms_L]
   7.792 +  and wellordered_iso_pred_eq = M_axioms.wellordered_iso_pred_eq [OF M_axioms_L]
   7.793 +  and wellfounded_on_asym = M_axioms.wellfounded_on_asym [OF M_axioms_L]
   7.794 +  and wellordered_asym = M_axioms.wellordered_asym [OF M_axioms_L]
   7.795 +  and ord_iso_pred_imp_lt = M_axioms.ord_iso_pred_imp_lt [OF M_axioms_L]
   7.796 +  and obase_iff = M_axioms.obase_iff [OF M_axioms_L]
   7.797 +  and omap_iff = M_axioms.omap_iff [OF M_axioms_L]
   7.798 +  and omap_unique = M_axioms.omap_unique [OF M_axioms_L]
   7.799 +  and omap_yields_Ord = M_axioms.omap_yields_Ord [OF M_axioms_L]
   7.800 +  and otype_iff = M_axioms.otype_iff [OF M_axioms_L]
   7.801 +  and otype_eq_range = M_axioms.otype_eq_range [OF M_axioms_L]
   7.802 +  and Ord_otype = M_axioms.Ord_otype [OF M_axioms_L]
   7.803 +  and domain_omap = M_axioms.domain_omap [OF M_axioms_L]
   7.804 +  and omap_subset = M_axioms.omap_subset [OF M_axioms_L]
   7.805 +  and omap_funtype = M_axioms.omap_funtype [OF M_axioms_L]
   7.806 +  and wellordered_omap_bij = M_axioms.wellordered_omap_bij [OF M_axioms_L]
   7.807 +  and omap_ord_iso = M_axioms.omap_ord_iso [OF M_axioms_L]
   7.808 +  and Ord_omap_image_pred = M_axioms.Ord_omap_image_pred [OF M_axioms_L]
   7.809 +  and restrict_omap_ord_iso = M_axioms.restrict_omap_ord_iso [OF M_axioms_L]
   7.810 +  and obase_equals = M_axioms.obase_equals [OF M_axioms_L]
   7.811 +  and omap_ord_iso_otype = M_axioms.omap_ord_iso_otype [OF M_axioms_L]
   7.812 +  and obase_exists = M_axioms.obase_exists [OF M_axioms_L]
   7.813 +  and omap_exists = M_axioms.omap_exists [OF M_axioms_L]
   7.814 +  and otype_exists = M_axioms.otype_exists [OF M_axioms_L]
   7.815 +  and omap_ord_iso_otype' = M_axioms.omap_ord_iso_otype' [OF M_axioms_L]
   7.816 +  and ordertype_exists = M_axioms.ordertype_exists [OF M_axioms_L]
   7.817 +  and relativized_imp_well_ord = M_axioms.relativized_imp_well_ord [OF M_axioms_L]
   7.818 +  and well_ord_abs = M_axioms.well_ord_abs [OF M_axioms_L]
   7.819 +
   7.820  
   7.821  declare cartprod_closed [intro,simp]
   7.822  declare sum_closed [intro,simp]
   7.823 @@ -614,7 +598,6 @@
   7.824  declare Inter_abs [simp]
   7.825  declare Inter_closed [intro,simp]
   7.826  declare Int_closed [intro,simp]
   7.827 -declare finite_fun_closed [rule_format]
   7.828  declare is_funspace_abs [simp]
   7.829  declare finite_funspace_closed [intro,simp]
   7.830  
     8.1 --- a/src/ZF/Constructible/WF_absolute.thy	Sun Jul 28 21:09:37 2002 +0200
     8.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Mon Jul 29 00:57:16 2002 +0200
     8.3 @@ -143,7 +143,7 @@
     8.4  by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD]) 
     8.5  
     8.6  
     8.7 -locale (open) M_trancl = M_axioms +
     8.8 +locale M_trancl = M_axioms +
     8.9    assumes rtrancl_separation:
    8.10  	 "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
    8.11        and wellfounded_trancl_separation:
    8.12 @@ -231,7 +231,7 @@
    8.13  rank function.*}
    8.14  
    8.15  
    8.16 -locale (open) M_wfrank = M_trancl +
    8.17 +locale M_wfrank = M_trancl +
    8.18    assumes wfrank_separation:
    8.19       "M(r) ==>
    8.20        separation (M, \<lambda>x. 
    8.21 @@ -317,7 +317,7 @@
    8.22      "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
    8.23       ==> \<forall>f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
    8.24  apply (drule wellfounded_trancl, assumption)
    8.25 -apply (rule wellfounded_induct, assumption+)
    8.26 +apply (rule wellfounded_induct, assumption, erule (1) transM)
    8.27    apply simp
    8.28   apply (blast intro: Ord_wfrank_separation', clarify)
    8.29  txt{*The reasoning in both cases is that we get @{term y} such that
    8.30 @@ -445,7 +445,8 @@
    8.31  apply (subgoal_tac "a\<in>A & b\<in>A")
    8.32   prefer 2 apply blast
    8.33  apply (simp add: lt_def Ord_wellfoundedrank, clarify)
    8.34 -apply (frule exists_wfrank [of concl: _ b], assumption+, clarify)
    8.35 +apply (frule exists_wfrank [of concl: _ b], erule (1) transM, assumption)
    8.36 +apply clarify
    8.37  apply (rename_tac fb)
    8.38  apply (frule is_recfun_restrict [of concl: "r^+" a])
    8.39      apply (rule trans_trancl, assumption)
     9.1 --- a/src/ZF/Constructible/WFrec.thy	Sun Jul 28 21:09:37 2002 +0200
     9.2 +++ b/src/ZF/Constructible/WFrec.thy	Mon Jul 29 00:57:16 2002 +0200
     9.3 @@ -378,7 +378,7 @@
     9.4                    fun_apply(M,f,j,fj) & fj = k"
     9.5  
     9.6  
     9.7 -locale (open) M_ord_arith = M_axioms +
     9.8 +locale M_ord_arith = M_axioms +
     9.9    assumes oadd_strong_replacement:
    9.10     "[| M(i); M(j) |] ==>
    9.11      strong_replacement(M, 
    10.1 --- a/src/ZF/Constructible/Wellorderings.thy	Sun Jul 28 21:09:37 2002 +0200
    10.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Mon Jul 29 00:57:16 2002 +0200
    10.3 @@ -603,7 +603,7 @@
    10.4  apply blast+
    10.5  done
    10.6  
    10.7 -theorem (in M_axioms) omap_ord_iso_otype:
    10.8 +theorem (in M_axioms) omap_ord_iso_otype':
    10.9       "[| wellordered(M,A,r); M(A); M(r) |]
   10.10        ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   10.11  apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
   10.12 @@ -619,7 +619,7 @@
   10.13        ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   10.14  apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
   10.15  apply (rename_tac i) 
   10.16 -apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) 
   10.17 +apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype')
   10.18  apply (rule Ord_otype) 
   10.19      apply (force simp add: otype_def range_closed) 
   10.20     apply (simp_all add: wellordered_is_trans_on)