# HG changeset patch
# User blanchet
# Date 1348101768 -7200
# Node ID 3cd2622d44664e8ad0a05d76f2f1b9f611bcb0a4
# Parent  cca4390e8071bc32d53ef9342a8e2584890b363d
don't define relators unless necessary

diff -r cca4390e8071 -r 3cd2622d4466 src/HOL/Codatatype/Basic_BNFs.thy
--- a/src/HOL/Codatatype/Basic_BNFs.thy	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Basic_BNFs.thy	Thu Sep 20 02:42:48 2012 +0200
@@ -25,7 +25,7 @@
 unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
 
 bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
-  "\<lambda>x :: ('a \<times> 'b) set. x"
+  "id :: ('a \<times> 'b) set \<Rightarrow> ('a \<times> 'b) set"
 apply auto
 apply (rule natLeq_card_order)
 apply (rule natLeq_cinfinite)
@@ -51,7 +51,10 @@
 apply (auto simp: Gr_def fun_eq_iff)
 done
 
-bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] Id
+definition DEADID_rel :: "('a \<times> 'a) set" where
+"DEADID_rel = {p. \<exists>x. p = (x, x)}"
+
+bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] DEADID_rel
 apply (auto simp add: wpull_id)
 apply (rule card_order_csum)
 apply (rule natLeq_card_order)
@@ -68,7 +71,7 @@
 apply (rule card_of_Card_order)
 apply (rule ctwo_Cnotzero)
 apply (rule card_of_Card_order)
-apply (auto simp: Id_def Gr_def fun_eq_iff)
+apply (auto simp: DEADID_rel_def Id_def Gr_def fun_eq_iff)
 done
 
 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
@@ -79,14 +82,13 @@
 
 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
 
-(*### RENAME TODO *)
-definition sum_rel0 :: "('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> (('a + 'c) \<times> ('b + 'd)) set" where
-"sum_rel0 R S =
+definition sum_rel :: "('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> (('a + 'c) \<times> ('b + 'd)) set" where
+"sum_rel R S =
    {x. case x of (Inl a, Inl c) \<Rightarrow> (a, c) \<in> R
        | (Inr b, Inr d) \<Rightarrow> (b, d) \<in> S
        | _ \<Rightarrow> False}"
 
-bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel0
+bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
 proof -
   show "sum_map id id = id" by (rule sum_map.id)
 next
@@ -197,10 +199,10 @@
   qed
 next
   fix R S
-  show "sum_rel0 R S =
+  show "sum_rel R S =
           (Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map fst fst))\<inverse> O
           Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map snd snd)"
-  unfolding setl_def setr_def sum_rel0_def Gr_def relcomp_unfold converse_unfold
+  unfolding setl_def setr_def sum_rel_def Gr_def relcomp_unfold converse_unfold
   by (fastforce split: sum.splits)
 qed (auto simp: sum_set_defs)
 
@@ -222,10 +224,10 @@
 
 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
 
-definition prod_rel0 :: "('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> (('a \<times> 'c) \<times> 'b \<times> 'd) set" where
-"prod_rel0 R S = {((a, c), b, d) | a b c d. (a, b) \<in> R \<and> (c, d) \<in> S}"
+definition prod_rel :: "('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> (('a \<times> 'c) \<times> 'b \<times> 'd) set" where
+"prod_rel R S = {((a, c), b, d) | a b c d. (a, b) \<in> R \<and> (c, d) \<in> S}"
 
-bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel0
+bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel
 proof (unfold prod_set_defs)
   show "map_pair id id = id" by (rule map_pair.id)
 next
@@ -302,10 +304,10 @@
     unfolding wpull_def by simp fast
 next
   fix R S
-  show "prod_rel0 R S =
+  show "prod_rel R S =
           (Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair fst fst))\<inverse> O
           Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair snd snd)"
-  unfolding prod_set_defs prod_rel0_def Gr_def relcomp_unfold converse_unfold
+  unfolding prod_set_defs prod_rel_def Gr_def relcomp_unfold converse_unfold
   by auto
 qed simp+
 
@@ -345,11 +347,11 @@
   ultimately show ?thesis using card_of_ordLeq by fast
 qed
 
-definition fun_rel0 :: "('a \<times> 'b) set \<Rightarrow> (('c \<Rightarrow> 'a) \<times> ('c \<Rightarrow> 'b)) set" where
-"fun_rel0 R = {(f, g) | f g. \<forall>x. (f x, g x) \<in> R}"
+definition fun_rel :: "('a \<times> 'b) set \<Rightarrow> (('c \<Rightarrow> 'a) \<times> ('c \<Rightarrow> 'b)) set" where
+"fun_rel R = {(f, g) | f g. \<forall>x. (f x, g x) \<in> R}"
 
 bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
-  fun_rel0
+  fun_rel
 proof
   fix f show "id \<circ> f = id f" by simp
 next
@@ -408,9 +410,8 @@
     using wpull_cat[OF p c r] by simp metis
   qed
 next
-  fix R
-  show "fun_rel0 R = (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)"
-  unfolding fun_rel0_def Gr_def relcomp_unfold converse_unfold
+  fix R show "fun_rel R = (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)"
+  unfolding fun_rel_def Gr_def relcomp_unfold converse_unfold
   by (auto intro!: exI dest!: in_mono)
 qed auto
 
diff -r cca4390e8071 -r 3cd2622d4466 src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -257,7 +257,7 @@
 
     val (bnf', lthy') =
       bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
-        ((((b, mapx), sets), bd), wits) lthy;
+        (((((b, mapx), sets), bd), wits), rel) lthy;
 
     val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
     val outer_rel_cong = rel_cong_of_bnf outer;
diff -r cca4390e8071 -r 3cd2622d4466 src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -607,7 +607,7 @@
         ||>> apfst split_list o fold_map (maybe_define false) set_binds_defs
         ||>> maybe_define false bd_bind_def
         ||>> apfst split_list o fold_map (maybe_define false) wit_binds_defs
-        ||>> maybe_define true(*###*) rel_bind_def
+        ||>> maybe_define false rel_bind_def
         ||> `(maybe_restore no_defs_lthy);
 
     (*transforms defined frees into consts (and more)*)