instantiation of locales M_trancl and M_wfrank;
authorpaulson
Tue Jul 16 16:29:36 2002 +0200 (2002-07-16)
changeset 13363c26eeb000470
parent 13362 cd7f9ea58338
child 13364 d3c7d05d8839
instantiation of locales M_trancl and M_wfrank;
proofs of list_replacement{1,2}
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/WF_absolute.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 16 16:28:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 16 16:29:36 2002 +0200
     1.3 @@ -101,17 +101,14 @@
     1.4  
     1.5    iterates_replacement :: "[i=>o, [i,i]=>o, i] => o"
     1.6     "iterates_replacement(M,isF,v) ==
     1.7 -      \<forall>n[M]. n\<in>nat -->
     1.8 +      \<forall>n[M]. n\<in>nat --> 
     1.9           wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
    1.10  
    1.11  lemma (in M_axioms) iterates_MH_abs:
    1.12    "[| relativize1(M,isF,F); M(n); M(g); M(z) |] 
    1.13     ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
    1.14 -apply (simp add: iterates_MH_def) 
    1.15 -apply (rule nat_case_abs) 
    1.16 -apply (simp_all add: relativize1_def) 
    1.17 -done
    1.18 -
    1.19 +by (simp add: nat_case_abs [of _ "\<lambda>m. F(g ` m)"]
    1.20 +              relativize1_def iterates_MH_def)  
    1.21  
    1.22  lemma (in M_axioms) iterates_imp_wfrec_replacement:
    1.23    "[|relativize1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|] 
    1.24 @@ -159,28 +156,20 @@
    1.25  
    1.26  locale M_datatypes = M_wfrank +
    1.27   assumes list_replacement1: 
    1.28 -   "M(A) ==> \<exists>zero[M]. empty(M,zero) & 
    1.29 -		       iterates_replacement(M, is_list_functor(M,A), zero)"
    1.30 +   "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    1.31    and list_replacement2: 
    1.32 -   "M(A) ==> 
    1.33 -    \<exists>zero[M]. empty(M,zero) & 
    1.34 -	      strong_replacement(M, 
    1.35 +   "M(A) ==> strong_replacement(M, 
    1.36           \<lambda>n y. n\<in>nat & 
    1.37                 (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
    1.38 -               is_wfrec(M, iterates_MH(M,is_list_functor(M,A), zero), 
    1.39 +               is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0), 
    1.40                          msn, n, y)))"
    1.41  
    1.42 -lemma (in M_datatypes) list_replacement1': 
    1.43 -   "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    1.44 -apply (insert list_replacement1, simp) 
    1.45 -done
    1.46 -
    1.47  lemma (in M_datatypes) list_replacement2': 
    1.48    "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
    1.49  apply (insert list_replacement2 [of A]) 
    1.50  apply (rule strong_replacement_cong [THEN iffD1])  
    1.51  apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]]) 
    1.52 -apply (simp_all add: list_replacement1' relativize1_def) 
    1.53 +apply (simp_all add: list_replacement1 relativize1_def) 
    1.54  done
    1.55  
    1.56  lemma (in M_datatypes) list_closed [intro,simp]:
     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Tue Jul 16 16:28:49 2002 +0200
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Tue Jul 16 16:29:36 2002 +0200
     2.3 @@ -66,7 +66,8 @@
     2.4  apply (simp_all add: Replace_iff univalent_def, blast) 
     2.5  done
     2.6  
     2.7 -subsection{*Instantiation of the locale @{text M_triv_axioms}*}
     2.8 +subsection{*Instantiating the locale @{text M_triv_axioms}*}
     2.9 +text{*No instances of Separation yet.*}
    2.10  
    2.11  lemma Lset_mono_le: "mono_le_subset(Lset)"
    2.12  by (simp add: mono_le_subset_def le_imp_subset Lset_mono) 
    2.13 @@ -90,57 +91,57 @@
    2.14  
    2.15  fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st);
    2.16  
    2.17 -fun trivaxL th =
    2.18 +fun triv_axioms_L th =
    2.19      kill_flex_triv_prems 
    2.20         ([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat] 
    2.21          MRS (inst "M" "L" th));
    2.22  
    2.23 -bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs"));
    2.24 -bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs"));
    2.25 -bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs"));
    2.26 -bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs"));
    2.27 -bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv"));
    2.28 -bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI"));
    2.29 -bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs"));
    2.30 -bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs"));
    2.31 -bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs"));
    2.32 -bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff"));
    2.33 -bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff"));
    2.34 -bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs"));
    2.35 -bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff"));
    2.36 -bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M"));
    2.37 -bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs"));
    2.38 -bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs"));
    2.39 -bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs"));
    2.40 -bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs"));
    2.41 -bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs"));
    2.42 -bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed"));
    2.43 -bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed"));
    2.44 -bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed"));
    2.45 -bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs"));
    2.46 -bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff"));
    2.47 -bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed"));
    2.48 -bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI"));
    2.49 -bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed"));
    2.50 -bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed"));
    2.51 -bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed"));
    2.52 -bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs"));
    2.53 -bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow"));
    2.54 -bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow"));
    2.55 -bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M"));
    2.56 -bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed"));
    2.57 -bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff"));
    2.58 -bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff"));
    2.59 -bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed"));
    2.60 -bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs"));
    2.61 -bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs"));
    2.62 -bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs"));
    2.63 -bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs"));
    2.64 -bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs"));
    2.65 -bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs"));
    2.66 -bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
    2.67 -bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
    2.68 -bind_thm ("number3_abs", trivaxL (thm "M_triv_axioms.number3_abs"));
    2.69 +bind_thm ("ball_abs", triv_axioms_L (thm "M_triv_axioms.ball_abs"));
    2.70 +bind_thm ("rall_abs", triv_axioms_L (thm "M_triv_axioms.rall_abs"));
    2.71 +bind_thm ("bex_abs", triv_axioms_L (thm "M_triv_axioms.bex_abs"));
    2.72 +bind_thm ("rex_abs", triv_axioms_L (thm "M_triv_axioms.rex_abs"));
    2.73 +bind_thm ("ball_iff_equiv", triv_axioms_L (thm "M_triv_axioms.ball_iff_equiv"));
    2.74 +bind_thm ("M_equalityI", triv_axioms_L (thm "M_triv_axioms.M_equalityI"));
    2.75 +bind_thm ("empty_abs", triv_axioms_L (thm "M_triv_axioms.empty_abs"));
    2.76 +bind_thm ("subset_abs", triv_axioms_L (thm "M_triv_axioms.subset_abs"));
    2.77 +bind_thm ("upair_abs", triv_axioms_L (thm "M_triv_axioms.upair_abs"));
    2.78 +bind_thm ("upair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.upair_in_M_iff"));
    2.79 +bind_thm ("singleton_in_M_iff", triv_axioms_L (thm "M_triv_axioms.singleton_in_M_iff"));
    2.80 +bind_thm ("pair_abs", triv_axioms_L (thm "M_triv_axioms.pair_abs"));
    2.81 +bind_thm ("pair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.pair_in_M_iff"));
    2.82 +bind_thm ("pair_components_in_M", triv_axioms_L (thm "M_triv_axioms.pair_components_in_M"));
    2.83 +bind_thm ("cartprod_abs", triv_axioms_L (thm "M_triv_axioms.cartprod_abs"));
    2.84 +bind_thm ("union_abs", triv_axioms_L (thm "M_triv_axioms.union_abs"));
    2.85 +bind_thm ("inter_abs", triv_axioms_L (thm "M_triv_axioms.inter_abs"));
    2.86 +bind_thm ("setdiff_abs", triv_axioms_L (thm "M_triv_axioms.setdiff_abs"));
    2.87 +bind_thm ("Union_abs", triv_axioms_L (thm "M_triv_axioms.Union_abs"));
    2.88 +bind_thm ("Union_closed", triv_axioms_L (thm "M_triv_axioms.Union_closed"));
    2.89 +bind_thm ("Un_closed", triv_axioms_L (thm "M_triv_axioms.Un_closed"));
    2.90 +bind_thm ("cons_closed", triv_axioms_L (thm "M_triv_axioms.cons_closed"));
    2.91 +bind_thm ("successor_abs", triv_axioms_L (thm "M_triv_axioms.successor_abs"));
    2.92 +bind_thm ("succ_in_M_iff", triv_axioms_L (thm "M_triv_axioms.succ_in_M_iff"));
    2.93 +bind_thm ("separation_closed", triv_axioms_L (thm "M_triv_axioms.separation_closed"));
    2.94 +bind_thm ("strong_replacementI", triv_axioms_L (thm "M_triv_axioms.strong_replacementI"));
    2.95 +bind_thm ("strong_replacement_closed", triv_axioms_L (thm "M_triv_axioms.strong_replacement_closed"));
    2.96 +bind_thm ("RepFun_closed", triv_axioms_L (thm "M_triv_axioms.RepFun_closed"));
    2.97 +bind_thm ("lam_closed", triv_axioms_L (thm "M_triv_axioms.lam_closed"));
    2.98 +bind_thm ("image_abs", triv_axioms_L (thm "M_triv_axioms.image_abs"));
    2.99 +bind_thm ("powerset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_Pow"));
   2.100 +bind_thm ("powerset_imp_subset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_imp_subset_Pow"));
   2.101 +bind_thm ("nat_into_M", triv_axioms_L (thm "M_triv_axioms.nat_into_M"));
   2.102 +bind_thm ("nat_case_closed", triv_axioms_L (thm "M_triv_axioms.nat_case_closed"));
   2.103 +bind_thm ("Inl_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inl_in_M_iff"));
   2.104 +bind_thm ("Inr_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inr_in_M_iff"));
   2.105 +bind_thm ("lt_closed", triv_axioms_L (thm "M_triv_axioms.lt_closed"));
   2.106 +bind_thm ("transitive_set_abs", triv_axioms_L (thm "M_triv_axioms.transitive_set_abs"));
   2.107 +bind_thm ("ordinal_abs", triv_axioms_L (thm "M_triv_axioms.ordinal_abs"));
   2.108 +bind_thm ("limit_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.limit_ordinal_abs"));
   2.109 +bind_thm ("successor_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.successor_ordinal_abs"));
   2.110 +bind_thm ("finite_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.finite_ordinal_abs"));
   2.111 +bind_thm ("omega_abs", triv_axioms_L (thm "M_triv_axioms.omega_abs"));
   2.112 +bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs"));
   2.113 +bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs"));
   2.114 +bind_thm ("number3_abs", triv_axioms_L (thm "M_triv_axioms.number3_abs"));
   2.115  *}
   2.116  
   2.117  declare ball_abs [simp] 
   2.118 @@ -563,6 +564,39 @@
   2.119  done
   2.120  
   2.121  
   2.122 +subsubsection{*The Number 1, Internalized*}
   2.123 +
   2.124 +(* "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))" *)
   2.125 +constdefs number1_fm :: "i=>i"
   2.126 +    "number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))"
   2.127 +
   2.128 +lemma number1_type [TC]:
   2.129 +     "x \<in> nat ==> number1_fm(x) \<in> formula"
   2.130 +by (simp add: number1_fm_def) 
   2.131 +
   2.132 +lemma arity_number1_fm [simp]:
   2.133 +     "x \<in> nat ==> arity(number1_fm(x)) = succ(x)"
   2.134 +by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac) 
   2.135 +
   2.136 +lemma sats_number1_fm [simp]:
   2.137 +   "[| x \<in> nat; env \<in> list(A)|]
   2.138 +    ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))"
   2.139 +by (simp add: number1_fm_def number1_def)
   2.140 +
   2.141 +lemma number1_iff_sats:
   2.142 +      "[| nth(i,env) = x; nth(j,env) = y; 
   2.143 +          i \<in> nat; env \<in> list(A)|]
   2.144 +       ==> number1(**A, x) <-> sats(A, number1_fm(i), env)"
   2.145 +by simp
   2.146 +
   2.147 +theorem number1_reflection:
   2.148 +     "REFLECTS[\<lambda>x. number1(L,f(x)), 
   2.149 +               \<lambda>i x. number1(**Lset(i),f(x))]"
   2.150 +apply (simp only: number1_def setclass_simps)
   2.151 +apply (intro FOL_reflections empty_reflection successor_reflection)
   2.152 +done
   2.153 +
   2.154 +
   2.155  subsubsection{*Big Union, Internalized*}
   2.156  
   2.157  (*  "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
   2.158 @@ -1076,7 +1110,8 @@
   2.159  by simp
   2.160  
   2.161  lemmas function_reflections = 
   2.162 -        empty_reflection upair_reflection pair_reflection union_reflection
   2.163 +        empty_reflection number1_reflection
   2.164 +	upair_reflection pair_reflection union_reflection
   2.165  	big_union_reflection cons_reflection successor_reflection 
   2.166          fun_apply_reflection subset_reflection
   2.167  	transitive_set_reflection membership_reflection
   2.168 @@ -1085,7 +1120,8 @@
   2.169  	is_relation_reflection is_function_reflection
   2.170  
   2.171  lemmas function_iff_sats = 
   2.172 -        empty_iff_sats upair_iff_sats pair_iff_sats union_iff_sats
   2.173 +        empty_iff_sats number1_iff_sats 
   2.174 +	upair_iff_sats pair_iff_sats union_iff_sats
   2.175  	cons_iff_sats successor_iff_sats
   2.176          fun_apply_iff_sats  Memrel_iff_sats
   2.177  	pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
     3.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 16 16:28:49 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 16 16:29:36 2002 +0200
     3.3 @@ -1,10 +1,13 @@
     3.4 -header{*Separation for the Absoluteness of Recursion*}
     3.5 +header{*Separation for Facts About Recursion*}
     3.6  
     3.7 -theory Rec_Separation = Separation:
     3.8 +theory Rec_Separation = Separation + Datatype_absolute:
     3.9  
    3.10  text{*This theory proves all instances needed for locales @{text
    3.11  "M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}
    3.12  
    3.13 +lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
    3.14 +by simp 
    3.15 +
    3.16  subsection{*The Locale @{text "M_trancl"}*}
    3.17  
    3.18  subsubsection{*Separation for Reflexive/Transitive Closure*}
    3.19 @@ -194,6 +197,40 @@
    3.20  apply (simp_all add: succ_Un_distrib [symmetric])
    3.21  done
    3.22  
    3.23 +
    3.24 +subsubsection{*Instantiating the locale @{text M_trancl}*}
    3.25 +ML
    3.26 +{*
    3.27 +val rtrancl_separation = thm "rtrancl_separation";
    3.28 +val wellfounded_trancl_separation = thm "wellfounded_trancl_separation";
    3.29 +
    3.30 +
    3.31 +val m_trancl = [rtrancl_separation, wellfounded_trancl_separation];
    3.32 +
    3.33 +fun trancl_L th =
    3.34 +    kill_flex_triv_prems (m_trancl MRS (axioms_L th));
    3.35 +
    3.36 +bind_thm ("iterates_abs", trancl_L (thm "M_trancl.iterates_abs"));
    3.37 +bind_thm ("rtran_closure_rtrancl", trancl_L (thm "M_trancl.rtran_closure_rtrancl"));
    3.38 +bind_thm ("rtrancl_closed", trancl_L (thm "M_trancl.rtrancl_closed"));
    3.39 +bind_thm ("rtrancl_abs", trancl_L (thm "M_trancl.rtrancl_abs"));
    3.40 +bind_thm ("trancl_closed", trancl_L (thm "M_trancl.trancl_closed"));
    3.41 +bind_thm ("trancl_abs", trancl_L (thm "M_trancl.trancl_abs"));
    3.42 +bind_thm ("wellfounded_on_trancl", trancl_L (thm "M_trancl.wellfounded_on_trancl"));
    3.43 +bind_thm ("wellfounded_trancl", trancl_L (thm "M_trancl.wellfounded_trancl"));
    3.44 +bind_thm ("wfrec_relativize", trancl_L (thm "M_trancl.wfrec_relativize"));
    3.45 +bind_thm ("trans_wfrec_relativize", trancl_L (thm "M_trancl.trans_wfrec_relativize"));
    3.46 +bind_thm ("trans_wfrec_abs", trancl_L (thm "M_trancl.trans_wfrec_abs"));
    3.47 +bind_thm ("trans_eq_pair_wfrec_iff", trancl_L (thm "M_trancl.trans_eq_pair_wfrec_iff"));
    3.48 +bind_thm ("eq_pair_wfrec_iff", trancl_L (thm "M_trancl.eq_pair_wfrec_iff"));
    3.49 +*}
    3.50 +
    3.51 +declare rtrancl_closed [intro,simp]
    3.52 +declare rtrancl_abs [simp]
    3.53 +declare trancl_closed [intro,simp]
    3.54 +declare trancl_abs [simp]
    3.55 +
    3.56 +
    3.57  subsection{*Well-Founded Recursion!*}
    3.58  
    3.59  (* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    3.60 @@ -275,7 +312,22 @@
    3.61               restriction_reflection MH_reflection)  
    3.62  done
    3.63  
    3.64 -subsection{*Separation for  @{term "wfrank"}*}
    3.65 +text{*Currently, @{text sats}-theorems for higher-order operators don't seem
    3.66 +useful.  Reflection theorems do work, though.  This one avoids the repetition
    3.67 +of the @{text MH}-term.*}
    3.68 +theorem is_wfrec_reflection:
    3.69 +  assumes MH_reflection:
    3.70 +    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)), 
    3.71 +                     \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
    3.72 +  shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L), f(x), g(x), h(x)), 
    3.73 +               \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
    3.74 +apply (simp (no_asm_use) only: is_wfrec_def setclass_simps)
    3.75 +apply (intro FOL_reflections MH_reflection is_recfun_reflection)  
    3.76 +done
    3.77 +
    3.78 +subsection{*The Locale @{text "M_wfrank"}*}
    3.79 +
    3.80 +subsubsection{*Separation for @{term "wfrank"}*}
    3.81  
    3.82  lemma wfrank_Reflects:
    3.83   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    3.84 @@ -305,7 +357,7 @@
    3.85  done
    3.86  
    3.87  
    3.88 -subsection{*Replacement for @{term "wfrank"}*}
    3.89 +subsubsection{*Replacement for @{term "wfrank"}*}
    3.90  
    3.91  lemma wfrank_replacement_Reflects:
    3.92   "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A & 
    3.93 @@ -347,7 +399,7 @@
    3.94  done
    3.95  
    3.96  
    3.97 -subsection{*Separation for  @{term "wfrank"}*}
    3.98 +subsubsection{*Separation for Proving @{text Ord_wfrank_range}*}
    3.99  
   3.100  lemma Ord_wfrank_Reflects:
   3.101   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> 
   3.102 @@ -387,4 +439,438 @@
   3.103  done
   3.104  
   3.105  
   3.106 +subsubsection{*Instantiating the locale @{text M_wfrank}*}
   3.107 +ML
   3.108 +{*
   3.109 +val wfrank_separation = thm "wfrank_separation";
   3.110 +val wfrank_strong_replacement = thm "wfrank_strong_replacement";
   3.111 +val Ord_wfrank_separation = thm "Ord_wfrank_separation";
   3.112 +
   3.113 +val m_wfrank = 
   3.114 +    [wfrank_separation, wfrank_strong_replacement, Ord_wfrank_separation];
   3.115 +
   3.116 +fun wfrank_L th =
   3.117 +    kill_flex_triv_prems (m_wfrank MRS (trancl_L th));
   3.118 +
   3.119 +
   3.120 +
   3.121 +bind_thm ("iterates_closed", wfrank_L (thm "M_wfrank.iterates_closed"));
   3.122 +bind_thm ("exists_wfrank", wfrank_L (thm "M_wfrank.exists_wfrank"));
   3.123 +bind_thm ("M_wellfoundedrank", wfrank_L (thm "M_wfrank.M_wellfoundedrank"));
   3.124 +bind_thm ("Ord_wfrank_range", wfrank_L (thm "M_wfrank.Ord_wfrank_range"));
   3.125 +bind_thm ("Ord_range_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_range_wellfoundedrank"));
   3.126 +bind_thm ("function_wellfoundedrank", wfrank_L (thm "M_wfrank.function_wellfoundedrank"));
   3.127 +bind_thm ("domain_wellfoundedrank", wfrank_L (thm "M_wfrank.domain_wellfoundedrank"));
   3.128 +bind_thm ("wellfoundedrank_type", wfrank_L (thm "M_wfrank.wellfoundedrank_type"));
   3.129 +bind_thm ("Ord_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_wellfoundedrank"));
   3.130 +bind_thm ("wellfoundedrank_eq", wfrank_L (thm "M_wfrank.wellfoundedrank_eq"));
   3.131 +bind_thm ("wellfoundedrank_lt", wfrank_L (thm "M_wfrank.wellfoundedrank_lt"));
   3.132 +bind_thm ("wellfounded_imp_subset_rvimage", wfrank_L (thm "M_wfrank.wellfounded_imp_subset_rvimage"));
   3.133 +bind_thm ("wellfounded_imp_wf", wfrank_L (thm "M_wfrank.wellfounded_imp_wf"));
   3.134 +bind_thm ("wellfounded_on_imp_wf_on", wfrank_L (thm "M_wfrank.wellfounded_on_imp_wf_on"));
   3.135 +bind_thm ("wf_abs", wfrank_L (thm "M_wfrank.wf_abs"));
   3.136 +bind_thm ("wf_on_abs", wfrank_L (thm "M_wfrank.wf_on_abs"));
   3.137 +bind_thm ("wfrec_replacement_iff", wfrank_L (thm "M_wfrank.wfrec_replacement_iff"));
   3.138 +bind_thm ("trans_wfrec_closed", wfrank_L (thm "M_wfrank.trans_wfrec_closed"));
   3.139 +bind_thm ("wfrec_closed", wfrank_L (thm "M_wfrank.wfrec_closed"));
   3.140 +*}
   3.141 +
   3.142 +declare iterates_closed [intro,simp]
   3.143 +declare Ord_wfrank_range [rule_format]
   3.144 +declare wf_abs [simp]
   3.145 +declare wf_on_abs [simp]
   3.146 +
   3.147 +
   3.148 +subsection{*For Datatypes*}
   3.149 +
   3.150 +subsubsection{*Binary Products, Internalized*}
   3.151 +
   3.152 +constdefs cartprod_fm :: "[i,i,i]=>i"
   3.153 +(* "cartprod(M,A,B,z) == 
   3.154 +	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
   3.155 +    "cartprod_fm(A,B,z) == 
   3.156 +       Forall(Iff(Member(0,succ(z)),
   3.157 +                  Exists(And(Member(0,succ(succ(A))),
   3.158 +                         Exists(And(Member(0,succ(succ(succ(B)))),
   3.159 +                                    pair_fm(1,0,2)))))))"
   3.160 +
   3.161 +lemma cartprod_type [TC]:
   3.162 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
   3.163 +by (simp add: cartprod_fm_def) 
   3.164 +
   3.165 +lemma arity_cartprod_fm [simp]:
   3.166 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   3.167 +      ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.168 +by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac) 
   3.169 +
   3.170 +lemma sats_cartprod_fm [simp]:
   3.171 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.172 +    ==> sats(A, cartprod_fm(x,y,z), env) <-> 
   3.173 +        cartprod(**A, nth(x,env), nth(y,env), nth(z,env))"
   3.174 +by (simp add: cartprod_fm_def cartprod_def)
   3.175 +
   3.176 +lemma cartprod_iff_sats:
   3.177 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   3.178 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   3.179 +       ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
   3.180 +by (simp add: sats_cartprod_fm)
   3.181 +
   3.182 +theorem cartprod_reflection:
   3.183 +     "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)), 
   3.184 +               \<lambda>i x. cartprod(**Lset(i),f(x),g(x),h(x))]"
   3.185 +apply (simp only: cartprod_def setclass_simps)
   3.186 +apply (intro FOL_reflections pair_reflection)  
   3.187 +done
   3.188 +
   3.189 +
   3.190 +subsubsection{*Binary Sums, Internalized*}
   3.191 +
   3.192 +(* "is_sum(M,A,B,Z) == 
   3.193 +       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
   3.194 +         3      2       1        0
   3.195 +       number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
   3.196 +       cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"  *)
   3.197 +constdefs sum_fm :: "[i,i,i]=>i"
   3.198 +    "sum_fm(A,B,Z) == 
   3.199 +       Exists(Exists(Exists(Exists(
   3.200 +	And(number1_fm(2),
   3.201 +            And(cartprod_fm(2,A#+4,3),
   3.202 +                And(upair_fm(2,2,1),
   3.203 +                    And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))"
   3.204 +
   3.205 +lemma sum_type [TC]:
   3.206 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
   3.207 +by (simp add: sum_fm_def) 
   3.208 +
   3.209 +lemma arity_sum_fm [simp]:
   3.210 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   3.211 +      ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.212 +by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac) 
   3.213 +
   3.214 +lemma sats_sum_fm [simp]:
   3.215 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.216 +    ==> sats(A, sum_fm(x,y,z), env) <-> 
   3.217 +        is_sum(**A, nth(x,env), nth(y,env), nth(z,env))"
   3.218 +by (simp add: sum_fm_def is_sum_def)
   3.219 +
   3.220 +lemma sum_iff_sats:
   3.221 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   3.222 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   3.223 +       ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
   3.224 +by simp
   3.225 +
   3.226 +theorem sum_reflection:
   3.227 +     "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)), 
   3.228 +               \<lambda>i x. is_sum(**Lset(i),f(x),g(x),h(x))]"
   3.229 +apply (simp only: is_sum_def setclass_simps)
   3.230 +apply (intro FOL_reflections function_reflections cartprod_reflection)  
   3.231 +done
   3.232 +
   3.233 +
   3.234 +subsubsection{*The List Functor, Internalized*}
   3.235 +
   3.236 +constdefs list_functor_fm :: "[i,i,i]=>i"
   3.237 +(* "is_list_functor(M,A,X,Z) == 
   3.238 +        \<exists>n1[M]. \<exists>AX[M]. 
   3.239 +         number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
   3.240 +    "list_functor_fm(A,X,Z) == 
   3.241 +       Exists(Exists(
   3.242 +	And(number1_fm(1),
   3.243 +            And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))"
   3.244 +
   3.245 +lemma list_functor_type [TC]:
   3.246 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
   3.247 +by (simp add: list_functor_fm_def) 
   3.248 +
   3.249 +lemma arity_list_functor_fm [simp]:
   3.250 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   3.251 +      ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.252 +by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac) 
   3.253 +
   3.254 +lemma sats_list_functor_fm [simp]:
   3.255 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.256 +    ==> sats(A, list_functor_fm(x,y,z), env) <-> 
   3.257 +        is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))"
   3.258 +by (simp add: list_functor_fm_def is_list_functor_def)
   3.259 +
   3.260 +lemma list_functor_iff_sats:
   3.261 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   3.262 +      i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   3.263 +   ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
   3.264 +by simp
   3.265 +
   3.266 +theorem list_functor_reflection:
   3.267 +     "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)), 
   3.268 +               \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
   3.269 +apply (simp only: is_list_functor_def setclass_simps)
   3.270 +apply (intro FOL_reflections number1_reflection
   3.271 +             cartprod_reflection sum_reflection)  
   3.272 +done
   3.273 +
   3.274 +subsubsection{*The Operator @{term quasinat}*}
   3.275 +
   3.276 +(* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *)
   3.277 +constdefs quasinat_fm :: "i=>i"
   3.278 +    "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))"
   3.279 +
   3.280 +lemma quasinat_type [TC]:
   3.281 +     "x \<in> nat ==> quasinat_fm(x) \<in> formula"
   3.282 +by (simp add: quasinat_fm_def) 
   3.283 +
   3.284 +lemma arity_quasinat_fm [simp]:
   3.285 +     "x \<in> nat ==> arity(quasinat_fm(x)) = succ(x)"
   3.286 +by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac) 
   3.287 +
   3.288 +lemma sats_quasinat_fm [simp]:
   3.289 +   "[| x \<in> nat; env \<in> list(A)|]
   3.290 +    ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))"
   3.291 +by (simp add: quasinat_fm_def is_quasinat_def)
   3.292 +
   3.293 +lemma quasinat_iff_sats:
   3.294 +      "[| nth(i,env) = x; nth(j,env) = y; 
   3.295 +          i \<in> nat; env \<in> list(A)|]
   3.296 +       ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)"
   3.297 +by simp
   3.298 +
   3.299 +theorem quasinat_reflection:
   3.300 +     "REFLECTS[\<lambda>x. is_quasinat(L,f(x)), 
   3.301 +               \<lambda>i x. is_quasinat(**Lset(i),f(x))]"
   3.302 +apply (simp only: is_quasinat_def setclass_simps)
   3.303 +apply (intro FOL_reflections function_reflections)  
   3.304 +done
   3.305 +
   3.306 +
   3.307 +subsubsection{*The Operator @{term is_nat_case}*}
   3.308 +
   3.309 +(* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
   3.310 +    "is_nat_case(M, a, is_b, k, z) == 
   3.311 +       (empty(M,k) --> z=a) &
   3.312 +       (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   3.313 +       (is_quasinat(M,k) | empty(M,z))" *)
   3.314 +text{*The formula @{term is_b} has free variables 1 and 0.*}
   3.315 +constdefs is_nat_case_fm :: "[i, [i,i]=>i, i, i]=>i"
   3.316 + "is_nat_case_fm(a,is_b,k,z) == 
   3.317 +    And(Implies(empty_fm(k), Equal(z,a)),
   3.318 +        And(Forall(Implies(succ_fm(0,succ(k)), 
   3.319 +                   Forall(Implies(Equal(0,succ(succ(z))), is_b(1,0))))),
   3.320 +            Or(quasinat_fm(k), empty_fm(z))))"
   3.321 +
   3.322 +lemma is_nat_case_type [TC]:
   3.323 +     "[| is_b(1,0) \<in> formula;  
   3.324 +         x \<in> nat; y \<in> nat; z \<in> nat |] 
   3.325 +      ==> is_nat_case_fm(x,is_b,y,z) \<in> formula"
   3.326 +by (simp add: is_nat_case_fm_def) 
   3.327 +
   3.328 +lemma arity_is_nat_case_fm [simp]:
   3.329 +     "[| is_b(1,0) \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
   3.330 +      ==> arity(is_nat_case_fm(x,is_b,y,z)) = 
   3.331 +          succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(is_b(1,0)) #- 2)" 
   3.332 +apply (subgoal_tac "arity(is_b(1,0)) \<in> nat")  
   3.333 +apply typecheck
   3.334 +(*FIXME: could nat_diff_split work?*)
   3.335 +apply (auto simp add: diff_def raw_diff_succ is_nat_case_fm_def nat_imp_quasinat
   3.336 +                 succ_Un_distrib [symmetric] Un_ac
   3.337 +                 split: split_nat_case) 
   3.338 +done
   3.339 +
   3.340 +lemma sats_is_nat_case_fm:
   3.341 +  assumes is_b_iff_sats: 
   3.342 +      "!!a b. [| a \<in> A; b \<in> A|] 
   3.343 +              ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))"
   3.344 +  shows 
   3.345 +      "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   3.346 +       ==> sats(A, is_nat_case_fm(x,p,y,z), env) <-> 
   3.347 +           is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))"
   3.348 +apply (frule lt_length_in_nat, assumption)  
   3.349 +apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym])
   3.350 +done
   3.351 +
   3.352 +lemma is_nat_case_iff_sats:
   3.353 +  "[| (!!a b. [| a \<in> A; b \<in> A|] 
   3.354 +              ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env))));
   3.355 +      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   3.356 +      i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   3.357 +   ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)" 
   3.358 +by (simp add: sats_is_nat_case_fm [of A is_b])
   3.359 +
   3.360 +
   3.361 +text{*The second argument of @{term is_b} gives it direct access to @{term x},
   3.362 +  which is essential for handling free variable references.  Without this 
   3.363 +  argument, we cannot prove reflection for @{term iterates_MH}.*}
   3.364 +theorem is_nat_case_reflection:
   3.365 +  assumes is_b_reflection:
   3.366 +    "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)), 
   3.367 +                     \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
   3.368 +  shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)), 
   3.369 +               \<lambda>i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]"
   3.370 +apply (simp (no_asm_use) only: is_nat_case_def setclass_simps)
   3.371 +apply (intro FOL_reflections function_reflections 
   3.372 +             restriction_reflection is_b_reflection quasinat_reflection)  
   3.373 +done
   3.374 +
   3.375 +
   3.376 +
   3.377 +subsection{*The Operator @{term iterates_MH}, Needed for Iteration*}
   3.378 +
   3.379 +(*  iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
   3.380 +   "iterates_MH(M,isF,v,n,g,z) ==
   3.381 +        is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
   3.382 +                    n, z)" *)
   3.383 +constdefs iterates_MH_fm :: "[[i,i]=>i, i, i, i, i]=>i"
   3.384 + "iterates_MH_fm(isF,v,n,g,z) == 
   3.385 +    is_nat_case_fm(v, 
   3.386 +      \<lambda>m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0), 
   3.387 +                     Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))), 
   3.388 +      n, z)"
   3.389 +
   3.390 +lemma iterates_MH_type [TC]:
   3.391 +     "[| p(1,0) \<in> formula;  
   3.392 +         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] 
   3.393 +      ==> iterates_MH_fm(p,v,x,y,z) \<in> formula"
   3.394 +by (simp add: iterates_MH_fm_def) 
   3.395 +
   3.396 +
   3.397 +lemma arity_iterates_MH_fm [simp]:
   3.398 +     "[| p(1,0) \<in> formula; 
   3.399 +         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] 
   3.400 +      ==> arity(iterates_MH_fm(p,v,x,y,z)) = 
   3.401 +          succ(v) \<union> succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(p(1,0)) #- 4)"
   3.402 +apply (subgoal_tac "arity(p(1,0)) \<in> nat")
   3.403 +apply typecheck
   3.404 +apply (simp add: nat_imp_quasinat iterates_MH_fm_def Un_ac
   3.405 +            split: split_nat_case, clarify)
   3.406 +apply (rename_tac i j)
   3.407 +apply (drule eq_succ_imp_eq_m1, simp) 
   3.408 +apply (drule eq_succ_imp_eq_m1, simp)
   3.409 +apply (simp add: diff_Un_distrib succ_Un_distrib Un_ac diff_diff_left)
   3.410 +done
   3.411 +
   3.412 +lemma sats_iterates_MH_fm:
   3.413 +  assumes is_F_iff_sats: 
   3.414 +      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|] 
   3.415 +              ==> is_F(a,b) <->
   3.416 +                  sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
   3.417 +  shows 
   3.418 +      "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   3.419 +       ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <-> 
   3.420 +           iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
   3.421 +by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm 
   3.422 +              is_F_iff_sats [symmetric])
   3.423 +
   3.424 +lemma iterates_MH_iff_sats:
   3.425 +  "[| (!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|] 
   3.426 +              ==> is_F(a,b) <->
   3.427 +                  sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env))))));
   3.428 +      nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   3.429 +      i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   3.430 +   ==> iterates_MH(**A, is_F, v, x, y, z) <-> 
   3.431 +       sats(A, iterates_MH_fm(p,i',i,j,k), env)"
   3.432 +apply (rule iff_sym) 
   3.433 +apply (rule iff_trans) 
   3.434 +apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all) 
   3.435 +done
   3.436 +
   3.437 +theorem iterates_MH_reflection:
   3.438 +  assumes p_reflection:
   3.439 +    "!!f g h. REFLECTS[\<lambda>x. p(L, f(x), g(x)), 
   3.440 +                     \<lambda>i x. p(**Lset(i), f(x), g(x))]"
   3.441 + shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)), 
   3.442 +               \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i)), e(x), f(x), g(x), h(x))]"
   3.443 +apply (simp (no_asm_use) only: iterates_MH_def)
   3.444 +txt{*Must be careful: simplifying with @{text setclass_simps} above would
   3.445 +     change @{text "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> Lset(i)"}, when
   3.446 +     it would no longer match rule @{text is_nat_case_reflection}. *}
   3.447 +apply (rule is_nat_case_reflection) 
   3.448 +apply (simp (no_asm_use) only: setclass_simps)
   3.449 +apply (intro FOL_reflections function_reflections is_nat_case_reflection
   3.450 +             restriction_reflection p_reflection)  
   3.451 +done
   3.452 +
   3.453 +
   3.454 +
   3.455 +subsection{*@{term L} is Closed Under the Operator @{term list}*} 
   3.456 +
   3.457 +
   3.458 +lemma list_replacement1_Reflects:
   3.459 + "REFLECTS
   3.460 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
   3.461 +         is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)),
   3.462 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
   3.463 +         is_wfrec(**Lset(i), 
   3.464 +                  iterates_MH(**Lset(i), 
   3.465 +                          is_list_functor(**Lset(i), A), 0), memsn, u, y))]"
   3.466 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
   3.467 +          iterates_MH_reflection list_functor_reflection) 
   3.468 +
   3.469 +lemma list_replacement1: 
   3.470 +   "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
   3.471 +apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   3.472 +apply (rule strong_replacementI) 
   3.473 +apply (rule rallI)
   3.474 +apply (rename_tac B)   
   3.475 +apply (rule separation_CollectI) 
   3.476 +apply (insert nonempty) 
   3.477 +apply (subgoal_tac "L(Memrel(succ(n)))") 
   3.478 +apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast ) 
   3.479 +apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
   3.480 +apply (drule subset_Lset_ltD, assumption) 
   3.481 +apply (erule reflection_imp_L_separation)
   3.482 +  apply (simp_all add: lt_Ord2)
   3.483 +apply (rule DPowI2)
   3.484 +apply (rename_tac v) 
   3.485 +apply (rule bex_iff_sats conj_iff_sats)+
   3.486 +apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
   3.487 +apply (rule sep_rules | simp)+
   3.488 +txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
   3.489 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   3.490 +apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
   3.491 +apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed)
   3.492 +done
   3.493 +
   3.494 +
   3.495 +lemma list_replacement2_Reflects:
   3.496 + "REFLECTS
   3.497 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
   3.498 +         (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
   3.499 +           is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0),
   3.500 +                              msn, u, x)),
   3.501 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
   3.502 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
   3.503 +          successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
   3.504 +           is_wfrec (**Lset(i), 
   3.505 +                 iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0),
   3.506 +                     msn, u, x))]"
   3.507 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
   3.508 +          iterates_MH_reflection list_functor_reflection) 
   3.509 +
   3.510 +
   3.511 +lemma list_replacement2: 
   3.512 +   "L(A) ==> strong_replacement(L, 
   3.513 +         \<lambda>n y. n\<in>nat & 
   3.514 +               (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
   3.515 +               is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), 
   3.516 +                        msn, n, y)))"
   3.517 +apply (rule strong_replacementI) 
   3.518 +apply (rule rallI)
   3.519 +apply (rename_tac B)   
   3.520 +apply (rule separation_CollectI) 
   3.521 +apply (insert nonempty) 
   3.522 +apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE) 
   3.523 +apply (blast intro: L_nat) 
   3.524 +apply (rule ReflectsE [OF list_replacement2_Reflects], assumption)
   3.525 +apply (drule subset_Lset_ltD, assumption) 
   3.526 +apply (erule reflection_imp_L_separation)
   3.527 +  apply (simp_all add: lt_Ord2)
   3.528 +apply (rule DPowI2)
   3.529 +apply (rename_tac v) 
   3.530 +apply (rule bex_iff_sats conj_iff_sats)+
   3.531 +apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
   3.532 +apply (rule sep_rules | simp)+
   3.533 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   3.534 +apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
   3.535 +apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed)
   3.536 +done
   3.537 +
   3.538 +
   3.539 +
   3.540  end
     4.1 --- a/src/ZF/Constructible/Relative.thy	Tue Jul 16 16:28:49 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Jul 16 16:29:36 2002 +0200
     4.3 @@ -28,6 +28,15 @@
     4.4    successor :: "[i=>o,i,i] => o"
     4.5      "successor(M,a,z) == is_cons(M,a,a,z)"
     4.6  
     4.7 +  number1 :: "[i=>o,i] => o"
     4.8 +    "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
     4.9 +
    4.10 +  number2 :: "[i=>o,i] => o"
    4.11 +    "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
    4.12 +
    4.13 +  number3 :: "[i=>o,i] => o"
    4.14 +    "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
    4.15 +
    4.16    powerset :: "[i=>o,i,i] => o"
    4.17      "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
    4.18  
    4.19 @@ -161,15 +170,6 @@
    4.20      --{*omega is a limit ordinal none of whose elements are limit*}
    4.21      "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
    4.22  
    4.23 -  number1 :: "[i=>o,i] => o"
    4.24 -    "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
    4.25 -
    4.26 -  number2 :: "[i=>o,i] => o"
    4.27 -    "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
    4.28 -
    4.29 -  number3 :: "[i=>o,i] => o"
    4.30 -    "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
    4.31 -
    4.32    is_quasinat :: "[i=>o,i] => o"
    4.33      "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
    4.34  
    4.35 @@ -177,7 +177,7 @@
    4.36      "is_nat_case(M, a, is_b, k, z) == 
    4.37         (empty(M,k) --> z=a) &
    4.38         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
    4.39 -       (is_quasinat(M,k) | z=0)"
    4.40 +       (is_quasinat(M,k) | empty(M,z))"
    4.41  
    4.42    relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o"
    4.43      "relativize1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
    4.44 @@ -669,8 +669,10 @@
    4.45   apply (simp_all add: relativize1_def) 
    4.46  done
    4.47  
    4.48 -(*Needed?  surely better to replace is_nat_case by nat_case?*)
    4.49 -lemma (in M_triv_axioms) is_nat_case_cong [cong]:
    4.50 +(*NOT for the simplifier.  The assumption M(z') is apparently necessary, but 
    4.51 +  causes the error "Failed congruence proof!"  It may be better to replace
    4.52 +  is_nat_case by nat_case before attempting congruence reasoning.*)
    4.53 +lemma (in M_triv_axioms) is_nat_case_cong:
    4.54       "[| a = a'; k = k';  z = z';  M(z');
    4.55         !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
    4.56        ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
     5.1 --- a/src/ZF/Constructible/Separation.thy	Tue Jul 16 16:28:49 2002 +0200
     5.2 +++ b/src/ZF/Constructible/Separation.thy	Tue Jul 16 16:29:36 2002 +0200
     5.3 @@ -457,6 +457,10 @@
     5.4  done
     5.5  
     5.6  
     5.7 +subsection{*Instantiating the locale @{text M_axioms}*}
     5.8 +text{*Separation (and Strong Replacement) for basic set-theoretic constructions
     5.9 +such as intersection, Cartesian Product and image.*}
    5.10 +
    5.11  ML
    5.12  {*
    5.13  val Inter_separation = thm "Inter_separation";
    5.14 @@ -481,119 +485,119 @@
    5.15       well_ord_iso_separation, obase_separation,
    5.16       obase_equals_separation, omap_replacement, is_recfun_separation]
    5.17  
    5.18 -fun axiomsL th =
    5.19 -    kill_flex_triv_prems (m_axioms MRS (trivaxL th));
    5.20 +fun axioms_L th =
    5.21 +    kill_flex_triv_prems (m_axioms MRS (triv_axioms_L th));
    5.22  
    5.23 -bind_thm ("cartprod_iff", axiomsL (thm "M_axioms.cartprod_iff"));
    5.24 -bind_thm ("cartprod_closed", axiomsL (thm "M_axioms.cartprod_closed"));
    5.25 -bind_thm ("sum_closed", axiomsL (thm "M_axioms.sum_closed"));
    5.26 -bind_thm ("M_converse_iff", axiomsL (thm "M_axioms.M_converse_iff"));
    5.27 -bind_thm ("converse_closed", axiomsL (thm "M_axioms.converse_closed"));
    5.28 -bind_thm ("converse_abs", axiomsL (thm "M_axioms.converse_abs"));
    5.29 -bind_thm ("image_closed", axiomsL (thm "M_axioms.image_closed"));
    5.30 -bind_thm ("vimage_abs", axiomsL (thm "M_axioms.vimage_abs"));
    5.31 -bind_thm ("vimage_closed", axiomsL (thm "M_axioms.vimage_closed"));
    5.32 -bind_thm ("domain_abs", axiomsL (thm "M_axioms.domain_abs"));
    5.33 -bind_thm ("domain_closed", axiomsL (thm "M_axioms.domain_closed"));
    5.34 -bind_thm ("range_abs", axiomsL (thm "M_axioms.range_abs"));
    5.35 -bind_thm ("range_closed", axiomsL (thm "M_axioms.range_closed"));
    5.36 -bind_thm ("field_abs", axiomsL (thm "M_axioms.field_abs"));
    5.37 -bind_thm ("field_closed", axiomsL (thm "M_axioms.field_closed"));
    5.38 -bind_thm ("relation_abs", axiomsL (thm "M_axioms.relation_abs"));
    5.39 -bind_thm ("function_abs", axiomsL (thm "M_axioms.function_abs"));
    5.40 -bind_thm ("apply_closed", axiomsL (thm "M_axioms.apply_closed"));
    5.41 -bind_thm ("apply_abs", axiomsL (thm "M_axioms.apply_abs"));
    5.42 -bind_thm ("typed_function_abs", axiomsL (thm "M_axioms.typed_function_abs"));
    5.43 -bind_thm ("injection_abs", axiomsL (thm "M_axioms.injection_abs"));
    5.44 -bind_thm ("surjection_abs", axiomsL (thm "M_axioms.surjection_abs"));
    5.45 -bind_thm ("bijection_abs", axiomsL (thm "M_axioms.bijection_abs"));
    5.46 -bind_thm ("M_comp_iff", axiomsL (thm "M_axioms.M_comp_iff"));
    5.47 -bind_thm ("comp_closed", axiomsL (thm "M_axioms.comp_closed"));
    5.48 -bind_thm ("composition_abs", axiomsL (thm "M_axioms.composition_abs"));
    5.49 -bind_thm ("restriction_is_function", axiomsL (thm "M_axioms.restriction_is_function"));
    5.50 -bind_thm ("restriction_abs", axiomsL (thm "M_axioms.restriction_abs"));
    5.51 -bind_thm ("M_restrict_iff", axiomsL (thm "M_axioms.M_restrict_iff"));
    5.52 -bind_thm ("restrict_closed", axiomsL (thm "M_axioms.restrict_closed"));
    5.53 -bind_thm ("Inter_abs", axiomsL (thm "M_axioms.Inter_abs"));
    5.54 -bind_thm ("Inter_closed", axiomsL (thm "M_axioms.Inter_closed"));
    5.55 -bind_thm ("Int_closed", axiomsL (thm "M_axioms.Int_closed"));
    5.56 -bind_thm ("finite_fun_closed", axiomsL (thm "M_axioms.finite_fun_closed"));
    5.57 -bind_thm ("is_funspace_abs", axiomsL (thm "M_axioms.is_funspace_abs"));
    5.58 -bind_thm ("succ_fun_eq2", axiomsL (thm "M_axioms.succ_fun_eq2"));
    5.59 -bind_thm ("funspace_succ", axiomsL (thm "M_axioms.funspace_succ"));
    5.60 -bind_thm ("finite_funspace_closed", axiomsL (thm "M_axioms.finite_funspace_closed"));
    5.61 +bind_thm ("cartprod_iff", axioms_L (thm "M_axioms.cartprod_iff"));
    5.62 +bind_thm ("cartprod_closed", axioms_L (thm "M_axioms.cartprod_closed"));
    5.63 +bind_thm ("sum_closed", axioms_L (thm "M_axioms.sum_closed"));
    5.64 +bind_thm ("M_converse_iff", axioms_L (thm "M_axioms.M_converse_iff"));
    5.65 +bind_thm ("converse_closed", axioms_L (thm "M_axioms.converse_closed"));
    5.66 +bind_thm ("converse_abs", axioms_L (thm "M_axioms.converse_abs"));
    5.67 +bind_thm ("image_closed", axioms_L (thm "M_axioms.image_closed"));
    5.68 +bind_thm ("vimage_abs", axioms_L (thm "M_axioms.vimage_abs"));
    5.69 +bind_thm ("vimage_closed", axioms_L (thm "M_axioms.vimage_closed"));
    5.70 +bind_thm ("domain_abs", axioms_L (thm "M_axioms.domain_abs"));
    5.71 +bind_thm ("domain_closed", axioms_L (thm "M_axioms.domain_closed"));
    5.72 +bind_thm ("range_abs", axioms_L (thm "M_axioms.range_abs"));
    5.73 +bind_thm ("range_closed", axioms_L (thm "M_axioms.range_closed"));
    5.74 +bind_thm ("field_abs", axioms_L (thm "M_axioms.field_abs"));
    5.75 +bind_thm ("field_closed", axioms_L (thm "M_axioms.field_closed"));
    5.76 +bind_thm ("relation_abs", axioms_L (thm "M_axioms.relation_abs"));
    5.77 +bind_thm ("function_abs", axioms_L (thm "M_axioms.function_abs"));
    5.78 +bind_thm ("apply_closed", axioms_L (thm "M_axioms.apply_closed"));
    5.79 +bind_thm ("apply_abs", axioms_L (thm "M_axioms.apply_abs"));
    5.80 +bind_thm ("typed_function_abs", axioms_L (thm "M_axioms.typed_function_abs"));
    5.81 +bind_thm ("injection_abs", axioms_L (thm "M_axioms.injection_abs"));
    5.82 +bind_thm ("surjection_abs", axioms_L (thm "M_axioms.surjection_abs"));
    5.83 +bind_thm ("bijection_abs", axioms_L (thm "M_axioms.bijection_abs"));
    5.84 +bind_thm ("M_comp_iff", axioms_L (thm "M_axioms.M_comp_iff"));
    5.85 +bind_thm ("comp_closed", axioms_L (thm "M_axioms.comp_closed"));
    5.86 +bind_thm ("composition_abs", axioms_L (thm "M_axioms.composition_abs"));
    5.87 +bind_thm ("restriction_is_function", axioms_L (thm "M_axioms.restriction_is_function"));
    5.88 +bind_thm ("restriction_abs", axioms_L (thm "M_axioms.restriction_abs"));
    5.89 +bind_thm ("M_restrict_iff", axioms_L (thm "M_axioms.M_restrict_iff"));
    5.90 +bind_thm ("restrict_closed", axioms_L (thm "M_axioms.restrict_closed"));
    5.91 +bind_thm ("Inter_abs", axioms_L (thm "M_axioms.Inter_abs"));
    5.92 +bind_thm ("Inter_closed", axioms_L (thm "M_axioms.Inter_closed"));
    5.93 +bind_thm ("Int_closed", axioms_L (thm "M_axioms.Int_closed"));
    5.94 +bind_thm ("finite_fun_closed", axioms_L (thm "M_axioms.finite_fun_closed"));
    5.95 +bind_thm ("is_funspace_abs", axioms_L (thm "M_axioms.is_funspace_abs"));
    5.96 +bind_thm ("succ_fun_eq2", axioms_L (thm "M_axioms.succ_fun_eq2"));
    5.97 +bind_thm ("funspace_succ", axioms_L (thm "M_axioms.funspace_succ"));
    5.98 +bind_thm ("finite_funspace_closed", axioms_L (thm "M_axioms.finite_funspace_closed"));
    5.99  *}
   5.100  
   5.101  ML
   5.102  {*
   5.103 -bind_thm ("is_recfun_equal", axiomsL (thm "M_axioms.is_recfun_equal"));  
   5.104 -bind_thm ("is_recfun_cut", axiomsL (thm "M_axioms.is_recfun_cut")); 
   5.105 -bind_thm ("is_recfun_functional", axiomsL (thm "M_axioms.is_recfun_functional"));
   5.106 -bind_thm ("is_recfun_relativize", axiomsL (thm "M_axioms.is_recfun_relativize"));
   5.107 -bind_thm ("is_recfun_restrict", axiomsL (thm "M_axioms.is_recfun_restrict"));
   5.108 -bind_thm ("univalent_is_recfun", axiomsL (thm "M_axioms.univalent_is_recfun"));
   5.109 -bind_thm ("exists_is_recfun_indstep", axiomsL (thm "M_axioms.exists_is_recfun_indstep"));
   5.110 -bind_thm ("wellfounded_exists_is_recfun", axiomsL (thm "M_axioms.wellfounded_exists_is_recfun"));
   5.111 -bind_thm ("wf_exists_is_recfun", axiomsL (thm "M_axioms.wf_exists_is_recfun")); 
   5.112 -bind_thm ("is_recfun_abs", axiomsL (thm "M_axioms.is_recfun_abs"));
   5.113 -bind_thm ("irreflexive_abs", axiomsL (thm "M_axioms.irreflexive_abs"));  
   5.114 -bind_thm ("transitive_rel_abs", axiomsL (thm "M_axioms.transitive_rel_abs"));  
   5.115 -bind_thm ("linear_rel_abs", axiomsL (thm "M_axioms.linear_rel_abs"));  
   5.116 -bind_thm ("wellordered_is_trans_on", axiomsL (thm "M_axioms.wellordered_is_trans_on")); 
   5.117 -bind_thm ("wellordered_is_linear", axiomsL (thm "M_axioms.wellordered_is_linear")); 
   5.118 -bind_thm ("wellordered_is_wellfounded_on", axiomsL (thm "M_axioms.wellordered_is_wellfounded_on")); 
   5.119 -bind_thm ("wellfounded_imp_wellfounded_on", axiomsL (thm "M_axioms.wellfounded_imp_wellfounded_on")); 
   5.120 -bind_thm ("wellfounded_on_subset_A", axiomsL (thm "M_axioms.wellfounded_on_subset_A"));
   5.121 -bind_thm ("wellfounded_on_iff_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_iff_wellfounded"));
   5.122 -bind_thm ("wellfounded_on_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_imp_wellfounded"));
   5.123 -bind_thm ("wellfounded_on_field_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_field_imp_wellfounded"));
   5.124 -bind_thm ("wellfounded_iff_wellfounded_on_field", axiomsL (thm "M_axioms.wellfounded_iff_wellfounded_on_field"));
   5.125 -bind_thm ("wellfounded_induct", axiomsL (thm "M_axioms.wellfounded_induct")); 
   5.126 -bind_thm ("wellfounded_on_induct", axiomsL (thm "M_axioms.wellfounded_on_induct")); 
   5.127 -bind_thm ("wellfounded_on_induct2", axiomsL (thm "M_axioms.wellfounded_on_induct2")); 
   5.128 -bind_thm ("linear_imp_relativized", axiomsL (thm "M_axioms.linear_imp_relativized")); 
   5.129 -bind_thm ("trans_on_imp_relativized", axiomsL (thm "M_axioms.trans_on_imp_relativized")); 
   5.130 -bind_thm ("wf_on_imp_relativized", axiomsL (thm "M_axioms.wf_on_imp_relativized")); 
   5.131 -bind_thm ("wf_imp_relativized", axiomsL (thm "M_axioms.wf_imp_relativized")); 
   5.132 -bind_thm ("well_ord_imp_relativized", axiomsL (thm "M_axioms.well_ord_imp_relativized")); 
   5.133 -bind_thm ("order_isomorphism_abs", axiomsL (thm "M_axioms.order_isomorphism_abs"));  
   5.134 -bind_thm ("pred_set_abs", axiomsL (thm "M_axioms.pred_set_abs"));  
   5.135 +bind_thm ("is_recfun_equal", axioms_L (thm "M_axioms.is_recfun_equal"));  
   5.136 +bind_thm ("is_recfun_cut", axioms_L (thm "M_axioms.is_recfun_cut")); 
   5.137 +bind_thm ("is_recfun_functional", axioms_L (thm "M_axioms.is_recfun_functional"));
   5.138 +bind_thm ("is_recfun_relativize", axioms_L (thm "M_axioms.is_recfun_relativize"));
   5.139 +bind_thm ("is_recfun_restrict", axioms_L (thm "M_axioms.is_recfun_restrict"));
   5.140 +bind_thm ("univalent_is_recfun", axioms_L (thm "M_axioms.univalent_is_recfun"));
   5.141 +bind_thm ("exists_is_recfun_indstep", axioms_L (thm "M_axioms.exists_is_recfun_indstep"));
   5.142 +bind_thm ("wellfounded_exists_is_recfun", axioms_L (thm "M_axioms.wellfounded_exists_is_recfun"));
   5.143 +bind_thm ("wf_exists_is_recfun", axioms_L (thm "M_axioms.wf_exists_is_recfun")); 
   5.144 +bind_thm ("is_recfun_abs", axioms_L (thm "M_axioms.is_recfun_abs"));
   5.145 +bind_thm ("irreflexive_abs", axioms_L (thm "M_axioms.irreflexive_abs"));  
   5.146 +bind_thm ("transitive_rel_abs", axioms_L (thm "M_axioms.transitive_rel_abs"));  
   5.147 +bind_thm ("linear_rel_abs", axioms_L (thm "M_axioms.linear_rel_abs"));  
   5.148 +bind_thm ("wellordered_is_trans_on", axioms_L (thm "M_axioms.wellordered_is_trans_on")); 
   5.149 +bind_thm ("wellordered_is_linear", axioms_L (thm "M_axioms.wellordered_is_linear")); 
   5.150 +bind_thm ("wellordered_is_wellfounded_on", axioms_L (thm "M_axioms.wellordered_is_wellfounded_on")); 
   5.151 +bind_thm ("wellfounded_imp_wellfounded_on", axioms_L (thm "M_axioms.wellfounded_imp_wellfounded_on")); 
   5.152 +bind_thm ("wellfounded_on_subset_A", axioms_L (thm "M_axioms.wellfounded_on_subset_A"));
   5.153 +bind_thm ("wellfounded_on_iff_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_iff_wellfounded"));
   5.154 +bind_thm ("wellfounded_on_imp_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_imp_wellfounded"));
   5.155 +bind_thm ("wellfounded_on_field_imp_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_field_imp_wellfounded"));
   5.156 +bind_thm ("wellfounded_iff_wellfounded_on_field", axioms_L (thm "M_axioms.wellfounded_iff_wellfounded_on_field"));
   5.157 +bind_thm ("wellfounded_induct", axioms_L (thm "M_axioms.wellfounded_induct")); 
   5.158 +bind_thm ("wellfounded_on_induct", axioms_L (thm "M_axioms.wellfounded_on_induct")); 
   5.159 +bind_thm ("wellfounded_on_induct2", axioms_L (thm "M_axioms.wellfounded_on_induct2")); 
   5.160 +bind_thm ("linear_imp_relativized", axioms_L (thm "M_axioms.linear_imp_relativized")); 
   5.161 +bind_thm ("trans_on_imp_relativized", axioms_L (thm "M_axioms.trans_on_imp_relativized")); 
   5.162 +bind_thm ("wf_on_imp_relativized", axioms_L (thm "M_axioms.wf_on_imp_relativized")); 
   5.163 +bind_thm ("wf_imp_relativized", axioms_L (thm "M_axioms.wf_imp_relativized")); 
   5.164 +bind_thm ("well_ord_imp_relativized", axioms_L (thm "M_axioms.well_ord_imp_relativized")); 
   5.165 +bind_thm ("order_isomorphism_abs", axioms_L (thm "M_axioms.order_isomorphism_abs"));  
   5.166 +bind_thm ("pred_set_abs", axioms_L (thm "M_axioms.pred_set_abs"));  
   5.167  *}
   5.168  
   5.169  ML
   5.170  {*
   5.171 -bind_thm ("pred_closed", axiomsL (thm "M_axioms.pred_closed"));  
   5.172 -bind_thm ("membership_abs", axiomsL (thm "M_axioms.membership_abs"));  
   5.173 -bind_thm ("M_Memrel_iff", axiomsL (thm "M_axioms.M_Memrel_iff"));
   5.174 -bind_thm ("Memrel_closed", axiomsL (thm "M_axioms.Memrel_closed"));  
   5.175 -bind_thm ("wellordered_iso_predD", axiomsL (thm "M_axioms.wellordered_iso_predD"));
   5.176 -bind_thm ("wellordered_iso_pred_eq", axiomsL (thm "M_axioms.wellordered_iso_pred_eq"));
   5.177 -bind_thm ("wellfounded_on_asym", axiomsL (thm "M_axioms.wellfounded_on_asym"));
   5.178 -bind_thm ("wellordered_asym", axiomsL (thm "M_axioms.wellordered_asym"));
   5.179 -bind_thm ("ord_iso_pred_imp_lt", axiomsL (thm "M_axioms.ord_iso_pred_imp_lt"));
   5.180 -bind_thm ("obase_iff", axiomsL (thm "M_axioms.obase_iff"));
   5.181 -bind_thm ("omap_iff", axiomsL (thm "M_axioms.omap_iff"));
   5.182 -bind_thm ("omap_unique", axiomsL (thm "M_axioms.omap_unique"));
   5.183 -bind_thm ("omap_yields_Ord", axiomsL (thm "M_axioms.omap_yields_Ord"));
   5.184 -bind_thm ("otype_iff", axiomsL (thm "M_axioms.otype_iff"));
   5.185 -bind_thm ("otype_eq_range", axiomsL (thm "M_axioms.otype_eq_range"));
   5.186 -bind_thm ("Ord_otype", axiomsL (thm "M_axioms.Ord_otype"));
   5.187 -bind_thm ("domain_omap", axiomsL (thm "M_axioms.domain_omap"));
   5.188 -bind_thm ("omap_subset", axiomsL (thm "M_axioms.omap_subset")); 
   5.189 -bind_thm ("omap_funtype", axiomsL (thm "M_axioms.omap_funtype")); 
   5.190 -bind_thm ("wellordered_omap_bij", axiomsL (thm "M_axioms.wellordered_omap_bij"));
   5.191 -bind_thm ("omap_ord_iso", axiomsL (thm "M_axioms.omap_ord_iso"));
   5.192 -bind_thm ("Ord_omap_image_pred", axiomsL (thm "M_axioms.Ord_omap_image_pred"));
   5.193 -bind_thm ("restrict_omap_ord_iso", axiomsL (thm "M_axioms.restrict_omap_ord_iso"));
   5.194 -bind_thm ("obase_equals", axiomsL (thm "M_axioms.obase_equals")); 
   5.195 -bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype"));
   5.196 -bind_thm ("obase_exists", axiomsL (thm "M_axioms.obase_exists"));
   5.197 -bind_thm ("omap_exists", axiomsL (thm "M_axioms.omap_exists"));
   5.198 -bind_thm ("otype_exists", axiomsL (thm "M_axioms.otype_exists"));
   5.199 -bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype"));
   5.200 -bind_thm ("ordertype_exists", axiomsL (thm "M_axioms.ordertype_exists"));
   5.201 -bind_thm ("relativized_imp_well_ord", axiomsL (thm "M_axioms.relativized_imp_well_ord")); 
   5.202 -bind_thm ("well_ord_abs", axiomsL (thm "M_axioms.well_ord_abs"));  
   5.203 +bind_thm ("pred_closed", axioms_L (thm "M_axioms.pred_closed"));  
   5.204 +bind_thm ("membership_abs", axioms_L (thm "M_axioms.membership_abs"));  
   5.205 +bind_thm ("M_Memrel_iff", axioms_L (thm "M_axioms.M_Memrel_iff"));
   5.206 +bind_thm ("Memrel_closed", axioms_L (thm "M_axioms.Memrel_closed"));  
   5.207 +bind_thm ("wellordered_iso_predD", axioms_L (thm "M_axioms.wellordered_iso_predD"));
   5.208 +bind_thm ("wellordered_iso_pred_eq", axioms_L (thm "M_axioms.wellordered_iso_pred_eq"));
   5.209 +bind_thm ("wellfounded_on_asym", axioms_L (thm "M_axioms.wellfounded_on_asym"));
   5.210 +bind_thm ("wellordered_asym", axioms_L (thm "M_axioms.wellordered_asym"));
   5.211 +bind_thm ("ord_iso_pred_imp_lt", axioms_L (thm "M_axioms.ord_iso_pred_imp_lt"));
   5.212 +bind_thm ("obase_iff", axioms_L (thm "M_axioms.obase_iff"));
   5.213 +bind_thm ("omap_iff", axioms_L (thm "M_axioms.omap_iff"));
   5.214 +bind_thm ("omap_unique", axioms_L (thm "M_axioms.omap_unique"));
   5.215 +bind_thm ("omap_yields_Ord", axioms_L (thm "M_axioms.omap_yields_Ord"));
   5.216 +bind_thm ("otype_iff", axioms_L (thm "M_axioms.otype_iff"));
   5.217 +bind_thm ("otype_eq_range", axioms_L (thm "M_axioms.otype_eq_range"));
   5.218 +bind_thm ("Ord_otype", axioms_L (thm "M_axioms.Ord_otype"));
   5.219 +bind_thm ("domain_omap", axioms_L (thm "M_axioms.domain_omap"));
   5.220 +bind_thm ("omap_subset", axioms_L (thm "M_axioms.omap_subset")); 
   5.221 +bind_thm ("omap_funtype", axioms_L (thm "M_axioms.omap_funtype")); 
   5.222 +bind_thm ("wellordered_omap_bij", axioms_L (thm "M_axioms.wellordered_omap_bij"));
   5.223 +bind_thm ("omap_ord_iso", axioms_L (thm "M_axioms.omap_ord_iso"));
   5.224 +bind_thm ("Ord_omap_image_pred", axioms_L (thm "M_axioms.Ord_omap_image_pred"));
   5.225 +bind_thm ("restrict_omap_ord_iso", axioms_L (thm "M_axioms.restrict_omap_ord_iso"));
   5.226 +bind_thm ("obase_equals", axioms_L (thm "M_axioms.obase_equals")); 
   5.227 +bind_thm ("omap_ord_iso_otype", axioms_L (thm "M_axioms.omap_ord_iso_otype"));
   5.228 +bind_thm ("obase_exists", axioms_L (thm "M_axioms.obase_exists"));
   5.229 +bind_thm ("omap_exists", axioms_L (thm "M_axioms.omap_exists"));
   5.230 +bind_thm ("otype_exists", axioms_L (thm "M_axioms.otype_exists"));
   5.231 +bind_thm ("omap_ord_iso_otype", axioms_L (thm "M_axioms.omap_ord_iso_otype"));
   5.232 +bind_thm ("ordertype_exists", axioms_L (thm "M_axioms.ordertype_exists"));
   5.233 +bind_thm ("relativized_imp_well_ord", axioms_L (thm "M_axioms.relativized_imp_well_ord")); 
   5.234 +bind_thm ("well_ord_abs", axioms_L (thm "M_axioms.well_ord_abs"));  
   5.235  *}
   5.236  
   5.237  declare cartprod_closed [intro,simp]
     6.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Jul 16 16:28:49 2002 +0200
     6.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Jul 16 16:29:36 2002 +0200
     6.3 @@ -611,19 +611,6 @@
     6.4  apply (simp add: wfrec_relativize, blast) 
     6.5  done
     6.6  
     6.7 -lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
     6.8 -     "[|wf(r); M(r); 
     6.9 -        strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
    6.10 -        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
    6.11 -      ==> M(a) --> M(wfrec(r,a,H))"
    6.12 -apply (rule_tac a=a in wf_induct, assumption+)
    6.13 -apply (subst wfrec, assumption, clarify)
    6.14 -apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" 
    6.15 -       in rspec [THEN rspec]) 
    6.16 -apply (simp_all add: function_lam) 
    6.17 -apply (blast intro: dest: pair_components_in_M ) 
    6.18 -done
    6.19 -
    6.20  text{*Full version not assuming transitivity, but maybe not very useful.*}
    6.21  theorem (in M_wfrank) wfrec_closed:
    6.22       "[|wf(r); M(r); M(a);