src/ZF/Constructible/Rec_Separation.thy
changeset 13687 22dce9134953
parent 13655 95b95cdb4704
child 13807 a28a8fbc76d4
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Oct 30 12:18:23 2002 +0100
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Oct 30 12:44:18 2002 +0100
     1.3 @@ -75,11 +75,10 @@
     1.4  text{*Separation for @{term "rtrancl(r)"}.*}
     1.5  lemma rtrancl_separation:
     1.6       "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
     1.7 -apply (rule gen_separation [OF rtran_closure_mem_reflection, of "{r,A}"], simp)
     1.8 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
     1.9 -apply (rule DPow_LsetI)
    1.10 -apply (rule_tac env = "[x,r,A]" in rtran_closure_mem_iff_sats)
    1.11 -apply (rule sep_rules | simp)+
    1.12 +apply (rule gen_separation_multi [OF rtran_closure_mem_reflection, of "{r,A}"],
    1.13 +       auto)
    1.14 +apply (rule_tac env="[r,A]" in DPow_LsetI)
    1.15 +apply (rule rtran_closure_mem_iff_sats sep_rules | simp)+
    1.16  done
    1.17  
    1.18  
    1.19 @@ -167,11 +166,9 @@
    1.20            separation (L, \<lambda>x.
    1.21                \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
    1.22                 w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
    1.23 -apply (rule gen_separation [OF wellfounded_trancl_reflects, of "{r,Z}"], simp)
    1.24 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.25 -apply (rule DPow_LsetI)
    1.26 -apply (rule bex_iff_sats conj_iff_sats)+
    1.27 -apply (rule_tac env = "[w,x,r,Z]" in mem_iff_sats)
    1.28 +apply (rule gen_separation_multi [OF wellfounded_trancl_reflects, of "{r,Z}"],
    1.29 +       auto)
    1.30 +apply (rule_tac env="[r,Z]" in DPow_LsetI)
    1.31  apply (rule sep_rules tran_closure_iff_sats | simp)+
    1.32  done
    1.33  
    1.34 @@ -214,14 +211,10 @@
    1.35     "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
    1.36  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
    1.37  apply (rule strong_replacementI)
    1.38 -apply (rename_tac B)
    1.39  apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" 
    1.40 -         in gen_separation [OF list_replacement1_Reflects], 
    1.41 -       simp add: nonempty)
    1.42 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.43 -apply (rule DPow_LsetI)
    1.44 -apply (rule bex_iff_sats conj_iff_sats)+
    1.45 -apply (rule_tac env = "[u,x,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
    1.46 +         in gen_separation_multi [OF list_replacement1_Reflects], 
    1.47 +       auto simp add: nonempty)
    1.48 +apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI)
    1.49  apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
    1.50              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
    1.51  done
    1.52 @@ -240,14 +233,10 @@
    1.53     "L(A) ==> strong_replacement(L,
    1.54           \<lambda>n y. n\<in>nat & is_iterates(L, is_list_functor(L,A), 0, n, y))"
    1.55  apply (rule strong_replacementI)
    1.56 -apply (rename_tac B)
    1.57  apply (rule_tac u="{A,B,0,nat}" 
    1.58 -         in gen_separation [OF list_replacement2_Reflects], 
    1.59 -       simp add: L_nat nonempty)
    1.60 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.61 -apply (rule DPow_LsetI)
    1.62 -apply (rule bex_iff_sats conj_iff_sats)+
    1.63 -apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats)
    1.64 +         in gen_separation_multi [OF list_replacement2_Reflects], 
    1.65 +       auto simp add: L_nat nonempty)
    1.66 +apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI)
    1.67  apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+
    1.68  done
    1.69  
    1.70 @@ -273,14 +262,10 @@
    1.71     "iterates_replacement(L, is_formula_functor(L), 0)"
    1.72  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
    1.73  apply (rule strong_replacementI)
    1.74 -apply (rename_tac B)
    1.75  apply (rule_tac u="{B,n,0,Memrel(succ(n))}" 
    1.76 -         in gen_separation [OF formula_replacement1_Reflects], 
    1.77 -       simp add: nonempty)
    1.78 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.79 -apply (rule DPow_LsetI)
    1.80 -apply (rule bex_iff_sats conj_iff_sats)+
    1.81 -apply (rule_tac env = "[u,x,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
    1.82 +         in gen_separation_multi [OF formula_replacement1_Reflects], 
    1.83 +       auto simp add: nonempty)
    1.84 +apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI)
    1.85  apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
    1.86              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
    1.87  done
    1.88 @@ -298,14 +283,10 @@
    1.89     "strong_replacement(L,
    1.90           \<lambda>n y. n\<in>nat & is_iterates(L, is_formula_functor(L), 0, n, y))"
    1.91  apply (rule strong_replacementI)
    1.92 -apply (rename_tac B)
    1.93  apply (rule_tac u="{B,0,nat}" 
    1.94 -         in gen_separation [OF formula_replacement2_Reflects], 
    1.95 -       simp add: nonempty L_nat)
    1.96 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.97 -apply (rule DPow_LsetI)
    1.98 -apply (rule bex_iff_sats conj_iff_sats)+
    1.99 -apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats)
   1.100 +         in gen_separation_multi [OF formula_replacement2_Reflects], 
   1.101 +       auto simp add: nonempty L_nat)
   1.102 +apply (rule_tac env="[B,0,nat]" in DPow_LsetI)
   1.103  apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+
   1.104  done
   1.105  
   1.106 @@ -368,13 +349,10 @@
   1.107     "L(w) ==> iterates_replacement(L, is_tl(L), w)"
   1.108  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   1.109  apply (rule strong_replacementI)
   1.110 -apply (rule_tac u="{A,n,w,Memrel(succ(n))}" 
   1.111 -         in gen_separation [OF nth_replacement_Reflects], 
   1.112 -       simp add: nonempty)
   1.113 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   1.114 -apply (rule DPow_LsetI)
   1.115 -apply (rule bex_iff_sats conj_iff_sats)+
   1.116 -apply (rule_tac env = "[u,x,A,w,Memrel(succ(n))]" in mem_iff_sats)
   1.117 +apply (rule_tac u="{B,w,Memrel(succ(n))}" 
   1.118 +         in gen_separation_multi [OF nth_replacement_Reflects], 
   1.119 +       auto)
   1.120 +apply (rule_tac env="[B,w,Memrel(succ(n))]" in DPow_LsetI)
   1.121  apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats
   1.122              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.123  done
   1.124 @@ -428,13 +406,9 @@
   1.125     "L(A) ==> iterates_replacement(L, big_union(L), A)"
   1.126  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   1.127  apply (rule strong_replacementI)
   1.128 -apply (rename_tac B)
   1.129  apply (rule_tac u="{B,A,n,Memrel(succ(n))}" 
   1.130 -         in gen_separation [OF eclose_replacement1_Reflects], simp)
   1.131 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   1.132 -apply (rule DPow_LsetI)
   1.133 -apply (rule bex_iff_sats conj_iff_sats)+
   1.134 -apply (rule_tac env = "[u,x,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
   1.135 +         in gen_separation_multi [OF eclose_replacement1_Reflects], auto)
   1.136 +apply (rule_tac env="[B,A,n,Memrel(succ(n))]" in DPow_LsetI)
   1.137  apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats
   1.138               is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
   1.139  done
   1.140 @@ -452,13 +426,10 @@
   1.141     "L(A) ==> strong_replacement(L,
   1.142           \<lambda>n y. n\<in>nat & is_iterates(L, big_union(L), A, n, y))"
   1.143  apply (rule strong_replacementI)
   1.144 -apply (rename_tac B)
   1.145  apply (rule_tac u="{A,B,nat}" 
   1.146 -         in gen_separation [OF eclose_replacement2_Reflects], simp add: L_nat)
   1.147 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   1.148 -apply (rule DPow_LsetI)
   1.149 -apply (rule bex_iff_sats conj_iff_sats)+
   1.150 -apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats)
   1.151 +         in gen_separation_multi [OF eclose_replacement2_Reflects],
   1.152 +       auto simp add: L_nat)
   1.153 +apply (rule_tac env="[A,B,nat]" in DPow_LsetI)
   1.154  apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+
   1.155  done
   1.156