# HG changeset patch # User ballarin # Date 1113832463 -7200 # Node ID b08feb003f3c930f51c647bb115c34ac6362898f # Parent 6472d4942992297a68de4a9d376b3b05b2d549b5 Cleaned up, now use interpretation. diff -r 6472d4942992 -r b08feb003f3c src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Mon Apr 18 15:53:51 2005 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Mon Apr 18 15:54:23 2005 +0200 @@ -184,11 +184,7 @@ by (rule M_trancl.intro [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L]) -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 trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L] - and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L] - +interpretation M_trancl [L] by (rule M_trancl_axioms_L) subsection{*@{term L} is Closed Under the Operator @{term list}*} @@ -374,17 +370,7 @@ 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] - and formula_abs = M_datatypes.formula_abs [OF M_datatypes_L] - and nth_abs = M_datatypes.nth_abs [OF M_datatypes_L] - -declare list_closed [intro,simp] -declare formula_closed [intro,simp] -declare list_abs [simp] -declare formula_abs [simp] -declare nth_abs [simp] +interpretation M_datatypes [L] by (rule M_datatypes_axioms_L) subsection{*@{term L} is Closed Under the Operator @{term eclose}*} @@ -447,8 +433,7 @@ 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] - and transrec_replacementI = M_eclose.transrec_replacementI [OF M_eclose_L] +interpretation M_eclose [L] by (rule M_eclose_axioms_L) + end diff -r 6472d4942992 -r b08feb003f3c src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Mon Apr 18 15:53:51 2005 +0200 +++ b/src/ZF/Constructible/Separation.thy Mon Apr 18 15:54:23 2005 +0200 @@ -305,113 +305,7 @@ 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_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 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] +interpretation M_basic [L] by (rule M_basic_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 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 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_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 wellfounded_on_asym = M_basic.wellfounded_on_asym [OF M_basic_L] - and wellordered_asym = M_basic.wellordered_asym [OF M_basic_L] - -declare cartprod_closed [intro, simp] -declare sum_closed [intro, simp] -declare converse_closed [intro, simp] -declare converse_abs [simp] -declare image_closed [intro, simp] -declare vimage_abs [simp] -declare vimage_closed [intro, simp] -declare domain_abs [simp] -declare domain_closed [intro, simp] -declare range_abs [simp] -declare range_closed [intro, simp] -declare field_abs [simp] -declare field_closed [intro, simp] -declare relation_abs [simp] -declare function_abs [simp] -declare apply_closed [intro, simp] -declare typed_function_abs [simp] -declare injection_abs [simp] -declare surjection_abs [simp] -declare bijection_abs [simp] -declare comp_closed [intro, simp] -declare composition_abs [simp] -declare restriction_abs [simp] -declare restrict_closed [intro, simp] -declare Inter_abs [simp] -declare Inter_closed [intro, simp] -declare Int_closed [intro, simp] -declare is_funspace_abs [simp] -declare finite_funspace_closed [intro, simp] -declare membership_abs [simp] -declare Memrel_closed [intro,simp] end