src/ZF/Constructible/Rec_Separation.thy
changeset 13429 2232810416fc
parent 13428 99e52e78eb65
child 13434 78b93a667c01
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Mon Jul 29 00:57:16 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Jul 29 18:07:53 2002 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4 -header{*Separation for Facts About Recursion*}
     1.5 +
     1.6 +header {*Separation for Facts About Recursion*}
     1.7  
     1.8  theory Rec_Separation = Separation + Datatype_absolute:
     1.9  
    1.10 @@ -198,19 +199,14 @@
    1.11  
    1.12  subsubsection{*Instantiating the locale @{text M_trancl}*}
    1.13  
    1.14 -theorem M_trancl_axioms_L: "M_trancl_axioms(L)"
    1.15 +theorem M_trancl_L: "PROP M_trancl(L)"
    1.16 +  apply (rule M_trancl.intro)
    1.17 +    apply (rule M_axioms.axioms [OF M_axioms_L])+
    1.18    apply (rule M_trancl_axioms.intro)
    1.19     apply (assumption | rule
    1.20       rtrancl_separation wellfounded_trancl_separation)+
    1.21    done
    1.22  
    1.23 -theorem M_trancl_L: "PROP M_trancl(L)"
    1.24 -  apply (rule M_trancl.intro)
    1.25 -    apply (rule M_triv_axioms_L)
    1.26 -   apply (rule M_axioms_axioms_L)
    1.27 -  apply (rule M_trancl_axioms_L)
    1.28 -  done
    1.29 -
    1.30  lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
    1.31    and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
    1.32    and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L]
    1.33 @@ -438,18 +434,12 @@
    1.34  
    1.35  subsubsection{*Instantiating the locale @{text M_wfrank}*}
    1.36  
    1.37 -theorem M_wfrank_axioms_L: "M_wfrank_axioms(L)"
    1.38 -  apply (rule M_wfrank_axioms.intro)
    1.39 -  apply (assumption | rule
    1.40 -    wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
    1.41 -  done
    1.42 -
    1.43  theorem M_wfrank_L: "PROP M_wfrank(L)"
    1.44    apply (rule M_wfrank.intro)
    1.45 -     apply (rule M_triv_axioms_L)
    1.46 -    apply (rule M_axioms_axioms_L)
    1.47 -   apply (rule M_trancl_axioms_L)
    1.48 -  apply (rule M_wfrank_axioms_L)
    1.49 +     apply (rule M_trancl.axioms [OF M_trancl_L])+
    1.50 +  apply (rule M_wfrank_axioms.intro)
    1.51 +   apply (assumption | rule
    1.52 +     wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
    1.53    done
    1.54  
    1.55  lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L]
    1.56 @@ -1224,7 +1214,9 @@
    1.57  
    1.58  subsubsection{*Instantiating the locale @{text M_datatypes}*}
    1.59  
    1.60 -theorem M_datatypes_axioms_L: "M_datatypes_axioms(L)"
    1.61 +theorem M_datatypes_L: "PROP M_datatypes(L)"
    1.62 +  apply (rule M_datatypes.intro)
    1.63 +      apply (rule M_wfrank.axioms [OF M_wfrank_L])+
    1.64    apply (rule M_datatypes_axioms.intro)
    1.65        apply (assumption | rule
    1.66          list_replacement1 list_replacement2
    1.67 @@ -1232,15 +1224,6 @@
    1.68          nth_replacement)+
    1.69    done
    1.70  
    1.71 -theorem M_datatypes_L: "PROP M_datatypes(L)"
    1.72 -  apply (rule M_datatypes.intro)
    1.73 -      apply (rule M_triv_axioms_L)
    1.74 -     apply (rule M_axioms_axioms_L)
    1.75 -    apply (rule M_trancl_axioms_L)
    1.76 -   apply (rule M_wfrank_axioms_L)
    1.77 -  apply (rule M_datatypes_axioms_L)
    1.78 -  done
    1.79 -
    1.80  lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
    1.81    and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L]
    1.82    and list_abs = M_datatypes.list_abs [OF M_datatypes_L]
    1.83 @@ -1338,19 +1321,11 @@
    1.84  
    1.85  subsubsection{*Instantiating the locale @{text M_eclose}*}
    1.86  
    1.87 -theorem M_eclose_axioms_L: "M_eclose_axioms(L)"
    1.88 -  apply (rule M_eclose_axioms.intro)
    1.89 -   apply (assumption | rule eclose_replacement1 eclose_replacement2)+
    1.90 -  done
    1.91 -
    1.92  theorem M_eclose_L: "PROP M_eclose(L)"
    1.93    apply (rule M_eclose.intro)
    1.94 -       apply (rule M_triv_axioms_L)
    1.95 -      apply (rule M_axioms_axioms_L)
    1.96 -     apply (rule M_trancl_axioms_L)
    1.97 -    apply (rule M_wfrank_axioms_L)
    1.98 -   apply (rule M_datatypes_axioms_L)
    1.99 -  apply (rule M_eclose_axioms_L)
   1.100 +       apply (rule M_datatypes.axioms [OF M_datatypes_L])+
   1.101 +  apply (rule M_eclose_axioms.intro)
   1.102 +   apply (assumption | rule eclose_replacement1 eclose_replacement2)+
   1.103    done
   1.104  
   1.105  lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]