diff options
author | Josh Chen | 2020-08-03 13:34:53 +0200 |
---|---|---|
committer | Josh Chen | 2020-08-03 13:34:53 +0200 |
commit | 710f314a9ccb84cdd9df9bc8bf52482b8d1f5a56 (patch) | |
tree | abbc3d847e17b9659b11eb8e4e2eda3430ba007a /spartan/core/tactics.ML | |
parent | 70fd3f72ef8f9cc01a071250d94e8c25ecb04c1d (diff) |
(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.
Diffstat (limited to 'spartan/core/tactics.ML')
-rw-r--r-- | spartan/core/tactics.ML | 20 |
1 files changed, 12 insertions, 8 deletions
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 *) |