# HG changeset patch
# User blanchet
# Date 1376313916 -7200
# Node ID 5e25877c51d4500f6b1327b1fbae71e5a28f635b
# Parent  3777ba39c660ddee038a785d5da74eed990b3582
introduced case tactics

diff -r 3777ba39c660 -r 5e25877c51d4 src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Mon Aug 12 15:25:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Mon Aug 12 15:25:16 2013 +0200
@@ -98,6 +98,26 @@
           ks ms disc_excludesss disc_excludesss' uncollapses))
     end;
 
+fun mk_case_same_ctr_tac ctxt injects =
+  REPEAT_DETERM o etac exE THEN' etac conjE THEN'
+    (case injects of
+      [] => atac
+    | [inject] => dtac (inject RS iffD1) THEN' REPEAT_DETERM o etac conjE THEN'
+        hyp_subst_tac ctxt THEN' rtac refl);
+
+fun mk_case_distinct_ctrs_tac ctxt distincts =
+  REPEAT_DETERM o etac exE THEN' etac conjE THEN' full_simp_tac (ss_only distincts ctxt);
+
+fun mk_case_tac ctxt n k def injects distinctss =
+  let val ks = 1 upto n in
+    HEADGOAL (rtac (def RS trans) THEN' rtac @{thm the_equality} THEN' rtac (mk_disjIN n k) THEN'
+      REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN' rtac refl THEN'
+      EVERY' (map2 (fn k' => fn distincts =>
+        (if k' < n then etac disjE else K all_tac) THEN'
+        (if k' = k then mk_case_same_ctr_tac ctxt injects
+         else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
+  end;
+
 fun mk_case_conv_tac ctxt n uexhaust cases discss' selss =
   HEADGOAL (rtac uexhaust THEN'
     EVERY' (map3 (fn casex => fn if_discs => fn sels =>