# HG changeset patch
# User blanchet
# Date 1403106144 -7200
# Node ID 88263522c31eab189ebfa3e4a31ee40317112ef6
# Parent  8f7d6f01a77588f588208edf020693d893442efb
made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'

diff -r 8f7d6f01a775 -r 88263522c31e src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Wed Jun 18 17:42:24 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy	Wed Jun 18 17:42:24 2014 +0200
@@ -71,9 +71,6 @@
 "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
 by simp
 
-lemma Inl_Inr_False: "(Inl x = Inr y) = False"
-by simp
-
 lemma prod_set_simps:
 "fsts (x, y) = {x}"
 "snds (x, y) = {y}"
diff -r 8f7d6f01a775 -r 88263522c31e src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jun 18 17:42:24 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jun 18 17:42:24 2014 +0200
@@ -1358,7 +1358,7 @@
                 fold_thms lthy ctr_defs'
                   (unfold_thms lthy (pre_rel_def :: abs_inverse ::
                        (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
-                       @{thms vimage2p_def sum.inject Inl_Inr_False})
+                       @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
                      (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
                 |> postproc
                 |> singleton (Proof_Context.export names_lthy no_defs_lthy);
diff -r 8f7d6f01a775 -r 88263522c31e src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed Jun 18 17:42:24 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed Jun 18 17:42:24 2014 +0200
@@ -138,7 +138,8 @@
     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
-       sum.case} @ mapsx @ map_comps @ map_idents))) ORELSE'
+         sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
+       mapsx @ map_comps @ map_idents))) ORELSE'
     fo_rtac @{thm cong} ctxt ORELSE'
     rtac @{thm ext}));