src/ZF/Constructible/Rec_Separation.thy

-header{*Separation for Facts About Recursion*}
+
+header {*Separation for Facts About Recursion*}
 
 theory Rec_Separation = Separation + Datatype_absolute:
 
 text{*This theory proves all instances needed for locales @{text
 "M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}

 done
 
 
 subsubsection{*Instantiating the locale @{text M_trancl}*}
 
-theorem M_trancl_axioms_L: "M_trancl_axioms(L)"
+theorem M_trancl_L: "PROP M_trancl(L)"
+  apply (rule M_trancl.intro)
+    apply (rule M_axioms.axioms [OF M_axioms_L])+
   apply (rule M_trancl_axioms.intro)
    apply (assumption | rule
      rtrancl_separation wellfounded_trancl_separation)+
-  done
-
-theorem M_trancl_L: "PROP M_trancl(L)"
-  apply (rule M_trancl.intro)
-    apply (rule M_triv_axioms_L)
-   apply (rule M_axioms_axioms_L)
-  apply (rule M_trancl_axioms_L)
   done
 
 lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
   and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
   and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L]

 done
 
 
 subsubsection{*Instantiating the locale @{text M_wfrank}*}
 
-theorem M_wfrank_axioms_L: "M_wfrank_axioms(L)"
-  apply (rule M_wfrank_axioms.intro)
-  apply (assumption | rule
-    wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
-  done
-
 theorem M_wfrank_L: "PROP M_wfrank(L)"
   apply (rule M_wfrank.intro)
-     apply (rule M_triv_axioms_L)
-    apply (rule M_axioms_axioms_L)
-   apply (rule M_trancl_axioms_L)
-  apply (rule M_wfrank_axioms_L)
+     apply (rule M_trancl.axioms [OF M_trancl_L])+
+  apply (rule M_wfrank_axioms.intro)
+   apply (assumption | rule
+     wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
   done
 
 lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L]
   and exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L]
   and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L]

 
 
 
 subsubsection{*Instantiating the locale @{text M_datatypes}*}
 
-theorem M_datatypes_axioms_L: "M_datatypes_axioms(L)"
+theorem M_datatypes_L: "PROP M_datatypes(L)"
+  apply (rule M_datatypes.intro)
+      apply (rule M_wfrank.axioms [OF M_wfrank_L])+
   apply (rule M_datatypes_axioms.intro)
       apply (assumption | rule
         list_replacement1 list_replacement2
         formula_replacement1 formula_replacement2
         nth_replacement)+
-  done
-
-theorem M_datatypes_L: "PROP M_datatypes(L)"
-  apply (rule M_datatypes.intro)
-      apply (rule M_triv_axioms_L)
-     apply (rule M_axioms_axioms_L)
-    apply (rule M_trancl_axioms_L)
-   apply (rule M_wfrank_axioms_L)
-  apply (rule M_datatypes_axioms_L)
   done
 
 lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
   and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L]
   and list_abs = M_datatypes.list_abs [OF M_datatypes_L]

 done
 
 
 subsubsection{*Instantiating the locale @{text M_eclose}*}
 
-theorem M_eclose_axioms_L: "M_eclose_axioms(L)"
+theorem M_eclose_L: "PROP M_eclose(L)"
+  apply (rule M_eclose.intro)
+       apply (rule M_datatypes.axioms [OF M_datatypes_L])+
   apply (rule M_eclose_axioms.intro)
    apply (assumption | rule eclose_replacement1 eclose_replacement2)+
   done
 
-theorem M_eclose_L: "PROP M_eclose(L)"
-  apply (rule M_eclose.intro)
-       apply (rule M_triv_axioms_L)
-      apply (rule M_axioms_axioms_L)
-     apply (rule M_trancl_axioms_L)
-    apply (rule M_wfrank_axioms_L)
-   apply (rule M_datatypes_axioms_L)
-  apply (rule M_eclose_axioms_L)
-  done
-
 lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]
   and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L]
 
 end