aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--spartan/core/Spartan.thy6
-rw-r--r--spartan/core/lib/cases.ML42
-rw-r--r--spartan/core/lib/tactics.ML21
3 files changed, 68 insertions, 1 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 4e53a45..b0fec5a 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -162,7 +162,8 @@ ML_file \<open>lib/congruence.ML\<close>
section \<open>Methods\<close>
-ML_file \<open>lib/elimination.ML\<close> \<comment> \<open>declares the [elims] attribute\<close>
+ML_file \<open>lib/elimination.ML\<close> \<comment> \<open>elimination rules\<close>
+ML_file \<open>lib/cases.ML\<close> \<comment> \<open>case reasoning rules\<close>
named_theorems intros and comps
lemmas
@@ -194,6 +195,9 @@ method_setup elim =
method elims = elim+
+method_setup cases =
+ \<open>Args.term >> (fn tm => fn ctxt => SIMPLE_METHOD' (cases_tac tm ctxt))\<close>
+
(*This could possibly use additional simplification hints via a simp: modifier*)
method_setup typechk =
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (
diff --git a/spartan/core/lib/cases.ML b/spartan/core/lib/cases.ML
new file mode 100644
index 0000000..560a9f1
--- /dev/null
+++ b/spartan/core/lib/cases.ML
@@ -0,0 +1,42 @@
+(* Title: cases.ML
+ Author: Joshua Chen
+
+Case reasoning.
+*)
+
+structure Case: sig
+
+val rules: Proof.context -> thm list
+val lookup_rule: Proof.context -> Termtab.key -> thm option
+val register_rule: thm -> Context.generic -> Context.generic
+
+end = struct
+
+(* Context data *)
+
+(*Stores elimination rules together with a list of the indexnames of the
+ variables each rule eliminates. Keyed by head of the type being eliminated.*)
+structure Rules = Generic_Data (
+ type T = thm Termtab.table
+ val empty = Termtab.empty
+ val extend = I
+ val merge = Termtab.merge Thm.eq_thm_prop
+)
+
+val rules = map #2 o Termtab.dest o Rules.get o Context.Proof
+fun lookup_rule ctxt = Termtab.lookup (Rules.get (Context.Proof ctxt))
+fun register_rule rl =
+ let val hd = Term.head_of (Lib.type_of_typing (Thm.major_prem_of rl))
+ in Rules.map (Termtab.update (hd, rl)) end
+
+
+(* [cases] attribute *)
+val _ = Theory.setup (
+ Attrib.setup \<^binding>\<open>cases\<close>
+ (Scan.succeed (Thm.declaration_attribute register_rule))
+ ""
+ #> Global_Theory.add_thms_dynamic (\<^binding>\<open>cases\<close>, rules o Context.proof_of)
+)
+
+
+end
diff --git a/spartan/core/lib/tactics.ML b/spartan/core/lib/tactics.ML
index 0e7db43..172ae90 100644
--- a/spartan/core/lib/tactics.ML
+++ b/spartan/core/lib/tactics.ML
@@ -17,6 +17,7 @@ val dest_tac: int option -> thm list -> Proof.context -> int -> tactic
val intro_tac: Proof.context -> int -> tactic
val intros_tac: Proof.context -> int -> tactic
val elim_context_tac: term list -> Proof.context -> int -> context_tactic
+val cases_tac: term -> Proof.context -> int -> tactic
end = struct
@@ -193,6 +194,26 @@ fun elim_context_tac tms ctxt = case tms of
end
end)
+fun cases_tac tm ctxt = SUBGOAL (fn (goal, i) =>
+ let
+ val facts = Proof_Context.facts_of ctxt
+ val prems = Logic.strip_assums_hyp goal
+ val template = Lib.typing_of_term tm
+ val types =
+ map (Thm.prop_of o #1) (Facts.could_unify facts template)
+ @ filter (fn prem => Term.could_unify (template, prem)) prems
+ |> map Lib.type_of_typing
+ val res = (case types of
+ [typ] => Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt tm)]
+ (the (Case.lookup_rule ctxt (Term.head_of typ)))
+ | [] => raise Option
+ | _ => raise error (Syntax.string_of_term ctxt tm ^ "not uniquely typed"))
+ handle Option => error ("no case rule known for "
+ ^ (Syntax.string_of_term ctxt tm))
+ in
+ SIDE_CONDS (resolve_tac ctxt [res]) ctxt i
+ end)
+
end
end