src/ZF/Constructible/Rec_Separation.thy

 
 lemma rtran_closure_mem_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> rtran_closure_mem(##A, x, y, z) \<longleftrightarrow> sats(A, rtran_closure_mem_fm(i,j,k), env)"
-by (simp add: sats_rtran_closure_mem_fm)
+by (simp)
 
 lemma rtran_closure_mem_reflection:
      "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
                \<lambda>i x. rtran_closure_mem(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: rtran_closure_mem_def)

 
 subsubsection\<open>Instantiating the locale \<open>M_trancl\<close>\<close>
 
 lemma M_trancl_axioms_L: "M_trancl_axioms(L)"
   apply (rule M_trancl_axioms.intro)
-   apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+
+   apply (assumption | rule rtrancl_separation wellfounded_trancl_separation L_nat)+
   done
 
-theorem M_trancl_L: "PROP M_trancl(L)"
+theorem M_trancl_L: "M_trancl(L)"
 by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
 
 interpretation L?: M_trancl L by (rule M_trancl_L)
 
 

    "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" 
          in gen_separation_multi [OF list_replacement1_Reflects], 
-       auto simp add: nonempty)
+       auto)
 apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI)
 apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
 

    "L(A) ==> strong_replacement(L,
          \<lambda>n y. n\<in>nat & is_iterates(L, is_list_functor(L,A), 0, n, y))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{A,B,0,nat}" 
          in gen_separation_multi [OF list_replacement2_Reflects], 
-       auto simp add: L_nat nonempty)
+       auto)
 apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI)
 apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+
 done
 
 

    "iterates_replacement(L, is_formula_functor(L), 0)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,n,0,Memrel(succ(n))}" 
          in gen_separation_multi [OF formula_replacement1_Reflects], 
-       auto simp add: nonempty)
+       auto)
 apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI)
 apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
 

    "strong_replacement(L,
          \<lambda>n y. n\<in>nat & is_iterates(L, is_formula_functor(L), 0, n, y))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,0,nat}" 
          in gen_separation_multi [OF formula_replacement2_Reflects], 
-       auto simp add: nonempty L_nat)
+       auto)
 apply (rule_tac env="[B,0,nat]" in DPow_LsetI)
 apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+
 done
 
 text\<open>NB The proofs for type \<^term>\<open>formula\<close> are virtually identical to those

 
 lemma nth_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> is_nth(##A, x, y, z) \<longleftrightarrow> sats(A, nth_fm(i,j,k), env)"
-by (simp add: sats_nth_fm)
+by (simp)
 
 theorem nth_reflection:
      "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),  
                \<lambda>i x. is_nth(##Lset(i), f(x), g(x), h(x))]"
 apply (simp only: is_nth_def)

         list_replacement1 list_replacement2
         formula_replacement1 formula_replacement2
         nth_replacement)+
   done
 
-theorem M_datatypes_L: "PROP M_datatypes(L)"
+theorem M_datatypes_L: "M_datatypes(L)"
   apply (rule M_datatypes.intro)
    apply (rule M_trancl_L)
   apply (rule M_datatypes_axioms_L) 
   done
 

    "L(A) ==> strong_replacement(L,
          \<lambda>n y. n\<in>nat & is_iterates(L, big_union(L), A, n, y))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{A,B,nat}" 
          in gen_separation_multi [OF eclose_replacement2_Reflects],
-       auto simp add: L_nat)
+       auto)
 apply (rule_tac env="[A,B,nat]" in DPow_LsetI)
 apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+
 done
 
 

 lemma M_eclose_axioms_L: "M_eclose_axioms(L)"
   apply (rule M_eclose_axioms.intro)
    apply (assumption | rule eclose_replacement1 eclose_replacement2)+
   done
 
-theorem M_eclose_L: "PROP M_eclose(L)"
+theorem M_eclose_L: "M_eclose(L)"
   apply (rule M_eclose.intro)
    apply (rule M_datatypes_L)
   apply (rule M_eclose_axioms_L)
   done