--- a/src/ZF/Constructible/Separation.thy Tue Sep 10 16:47:17 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy Tue Sep 10 16:51:31 2002 +0200
@@ -8,7 +8,7 @@
theory Separation = L_axioms + WF_absolute:
-text{*This theory proves all instances needed for locale @{text "M_axioms"}*}
+text{*This theory proves all instances needed for locale @{text "M_basic"}*}
text{*Helps us solve for de Bruijn indices!*}
lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
@@ -470,12 +470,12 @@
done
-subsection{*Instantiating the locale @{text M_axioms}*}
+subsection{*Instantiating the locale @{text M_basic}*}
text{*Separation (and Strong Replacement) for basic set-theoretic constructions
such as intersection, Cartesian Product and image.*}
-lemma M_axioms_axioms_L: "M_axioms_axioms(L)"
- apply (rule M_axioms_axioms.intro)
+lemma M_basic_axioms_L: "M_basic_axioms(L)"
+ apply (rule M_basic_axioms.intro)
apply (assumption | rule
Inter_separation Diff_separation cartprod_separation image_separation
converse_separation restrict_separation
@@ -485,114 +485,114 @@
omap_replacement is_recfun_separation)+
done
-theorem M_axioms_L: "PROP M_axioms(L)"
-by (rule M_axioms.intro [OF M_triv_axioms_L M_axioms_axioms_L])
+theorem M_basic_L: "PROP M_basic(L)"
+by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
-lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L]
- and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L]
- and sum_closed = M_axioms.sum_closed [OF M_axioms_L]
- and M_converse_iff = M_axioms.M_converse_iff [OF M_axioms_L]
- and converse_closed = M_axioms.converse_closed [OF M_axioms_L]
- and converse_abs = M_axioms.converse_abs [OF M_axioms_L]
- and image_closed = M_axioms.image_closed [OF M_axioms_L]
- and vimage_abs = M_axioms.vimage_abs [OF M_axioms_L]
- and vimage_closed = M_axioms.vimage_closed [OF M_axioms_L]
- and domain_abs = M_axioms.domain_abs [OF M_axioms_L]
- and domain_closed = M_axioms.domain_closed [OF M_axioms_L]
- and range_abs = M_axioms.range_abs [OF M_axioms_L]
- and range_closed = M_axioms.range_closed [OF M_axioms_L]
- and field_abs = M_axioms.field_abs [OF M_axioms_L]
- and field_closed = M_axioms.field_closed [OF M_axioms_L]
- and relation_abs = M_axioms.relation_abs [OF M_axioms_L]
- and function_abs = M_axioms.function_abs [OF M_axioms_L]
- and apply_closed = M_axioms.apply_closed [OF M_axioms_L]
- and apply_abs = M_axioms.apply_abs [OF M_axioms_L]
- and typed_function_abs = M_axioms.typed_function_abs [OF M_axioms_L]
- and injection_abs = M_axioms.injection_abs [OF M_axioms_L]
- and surjection_abs = M_axioms.surjection_abs [OF M_axioms_L]
- and bijection_abs = M_axioms.bijection_abs [OF M_axioms_L]
- and M_comp_iff = M_axioms.M_comp_iff [OF M_axioms_L]
- and comp_closed = M_axioms.comp_closed [OF M_axioms_L]
- and composition_abs = M_axioms.composition_abs [OF M_axioms_L]
- and restriction_is_function = M_axioms.restriction_is_function [OF M_axioms_L]
- and restriction_abs = M_axioms.restriction_abs [OF M_axioms_L]
- and M_restrict_iff = M_axioms.M_restrict_iff [OF M_axioms_L]
- and restrict_closed = M_axioms.restrict_closed [OF M_axioms_L]
- and Inter_abs = M_axioms.Inter_abs [OF M_axioms_L]
- and Inter_closed = M_axioms.Inter_closed [OF M_axioms_L]
- and Int_closed = M_axioms.Int_closed [OF M_axioms_L]
- and finite_fun_closed = M_axioms.finite_fun_closed [OF M_axioms_L]
- and is_funspace_abs = M_axioms.is_funspace_abs [OF M_axioms_L]
- and succ_fun_eq2 = M_axioms.succ_fun_eq2 [OF M_axioms_L]
- and funspace_succ = M_axioms.funspace_succ [OF M_axioms_L]
- and finite_funspace_closed = M_axioms.finite_funspace_closed [OF M_axioms_L]
+lemmas cartprod_iff = M_basic.cartprod_iff [OF M_basic_L]
+ and cartprod_closed = M_basic.cartprod_closed [OF M_basic_L]
+ and sum_closed = M_basic.sum_closed [OF M_basic_L]
+ and M_converse_iff = M_basic.M_converse_iff [OF M_basic_L]
+ and converse_closed = M_basic.converse_closed [OF M_basic_L]
+ and converse_abs = M_basic.converse_abs [OF M_basic_L]
+ and image_closed = M_basic.image_closed [OF M_basic_L]
+ and vimage_abs = M_basic.vimage_abs [OF M_basic_L]
+ and vimage_closed = M_basic.vimage_closed [OF M_basic_L]
+ and domain_abs = M_basic.domain_abs [OF M_basic_L]
+ and domain_closed = M_basic.domain_closed [OF M_basic_L]
+ and range_abs = M_basic.range_abs [OF M_basic_L]
+ and range_closed = M_basic.range_closed [OF M_basic_L]
+ and field_abs = M_basic.field_abs [OF M_basic_L]
+ and field_closed = M_basic.field_closed [OF M_basic_L]
+ and relation_abs = M_basic.relation_abs [OF M_basic_L]
+ and function_abs = M_basic.function_abs [OF M_basic_L]
+ and apply_closed = M_basic.apply_closed [OF M_basic_L]
+ and apply_abs = M_basic.apply_abs [OF M_basic_L]
+ and typed_function_abs = M_basic.typed_function_abs [OF M_basic_L]
+ and injection_abs = M_basic.injection_abs [OF M_basic_L]
+ and surjection_abs = M_basic.surjection_abs [OF M_basic_L]
+ and bijection_abs = M_basic.bijection_abs [OF M_basic_L]
+ and M_comp_iff = M_basic.M_comp_iff [OF M_basic_L]
+ and comp_closed = M_basic.comp_closed [OF M_basic_L]
+ and composition_abs = M_basic.composition_abs [OF M_basic_L]
+ and restriction_is_function = M_basic.restriction_is_function [OF M_basic_L]
+ and restriction_abs = M_basic.restriction_abs [OF M_basic_L]
+ and M_restrict_iff = M_basic.M_restrict_iff [OF M_basic_L]
+ and restrict_closed = M_basic.restrict_closed [OF M_basic_L]
+ and Inter_abs = M_basic.Inter_abs [OF M_basic_L]
+ and Inter_closed = M_basic.Inter_closed [OF M_basic_L]
+ and Int_closed = M_basic.Int_closed [OF M_basic_L]
+ and finite_fun_closed = M_basic.finite_fun_closed [OF M_basic_L]
+ and is_funspace_abs = M_basic.is_funspace_abs [OF M_basic_L]
+ and succ_fun_eq2 = M_basic.succ_fun_eq2 [OF M_basic_L]
+ and funspace_succ = M_basic.funspace_succ [OF M_basic_L]
+ and finite_funspace_closed = M_basic.finite_funspace_closed [OF M_basic_L]
-lemmas is_recfun_equal = M_axioms.is_recfun_equal [OF M_axioms_L]
- and is_recfun_cut = M_axioms.is_recfun_cut [OF M_axioms_L]
- and is_recfun_functional = M_axioms.is_recfun_functional [OF M_axioms_L]
- and is_recfun_relativize = M_axioms.is_recfun_relativize [OF M_axioms_L]
- and is_recfun_restrict = M_axioms.is_recfun_restrict [OF M_axioms_L]
- and univalent_is_recfun = M_axioms.univalent_is_recfun [OF M_axioms_L]
- and exists_is_recfun_indstep = M_axioms.exists_is_recfun_indstep [OF M_axioms_L]
- and wellfounded_exists_is_recfun = M_axioms.wellfounded_exists_is_recfun [OF M_axioms_L]
- and wf_exists_is_recfun = M_axioms.wf_exists_is_recfun [OF M_axioms_L]
- and is_recfun_abs = M_axioms.is_recfun_abs [OF M_axioms_L]
- and irreflexive_abs = M_axioms.irreflexive_abs [OF M_axioms_L]
- and transitive_rel_abs = M_axioms.transitive_rel_abs [OF M_axioms_L]
- and linear_rel_abs = M_axioms.linear_rel_abs [OF M_axioms_L]
- and wellordered_is_trans_on = M_axioms.wellordered_is_trans_on [OF M_axioms_L]
- and wellordered_is_linear = M_axioms.wellordered_is_linear [OF M_axioms_L]
- and wellordered_is_wellfounded_on = M_axioms.wellordered_is_wellfounded_on [OF M_axioms_L]
- and wellfounded_imp_wellfounded_on = M_axioms.wellfounded_imp_wellfounded_on [OF M_axioms_L]
- and wellfounded_on_subset_A = M_axioms.wellfounded_on_subset_A [OF M_axioms_L]
- and wellfounded_on_iff_wellfounded = M_axioms.wellfounded_on_iff_wellfounded [OF M_axioms_L]
- and wellfounded_on_imp_wellfounded = M_axioms.wellfounded_on_imp_wellfounded [OF M_axioms_L]
- and wellfounded_on_field_imp_wellfounded = M_axioms.wellfounded_on_field_imp_wellfounded [OF M_axioms_L]
- and wellfounded_iff_wellfounded_on_field = M_axioms.wellfounded_iff_wellfounded_on_field [OF M_axioms_L]
- and wellfounded_induct = M_axioms.wellfounded_induct [OF M_axioms_L]
- and wellfounded_on_induct = M_axioms.wellfounded_on_induct [OF M_axioms_L]
- and wellfounded_on_induct2 = M_axioms.wellfounded_on_induct2 [OF M_axioms_L]
- and linear_imp_relativized = M_axioms.linear_imp_relativized [OF M_axioms_L]
- and trans_on_imp_relativized = M_axioms.trans_on_imp_relativized [OF M_axioms_L]
- and wf_on_imp_relativized = M_axioms.wf_on_imp_relativized [OF M_axioms_L]
- and wf_imp_relativized = M_axioms.wf_imp_relativized [OF M_axioms_L]
- and well_ord_imp_relativized = M_axioms.well_ord_imp_relativized [OF M_axioms_L]
- and order_isomorphism_abs = M_axioms.order_isomorphism_abs [OF M_axioms_L]
- and pred_set_abs = M_axioms.pred_set_abs [OF M_axioms_L]
+lemmas is_recfun_equal = M_basic.is_recfun_equal [OF M_basic_L]
+ and is_recfun_cut = M_basic.is_recfun_cut [OF M_basic_L]
+ and is_recfun_functional = M_basic.is_recfun_functional [OF M_basic_L]
+ and is_recfun_relativize = M_basic.is_recfun_relativize [OF M_basic_L]
+ and is_recfun_restrict = M_basic.is_recfun_restrict [OF M_basic_L]
+ and univalent_is_recfun = M_basic.univalent_is_recfun [OF M_basic_L]
+ and exists_is_recfun_indstep = M_basic.exists_is_recfun_indstep [OF M_basic_L]
+ and wellfounded_exists_is_recfun = M_basic.wellfounded_exists_is_recfun [OF M_basic_L]
+ and wf_exists_is_recfun = M_basic.wf_exists_is_recfun [OF M_basic_L]
+ and is_recfun_abs = M_basic.is_recfun_abs [OF M_basic_L]
+ and irreflexive_abs = M_basic.irreflexive_abs [OF M_basic_L]
+ and transitive_rel_abs = M_basic.transitive_rel_abs [OF M_basic_L]
+ and linear_rel_abs = M_basic.linear_rel_abs [OF M_basic_L]
+ and wellordered_is_trans_on = M_basic.wellordered_is_trans_on [OF M_basic_L]
+ and wellordered_is_linear = M_basic.wellordered_is_linear [OF M_basic_L]
+ and wellordered_is_wellfounded_on = M_basic.wellordered_is_wellfounded_on [OF M_basic_L]
+ and wellfounded_imp_wellfounded_on = M_basic.wellfounded_imp_wellfounded_on [OF M_basic_L]
+ and wellfounded_on_subset_A = M_basic.wellfounded_on_subset_A [OF M_basic_L]
+ and wellfounded_on_iff_wellfounded = M_basic.wellfounded_on_iff_wellfounded [OF M_basic_L]
+ and wellfounded_on_imp_wellfounded = M_basic.wellfounded_on_imp_wellfounded [OF M_basic_L]
+ and wellfounded_on_field_imp_wellfounded = M_basic.wellfounded_on_field_imp_wellfounded [OF M_basic_L]
+ and wellfounded_iff_wellfounded_on_field = M_basic.wellfounded_iff_wellfounded_on_field [OF M_basic_L]
+ and wellfounded_induct = M_basic.wellfounded_induct [OF M_basic_L]
+ and wellfounded_on_induct = M_basic.wellfounded_on_induct [OF M_basic_L]
+ and wellfounded_on_induct2 = M_basic.wellfounded_on_induct2 [OF M_basic_L]
+ and linear_imp_relativized = M_basic.linear_imp_relativized [OF M_basic_L]
+ and trans_on_imp_relativized = M_basic.trans_on_imp_relativized [OF M_basic_L]
+ and wf_on_imp_relativized = M_basic.wf_on_imp_relativized [OF M_basic_L]
+ and wf_imp_relativized = M_basic.wf_imp_relativized [OF M_basic_L]
+ and well_ord_imp_relativized = M_basic.well_ord_imp_relativized [OF M_basic_L]
+ and order_isomorphism_abs = M_basic.order_isomorphism_abs [OF M_basic_L]
+ and pred_set_abs = M_basic.pred_set_abs [OF M_basic_L]
-lemmas pred_closed = M_axioms.pred_closed [OF M_axioms_L]
- and membership_abs = M_axioms.membership_abs [OF M_axioms_L]
- and M_Memrel_iff = M_axioms.M_Memrel_iff [OF M_axioms_L]
- and Memrel_closed = M_axioms.Memrel_closed [OF M_axioms_L]
- and wellordered_iso_predD = M_axioms.wellordered_iso_predD [OF M_axioms_L]
- and wellordered_iso_pred_eq = M_axioms.wellordered_iso_pred_eq [OF M_axioms_L]
- and wellfounded_on_asym = M_axioms.wellfounded_on_asym [OF M_axioms_L]
- and wellordered_asym = M_axioms.wellordered_asym [OF M_axioms_L]
- and ord_iso_pred_imp_lt = M_axioms.ord_iso_pred_imp_lt [OF M_axioms_L]
- and obase_iff = M_axioms.obase_iff [OF M_axioms_L]
- and omap_iff = M_axioms.omap_iff [OF M_axioms_L]
- and omap_unique = M_axioms.omap_unique [OF M_axioms_L]
- and omap_yields_Ord = M_axioms.omap_yields_Ord [OF M_axioms_L]
- and otype_iff = M_axioms.otype_iff [OF M_axioms_L]
- and otype_eq_range = M_axioms.otype_eq_range [OF M_axioms_L]
- and Ord_otype = M_axioms.Ord_otype [OF M_axioms_L]
- and domain_omap = M_axioms.domain_omap [OF M_axioms_L]
- and omap_subset = M_axioms.omap_subset [OF M_axioms_L]
- and omap_funtype = M_axioms.omap_funtype [OF M_axioms_L]
- and wellordered_omap_bij = M_axioms.wellordered_omap_bij [OF M_axioms_L]
- and omap_ord_iso = M_axioms.omap_ord_iso [OF M_axioms_L]
- and Ord_omap_image_pred = M_axioms.Ord_omap_image_pred [OF M_axioms_L]
- and restrict_omap_ord_iso = M_axioms.restrict_omap_ord_iso [OF M_axioms_L]
- and obase_equals = M_axioms.obase_equals [OF M_axioms_L]
- and omap_ord_iso_otype = M_axioms.omap_ord_iso_otype [OF M_axioms_L]
- and obase_exists = M_axioms.obase_exists [OF M_axioms_L]
- and omap_exists = M_axioms.omap_exists [OF M_axioms_L]
- and otype_exists = M_axioms.otype_exists [OF M_axioms_L]
- and omap_ord_iso_otype' = M_axioms.omap_ord_iso_otype' [OF M_axioms_L]
- and ordertype_exists = M_axioms.ordertype_exists [OF M_axioms_L]
- and relativized_imp_well_ord = M_axioms.relativized_imp_well_ord [OF M_axioms_L]
- and well_ord_abs = M_axioms.well_ord_abs [OF M_axioms_L]
+lemmas pred_closed = M_basic.pred_closed [OF M_basic_L]
+ and membership_abs = M_basic.membership_abs [OF M_basic_L]
+ and M_Memrel_iff = M_basic.M_Memrel_iff [OF M_basic_L]
+ and Memrel_closed = M_basic.Memrel_closed [OF M_basic_L]
+ and wellordered_iso_predD = M_basic.wellordered_iso_predD [OF M_basic_L]
+ and wellordered_iso_pred_eq = M_basic.wellordered_iso_pred_eq [OF M_basic_L]
+ and wellfounded_on_asym = M_basic.wellfounded_on_asym [OF M_basic_L]
+ and wellordered_asym = M_basic.wellordered_asym [OF M_basic_L]
+ and ord_iso_pred_imp_lt = M_basic.ord_iso_pred_imp_lt [OF M_basic_L]
+ and obase_iff = M_basic.obase_iff [OF M_basic_L]
+ and omap_iff = M_basic.omap_iff [OF M_basic_L]
+ and omap_unique = M_basic.omap_unique [OF M_basic_L]
+ and omap_yields_Ord = M_basic.omap_yields_Ord [OF M_basic_L]
+ and otype_iff = M_basic.otype_iff [OF M_basic_L]
+ and otype_eq_range = M_basic.otype_eq_range [OF M_basic_L]
+ and Ord_otype = M_basic.Ord_otype [OF M_basic_L]
+ and domain_omap = M_basic.domain_omap [OF M_basic_L]
+ and omap_subset = M_basic.omap_subset [OF M_basic_L]
+ and omap_funtype = M_basic.omap_funtype [OF M_basic_L]
+ and wellordered_omap_bij = M_basic.wellordered_omap_bij [OF M_basic_L]
+ and omap_ord_iso = M_basic.omap_ord_iso [OF M_basic_L]
+ and Ord_omap_image_pred = M_basic.Ord_omap_image_pred [OF M_basic_L]
+ and restrict_omap_ord_iso = M_basic.restrict_omap_ord_iso [OF M_basic_L]
+ and obase_equals = M_basic.obase_equals [OF M_basic_L]
+ and omap_ord_iso_otype = M_basic.omap_ord_iso_otype [OF M_basic_L]
+ and obase_exists = M_basic.obase_exists [OF M_basic_L]
+ and omap_exists = M_basic.omap_exists [OF M_basic_L]
+ and otype_exists = M_basic.otype_exists [OF M_basic_L]
+ and omap_ord_iso_otype' = M_basic.omap_ord_iso_otype' [OF M_basic_L]
+ and ordertype_exists = M_basic.ordertype_exists [OF M_basic_L]
+ and relativized_imp_well_ord = M_basic.relativized_imp_well_ord [OF M_basic_L]
+ and well_ord_abs = M_basic.well_ord_abs [OF M_basic_L]
declare cartprod_closed [intro, simp]
declare sum_closed [intro, simp]