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/Spartan.thy | 30 +++++++++++++++++------------- spartan/core/context_tactical.ML | 4 ++++ spartan/core/eqsubst.ML | 2 +- spartan/core/rewrite.ML | 2 +- spartan/core/tactics.ML | 20 ++++++++++++-------- 5 files changed, 35 insertions(+), 23 deletions(-) (limited to 'spartan') 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 \Type-checking/inference\ named_theorems form and intr and comp and type \ \Defines elimination automation and the `elim` attribute\ -ML_file \elimination.ML\ +ML_file \elimination.ML\ lemmas [form] = PiF SigF and @@ -225,36 +225,40 @@ named_theorems intro \ \Logical introduction rules\ lemmas [intro] = PiI[rotated] SigI -ML_file \cases.ML\ \ \case reasoning rules\ +\ \Case reasoning rules\ +ML_file \cases.ML\ + ML_file \tactics.ML\ method_setup rule = \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\ + CHEADGOAL o SIDE_CONDS 0 (rule_ctac ths))))\ method_setup dest = - \Scan.lift (Scan.option (Args.parens Parse.int)) + \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))))\ + CHEADGOAL o SIDE_CONDS 0 (dest_ctac n_opt ths))))\ method_setup intro = \Scan.succeed (K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (intro_ctac))))\ + CHEADGOAL o SIDE_CONDS 0 intro_ctac)))\ method_setup intros = - \Scan.succeed (K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (CREPEAT o intro_ctac))))\ + \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))))))\ method_setup elim = \Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (elim_ctac tms))))\ - -method elims = elim+ + CHEADGOAL o SIDE_CONDS 0 (elim_ctac tms))))\ method_setup cases = \Args.term >> (fn tm => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (cases_ctac tm))))\ + CHEADGOAL o SIDE_CONDS 0 (cases_ctac tm))))\ +method elims = elim+ method facts = fact+ @@ -267,7 +271,7 @@ subsection \Trivial proofs (modulo automatic discharge of side conditions) method_setup this = \Scan.succeed (K (CONTEXT_METHOD (fn facts => - CHEADGOAL (SIDE_CONDS + CHEADGOAL (SIDE_CONDS 0 (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts)) facts))))\ 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>\subst\ (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>\rewrite\ (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>\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