# HG changeset patch
# User blanchet
# Date 1394109410 -3600
# Node ID 800e155d051a115ef947af20634b20f27a8e248a
# Parent  12ee2c407dadb48eb787192b3efa9f00d48a04b0
renamed 'cset_rel' to 'rel_cset'

diff -r 12ee2c407dad -r 800e155d051a NEWS
--- a/NEWS	Thu Mar 06 13:36:49 2014 +0100
+++ b/NEWS	Thu Mar 06 13:36:50 2014 +0100
@@ -194,6 +194,7 @@
     map_sum ~> sum_map
     map_pair ~> prod_map
     fset_rel ~> rel_fset
+    cset_rel ~> rel_cset
 
 * New theory:
     Cardinals/Ordinal_Arithmetic.thy
diff -r 12ee2c407dad -r 800e155d051a src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Thu Mar 06 13:36:49 2014 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy	Thu Mar 06 13:36:50 2014 +0100
@@ -124,12 +124,12 @@
 "{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
 by auto
 
-definition cset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
-"cset_rel R a b \<longleftrightarrow>
+definition rel_cset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
+"rel_cset R a b \<longleftrightarrow>
  (\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>
  (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)"
 
-lemma cset_rel_aux:
+lemma rel_cset_aux:
 "(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t) \<longleftrightarrow>
  ((Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage fst))\<inverse>\<inverse> OO
           Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R")
@@ -155,7 +155,7 @@
   sets: rcset
   bd: natLeq
   wits: "cempty"
-  rel: cset_rel
+  rel: rel_cset
 proof -
   show "cimage id = id" by transfer' simp
 next
@@ -173,14 +173,14 @@
   fix C show "|rcset C| \<le>o natLeq" by transfer (unfold countable_card_le_natLeq)
 next
   fix R S
-  show "cset_rel R OO cset_rel S \<le> cset_rel (R OO S)"
-    unfolding cset_rel_def[abs_def] by fast
+  show "rel_cset R OO rel_cset S \<le> rel_cset (R OO S)"
+    unfolding rel_cset_def[abs_def] by fast
 next
   fix R
-  show "cset_rel R =
+  show "rel_cset R =
         (Grp {x. rcset x \<subseteq> Collect (split R)} (cimage fst))\<inverse>\<inverse> OO
          Grp {x. rcset x \<subseteq> Collect (split R)} (cimage snd)"
-  unfolding cset_rel_def[abs_def] cset_rel_aux by simp
+  unfolding rel_cset_def[abs_def] rel_cset_aux by simp
 qed (transfer, simp)
 
 end