# HG changeset patch # User wenzelm # Date 1634328028 -7200 # Node ID 823ccd84b8795c785912b8797084fad6fbba3034 # Parent a1aa42743d7dab2985a5ed50d1742ddcdffc4d5a revert bbfed17243af, breaks HOL-Proofs extraction; diff -r a1aa42743d7d -r 823ccd84b879 src/HOL/TPTP/atp_problem_import.ML --- 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>\Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj) - (fn {context = goal_ctxt, prems = []} => tactic goal_ctxt)\ + can (Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)) (fn [] => tactic ctxt) fun SOLVE_TIMEOUT seconds name tac st = let diff -r a1aa42743d7d -r 823ccd84b879 src/HOL/Tools/Function/function_lib.ML --- 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 *) diff -r a1aa42743d7d -r 823ccd84b879 src/HOL/Tools/Function/partial_function.ML --- 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); diff -r a1aa42743d7d -r 823ccd84b879 src/HOL/Tools/Meson/meson_clausify.ML --- 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: "\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', []) @@ -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 diff -r a1aa42743d7d -r 823ccd84b879 src/HOL/Tools/Metis/metis_tactic.ML --- 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 = diff -r a1aa42743d7d -r 823ccd84b879 src/HOL/Tools/Qelim/cooper.ML --- 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>\Goal.prove_internal ctxt [] g - (fn {context = goal_ctxt, ...} => blast_tac (put_claset HOL_cs goal_ctxt) 1)\ of + (case \<^try>\Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))\ of NONE => no_tac | SOME r => resolve_tac ctxt [r] i) end) diff -r a1aa42743d7d -r 823ccd84b879 src/HOL/Tools/Transfer/transfer.ML --- 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>\bool\)))) - (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>\bool\)))) - (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 diff -r a1aa42743d7d -r 823ccd84b879 src/HOL/Tools/datatype_realizer.ML --- 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; diff -r a1aa42743d7d -r 823ccd84b879 src/Pure/goal.ML --- 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 *)