# HG changeset patch # User wenzelm # Date 1634324053 -7200 # Node ID bbfed17243afc7f0ffa11328137c09efd3a198f7 # Parent c960bfcb91db9384ec10323b2ba7a3124b035650 proper context for Goal.prove_internal; diff -r c960bfcb91db -r bbfed17243af src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Fri Oct 15 19:25:31 2021 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Fri Oct 15 20:54:13 2021 +0200 @@ -130,7 +130,8 @@ (** Sledgehammer and Isabelle (combination of provers) **) fun can_tac ctxt tactic conj = - can (Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)) (fn [] => tactic ctxt) + \<^can>\Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj) + (fn {context = goal_ctxt, prems = []} => tactic goal_ctxt)\ fun SOLVE_TIMEOUT seconds name tac st = let diff -r c960bfcb91db -r bbfed17243af src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Fri Oct 15 19:25:31 2021 +0200 +++ b/src/HOL/Tools/Function/function_lib.ML Fri Oct 15 20:54:13 2021 +0200 @@ -123,8 +123,8 @@ else if null js then mk (foldr1 mk (map (nth xs) is), Const (neu, ty)) else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js))))) - (K (rewrite_goals_tac ctxt ac - THEN resolve_tac ctxt [Drule.reflexive_thm] 1)) + (fn {context = goal_ctxt, ...} => + rewrite_goals_tac goal_ctxt ac THEN resolve_tac goal_ctxt [Drule.reflexive_thm] 1) end (* instance for unions *) diff -r c960bfcb91db -r bbfed17243af src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Fri Oct 15 19:25:31 2021 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Fri Oct 15 20:54:13 2021 +0200 @@ -260,8 +260,9 @@ |> HOLogic.mk_Trueprop |> Logic.all x_uc; - val mono_thm = Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal) - (K (mono_tac lthy 1)) + val mono_thm = + Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal) + (fn {context = goal_ctxt, ...} => mono_tac goal_ctxt 1) val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc); diff -r c960bfcb91db -r bbfed17243af src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 15 19:25:31 2021 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 15 20:54:13 2021 +0200 @@ -183,6 +183,7 @@ Example: "\x. x \ A \ x \ B \ sko A B \ A \ sko A B \ B" *) fun old_skolem_theorem_of_def ctxt rhs0 = let + val thy = Proof_Context.theory_of ctxt val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of ctxt val rhs' = rhs |> Thm.dest_comb |> snd val (ch, frees) = c_variant_abs_multi (rhs', []) @@ -196,13 +197,13 @@ val conc = Drule.list_comb (rhs, frees) |> Drule.beta_conv cabs |> Thm.apply cTrueprop - fun tacf [prem] = - rewrite_goals_tac ctxt @{thms skolem_def [abs_def]} - THEN resolve_tac ctxt - [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]}) - RS Global_Theory.get_thm (Proof_Context.theory_of ctxt) "Hilbert_Choice.someI_ex"] 1 in - Goal.prove_internal ctxt [ex_tm] conc tacf + Goal.prove_internal ctxt [ex_tm] conc + (fn {context = goal_ctxt, prems = [prem]} => + rewrite_goals_tac goal_ctxt @{thms skolem_def [abs_def]} THEN + resolve_tac goal_ctxt + [(prem |> rewrite_rule goal_ctxt @{thms skolem_def [abs_def]}) + RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex"] 1) |> forall_intr_list frees |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |> Thm.varifyT_global diff -r c960bfcb91db -r bbfed17243af src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Oct 15 19:25:31 2021 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Oct 15 20:54:13 2021 +0200 @@ -61,11 +61,13 @@ fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth = let - val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1 val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) in - Goal.prove_internal ctxt [] ct (K tac) + Goal.prove_internal ctxt [] ct + (fn {context = goal_ctxt, ...} => + rewrite_goals_tac goal_ctxt @{thms lambda_def [abs_def]} THEN + resolve_tac goal_ctxt [refl] 1) |> Meson.make_meta_clause ctxt end @@ -101,7 +103,9 @@ so that "Thm.equal_elim" works below. *) val t0 $ _ $ t2 = Thm.prop_of eq_th val eq_ct = t0 $ Thm.prop_of th $ t2 |> Thm.cterm_of ctxt - val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac ctxt [eq_th] 1)) + val eq_th' = + Goal.prove_internal ctxt [] eq_ct + (fn {context = goal_ctxt, ...} => resolve_tac goal_ctxt [eq_th] 1) in Thm.equal_elim eq_th' th end fun clause_params ordering = diff -r c960bfcb91db -r bbfed17243af src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Fri Oct 15 19:25:31 2021 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri Oct 15 20:54:13 2021 +0200 @@ -743,7 +743,8 @@ in if ntac then no_tac else - (case \<^try>\Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))\ of + (case \<^try>\Goal.prove_internal ctxt [] g + (fn {context = goal_ctxt, ...} => blast_tac (put_claset HOL_cs goal_ctxt) 1)\ of NONE => no_tac | SOME r => resolve_tac ctxt [r] i) end) diff -r c960bfcb91db -r bbfed17243af src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Fri Oct 15 19:25:31 2021 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Fri Oct 15 20:54:13 2021 +0200 @@ -708,12 +708,12 @@ in Goal.prove_internal ctxt' [] (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\bool\)))) - (fn _ => - resolve_tac ctxt' [thm2 RS @{thm transfer_start'}, thm2 RS @{thm transfer_start}] 1 THEN - (resolve_tac ctxt' [rule] + (fn {context = goal_ctxt, ...} => + resolve_tac goal_ctxt [thm2 RS @{thm transfer_start'}, thm2 RS @{thm transfer_start}] 1 THEN + (resolve_tac goal_ctxt [rule] THEN_ALL_NEW - (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules) - THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 + (SOLVED' (REPEAT_ALL_NEW (resolve_tac goal_ctxt rules) + THEN_ALL_NEW (DETERM o eq_rules_tac goal_ctxt eq_rules)))) 1 handle TERM (_, ts) => raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) |> Raw_Simplifier.rewrite_rule ctxt' post_simps @@ -744,12 +744,12 @@ in Goal.prove_internal ctxt' [] (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\bool\)))) - (fn _ => - resolve_tac ctxt' [thm2 RS @{thm untransfer_start}] 1 THEN - (resolve_tac ctxt' [rule] + (fn {context = goal_ctxt, ...} => + resolve_tac goal_ctxt [thm2 RS @{thm untransfer_start}] 1 THEN + (resolve_tac goal_ctxt [rule] THEN_ALL_NEW - (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules) - THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 + (SOLVED' (REPEAT_ALL_NEW (resolve_tac goal_ctxt rules) + THEN_ALL_NEW (DETERM o eq_rules_tac goal_ctxt eq_rules)))) 1 handle TERM (_, ts) => raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) |> Raw_Simplifier.rewrite_rule ctxt' post_simps diff -r c960bfcb91db -r bbfed17243af src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Fri Oct 15 19:25:31 2021 +0200 +++ b/src/HOL/Tools/datatype_realizer.ML Fri Oct 15 20:54:13 2021 +0200 @@ -112,14 +112,14 @@ val thm = Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl) - (fn prems => + (fn {context = goal_ctxt, prems} => EVERY [ - rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]), - resolve_tac ctxt [infer_instantiate ctxt inst induct] 1, - ALLGOALS (Object_Logic.atomize_prems_tac ctxt), - rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites), - REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (fn i => - REPEAT (eresolve_tac ctxt [allE] i) THEN assume_tac ctxt i)) 1)]) + rewrite_goals_tac goal_ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]), + resolve_tac goal_ctxt [infer_instantiate goal_ctxt inst induct] 1, + ALLGOALS (Object_Logic.atomize_prems_tac goal_ctxt), + rewrite_goals_tac goal_ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites), + REPEAT ((resolve_tac goal_ctxt prems THEN_ALL_NEW (fn i => + REPEAT (eresolve_tac goal_ctxt [allE] i) THEN assume_tac goal_ctxt i)) 1)]) |> Drule.export_without_context; val ind_name = Thm.derivation_name induct; @@ -190,12 +190,13 @@ Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y'])))) - (fn prems => - EVERY [ - resolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var y), Thm.cterm_of ctxt y')] exhaust] 1, + (fn {context = goal_ctxt, prems} => + EVERY [ + resolve_tac goal_ctxt + [infer_instantiate goal_ctxt [(#1 (dest_Var y), Thm.cterm_of goal_ctxt y')] exhaust] 1, ALLGOALS (EVERY' - [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites), - resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])]) + [asm_simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps case_rewrites), + resolve_tac goal_ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss goal_ctxt)])]) |> Drule.export_without_context; val exh_name = Thm.derivation_name exhaust; diff -r c960bfcb91db -r bbfed17243af src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Oct 15 19:25:31 2021 +0200 +++ b/src/Pure/goal.ML Fri Oct 15 20:54:13 2021 +0200 @@ -24,22 +24,23 @@ val norm_result: Proof.context -> thm -> thm val skip_proofs_enabled: unit -> bool val future_result: Proof.context -> thm future -> term -> thm - val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm + type goal_context = {prems: thm list, context: Proof.context} + val prove_internal: Proof.context -> cterm list -> cterm -> (goal_context -> tactic) -> thm val is_schematic: term -> bool val prove_common: Proof.context -> int option -> string list -> term list -> term list -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm list + (goal_context -> tactic) -> thm list val prove_future: Proof.context -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val prove: Proof.context -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val prove_global_future: theory -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val prove_global: theory -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val prove_sorry: Proof.context -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val prove_sorry_global: theory -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val restrict: int -> int -> thm -> thm val unrestrict: int -> thm -> thm val conjunction_tac: int -> tactic @@ -152,12 +153,21 @@ (** tactical theorem proving **) +type goal_context = {prems: thm list, context: Proof.context}; + + (* prove_internal -- minimal checks, no normalization of result! *) fun prove_internal ctxt casms cprop tac = - (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of - SOME th => Drule.implies_intr_list casms (finish ctxt th) - | NONE => error "Tactic failed"); + let + val (prems, ctxt') = ctxt + |> fold (Variable.declare_term o Thm.term_of) (casms @ [cprop]) + |> fold_map Thm.assume_hyps casms; + in + (case SINGLE (tac {prems = prems, context = ctxt'}) (init cprop) of + SOME th => Drule.implies_intr_list casms (finish ctxt' th) + | NONE => error "Tactic failed") + end; (* prove variations *)