# HG changeset patch
# User blanchet
# Date 1346768847 -7200
# Node ID f7326a0d7f194a4c7f739170dd7772c85065d2ff
# Parent  1bbd7a37fc2955dd18adbc32bedccd1c6c11828b
implemented "mk_half_distinct_tac"

diff -r 1bbd7a37fc29 -r f7326a0d7f19 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 16:17:22 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 16:27:27 2012 +0200
@@ -185,11 +185,13 @@
                      mk_inject_tac ctxt ctr_def fld_inject])
             ms ctr_defs;
 
+        val half_distinct_tacss =
+          map (map (fn (def, def') => fn {context = ctxt, ...} =>
+            mk_half_distinct_tac ctxt fld_inject [def, def'])) (mk_half_pairss ctr_defs);
+
         (*###*)
         fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
 
-        val half_distinct_tacss = map (map (K cheat_tac)) (mk_half_pairss ks);
-
         val case_tacs = map (K cheat_tac) ks;
 
         val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
diff -r 1bbd7a37fc29 -r f7326a0d7f19 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 16:17:22 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 16:27:27 2012 +0200
@@ -10,6 +10,7 @@
   val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
   val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     -> tactic
+  val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
   val mk_inject_tac: Proof.context -> thm -> thm -> tactic
 end;
 
@@ -34,6 +35,10 @@
      SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
      atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
 
+fun mk_half_distinct_tac ctxt fld_inject ctr_defs =
+  Local_Defs.unfold_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN
+  rtac @{thm sum.distinct(1)} 1;
+
 fun mk_inject_tac ctxt ctr_def fld_inject =
   Local_Defs.unfold_tac ctxt [ctr_def] THEN
   rtac (fld_inject RS ssubst) 1 THEN