--- a/src/HOL/TPTP/atp_problem_import.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Oct 15 22:00:28 2021 +0200
@@ -130,8 +130,7 @@
(** Sledgehammer and Isabelle (combination of provers) **)
fun can_tac ctxt tactic conj =
- \<^can>\<open>Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)
- (fn {context = goal_ctxt, prems = []} => tactic goal_ctxt)\<close>
+ can (Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)) (fn [] => tactic ctxt)
fun SOLVE_TIMEOUT seconds name tac st =
let
--- a/src/HOL/Tools/Function/function_lib.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Fri Oct 15 22:00:28 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)))))
- (fn {context = goal_ctxt, ...} =>
- rewrite_goals_tac goal_ctxt ac THEN resolve_tac goal_ctxt [Drule.reflexive_thm] 1)
+ (K (rewrite_goals_tac ctxt ac
+ THEN resolve_tac ctxt [Drule.reflexive_thm] 1))
end
(* instance for unions *)
--- a/src/HOL/Tools/Function/partial_function.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Fri Oct 15 22:00:28 2021 +0200
@@ -260,9 +260,8 @@
|> HOLogic.mk_Trueprop
|> Logic.all x_uc;
- val mono_thm =
- Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal)
- (fn {context = goal_ctxt, ...} => mono_tac goal_ctxt 1)
+ val mono_thm = Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal)
+ (K (mono_tac lthy 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);
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 15 22:00:28 2021 +0200
@@ -183,7 +183,6 @@
Example: "\<exists>x. x \<in> A \<and> x \<notin> B \<Longrightarrow> sko A B \<in> A \<and> sko A B \<notin> 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', [])
@@ -197,13 +196,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
- (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)
+ Goal.prove_internal ctxt [ex_tm] conc tacf
|> forall_intr_list frees
|> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
|> Thm.varifyT_global
--- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Oct 15 22:00:28 2021 +0200
@@ -61,13 +61,11 @@
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
- (fn {context = goal_ctxt, ...} =>
- rewrite_goals_tac goal_ctxt @{thms lambda_def [abs_def]} THEN
- resolve_tac goal_ctxt [refl] 1)
+ Goal.prove_internal ctxt [] ct (K tac)
|> Meson.make_meta_clause ctxt
end
@@ -103,9 +101,7 @@
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
- (fn {context = goal_ctxt, ...} => resolve_tac goal_ctxt [eq_th] 1)
+ val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac ctxt [eq_th] 1))
in Thm.equal_elim eq_th' th end
fun clause_params ordering =
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Oct 15 22:00:28 2021 +0200
@@ -743,8 +743,7 @@
in
if ntac then no_tac
else
- (case \<^try>\<open>Goal.prove_internal ctxt [] g
- (fn {context = goal_ctxt, ...} => blast_tac (put_claset HOL_cs goal_ctxt) 1)\<close> of
+ (case \<^try>\<open>Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))\<close> of
NONE => no_tac
| SOME r => resolve_tac ctxt [r] i)
end)
--- a/src/HOL/Tools/Transfer/transfer.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Fri Oct 15 22:00:28 2021 +0200
@@ -708,12 +708,12 @@
in
Goal.prove_internal ctxt' []
(Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\<open>bool\<close>))))
- (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]
+ (fn _ =>
+ resolve_tac ctxt' [thm2 RS @{thm transfer_start'}, thm2 RS @{thm transfer_start}] 1 THEN
+ (resolve_tac ctxt' [rule]
THEN_ALL_NEW
- (SOLVED' (REPEAT_ALL_NEW (resolve_tac goal_ctxt rules)
- THEN_ALL_NEW (DETERM o eq_rules_tac goal_ctxt eq_rules)))) 1
+ (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
+ THEN_ALL_NEW (DETERM o eq_rules_tac 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>\<open>bool\<close>))))
- (fn {context = goal_ctxt, ...} =>
- resolve_tac goal_ctxt [thm2 RS @{thm untransfer_start}] 1 THEN
- (resolve_tac goal_ctxt [rule]
+ (fn _ =>
+ resolve_tac ctxt' [thm2 RS @{thm untransfer_start}] 1 THEN
+ (resolve_tac ctxt' [rule]
THEN_ALL_NEW
- (SOLVED' (REPEAT_ALL_NEW (resolve_tac goal_ctxt rules)
- THEN_ALL_NEW (DETERM o eq_rules_tac goal_ctxt eq_rules)))) 1
+ (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
+ THEN_ALL_NEW (DETERM o eq_rules_tac 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
--- a/src/HOL/Tools/datatype_realizer.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Oct 15 22:00:28 2021 +0200
@@ -112,14 +112,14 @@
val thm =
Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl)
- (fn {context = goal_ctxt, prems} =>
+ (fn prems =>
EVERY [
- 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)])
+ 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)])
|> Drule.export_without_context;
val ind_name = Thm.derivation_name induct;
@@ -190,13 +190,12 @@
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 {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,
+ (fn prems =>
+ EVERY [
+ resolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var y), Thm.cterm_of ctxt y')] exhaust] 1,
ALLGOALS (EVERY'
- [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)])])
+ [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)])])
|> Drule.export_without_context;
val exh_name = Thm.derivation_name exhaust;
--- a/src/Pure/goal.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/Pure/goal.ML Fri Oct 15 22:00:28 2021 +0200
@@ -24,23 +24,22 @@
val norm_result: Proof.context -> thm -> thm
val skip_proofs_enabled: unit -> bool
val future_result: Proof.context -> thm future -> term -> thm
- type goal_context = {prems: thm list, context: Proof.context}
- val prove_internal: Proof.context -> cterm list -> cterm -> (goal_context -> tactic) -> thm
+ val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
val is_schematic: term -> bool
val prove_common: Proof.context -> int option -> string list -> term list -> term list ->
- (goal_context -> tactic) -> thm list
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm list
val prove_future: Proof.context -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove: Proof.context -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_global_future: theory -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_global: theory -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_sorry: Proof.context -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_sorry_global: theory -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val restrict: int -> int -> thm -> thm
val unrestrict: int -> thm -> thm
val conjunction_tac: int -> tactic
@@ -153,21 +152,12 @@
(** 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 =
- 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;
+ (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");
(* prove variations *)