# 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}));