(FEAT) SIDE_CONDS tactical has additional argument specifying how many initial subgoals to skip applying the side condition solver to.

(FEAT) `intro`, `intros` methods for "logical introduction rules" (as opposed to typechecking `intr` attribute), only works on conclusions with rigid type.

(FEAT) CREPEAT_N bounded repetition tactical, used in `intros n` method.

5 files changed, 35 insertions, 23 deletions

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 180354c..ea72208 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -192,7 +192,7 @@ subsection \<open>Type-checking/inference\<close>
 named_theorems form and intr and comp and type
 
 \<comment> \<open>Defines elimination automation and the `elim` attribute\<close>
-ML_file \<open>elimination.ML\<close>  
+ML_file \<open>elimination.ML\<close>
 
 lemmas
   [form] = PiF SigF and
@@ -225,36 +225,40 @@ named_theorems intro \<comment> \<open>Logical introduction rules\<close>
 
 lemmas [intro] = PiI[rotated] SigI
 
-ML_file \<open>cases.ML\<close> \<comment> \<open>case reasoning rules\<close>
+\<comment> \<open>Case reasoning rules\<close>
+ML_file \<open>cases.ML\<close>
+
 ML_file \<open>tactics.ML\<close>
 
 method_setup rule =
   \<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\<close>
+    CHEADGOAL o SIDE_CONDS 0 (rule_ctac ths))))\<close>
 
 method_setup dest =
-  \<open>Scan.lift (Scan.option (Args.parens Parse.int))
+  \<open>Scan.lift (Scan.option (Args.parens Parse.nat))
     -- Attrib.thms >> (fn (n_opt, ths) => K (CONTEXT_METHOD (
-      CHEADGOAL o SIDE_CONDS (dest_ctac n_opt ths))))\<close>
+      CHEADGOAL o SIDE_CONDS 0 (dest_ctac n_opt ths))))\<close>
 
 method_setup intro =
   \<open>Scan.succeed (K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (intro_ctac))))\<close>
+    CHEADGOAL o SIDE_CONDS 0 intro_ctac)))\<close>
 
 method_setup intros =
-  \<open>Scan.succeed (K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (CREPEAT o intro_ctac))))\<close>
+  \<open>Scan.lift (Scan.option Parse.nat) >> (fn n_opt =>
+    K (CONTEXT_METHOD (fn facts =>
+      case n_opt of
+        SOME n => CREPEAT_N n (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))
+      | NONE => CREPEAT (CCHANGED (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))))))\<close>
 
 method_setup elim =
   \<open>Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (elim_ctac tms))))\<close>
-
-method elims = elim+
+    CHEADGOAL o SIDE_CONDS 0 (elim_ctac tms))))\<close>
 
 method_setup cases =
   \<open>Args.term >> (fn tm => K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (cases_ctac tm))))\<close>
+    CHEADGOAL o SIDE_CONDS 0 (cases_ctac tm))))\<close>
 
+method elims = elim+
 method facts = fact+
 
 
@@ -267,7 +271,7 @@ subsection \<open>Trivial proofs (modulo automatic discharge of side conditions)
 
 method_setup this =
   \<open>Scan.succeed (K (CONTEXT_METHOD (fn facts =>
-    CHEADGOAL (SIDE_CONDS
+    CHEADGOAL (SIDE_CONDS 0
       (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts))
       facts))))\<close>
 
diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML
index b5a6c00..0aa6f20 100644
--- a/spartan/core/context_tactical.ML
+++ b/spartan/core/context_tactical.ML
@@ -28,6 +28,7 @@ val CAPPEND': context_tactic' * context_tactic' -> context_tactic'
 val CTRY: context_tactic -> context_tactic
 val CREPEAT: context_tactic -> context_tactic
 val CREPEAT1: context_tactic -> context_tactic
+val CREPEAT_N: int -> context_tactic -> context_tactic
 val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic
 val CCHANGED: context_tactic -> context_tactic
 val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic'
