case distinction

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