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/Spartan.thy | |
| 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/Spartan.thy')
| -rw-r--r-- | spartan/core/Spartan.thy | 30 |
1 files changed, 17 insertions, 13 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> |