# HG changeset patch # User wenzelm # Date 1565117526 -7200 # Node ID 5c1b2f616d15584f43a533b8ca0c9c21077745d9 # Parent 8406a2c296e08c8f15d93226888c9047e2ae0dd1# Parent 98b6da301e139fe742e014e314de17dcce65b89c merged diff -r 8406a2c296e0 -r 5c1b2f616d15 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Aug 06 20:52:06 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 8406a2c296e0 -r 5c1b2f616d15 src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Aug 06 20:52:06 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 8406a2c296e0 -r 5c1b2f616d15 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Aug 06 20:52:06 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 8406a2c296e0 -r 5c1b2f616d15 src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Tue Aug 06 20:52:06 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 diff -r 8406a2c296e0 -r 5c1b2f616d15 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/Pure/Isar/object_logic.ML Tue Aug 06 20:52:06 2019 +0200 @@ -171,8 +171,9 @@ (* maintain rules *) -val get_atomize = #1 o #atomize_rulify o get_data; -val get_rulify = #2 o #atomize_rulify o get_data; +fun get_atomize_rulify f ctxt = map (Thm.transfer' ctxt) (f (#atomize_rulify (get_data ctxt))); +val get_atomize = get_atomize_rulify #1; +val get_rulify = get_atomize_rulify #2; fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) => (base_sort, judgment, (Thm.add_thm (Thm.trim_context th) atomize, rulify))); diff -r 8406a2c296e0 -r 5c1b2f616d15 src/Pure/axclass.ML diff -r 8406a2c296e0 -r 5c1b2f616d15 src/Pure/drule.ML --- a/src/Pure/drule.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/Pure/drule.ML Tue Aug 06 20:52:06 2019 +0200 @@ -281,7 +281,8 @@ (*Resolution: multiple arguments, multiple results*) local fun res opt_ctxt th i rule = - Thm.biresolution opt_ctxt false [(false, th)] i rule handle THM _ => Seq.empty; + (Thm.biresolution opt_ctxt false [(false, th)] i rule handle THM _ => Seq.empty) + |> Seq.map Thm.solve_constraints; fun multi_res _ _ [] rule = Seq.single rule | multi_res opt_ctxt i (th :: ths) rule = @@ -297,14 +298,14 @@ let val resolve = Thm.biresolution NONE false (map (pair false) thas) i fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] - in maps resb thbs end; + in maps resb thbs |> map Thm.solve_constraints end; fun thas RL thbs = thas RLN (1, thbs); (*Isar-style multi-resolution*) fun bottom_rl OF rls = (case Seq.chop 2 (multi_resolve NONE rls bottom_rl) of - ([th], _) => th + ([th], _) => Thm.solve_constraints th | ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls) | _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls)); @@ -318,7 +319,8 @@ fun compose (tha, i, thb) = Thm.bicompose NONE {flatten = true, match = false, incremented = false} (false, tha, 0) i thb |> Seq.list_of |> distinct Thm.eq_thm - |> (fn [th] => th | _ => raise THM ("compose: unique result expected", i, [tha, thb])); + |> (fn [th] => Thm.solve_constraints th + | _ => raise THM ("compose: unique result expected", i, [tha, thb])); (** theorem equality **) @@ -695,7 +697,7 @@ Thm.bicompose NONE {flatten = true, match = false, incremented = incremented} (false, th1, 0) 1 th2 |> Seq.list_of |> distinct Thm.eq_thm - |> (fn [th] => th | _ => raise THM ("COMP", 1, [th1, th2])); + |> (fn [th] => Thm.solve_constraints th | _ => raise THM ("COMP", 1, [th1, th2])); in @@ -709,7 +711,7 @@ (case distinct Thm.eq_thm (Seq.list_of (Thm.bicompose NONE {flatten = false, match = false, incremented = true} (false, th, n) i (incr_indexes th rule))) of - [th'] => th' + [th'] => Thm.solve_constraints th' | [] => raise THM ("comp_no_flatten", i, [th, rule]) | _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule])); diff -r 8406a2c296e0 -r 5c1b2f616d15 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/Pure/raw_simplifier.ML Tue Aug 06 20:52:06 2019 +0200 @@ -533,7 +533,9 @@ if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (Thm.term_of elhs) then mk_eq_True ctxt (thm, name) else rrule_eq_True ctxt thm name lhs elhs rhs thm - end; + end |> map (fn {thm, name, lhs, elhs, perm} => + {thm = Thm.trim_context thm, name = name, lhs = lhs, + elhs = Thm.trim_context_cterm elhs, perm = perm}); fun orient_rrule ctxt (thm, name) = let @@ -690,8 +692,7 @@ raise SIMPLIFIER ("Congruence must start with a constant", [thm]); val (xs, _) = congs; val xs' = filter_out (fn (x : cong_name, _) => x = a) xs; - val weak' = xs' |> map_filter (fn (a, thm) => - if is_full_cong thm then NONE else SOME a); + val weak' = xs' |> map_filter (fn (a, th) => if is_full_cong th then NONE else SOME a); in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end); fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt; @@ -1351,7 +1352,11 @@ val _ = cond_tracing ctxt (fn () => print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (Thm.term_of ct)); - in bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt ct end; + in + ct + |> bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt + |> Thm.solve_constraints + end; val simple_prover = SINGLE o (fn ctxt => ALLGOALS (resolve_tac ctxt (prems_of ctxt))); diff -r 8406a2c296e0 -r 5c1b2f616d15 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/Pure/thm.ML Tue Aug 06 20:52:06 2019 +0200 @@ -1576,6 +1576,7 @@ hyps = hyps, tpairs = tpairs', prop = prop'}) + |> solve_constraints end handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); @@ -2155,7 +2156,7 @@ (*Resolution: exactly one resolvent must be produced*) fun tha RSN (i, thb) = (case Seq.chop 2 (biresolution NONE false [(false, tha)] i thb) of - ([th], _) => th + ([th], _) => solve_constraints th | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb]) | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb])); diff -r 8406a2c296e0 -r 5c1b2f616d15 src/Tools/Code/code_symbol.ML diff -r 8406a2c296e0 -r 5c1b2f616d15 src/ZF/Datatype.thy --- a/src/ZF/Datatype.thy Tue Aug 06 18:04:06 2019 +0200 +++ b/src/ZF/Datatype.thy Tue Aug 06 20:52:06 2019 +0200 @@ -97,7 +97,8 @@ val goal = Logic.mk_equals (old, new) val thm = Goal.prove ctxt [] [] goal (fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN - simp_tac (put_simpset datatype_ss ctxt addsimps #free_iffs lcon_info) 1) + simp_tac (put_simpset datatype_ss ctxt addsimps + (map (Thm.transfer thy) (#free_iffs lcon_info))) 1) handle ERROR msg => (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal); raise Match) diff -r 8406a2c296e0 -r 5c1b2f616d15 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/ZF/Tools/datatype_package.ML Tue Aug 06 20:52:06 2019 +0200 @@ -369,19 +369,20 @@ val dt_info = {inductive = true, constructors = constructors, - rec_rewrites = recursor_eqns, - case_rewrites = case_eqns, - induct = induct, - mutual_induct = mutual_induct, - exhaustion = elim}; + rec_rewrites = map Thm.trim_context recursor_eqns, + case_rewrites = map Thm.trim_context case_eqns, + induct = Thm.trim_context induct, + mutual_induct = Thm.trim_context mutual_induct, + exhaustion = Thm.trim_context elim}; val con_info = {big_rec_name = big_rec_name, constructors = constructors, (*let primrec handle definition by cases*) - free_iffs = free_iffs, - rec_rewrites = (case recursor_eqns of - [] => case_eqns | _ => recursor_eqns)}; + free_iffs = map Thm.trim_context free_iffs, + rec_rewrites = + (case recursor_eqns of [] => case_eqns | _ => recursor_eqns) + |> map Thm.trim_context}; (*associate with each constructor the datatype name and rewrites*) val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors diff -r 8406a2c296e0 -r 5c1b2f616d15 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/ZF/Tools/induct_tacs.ML Tue Aug 06 20:52:06 2019 +0200 @@ -96,8 +96,9 @@ val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i NONE state val tn = find_tname ctxt' var (map Thm.term_of asms) val rule = - if exh then #exhaustion (datatype_info thy tn) - else #induct (datatype_info thy tn) + datatype_info thy tn + |> (if exh then #exhaustion else #induct) + |> Thm.transfer thy; val (Const(\<^const_name>\mem\,_) $ Var(ixn,_) $ _) = (case Thm.prems_of rule of [] => error "induction is not available for this datatype" @@ -136,11 +137,11 @@ val dt_info = {inductive = true, constructors = constructors, - rec_rewrites = recursor_eqns, - case_rewrites = case_eqns, - induct = induct, - mutual_induct = @{thm TrueI}, (*No need for mutual induction*) - exhaustion = elim}; + rec_rewrites = map Thm.trim_context recursor_eqns, + case_rewrites = map Thm.trim_context case_eqns, + induct = Thm.trim_context induct, + mutual_induct = Thm.trim_context @{thm TrueI}, (*No need for mutual induction*) + exhaustion = Thm.trim_context elim}; val con_info = {big_rec_name = big_rec_name, @@ -149,8 +150,9 @@ free_iffs = [], (*thus we expect the necessary freeness rewrites to be in the simpset already, as is the case for Nat and disjoint sum*) - rec_rewrites = (case recursor_eqns of - [] => case_eqns | _ => recursor_eqns)}; + rec_rewrites = + (case recursor_eqns of [] => case_eqns | _ => recursor_eqns) + |> map Thm.trim_context}; (*associate with each constructor the datatype name and rewrites*) val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors diff -r 8406a2c296e0 -r 5c1b2f616d15 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/ZF/Tools/primrec_package.ML Tue Aug 06 20:52:06 2019 +0200 @@ -172,7 +172,7 @@ |> Sign.add_path (Long_Name.base_name fname) |> Global_Theory.add_defs false [Thm.no_attributes (apfst Binding.name def)]; - val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info) + val rewrites = def_thm :: map (mk_meta_eq o Thm.transfer thy1) (#rec_rewrites con_info) val eqn_thms = eqn_terms |> map (fn t => Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) diff -r 8406a2c296e0 -r 5c1b2f616d15 src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Tue Aug 06 18:04:06 2019 +0200 +++ b/src/ZF/arith_data.ML Tue Aug 06 20:52:06 2019 +0200 @@ -164,8 +164,8 @@ val prove_conv = prove_conv "nateq_cancel_numerals" val mk_bal = FOLogic.mk_eq val dest_bal = FOLogic.dest_eq - val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans} - val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans} + val bal_add1 = @{thm eq_add_iff [THEN iff_trans]} + val bal_add2 = @{thm eq_add_iff [THEN iff_trans]} fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans} end; @@ -177,8 +177,8 @@ val prove_conv = prove_conv "natless_cancel_numerals" val mk_bal = FOLogic.mk_binrel \<^const_name>\Ordinal.lt\ val dest_bal = FOLogic.dest_bin \<^const_name>\Ordinal.lt\ iT - val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans} - val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans} + val bal_add1 = @{thm less_add_iff [THEN iff_trans]} + val bal_add2 = @{thm less_add_iff [THEN iff_trans]} fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans} end; @@ -190,8 +190,8 @@ val prove_conv = prove_conv "natdiff_cancel_numerals" val mk_bal = FOLogic.mk_binop \<^const_name>\Arith.diff\ val dest_bal = FOLogic.dest_bin \<^const_name>\Arith.diff\ iT - val bal_add1 = @{thm diff_add_eq} RS @{thm trans} - val bal_add2 = @{thm diff_add_eq} RS @{thm trans} + val bal_add1 = @{thm diff_add_eq [THEN trans]} + val bal_add2 = @{thm diff_add_eq [THEN trans]} fun trans_tac ctxt = gen_trans_tac ctxt @{thm trans} end;