lib: add rules_tac and related multi-thm instantiators

In `Rules_Tac`, add a `rules_tac` which is `rule_tac` but with the
ability to instantiate the same variable name in multiple theorems.

Also add the specialised `single_instantiate_tac` which allows using the
above mechanism to instantiate a specific variable name in a specific
set of theorems (e.g. "rv" in a set of symbolic-execution lemmas).

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

lib/ROOT

@@ -84,6 +84,7 @@ session Lib (lib) = Word_Lib +
     ML_Goal_Test
     Value_Type
     Named_Eta
+    Rules_Tac
 
     (* should really be a separate session, but too entangled atm: *)
     NonDetMonadLemmaBucket
@@ -163,6 +164,7 @@ session LibTest (lib) in test = Refine +
     Locale_Abbrev_Test
     Value_Type_Test
     Named_Eta_Test
+    Rules_Tac_Test
   (* use virtual memory function as an example, only makes sense on ARM: *)
   theories [condition = "L4V_ARCH_IS_ARM"]
     Corres_Test

lib/Rules_Tac.thy

@@ -0,0 +1,55 @@
+(*
+ * Copyright 2022, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+(* Tactics/methods related to instantiating variables in multiple thms. *)
+
+theory Rules_Tac
+imports Main
+begin
+
+ML \<open>
+structure Multi_Rule_Insts = struct
+
+(* copied verbatim from rule_insts.ML *)
+val named_insts =
+  Parse.and_list1
+    (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Parse.embedded_inner_syntax))
+    -- Parse.for_fixes
+
+(* copied from rule_insts.ML, modified to allow instantiation in multiple rules simultanously *)
+fun method inst_tac tac =
+  Args.goal_spec -- Scan.optional (Scan.lift (named_insts --| Args.$$$ "in")) ([], []) --
+  Attrib.thms >> (fn ((quant, (insts, fixes)), thms) => fn ctxt => METHOD (fn facts =>
+    if null insts andalso null fixes
+    then quant (Method.insert_tac ctxt facts THEN' tac ctxt thms)
+    else
+      map (fn thm => quant (Method.insert_tac ctxt facts THEN' inst_tac ctxt insts fixes thm)) thms
+      |> FIRST))
+
+(* Instantiate a single named variable in thms with a value, apply to inst_tac *)
+fun single_instantiate_tac inst_tac var_name syn_value fixes thms ctxt facts =
+  let
+    val var = Option.valOf (Lexicon.read_variable var_name)
+    val insts = [((var, Position.none), syn_value)]
+  in
+    map (fn thm => HEADGOAL (Method.insert_tac ctxt facts THEN' inst_tac ctxt insts fixes thm)) thms
+    |> FIRST
+  end
+
+(* Example of how use embed single_instantiate_tac in a method *)
+fun single_instantiate_method inst_tac var_name thms =
+  Scan.lift Parse.embedded_inner_syntax -- Scan.lift Parse.for_fixes
+  >> (fn (syn, fixes) => fn ctxt =>
+        METHOD (single_instantiate_tac inst_tac var_name syn fixes thms ctxt))
+
+end\<close>
+
+method_setup rules_tac = \<open>Multi_Rule_Insts.method Rule_Insts.res_inst_tac resolve_tac\<close>
+  "apply rule (dynamic instantiation for multiple thms containing same variable)"
+
+(* see Rules_Tac_Test.thy for examples/demo *)
+
+end

lib/test/Rules_Tac_Test.thy

@@ -0,0 +1,72 @@
+(*
+ * Copyright 2022, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+(* Tactics/methods related to instantiating variables in multiple thms - Examples *)
+
+theory Rules_Tac_Test
+imports Lib.Rules_Tac
+begin
+
+experiment begin
+
+lemmas thms = bexI exI
+
+(* instantiating a variable in multiple thms *)
+
+lemma "P n \<Longrightarrow> \<exists>x. P x"
+  apply (rules_tac x=n in thms) (* combined thms *)
+  apply assumption
+  done
+
+lemma "P n \<Longrightarrow> \<exists>x. P x"
+  apply (rules_tac x=n in bexI exI) (* thms listed separately *)
+  apply assumption
+  done
+
+lemma "P n \<Longrightarrow> \<exists>x. P x"
+  apply (rules_tac x=n and P=k for z k in thms) (* irrelevant "for" fixes *)
+  apply assumption
+  done
+
+lemma "P n \<Longrightarrow> \<exists>x. P x"
+  apply (rules_tac x="P n" for P in exI) (* used for fixes *)
+  oops
+
+(* single-variable instantiation using single_instantiate_tac *)
+lemma "P n \<Longrightarrow> \<exists>x. P x"
+  apply (tactic \<open>
+    let
+      val v = Token.explode (Thy_Header.get_keywords' @{context}) Position.none "n"
+              |> Parse.embedded_inner_syntax |> #1
+    in
+      Multi_Rule_Insts.single_instantiate_tac Rule_Insts.res_inst_tac "x" v [] @{thms thms}
+      @{context} []
+    end\<close>)
+  apply assumption
+  done
+
+(* single-variable instantiation using single_instantiate_tac via a method *)
+
+method_setup inst_x_exI_tac =
+  \<open>Multi_Rule_Insts.single_instantiate_method Rule_Insts.res_inst_tac "x" @{thms thms}\<close>
+  \<open>instantiate "x" in thms and apply the result with rule_tac\<close>
+
+lemma "P n \<Longrightarrow> \<exists>x. P x"
+  apply (inst_x_exI_tac n)
+  apply assumption
+  done
+
+(* instantiation of same variable with a different type in each theorem *)
+lemma
+  assumes a: "\<And>x P. Z x \<Longrightarrow> P (x::nat)"
+  assumes b: "\<And>x P. Y x \<Longrightarrow> P (x::int)"
+  shows "P (2::nat)"
+  apply (rules_tac x=2 in b a)
+  oops
+
+end
+
+end