--- 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
--- 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
--- 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 =
--- 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>\<open>Rel\<close>, _) $ _ $ (lhs as (_ $ _)) $ _ =>
- Item_Net.update (lhs, thm)
- | _ => I) o
- map_compound_rhs
- (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
- Const (\<^const_name>\<open>Rel\<close>, _) $ _ $ _ $ (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>\<open>Rel\<close>, _) $ _ $ (lhs as (_ $ _)) $ _ =>
+ Item_Net.update (lhs, thm)
+ | _ => I) o
+ map_compound_rhs
+ (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
+ Const (\<^const_name>\<open>Rel\<close>, _) $ _ $ _ $ (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>\<open>relator_eq\<close>
- 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>\<open>relator_domain\<close>
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
--- 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)));
--- 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]));
--- 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)));
--- 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]));
--- 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)
--- 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
--- 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>\<open>mem\<close>,_) $ 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
--- 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)
--- 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>\<open>Ordinal.lt\<close>
val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Ordinal.lt\<close> 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>\<open>Arith.diff\<close>
val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Arith.diff\<close> 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;