merged

--- a/src/HOL/BNF/BNF_FP.thy	Fri Sep 28 16:59:53 2012 +0200
+++ b/src/HOL/BNF/BNF_FP.thy	Fri Sep 28 17:06:07 2012 +0200
@@ -120,6 +120,17 @@
 "setr (Inr x) = {x}"
 unfolding sum_set_defs by simp+
 
+lemma prod_rel_simp:
+"prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'"
+unfolding prod_rel_def by simp
+
+lemma sum_rel_simps:
+"sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'"
+"sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'"
+"sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False"
+"sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False"
+unfolding sum_rel_def by simp+
+
 ML_file "Tools/bnf_fp.ML"
 ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/bnf_fp_def_sugar.ML"

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Sep 28 16:59:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Sep 28 17:06:07 2012 +0200
@@ -42,9 +42,7 @@
       Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
       mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
 val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0;
-val sum_prod_thms_rel =
-  @{thms prod.cases prod_rel_def sum.cases sum_rel_def
-      sum.inject sum.distinct[THEN eq_False[THEN iffD2]]};
+val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps};
 
 val ss_if_True_False = ss_only @{thms if_True if_False};
 
@@ -146,6 +144,7 @@
 fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
   hyp_subst_tac THEN'
   subst_tac ctxt (SOME [1, 2]) [ctr_def] THEN'
+  SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
   SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels @ sum_prod_thms_rel)) THEN'
   (atac ORELSE' REPEAT o etac conjE THEN'
      full_simp_tac