src/ZF/Constructible/Rec_Separation.thy
changeset 13385 31df66ca0780
parent 13363 c26eeb000470
child 13386 f3e9e8b21aba
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 16 20:25:21 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 17 15:48:54 2002 +0200
     1.3 @@ -80,11 +80,10 @@
     1.4  apply (drule subset_Lset_ltD, assumption) 
     1.5  apply (erule reflection_imp_L_separation)
     1.6    apply (simp_all add: lt_Ord2)
     1.7 -apply (rule DPowI2)
     1.8 +apply (rule DPow_LsetI)
     1.9  apply (rename_tac u)
    1.10  apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats)
    1.11  apply (rule sep_rules | simp)+
    1.12 -apply (simp_all add: succ_Un_distrib [symmetric])
    1.13  done
    1.14  
    1.15  
    1.16 @@ -189,12 +188,11 @@
    1.17  apply (drule subset_Lset_ltD, assumption) 
    1.18  apply (erule reflection_imp_L_separation)
    1.19    apply (simp_all add: lt_Ord2)
    1.20 -apply (rule DPowI2)
    1.21 +apply (rule DPow_LsetI)
    1.22  apply (rename_tac u) 
    1.23  apply (rule bex_iff_sats conj_iff_sats)+
    1.24  apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats) 
    1.25  apply (rule sep_rules tran_closure_iff_sats | simp)+
    1.26 -apply (simp_all add: succ_Un_distrib [symmetric])
    1.27  done
    1.28  
    1.29  
    1.30 @@ -348,12 +346,11 @@
    1.31  apply (drule subset_Lset_ltD, assumption) 
    1.32  apply (erule reflection_imp_L_separation)
    1.33    apply (simp_all add: lt_Ord2, clarify)
    1.34 -apply (rule DPowI2)
    1.35 +apply (rule DPow_LsetI)
    1.36  apply (rename_tac u)  
    1.37  apply (rule ball_iff_sats imp_iff_sats)+
    1.38  apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
    1.39  apply (rule sep_rules is_recfun_iff_sats | simp)+
    1.40 -apply (simp_all add: succ_Un_distrib [symmetric])
    1.41  done
    1.42  
    1.43  
    1.44 @@ -390,12 +387,11 @@
    1.45  apply (drule subset_Lset_ltD, assumption) 
    1.46  apply (erule reflection_imp_L_separation)
    1.47    apply (simp_all add: lt_Ord2)
    1.48 -apply (rule DPowI2)
    1.49 +apply (rule DPow_LsetI)
    1.50  apply (rename_tac u) 
    1.51  apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
    1.52  apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats) 
    1.53  apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
    1.54 -apply (simp_all add: succ_Un_distrib [symmetric])
    1.55  done
    1.56  
    1.57  
    1.58 @@ -430,12 +426,11 @@
    1.59  apply (drule subset_Lset_ltD, assumption) 
    1.60  apply (erule reflection_imp_L_separation)
    1.61    apply (simp_all add: lt_Ord2, clarify)
    1.62 -apply (rule DPowI2)
    1.63 +apply (rule DPow_LsetI)
    1.64  apply (rename_tac u)  
    1.65  apply (rule ball_iff_sats imp_iff_sats)+
    1.66  apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
    1.67  apply (rule sep_rules is_recfun_iff_sats | simp)+
    1.68 -apply (simp_all add: succ_Un_distrib [symmetric])
    1.69  done
    1.70  
    1.71  
    1.72 @@ -790,7 +785,6 @@
    1.73  
    1.74  subsection{*@{term L} is Closed Under the Operator @{term list}*} 
    1.75  
    1.76 -
    1.77  lemma list_replacement1_Reflects:
    1.78   "REFLECTS
    1.79     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
    1.80 @@ -816,7 +810,7 @@
    1.81  apply (drule subset_Lset_ltD, assumption) 
    1.82  apply (erule reflection_imp_L_separation)
    1.83    apply (simp_all add: lt_Ord2)
    1.84 -apply (rule DPowI2)
    1.85 +apply (rule DPow_LsetI)
    1.86  apply (rename_tac v) 
    1.87  apply (rule bex_iff_sats conj_iff_sats)+
    1.88  apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
    1.89 @@ -861,16 +855,13 @@
    1.90  apply (drule subset_Lset_ltD, assumption) 
    1.91  apply (erule reflection_imp_L_separation)
    1.92    apply (simp_all add: lt_Ord2)
    1.93 -apply (rule DPowI2)
    1.94 +apply (rule DPow_LsetI)
    1.95  apply (rename_tac v) 
    1.96  apply (rule bex_iff_sats conj_iff_sats)+
    1.97  apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
    1.98  apply (rule sep_rules | simp)+
    1.99  apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.100  apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
   1.101 -apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed)
   1.102  done
   1.103  
   1.104 -
   1.105 -
   1.106  end