# HG changeset patch # User wenzelm # Date 1565105200 -7200 # Node ID 9179e7a98196df46dfb6e2e158b243a37f33a660 # Parent cf66d2db97fe7ea8f235c2d573f236b766608407 clarified signature; more careful treatment of implicit context; diff -r cf66d2db97fe -r 9179e7a98196 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Aug 06 16:29:28 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Aug 06 17:26:40 2019 +0200 @@ -624,7 +624,7 @@ let fun collect (data : Lifting_Info.quotient) l = if is_some (#pcr_info data) - then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l) + then ((Thm.symmetric o safe_mk_meta_eq o Thm.transfer' ctxt o #pcr_cr_eq o the o #pcr_info) data :: l) else l val table = Lifting_Info.get_quotients ctxt in diff -r cf66d2db97fe -r 9179e7a98196 src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Tue Aug 06 16:29:28 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Aug 06 17:26:40 2019 +0200 @@ -185,7 +185,7 @@ val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs - val minfo = {rel_quot_thm = rel_quot_thm} + val minfo = {rel_quot_thm = Thm.trim_context rel_quot_thm} in Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) context end @@ -218,7 +218,9 @@ fun transform_quotient phi {quot_thm, pcr_info} = {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info} -fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name +fun lookup_quotients ctxt type_name = + Symtab.lookup (get_quotients ctxt) type_name + |> Option.map (transform_quotient (Morphism.transfer_morphism' ctxt)) fun lookup_quot_thm_quotients ctxt quot_thm = let @@ -232,7 +234,8 @@ end fun update_quotients type_name qinfo context = - Data.map (map_quotients (Symtab.update (type_name, qinfo))) context + let val qinfo' = transform_quotient Morphism.trim_context_morphism qinfo + in Data.map (map_quotients (Symtab.update (type_name, qinfo'))) context end fun delete_quotients quot_thm context = let @@ -292,9 +295,13 @@ (* info about reflexivity rules *) -val get_reflexivity_rules = Item_Net.content o get_reflexivity_rules' o Context.Proof +fun get_reflexivity_rules ctxt = + Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt)) + |> map (Thm.transfer' ctxt) -fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm)) +fun add_reflexivity_rule thm = + Data.map (map_reflexivity_rules (Item_Net.update (Thm.trim_context thm))) + val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule @@ -360,16 +367,19 @@ fun add_reflexivity_rules mono_rule context = let - fun find_eq_rule thm ctxt = + val ctxt = Context.proof_of context + val thy = Context.theory_of context + + fun find_eq_rule thm = let - val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm; - val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs; + val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm + val rules = Transfer.retrieve_relator_eq ctxt concl_rhs in - find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs, - (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules + find_first (fn th => Pattern.matches thy (concl_rhs, + (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) th)) rules end - val eq_rule = find_eq_rule mono_rule (Context.proof_of context); + val eq_rule = find_eq_rule mono_rule; val eq_rule = if is_some eq_rule then the eq_rule else error "No corresponding rule that the relator preserves equality was found." in @@ -505,13 +515,17 @@ end end -fun get_distr_rules_raw context = Symtab.fold - (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) +fun get_distr_rules_raw context = + Symtab.fold (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => + pos_distr_rules @ neg_distr_rules @ rules) (get_relator_distr_data' context) [] + |> map (Thm.transfer'' context) -fun get_mono_rules_raw context = Symtab.fold - (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) +fun get_mono_rules_raw context = + Symtab.fold (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => + [pos_mono_rule, neg_mono_rule] @ rules) (get_relator_distr_data' context) [] + |> map (Thm.transfer'' context) val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data diff -r cf66d2db97fe -r 9179e7a98196 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Aug 06 16:29:28 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Aug 06 17:26:40 2019 +0200 @@ -426,10 +426,10 @@ thm |> Thm.cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg val pcrel_def = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) pcrel_def - val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm + val thm' = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def]) in - rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm + rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm' end fun reduce_Domainp ctxt rules thm = diff -r cf66d2db97fe -r 9179e7a98196 src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Tue Aug 06 16:29:28 2019 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Tue Aug 06 17:26:40 2019 +0200 @@ -22,16 +22,16 @@ val fold_relator_eqs_conv: Proof.context -> conv val unfold_relator_eqs_conv: Proof.context -> conv val get_transfer_raw: Proof.context -> thm list - val get_relator_eq_item_net: Proof.context -> thm Item_Net.T val get_relator_eq: Proof.context -> thm list + val retrieve_relator_eq: Proof.context -> term -> thm list val get_sym_relator_eq: Proof.context -> thm list val get_relator_eq_raw: Proof.context -> thm list val get_relator_domain: Proof.context -> thm list val morph_pred_data: morphism -> pred_data -> pred_data val lookup_pred_data: Proof.context -> string -> pred_data option val update_pred_data: string -> pred_data -> Context.generic -> Context.generic - val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T - val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T + val is_compound_lhs: Proof.context -> term -> bool + val is_compound_rhs: Proof.context -> term -> bool val transfer_add: attribute val transfer_del: attribute val transfer_raw_add: thm -> Context.generic -> Context.generic @@ -67,7 +67,7 @@ val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of); -datatype pred_data = PRED_DATA of {pred_def:thm, rel_eq_onp: thm, pred_simps: thm list} +datatype pred_data = PRED_DATA of {pred_def: thm, rel_eq_onp: thm, pred_simps: thm list} fun mk_pred_data pred_def rel_eq_onp pred_simps = PRED_DATA {pred_def = pred_def, rel_eq_onp = rel_eq_onp, pred_simps = pred_simps} @@ -124,25 +124,32 @@ pred_data = Symtab.merge (K true) (pd1, pd2) } ) -val get_transfer_raw = Item_Net.content o #transfer_raw o Data.get o Context.Proof +fun get_net_content f ctxt = + Item_Net.content (f (Data.get (Context.Proof ctxt))) + |> map (Thm.transfer' ctxt) + +val get_transfer_raw = get_net_content #transfer_raw val get_known_frees = #known_frees o Data.get o Context.Proof -val get_compound_lhs = #compound_lhs o Data.get o Context.Proof +fun is_compound f ctxt t = + Item_Net.retrieve (f (Data.get (Context.Proof ctxt))) t + |> exists (fn (pat, _) => Pattern.matches (Proof_Context.theory_of ctxt) (pat, t)); -val get_compound_rhs = #compound_rhs o Data.get o Context.Proof +val is_compound_lhs = is_compound #compound_lhs +val is_compound_rhs = is_compound #compound_rhs -val get_relator_eq_item_net = #relator_eq o Data.get o Context.Proof +val get_relator_eq = get_net_content #relator_eq #> map safe_mk_meta_eq -val get_relator_eq = - map safe_mk_meta_eq o Item_Net.content o #relator_eq o Data.get o Context.Proof +fun retrieve_relator_eq ctxt t = + Item_Net.retrieve (#relator_eq (Data.get (Context.Proof ctxt))) t + |> map (Thm.transfer' ctxt) -val get_sym_relator_eq = - map (Thm.symmetric o safe_mk_meta_eq) o Item_Net.content o #relator_eq o Data.get o Context.Proof +val get_sym_relator_eq = get_net_content #relator_eq #> map (safe_mk_meta_eq #> Thm.symmetric) -val get_relator_eq_raw = Item_Net.content o #relator_eq_raw o Data.get o Context.Proof +val get_relator_eq_raw = get_net_content #relator_eq_raw -val get_relator_domain = Item_Net.content o #relator_domain o Data.get o Context.Proof +val get_relator_domain = get_net_content #relator_domain val get_pred_data = #pred_data o Data.get o Context.Proof @@ -167,19 +174,20 @@ fun map_relator_domain f = map_data I I I I I I f I fun map_pred_data f = map_data I I I I I I I f -fun add_transfer_thm thm = Data.map - (map_transfer_raw (Item_Net.update thm) o - map_compound_lhs - (case HOLogic.dest_Trueprop (Thm.concl_of thm) of - Const (\<^const_name>\Rel\, _) $ _ $ (lhs as (_ $ _)) $ _ => - Item_Net.update (lhs, thm) - | _ => I) o - map_compound_rhs - (case HOLogic.dest_Trueprop (Thm.concl_of thm) of - Const (\<^const_name>\Rel\, _) $ _ $ _ $ (rhs as (_ $ _)) => - Item_Net.update (rhs, thm) - | _ => I) o - map_known_frees (Term.add_frees (Thm.concl_of thm))) +val add_transfer_thm = + Thm.trim_context #> (fn thm => Data.map + (map_transfer_raw (Item_Net.update thm) o + map_compound_lhs + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of + Const (\<^const_name>\Rel\, _) $ _ $ (lhs as (_ $ _)) $ _ => + Item_Net.update (lhs, thm) + | _ => I) o + map_compound_rhs + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of + Const (\<^const_name>\Rel\, _) $ _ $ _ $ (rhs as (_ $ _)) => + Item_Net.update (rhs, thm) + | _ => I) o + map_known_frees (Term.add_frees (Thm.concl_of thm)))) fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm) o @@ -560,16 +568,9 @@ map_filter f (Symtab.dest tab) end -fun retrieve_terms t net = map fst (Item_Net.retrieve net t) - -fun matches_list ctxt term = - is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term)) - fun transfer_rule_of_term ctxt equiv t = let - val compound_rhs = get_compound_rhs ctxt - fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t - val s = skeleton is_rhs ctxt t + val s = skeleton (is_compound_rhs ctxt) ctxt t val frees = map fst (Term.add_frees s []) val tfrees = map fst (Term.add_tfrees s []) fun prep a = "R" ^ Library.unprefix "'" a @@ -590,9 +591,7 @@ fun transfer_rule_of_lhs ctxt t = let - val compound_lhs = get_compound_lhs ctxt - fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t - val s = skeleton is_lhs ctxt t + val s = skeleton (is_compound_lhs ctxt) ctxt t val frees = map fst (Term.add_frees s []) val tfrees = map fst (Term.add_tfrees s []) fun prep a = "R" ^ Library.unprefix "'" a @@ -853,10 +852,12 @@ Theory.setup let val name = \<^binding>\relator_eq\ - fun add_thm thm context = context - |> Data.map (map_relator_eq (Item_Net.update thm)) + fun add_thm thm context = + context + |> Data.map (map_relator_eq (Item_Net.update (Thm.trim_context thm))) |> Data.map (map_relator_eq_raw - (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm))) + (Item_Net.update + (Thm.trim_context (abstract_equalities_relator_eq (Context.proof_of context) thm)))) fun del_thm thm context = context |> Data.map (map_relator_eq (Item_Net.remove thm)) |> Data.map (map_relator_eq_raw @@ -876,15 +877,21 @@ val name = \<^binding>\relator_domain\ fun add_thm thm context = let - val thm = abstract_domains_relator_domain (Context.proof_of context) thm + val thm' = thm + |> abstract_domains_relator_domain (Context.proof_of context) + |> Thm.trim_context in - context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm + context + |> Data.map (map_relator_domain (Item_Net.update thm')) + |> add_transfer_domain_thm thm' end fun del_thm thm context = let - val thm = abstract_domains_relator_domain (Context.proof_of context) thm + val thm' = abstract_domains_relator_domain (Context.proof_of context) thm in - context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm + context + |> Data.map (map_relator_domain (Item_Net.remove thm')) + |> del_transfer_domain_thm thm' end val add = Thm.declaration_attribute add_thm val del = Thm.declaration_attribute del_thm