# HG changeset patch
# User blanchet
# Date 1348838051 -7200
# Node ID 9f884142334cba0fbfd6a9011ec730a07a67319a
# Parent  9b831f93d4e8e32e4ce25102c7ab2f55dcaa2810
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"

diff -r 9b831f93d4e8 -r 9f884142334c src/HOL/BNF/BNF_FP.thy
--- a/src/HOL/BNF/BNF_FP.thy	Fri Sep 28 13:16:10 2012 +0200
+++ b/src/HOL/BNF/BNF_FP.thy	Fri Sep 28 15:14:11 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"
diff -r 9b831f93d4e8 -r 9f884142334c src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Sep 28 13:16:10 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Sep 28 15:14:11 2012 +0200
@@ -42,8 +42,9 @@
       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;
+(* FIXME: Need "prod.cases" and "sum.cases"? And why "sum.inject" but no "prod.inject"? *)
 val sum_prod_thms_rel =
-  @{thms prod.cases prod_rel_def sum.cases sum_rel_def
+  @{thms prod.cases prod_rel_simp sum.cases sum_rel_simps
       sum.inject sum.distinct[THEN eq_False[THEN iffD2]]};
 
 val ss_if_True_False = ss_only @{thms if_True if_False};
@@ -146,6 +147,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