From 6ff59c83de9ce7d5715fae19f50d94b0b973414a Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 28 May 2020 14:07:52 +0200
Subject: case distinction

---
 spartan/core/lib/cases.ML   | 42 ++++++++++++++++++++++++++++++++++++++++++
 spartan/core/lib/tactics.ML | 21 +++++++++++++++++++++
 2 files changed, 63 insertions(+)
 create mode 100644 spartan/core/lib/cases.ML

(limited to 'spartan/core/lib')

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
-- 
cgit v1.2.3