# HG changeset patch # User desharna # Date 1745478993 -7200 # Node ID c17936c7a5095a8c4ad2eb15908015b646561b8a # Parent 4b13f46ff8ff4dee873b402fbe2b8d98780bbbe9# Parent 318526b74e6f88391f0ce19a7a95fec44ea3107c merged diff -r 4b13f46ff8ff -r c17936c7a509 src/HOL/Tools/Metis/metis_instantiations.ML --- a/src/HOL/Tools/Metis/metis_instantiations.ML Wed Apr 23 17:34:13 2025 +0200 +++ b/src/HOL/Tools/Metis/metis_instantiations.ML Thu Apr 24 09:16:33 2025 +0200 @@ -9,7 +9,7 @@ type inst type infer_params = { - ctxt : Proof.context, + infer_ctxt : Proof.context, type_enc : string, lam_trans : string, th_name : thm -> string option, @@ -27,8 +27,8 @@ val table_of_thm_inst : thm * inst -> cterm Vars.table val pretty_name_inst : Proof.context -> string * inst -> Pretty.T val string_of_name_inst : Proof.context -> string * inst -> string - val infer_thm_insts : infer_params -> (thm * inst) list option - val instantiate_call : infer_params -> thm -> unit + val infer_thm_insts : Proof.context -> infer_params -> (thm * inst) list option + val instantiate_call : Proof.context -> infer_params -> thm -> unit end; structure Metis_Instantiations : METIS_INSTANTIATIONS = @@ -45,7 +45,7 @@ (* Params needed for inference of variable instantiations *) type infer_params = { - ctxt : Proof.context, + infer_ctxt : Proof.context, type_enc : string, lam_trans : string, th_name : thm -> string option, @@ -149,7 +149,7 @@ (* Find the theorem corresponding to a Metis axiom if it has a name. * "Theorems" are Isabelle theorems given to the metis tactic. * "Axioms" are clauses given to the Metis prover. *) -fun metis_axiom_to_thm {ctxt, th_name, th_cls_pairs, axioms, ...} (msubst, maxiom) = +fun metis_axiom_to_thm ctxt {th_name, th_cls_pairs, axioms, ...} (msubst, maxiom) = let val axiom = lookth axioms maxiom in @@ -161,7 +161,8 @@ (* Build a table : term Vartab.table list Thmtab.table that maps a theorem to a * list of variable substitutions (theorems can be instantiated multiple times) * from Metis substitutions *) -fun metis_substs_to_table {ctxt, type_enc, lifted, new_skolem, sym_tab, ...} th_of_vars th_msubsts = +fun metis_substs_to_table ctxt {infer_ctxt, type_enc, lifted, new_skolem, sym_tab, ...} + th_of_vars th_msubsts = let val _ = trace_msg ctxt (K "AXIOM SUBSTITUTIONS") val type_enc = type_enc_of_string Strict type_enc @@ -179,7 +180,7 @@ (* Infer types and replace "_" terms/types with schematic variables *) val infer_types_pattern = singleton (Type_Infer_Context.infer_types_finished - (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) + (Proof_Context.set_mode Proof_Context.mode_pattern infer_ctxt)) (* "undefined" if allowed and not using new_skolem, "_" otherwise. *) val undefined_pattern = @@ -192,11 +193,16 @@ (* Instantiate schematic and free variables *) val inst_vars_frees = map_aterms (fn t as Free (x, T) => - (* an unfixed/internal free variable is unknown/inaccessible to the user, + (* an undeclared/internal free variable is unknown/inaccessible to the user, * so we replace it with "_" *) - if not (Variable.is_fixed ctxt x) orelse Name.is_internal (Variable.revert_fixed ctxt x) - then Term.dummy_pattern T - else t + let + val x' = Variable.revert_fixed ctxt x + in + if not (Variable.is_declared ctxt x') orelse Name.is_internal x' then + Term.dummy_pattern T + else + t + end | Var (_, T) => (* a schematic variable can be replaced with any term, * so we replace it with "undefined" *) @@ -237,7 +243,7 @@ let val _ = trace_msg ctxt (fn () => "Metis axiom: " ^ Metis_Thm.toString maxiom) val _ = trace_msg ctxt (fn () => "Metis substitution: " ^ Metis_Subst.toString msubst) - val _ = trace_msg ctxt (fn () => "Isabelle axiom: " ^ Thm.string_of_thm ctxt axiom) + val _ = trace_msg ctxt (fn () => "Isabelle axiom: " ^ Thm.string_of_thm infer_ctxt axiom) val _ = trace_msg ctxt (fn () => "Isabelle theorem: " ^ Thm.string_of_thm ctxt th ^ " (" ^ name ^ ")") @@ -255,7 +261,7 @@ (* cf. find_var in Metis_Reconstruct.inst_inference *) |> Option.mapPartial (fn name => List.find (fn (a, _) => a = name) vars) (* cf. subst_translation in Metis_Reconstruct.inst_inference *) - |> Option.map (fn var => (var, hol_term_of_metis ctxt type_enc sym_tab mt)) + |> Option.map (fn var => (var, hol_term_of_metis infer_ctxt type_enc sym_tab mt)) (* Build the substitution table and instantiate the remaining schematic variables *) fun build_subst_table substs = @@ -275,7 +281,7 @@ trace_msg ctxt (fn () => cat_lines ("Raw Isabelle substitution:" :: (raw_substs |> map (fn (var, t) => Term.string_of_vname var ^ " |-> " ^ - Syntax.string_of_term ctxt t)))) + Syntax.string_of_term infer_ctxt t)))) val subst = raw_substs |> map (apsnd polish_term) @@ -319,16 +325,16 @@ (t', Sign.typ_unify thy (T, U) (tyenv, maxidx')) end - (* Instantiate type variables with a type unifier or a dummy type + (* Instantiate type variables with a type unifier and import remaining ones * (cf. Drule.infer_instantiate_types) *) fun inst_unifier (ts, tyenv) = let val instT = TVars.build (tyenv |> Vartab.fold (fn (xi, (S, T)) => TVars.add ((xi, S), Envir.norm_type tyenv T))) - val dummy_tvars = Term.map_types (map_type_tvar (K Term.dummyT)) + val ts' = map (Term_Subst.instantiate (instT, Vars.empty)) ts in - map (dummy_tvars o Term_Subst.instantiate (instT, Vars.empty)) ts + Variable.importT_terms ts' ctxt |> fst end (* Build variable instantiations from a substitution table and instantiate @@ -351,7 +357,7 @@ Thmtab.fold_rev (fn (th, substs) => fold (add_subst th) substs) th_substs_table [] end -fun really_infer_thm_insts (infer_params as {ctxt, th_name, th_cls_pairs, mth, ...}) = +fun really_infer_thm_insts ctxt (infer_params as {th_name, th_cls_pairs, mth, ...}) = let (* Compute the theorem variables ordered as in of-instantiations. * import_export_thm is used to get the same variables as in axioms. *) @@ -361,8 +367,8 @@ val th_insts = infer_metis_axiom_substs mth - |> map_filter (metis_axiom_to_thm infer_params) - |> metis_substs_to_table infer_params th_of_vars + |> map_filter (metis_axiom_to_thm ctxt infer_params) + |> metis_substs_to_table ctxt infer_params th_of_vars |> table_to_thm_insts ctxt th_of_vars val _ = trace_msg ctxt (fn () => cat_lines ("THEOREM INSTANTIATIONS" :: @@ -386,12 +392,12 @@ end (* Infer variable instantiations *) -fun infer_thm_insts (infer_params as {ctxt, ...}) = - \<^try>\SOME (really_infer_thm_insts infer_params) +fun infer_thm_insts ctxt infer_params = + \<^try>\SOME (really_infer_thm_insts ctxt infer_params) catch exn => (trace_msg ctxt (fn () => Runtime.exn_message exn); NONE)\ (* Write suggested command with of-instantiations *) -fun write_command {ctxt, type_enc, lam_trans, th_name, ...} st th_insts = +fun write_command ctxt {type_enc, lam_trans, th_name, ...} st th_insts = let val _ = trace_msg ctxt (K "SUGGEST OF-INSTANTIATIONS") val apply_str = if Thm.nprems_of st = 0 then "by" else "apply" @@ -408,9 +414,9 @@ end (* Infer variable instantiations and suggest of-instantiations *) -fun instantiate_call infer_params st = - infer_thm_insts infer_params +fun instantiate_call ctxt infer_params st = + infer_thm_insts ctxt infer_params |> Option.mapPartial (Option.filter (not o thm_insts_trivial)) - |> Option.app (write_command infer_params st) + |> Option.app (write_command ctxt infer_params st) end; diff -r 4b13f46ff8ff -r c17936c7a509 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Wed Apr 23 17:34:13 2025 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Apr 24 09:16:33 2025 +0200 @@ -211,7 +211,7 @@ val _ = if exists is_some (map th_name used_ths) then infer_params := SOME ({ - ctxt = ctxt', + infer_ctxt = ctxt', type_enc = type_enc_str, lam_trans = lam_trans, th_name = th_name, @@ -308,7 +308,7 @@ val instantiate_tac = if instantiate then (fn (NONE, st) => st - | (SOME infer_params, st) => tap (instantiate_call infer_params) st) + | (SOME infer_params, st) => tap (instantiate_call ctxt infer_params) st) else snd in @@ -356,7 +356,7 @@ (the_default default_metis_lam_trans lam_trans) false ctxt (schem_facts @ ths) i in Seq.THEN (insert_tac, metis_tac) - #> Seq.map (Option.mapPartial infer_thm_insts o fst) + #> Seq.map (Option.mapPartial (infer_thm_insts ctxt) o fst) #> Option.mapPartial fst o Seq.pull end