aboutsummaryrefslogtreecommitdiff
path: root/spartan/core
diff options
context:
space:
mode:
Diffstat (limited to 'spartan/core')
-rw-r--r--spartan/core/Spartan.thy30
-rw-r--r--spartan/core/context_tactical.ML4
-rw-r--r--spartan/core/eqsubst.ML2
-rw-r--r--spartan/core/rewrite.ML2
-rw-r--r--spartan/core/tactics.ML20
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 *)