renamed 'cset_rel' to 'rel_cset'
authorblanchet
Thu Mar 06 13:36:50 2014 +0100 (2014-03-06)
changeset 55934800e155d051a
parent 55933 12ee2c407dad
child 55935 8f20d09d294e
renamed 'cset_rel' to 'rel_cset'
NEWS
src/HOL/Library/Countable_Set_Type.thy
     1.1 --- a/NEWS	Thu Mar 06 13:36:49 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 06 13:36:50 2014 +0100
     1.3 @@ -194,6 +194,7 @@
     1.4      map_sum ~> sum_map
     1.5      map_pair ~> prod_map
     1.6      fset_rel ~> rel_fset
     1.7 +    cset_rel ~> rel_cset
     1.8  
     1.9  * New theory:
    1.10      Cardinals/Ordinal_Arithmetic.thy
     2.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Thu Mar 06 13:36:49 2014 +0100
     2.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Thu Mar 06 13:36:50 2014 +0100
     2.3 @@ -124,12 +124,12 @@
     2.4  "{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
     2.5  by auto
     2.6  
     2.7 -definition cset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
     2.8 -"cset_rel R a b \<longleftrightarrow>
     2.9 +definition rel_cset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
    2.10 +"rel_cset R a b \<longleftrightarrow>
    2.11   (\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>
    2.12   (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)"
    2.13  
    2.14 -lemma cset_rel_aux:
    2.15 +lemma rel_cset_aux:
    2.16  "(\<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>
    2.17   ((Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage fst))\<inverse>\<inverse> OO
    2.18            Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R")
    2.19 @@ -155,7 +155,7 @@
    2.20    sets: rcset
    2.21    bd: natLeq
    2.22    wits: "cempty"
    2.23 -  rel: cset_rel
    2.24 +  rel: rel_cset
    2.25  proof -
    2.26    show "cimage id = id" by transfer' simp
    2.27  next
    2.28 @@ -173,14 +173,14 @@
    2.29    fix C show "|rcset C| \<le>o natLeq" by transfer (unfold countable_card_le_natLeq)
    2.30  next
    2.31    fix R S
    2.32 -  show "cset_rel R OO cset_rel S \<le> cset_rel (R OO S)"
    2.33 -    unfolding cset_rel_def[abs_def] by fast
    2.34 +  show "rel_cset R OO rel_cset S \<le> rel_cset (R OO S)"
    2.35 +    unfolding rel_cset_def[abs_def] by fast
    2.36  next
    2.37    fix R
    2.38 -  show "cset_rel R =
    2.39 +  show "rel_cset R =
    2.40          (Grp {x. rcset x \<subseteq> Collect (split R)} (cimage fst))\<inverse>\<inverse> OO
    2.41           Grp {x. rcset x \<subseteq> Collect (split R)} (cimage snd)"
    2.42 -  unfolding cset_rel_def[abs_def] cset_rel_aux by simp
    2.43 +  unfolding rel_cset_def[abs_def] rel_cset_aux by simp
    2.44  qed (transfer, simp)
    2.45  
    2.46  end