@@ -91,6 +92,9 @@ fun CREPEAT ctac =
 
 fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac
 
+fun CREPEAT_N 0 _ = all_ctac
+  | CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac
+
 fun CFILTER pred ctac cst =
   ctac cst
   |> Seq.filter_results
diff --git a/spartan/core/eqsubst.ML b/spartan/core/eqsubst.ML
index e7ecf63..31d5126 100644
--- a/spartan/core/eqsubst.ML
+++ b/spartan/core/eqsubst.ML
@@ -433,7 +433,7 @@ val _ =
         "single-step substitution" #>
       Method.setup \<^binding>\<open>subst\<close>
         (parser >> (fn ((asm, occs), inthms) => K (CONTEXT_METHOD (
-          CHEADGOAL o SIDE_CONDS
+          CHEADGOAL o SIDE_CONDS 0
             ((if asm then eqsubst_asm_ctac else eqsubst_ctac) occs inthms)))))
         "single-step substitution with automatic discharge of side conditions"
     )
diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML
index eba0e81..99c21b5 100644
--- a/spartan/core/rewrite.ML
+++ b/spartan/core/rewrite.ML
@@ -458,7 +458,7 @@ val _ =
       "single-step rewriting, allowing subterm selection via patterns" #>
     Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >>
       (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD (
-        CHEADGOAL o SIDE_CONDS
+        CHEADGOAL o SIDE_CONDS 0
           (rewrite_export_ctac ((pattern, to), SOME pat_ctxt) inthms)))))
       "single-step rewriting with auto-typechecking"
   end
diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
index 959050e..446af15 100644
--- a/spartan/core/tactics.ML
+++ b/spartan/core/tactics.ML
@@ -8,7 +8,7 @@ structure Tactics:
 sig
 
 val solve_side_conds: int Config.T
-val SIDE_CONDS: context_tactic' -> thm list -> context_tactic'
+val SIDE_CONDS: int -> context_tactic' -> thm list -> context_tactic'
 val rule_ctac: thm list -> context_tactic'
 val dest_ctac: int option -> thm list -> context_tactic'
 val intro_ctac: context_tactic'
@@ -21,12 +21,12 @@ end = struct
 (* Side conditions *)
 val solve_side_conds = Attrib.setup_config_int \<^binding>\<open>solve_side_conds\<close> (K 2)
 
-fun SIDE_CONDS ctac facts i (cst as (ctxt, st)) = cst |> (ctac i CTHEN
+fun SIDE_CONDS j ctac facts i (cst as (ctxt, st)) = cst |>
   (case Config.get ctxt solve_side_conds of
-    1 => CALLGOALS (CTRY o Types.known_ctac facts)
-  | 2 => CREPEAT_IN_RANGE i (Thm.nprems_of st - i)
+    1 => (ctac CTHEN_ALL_NEW (CTRY o Types.known_ctac facts)) i
+  | 2 => ctac i CTHEN CREPEAT_IN_RANGE (i + j) (Thm.nprems_of st - i)
       (CTRY o CREPEAT_ALL_NEW_FWD (Types.check_infer facts))
-  | _ => all_ctac))
+  | _ => ctac i)
 
 
 (* rule, dest, intro *)
@@ -55,9 +55,13 @@ fun dest_ctac opt_n ths i (ctxt, st) =
 
 end
 
-(*Applies some introduction rule*)
-fun intro_ctac i (ctxt, st) = TACTIC_CONTEXT ctxt (resolve_tac ctxt
-  (Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) i st)
+(*Applies an appropriate introduction rule*)
+val intro_ctac = CONTEXT_TACTIC' (fn ctxt => SUBGOAL (fn (goal, i) =>
+  let val concl = Logic.strip_assums_concl goal in
+    if Lib.is_typing concl andalso Lib.is_rigid (Lib.type_of_typing concl)
+    then resolve_tac ctxt (Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) i
+    else no_tac
+  end))
 
 
 (* Induction/elimination *)