From 710f314a9ccb84cdd9df9bc8bf52482b8d1f5a56 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 3 Aug 2020 13:34:53 +0200 Subject: (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. --- spartan/core/tactics.ML | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) (limited to 'spartan/core/tactics.ML') 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>\solve_side_conds\ (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>\intro\) 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>\intro\) i + else no_tac + end)) (* Induction/elimination *) -- cgit v1.2.3