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/tactics.ML | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'spartan/core/lib/tactics.ML')

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