# HG changeset patch # User haftmann # Date 1747851223 -7200 # Node ID e153ab596247086bbb79739d0669b618a2a213aa # Parent f03b71078a47708785e08ec3e5ca4b3c788ef5f4 provide modern interface for loopers diff -r f03b71078a47 -r e153ab596247 src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Wed May 21 20:13:43 2025 +0200 +++ b/src/Doc/Isar_Ref/Generic.thy Wed May 21 20:13:43 2025 +0200 @@ -1038,12 +1038,11 @@ text \ \begin{mldecls} - @{define_ML_infix setloop: "Proof.context * - (Proof.context -> int -> tactic) -> Proof.context"} \\ - @{define_ML_infix addloop: "Proof.context * - (string * (Proof.context -> int -> tactic)) - -> Proof.context"} \\ - @{define_ML_infix delloop: "Proof.context * string -> Proof.context"} \\ + @{define_ML Simplifier.set_loop: "(Proof.context -> int -> tactic) -> + Proof.context -> Proof.context"} \\ + @{define_ML Simplifier.add_loop: "string * (Proof.context -> int -> tactic) -> + Proof.context -> Proof.context"} \\ + @{define_ML Simplifier.del_loop: "string -> Proof.context -> Proof.context"} \\ @{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\ @{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\ @{define_ML Splitter.add_split_bang: " @@ -1060,14 +1059,14 @@ Another possibility is to apply an elimination rule on the assumptions. More adventurous loopers could start an induction. - \<^descr> \ctxt setloop tac\ installs \tac\ as the only looper tactic of \ctxt\. + \<^descr> \<^ML>\Simplifier.set_loop\~\tac ctxt\ installs \tac\ as the only looper tactic of \ctxt\. - \<^descr> \ctxt addloop (name, tac)\ adds \tac\ as an additional looper tactic + \<^descr> \<^ML>\Simplifier.add_loop\~\(name, tac) ctxt\ adds \tac\ as an additional looper tactic with name \name\, which is significant for managing the collection of loopers. The tactic will be tried after the looper tactics that had already been present in \ctxt\. - \<^descr> \ctxt delloop name\ deletes the looper tactic that was associated with + \<^descr> \<^ML>\Simplifier.del_loop\~\name ctxt\ deletes the looper tactic that was associated with \name\ from \ctxt\. \<^descr> \<^ML>\Splitter.add_split\~\thm ctxt\ adds split tactic diff -r f03b71078a47 -r e153ab596247 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Wed May 21 20:13:43 2025 +0200 +++ b/src/Pure/raw_simplifier.ML Wed May 21 20:13:43 2025 +0200 @@ -102,10 +102,13 @@ val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context val prems_of: Proof.context -> thm list val add_prems: thm list -> Proof.context -> Proof.context + val loop_tac: Proof.context -> int -> tactic + val set_loop: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context + val add_loop: string * (Proof.context -> int -> tactic) -> Proof.context -> Proof.context + val del_loop: string -> Proof.context -> Proof.context val solvers: Proof.context -> solver list * solver list val solver: Proof.context -> solver -> int -> tactic val set_solvers: solver list -> Proof.context -> Proof.context - val loop_tac: Proof.context -> int -> tactic val default_mk_sym: Proof.context -> thm -> thm option val set_reorient: (Proof.context -> term list -> term -> term -> bool) -> Proof.context -> Proof.context @@ -868,22 +871,28 @@ map_simpset2 (fn (congs, procs, mk_rews, term_ord, _, loop_tacs, solvers) => (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers)); -fun ctxt setloop tac = ctxt |> +fun set_loop tac = map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, _, solvers) => (congs, procs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers)); -fun ctxt addloop (name, tac) = ctxt |> +fun ctxt setloop tac = ctxt |> set_loop tac; + +fun add_loop (name, tac) = map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => (congs, procs, mk_rews, term_ord, subgoal_tac, AList.update (op =) (name, tac) loop_tacs, solvers)); -fun ctxt delloop name = ctxt |> +fun ctxt addloop tac = ctxt |> add_loop tac; + +fun del_loop name ctxt = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => (congs, procs, mk_rews, term_ord, subgoal_tac, (if AList.defined (op =) loop_tacs name then () else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name); AList.delete (op =) name loop_tacs), solvers)); +fun ctxt delloop name = ctxt |> del_loop name; + fun ctxt setSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) => (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));