renamed 'set_rel' to 'rel_set'
authorblanchet
Thu Mar 06 14:57:14 2014 +0100 (2014-03-06)
changeset 55938f20d1db5aa3c
parent 55937 18e52e8c6300
child 55939 682fc100dbff
renamed 'set_rel' to 'rel_set'
NEWS
src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Mapping.thy
src/HOL/Lifting_Set.thy
src/HOL/List.thy
src/HOL/Topological_Spaces.thy
src/HOL/ex/Transfer_Int_Nat.thy
     1.1 --- a/NEWS	Thu Mar 06 14:25:55 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 06 14:57:14 2014 +0100
     1.3 @@ -195,6 +195,7 @@
     1.4      map_pair ~> prod_map
     1.5      fset_rel ~> rel_fset
     1.6      cset_rel ~> rel_cset
     1.7 +    set_rel ~> rel_set
     1.8  
     1.9  * New theory:
    1.10      Cardinals/Ordinal_Arithmetic.thy
     2.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 14:25:55 2014 +0100
     2.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 14:57:14 2014 +0100
     2.3 @@ -60,17 +60,17 @@
     2.4  shows "tr = tr'"
     2.5  by (metis Node_root_cont assms)
     2.6  
     2.7 -lemma set_rel_cont:
     2.8 -"set_rel \<chi> (cont tr1) (cont tr2) = rel_fset \<chi> (ccont tr1) (ccont tr2)"
     2.9 +lemma rel_set_cont:
    2.10 +"rel_set \<chi> (cont tr1) (cont tr2) = rel_fset \<chi> (ccont tr1) (ccont tr2)"
    2.11  unfolding cont_def comp_def rel_fset_fset ..
    2.12  
    2.13  lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]:
    2.14  assumes phi: "\<phi> tr1 tr2" and
    2.15  Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
    2.16 -                  root tr1 = root tr2 \<and> set_rel (sum_rel op = \<phi>) (cont tr1) (cont tr2)"
    2.17 +                  root tr1 = root tr2 \<and> rel_set (sum_rel op = \<phi>) (cont tr1) (cont tr2)"
    2.18  shows "tr1 = tr2"
    2.19  using phi apply(elim dtree.coinduct)
    2.20 -apply(rule Lift[unfolded set_rel_cont]) .
    2.21 +apply(rule Lift[unfolded rel_set_cont]) .
    2.22  
    2.23  lemma unfold:
    2.24  "root (unfold rt ct b) = rt b"
     3.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy	Thu Mar 06 14:25:55 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy	Thu Mar 06 14:57:14 2014 +0100
     3.3 @@ -67,10 +67,10 @@
     3.4  
     3.5  subsection{* Structural Coinduction Proofs *}
     3.6  
     3.7 -lemma set_rel_sum_rel_eq[simp]:
     3.8 -"set_rel (sum_rel (op =) \<phi>) A1 A2 \<longleftrightarrow>
     3.9 - Inl -` A1 = Inl -` A2 \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
    3.10 -unfolding set_rel_sum_rel set_rel_eq ..
    3.11 +lemma rel_set_sum_rel_eq[simp]:
    3.12 +"rel_set (sum_rel (op =) \<phi>) A1 A2 \<longleftrightarrow>
    3.13 + Inl -` A1 = Inl -` A2 \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
    3.14 +unfolding rel_set_sum_rel rel_set_eq ..
    3.15  
    3.16  (* Detailed proofs of commutativity and associativity: *)
    3.17  theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1"
    3.18 @@ -79,7 +79,7 @@
    3.19    {fix trA trB
    3.20     assume "?\<theta> trA trB" hence "trA = trB"
    3.21     apply (induct rule: dtree_coinduct)
    3.22 -   unfolding set_rel_sum_rel set_rel_eq unfolding set_rel_def proof safe
    3.23 +   unfolding rel_set_sum_rel rel_set_eq unfolding rel_set_def proof safe
    3.24       fix tr1 tr2  show "root (tr1 \<parallel> tr2) = root (tr2 \<parallel> tr1)"
    3.25       unfolding root_par by (rule Nplus_comm)
    3.26     next
    3.27 @@ -114,7 +114,7 @@
    3.28    {fix trA trB
    3.29     assume "?\<theta> trA trB" hence "trA = trB"
    3.30     apply (induct rule: dtree_coinduct)
    3.31 -   unfolding set_rel_sum_rel set_rel_eq unfolding set_rel_def proof safe
    3.32 +   unfolding rel_set_sum_rel rel_set_eq unfolding rel_set_def proof safe
    3.33       fix tr1 tr2 tr3  show "root ((tr1 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))"
    3.34       unfolding root_par by (rule Nplus_assoc)
    3.35     next
     4.1 --- a/src/HOL/Library/FSet.thy	Thu Mar 06 14:25:55 2014 +0100
     4.2 +++ b/src/HOL/Library/FSet.thy	Thu Mar 06 14:57:14 2014 +0100
     4.3 @@ -78,14 +78,14 @@
     4.4  
     4.5  lemma right_total_Inf_fset_transfer:
     4.6    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
     4.7 -  shows "(set_rel (set_rel A) ===> set_rel A) 
     4.8 +  shows "(rel_set (rel_set A) ===> rel_set A) 
     4.9      (\<lambda>S. if finite (Inter S \<inter> Collect (Domainp A)) then Inter S \<inter> Collect (Domainp A) else {}) 
    4.10        (\<lambda>S. if finite (Inf S) then Inf S else {})"
    4.11      by transfer_prover
    4.12  
    4.13  lemma Inf_fset_transfer:
    4.14    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
    4.15 -  shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>A. if finite (Inf A) then Inf A else {}) 
    4.16 +  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Inf A) then Inf A else {}) 
    4.17      (\<lambda>A. if finite (Inf A) then Inf A else {})"
    4.18    by transfer_prover
    4.19  
    4.20 @@ -94,7 +94,7 @@
    4.21  
    4.22  lemma Sup_fset_transfer:
    4.23    assumes [transfer_rule]: "bi_unique A"
    4.24 -  shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>A. if finite (Sup A) then Sup A else {})
    4.25 +  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Sup A) then Sup A else {})
    4.26    (\<lambda>A. if finite (Sup A) then Sup A else {})" by transfer_prover
    4.27  
    4.28  lift_definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Sup A) then Sup A else {}"
    4.29 @@ -103,7 +103,7 @@
    4.30  lemma finite_Sup: "\<exists>z. finite z \<and> (\<forall>a. a \<in> X \<longrightarrow> a \<le> z) \<Longrightarrow> finite (Sup X)"
    4.31  by (auto intro: finite_subset)
    4.32  
    4.33 -lemma transfer_bdd_below[transfer_rule]: "(set_rel (pcr_fset op =) ===> op =) bdd_below bdd_below"
    4.34 +lemma transfer_bdd_below[transfer_rule]: "(rel_set (pcr_fset op =) ===> op =) bdd_below bdd_below"
    4.35    by auto
    4.36  
    4.37  instance
    4.38 @@ -762,53 +762,53 @@
    4.39  
    4.40  subsubsection {* Relator and predicator properties *}
    4.41  
    4.42 -lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is set_rel
    4.43 -parametric set_rel_transfer .
    4.44 +lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is rel_set
    4.45 +parametric rel_set_transfer .
    4.46  
    4.47  lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y) 
    4.48    \<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
    4.49  apply (rule ext)+
    4.50  apply transfer'
    4.51 -apply (subst set_rel_def[unfolded fun_eq_iff]) 
    4.52 +apply (subst rel_set_def[unfolded fun_eq_iff]) 
    4.53  by blast
    4.54  
    4.55  lemma rel_fset_conversep: "rel_fset (conversep R) = conversep (rel_fset R)"
    4.56    unfolding rel_fset_alt_def by auto
    4.57  
    4.58 -lemmas rel_fset_eq [relator_eq] = set_rel_eq[Transfer.transferred]
    4.59 +lemmas rel_fset_eq [relator_eq] = rel_set_eq[Transfer.transferred]
    4.60  
    4.61  lemma rel_fset_mono[relator_mono]: "A \<le> B \<Longrightarrow> rel_fset A \<le> rel_fset B"
    4.62  unfolding rel_fset_alt_def by blast
    4.63  
    4.64 -lemma finite_set_rel:
    4.65 +lemma finite_rel_set:
    4.66    assumes fin: "finite X" "finite Z"
    4.67 -  assumes R_S: "set_rel (R OO S) X Z"
    4.68 -  shows "\<exists>Y. finite Y \<and> set_rel R X Y \<and> set_rel S Y Z"
    4.69 +  assumes R_S: "rel_set (R OO S) X Z"
    4.70 +  shows "\<exists>Y. finite Y \<and> rel_set R X Y \<and> rel_set S Y Z"
    4.71  proof -
    4.72    obtain f where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)"
    4.73    apply atomize_elim
    4.74    apply (subst bchoice_iff[symmetric])
    4.75 -  using R_S[unfolded set_rel_def OO_def] by blast
    4.76 +  using R_S[unfolded rel_set_def OO_def] by blast
    4.77    
    4.78    obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R  x (g z))"
    4.79    apply atomize_elim
    4.80    apply (subst bchoice_iff[symmetric])
    4.81 -  using R_S[unfolded set_rel_def OO_def] by blast
    4.82 +  using R_S[unfolded rel_set_def OO_def] by blast
    4.83    
    4.84    let ?Y = "f ` X \<union> g ` Z"
    4.85    have "finite ?Y" by (simp add: fin)
    4.86 -  moreover have "set_rel R X ?Y"
    4.87 -    unfolding set_rel_def
    4.88 +  moreover have "rel_set R X ?Y"
    4.89 +    unfolding rel_set_def
    4.90      using f g by clarsimp blast
    4.91 -  moreover have "set_rel S ?Y Z"
    4.92 -    unfolding set_rel_def
    4.93 +  moreover have "rel_set S ?Y Z"
    4.94 +    unfolding rel_set_def
    4.95      using f g by clarsimp blast
    4.96    ultimately show ?thesis by metis
    4.97  qed
    4.98  
    4.99  lemma rel_fset_OO[relator_distr]: "rel_fset R OO rel_fset S = rel_fset (R OO S)"
   4.100  apply (rule ext)+
   4.101 -by transfer (auto intro: finite_set_rel set_rel_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
   4.102 +by transfer (auto intro: finite_rel_set rel_set_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
   4.103  
   4.104  lemma Domainp_fset[relator_domain]:
   4.105    assumes "Domainp T = P"
   4.106 @@ -832,7 +832,7 @@
   4.107  apply (subst(asm) choice_iff)
   4.108  apply clarsimp
   4.109  apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
   4.110 -by (auto simp add: set_rel_def)
   4.111 +by (auto simp add: rel_set_def)
   4.112  
   4.113  lemma left_total_rel_fset[reflexivity_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
   4.114  unfolding left_total_def 
   4.115 @@ -840,10 +840,10 @@
   4.116  apply (subst(asm) choice_iff)
   4.117  apply clarsimp
   4.118  apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
   4.119 -by (auto simp add: set_rel_def)
   4.120 +by (auto simp add: rel_set_def)
   4.121  
   4.122 -lemmas right_unique_rel_fset[transfer_rule] = right_unique_set_rel[Transfer.transferred]
   4.123 -lemmas left_unique_rel_fset[reflexivity_rule] = left_unique_set_rel[Transfer.transferred]
   4.124 +lemmas right_unique_rel_fset[transfer_rule] = right_unique_rel_set[Transfer.transferred]
   4.125 +lemmas left_unique_rel_fset[reflexivity_rule] = left_unique_rel_set[Transfer.transferred]
   4.126  
   4.127  thm right_unique_rel_fset left_unique_rel_fset
   4.128  
   4.129 @@ -911,7 +911,7 @@
   4.130    "((A ===> B ===> op =) ===> rel_fset A ===> rel_fset B ===> op =)
   4.131      rel_fset rel_fset"
   4.132    unfolding fun_rel_def
   4.133 -  using set_rel_transfer[unfolded fun_rel_def,rule_format, Transfer.transferred, where A = A and B = B]
   4.134 +  using rel_set_transfer[unfolded fun_rel_def,rule_format, Transfer.transferred, where A = A and B = B]
   4.135    by simp
   4.136  
   4.137  lemma bind_transfer [transfer_rule]:
   4.138 @@ -945,7 +945,7 @@
   4.139    using subset_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   4.140  
   4.141  lemma fSup_transfer [transfer_rule]:
   4.142 -  "bi_unique A \<Longrightarrow> (set_rel (rel_fset A) ===> rel_fset A) Sup Sup"
   4.143 +  "bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup"
   4.144    using assms unfolding fun_rel_def
   4.145    apply clarify
   4.146    apply transfer'
   4.147 @@ -955,7 +955,7 @@
   4.148  
   4.149  lemma fInf_transfer [transfer_rule]:
   4.150    assumes "bi_unique A" and "bi_total A"
   4.151 -  shows "(set_rel (rel_fset A) ===> rel_fset A) Inf Inf"
   4.152 +  shows "(rel_set (rel_fset A) ===> rel_fset A) Inf Inf"
   4.153    using assms unfolding fun_rel_def
   4.154    apply clarify
   4.155    apply transfer'
   4.156 @@ -986,7 +986,7 @@
   4.157  
   4.158  lemma rel_fset_alt:
   4.159    "rel_fset R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
   4.160 -by transfer (simp add: set_rel_def)
   4.161 +by transfer (simp add: rel_set_def)
   4.162  
   4.163  lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
   4.164  apply (rule f_the_inv_into_f[unfolded inj_on_def])
   4.165 @@ -1037,7 +1037,7 @@
   4.166  apply transfer apply simp
   4.167  done
   4.168  
   4.169 -lemma rel_fset_fset: "set_rel \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2"
   4.170 +lemma rel_fset_fset: "rel_set \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2"
   4.171    by transfer (rule refl)
   4.172  
   4.173  end
   4.174 @@ -1049,50 +1049,50 @@
   4.175  
   4.176  (* Set vs. sum relators: *)
   4.177  
   4.178 -lemma set_rel_sum_rel[simp]: 
   4.179 -"set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow> 
   4.180 - set_rel \<chi> (Inl -` A1) (Inl -` A2) \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
   4.181 +lemma rel_set_sum_rel[simp]: 
   4.182 +"rel_set (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow> 
   4.183 + rel_set \<chi> (Inl -` A1) (Inl -` A2) \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
   4.184  (is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
   4.185  proof safe
   4.186    assume L: "?L"
   4.187 -  show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe
   4.188 +  show ?Rl unfolding rel_set_def Bex_def vimage_eq proof safe
   4.189      fix l1 assume "Inl l1 \<in> A1"
   4.190      then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2"
   4.191 -    using L unfolding set_rel_def by auto
   4.192 +    using L unfolding rel_set_def by auto
   4.193      then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto)
   4.194      thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto
   4.195    next
   4.196      fix l2 assume "Inl l2 \<in> A2"
   4.197      then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)"
   4.198 -    using L unfolding set_rel_def by auto
   4.199 +    using L unfolding rel_set_def by auto
   4.200      then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto)
   4.201      thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto
   4.202    qed
   4.203 -  show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe
   4.204 +  show ?Rr unfolding rel_set_def Bex_def vimage_eq proof safe
   4.205      fix r1 assume "Inr r1 \<in> A1"
   4.206      then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2"
   4.207 -    using L unfolding set_rel_def by auto
   4.208 +    using L unfolding rel_set_def by auto
   4.209      then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto)
   4.210      thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto
   4.211    next
   4.212      fix r2 assume "Inr r2 \<in> A2"
   4.213      then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)"
   4.214 -    using L unfolding set_rel_def by auto
   4.215 +    using L unfolding rel_set_def by auto
   4.216      then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto)
   4.217      thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto
   4.218    qed
   4.219  next
   4.220    assume Rl: "?Rl" and Rr: "?Rr"
   4.221 -  show ?L unfolding set_rel_def Bex_def vimage_eq proof safe
   4.222 +  show ?L unfolding rel_set_def Bex_def vimage_eq proof safe
   4.223      fix a1 assume a1: "a1 \<in> A1"
   4.224      show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2"
   4.225      proof(cases a1)
   4.226        case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2"
   4.227 -      using Rl a1 unfolding set_rel_def by blast
   4.228 +      using Rl a1 unfolding rel_set_def by blast
   4.229        thus ?thesis unfolding Inl by auto
   4.230      next
   4.231        case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2"
   4.232 -      using Rr a1 unfolding set_rel_def by blast
   4.233 +      using Rr a1 unfolding rel_set_def by blast
   4.234        thus ?thesis unfolding Inr by auto
   4.235      qed
   4.236    next
   4.237 @@ -1100,11 +1100,11 @@
   4.238      show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2"
   4.239      proof(cases a2)
   4.240        case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2"
   4.241 -      using Rl a2 unfolding set_rel_def by blast
   4.242 +      using Rl a2 unfolding rel_set_def by blast
   4.243        thus ?thesis unfolding Inl by auto
   4.244      next
   4.245        case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2"
   4.246 -      using Rr a2 unfolding set_rel_def by blast
   4.247 +      using Rr a2 unfolding rel_set_def by blast
   4.248        thus ?thesis unfolding Inr by auto
   4.249      qed
   4.250    qed
     5.1 --- a/src/HOL/Library/Mapping.thy	Thu Mar 06 14:25:55 2014 +0100
     5.2 +++ b/src/HOL/Library/Mapping.thy	Thu Mar 06 14:57:14 2014 +0100
     5.3 @@ -37,7 +37,7 @@
     5.4  
     5.5  lemma dom_transfer:
     5.6    assumes [transfer_rule]: "bi_total A"
     5.7 -  shows "((A ===> rel_option B) ===> set_rel A) dom dom" 
     5.8 +  shows "((A ===> rel_option B) ===> rel_set A) dom dom" 
     5.9  unfolding dom_def[abs_def] equal_None_def[symmetric] 
    5.10  by transfer_prover
    5.11  
     6.1 --- a/src/HOL/Lifting_Set.thy	Thu Mar 06 14:25:55 2014 +0100
     6.2 +++ b/src/HOL/Lifting_Set.thy	Thu Mar 06 14:57:14 2014 +0100
     6.3 @@ -10,90 +10,90 @@
     6.4  
     6.5  subsection {* Relator and predicator properties *}
     6.6  
     6.7 -definition set_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
     6.8 -  where "set_rel R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))"
     6.9 +definition rel_set :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
    6.10 +  where "rel_set R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))"
    6.11  
    6.12 -lemma set_relI:
    6.13 +lemma rel_setI:
    6.14    assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y"
    6.15    assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y"
    6.16 -  shows "set_rel R A B"
    6.17 -  using assms unfolding set_rel_def by simp
    6.18 +  shows "rel_set R A B"
    6.19 +  using assms unfolding rel_set_def by simp
    6.20  
    6.21 -lemma set_relD1: "\<lbrakk> set_rel R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"
    6.22 -  and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
    6.23 -by(simp_all add: set_rel_def)
    6.24 +lemma rel_setD1: "\<lbrakk> rel_set R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"
    6.25 +  and rel_setD2: "\<lbrakk> rel_set R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
    6.26 +by(simp_all add: rel_set_def)
    6.27  
    6.28 -lemma set_rel_conversep [simp]: "set_rel A\<inverse>\<inverse> = (set_rel A)\<inverse>\<inverse>"
    6.29 -  unfolding set_rel_def by auto
    6.30 +lemma rel_set_conversep [simp]: "rel_set A\<inverse>\<inverse> = (rel_set A)\<inverse>\<inverse>"
    6.31 +  unfolding rel_set_def by auto
    6.32  
    6.33 -lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
    6.34 -  unfolding set_rel_def fun_eq_iff by auto
    6.35 +lemma rel_set_eq [relator_eq]: "rel_set (op =) = (op =)"
    6.36 +  unfolding rel_set_def fun_eq_iff by auto
    6.37  
    6.38 -lemma set_rel_mono[relator_mono]:
    6.39 +lemma rel_set_mono[relator_mono]:
    6.40    assumes "A \<le> B"
    6.41 -  shows "set_rel A \<le> set_rel B"
    6.42 -using assms unfolding set_rel_def by blast
    6.43 +  shows "rel_set A \<le> rel_set B"
    6.44 +using assms unfolding rel_set_def by blast
    6.45  
    6.46 -lemma set_rel_OO[relator_distr]: "set_rel R OO set_rel S = set_rel (R OO S)"
    6.47 +lemma rel_set_OO[relator_distr]: "rel_set R OO rel_set S = rel_set (R OO S)"
    6.48    apply (rule sym)
    6.49    apply (intro ext, rename_tac X Z)
    6.50    apply (rule iffI)
    6.51    apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI)
    6.52 -  apply (simp add: set_rel_def, fast)
    6.53 -  apply (simp add: set_rel_def, fast)
    6.54 -  apply (simp add: set_rel_def, fast)
    6.55 +  apply (simp add: rel_set_def, fast)
    6.56 +  apply (simp add: rel_set_def, fast)
    6.57 +  apply (simp add: rel_set_def, fast)
    6.58    done
    6.59  
    6.60  lemma Domainp_set[relator_domain]:
    6.61    assumes "Domainp T = R"
    6.62 -  shows "Domainp (set_rel T) = (\<lambda>A. Ball A R)"
    6.63 -using assms unfolding set_rel_def Domainp_iff[abs_def]
    6.64 +  shows "Domainp (rel_set T) = (\<lambda>A. Ball A R)"
    6.65 +using assms unfolding rel_set_def Domainp_iff[abs_def]
    6.66  apply (intro ext)
    6.67  apply (rule iffI) 
    6.68  apply blast
    6.69  apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
    6.70  done
    6.71  
    6.72 -lemma left_total_set_rel[reflexivity_rule]: 
    6.73 -  "left_total A \<Longrightarrow> left_total (set_rel A)"
    6.74 -  unfolding left_total_def set_rel_def
    6.75 +lemma left_total_rel_set[reflexivity_rule]: 
    6.76 +  "left_total A \<Longrightarrow> left_total (rel_set A)"
    6.77 +  unfolding left_total_def rel_set_def
    6.78    apply safe
    6.79    apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
    6.80  done
    6.81  
    6.82 -lemma left_unique_set_rel[reflexivity_rule]: 
    6.83 -  "left_unique A \<Longrightarrow> left_unique (set_rel A)"
    6.84 -  unfolding left_unique_def set_rel_def
    6.85 +lemma left_unique_rel_set[reflexivity_rule]: 
    6.86 +  "left_unique A \<Longrightarrow> left_unique (rel_set A)"
    6.87 +  unfolding left_unique_def rel_set_def
    6.88    by fast
    6.89  
    6.90 -lemma right_total_set_rel [transfer_rule]:
    6.91 -  "right_total A \<Longrightarrow> right_total (set_rel A)"
    6.92 -using left_total_set_rel[of "A\<inverse>\<inverse>"] by simp
    6.93 +lemma right_total_rel_set [transfer_rule]:
    6.94 +  "right_total A \<Longrightarrow> right_total (rel_set A)"
    6.95 +using left_total_rel_set[of "A\<inverse>\<inverse>"] by simp
    6.96  
    6.97 -lemma right_unique_set_rel [transfer_rule]:
    6.98 -  "right_unique A \<Longrightarrow> right_unique (set_rel A)"
    6.99 -  unfolding right_unique_def set_rel_def by fast
   6.100 +lemma right_unique_rel_set [transfer_rule]:
   6.101 +  "right_unique A \<Longrightarrow> right_unique (rel_set A)"
   6.102 +  unfolding right_unique_def rel_set_def by fast
   6.103  
   6.104 -lemma bi_total_set_rel [transfer_rule]:
   6.105 -  "bi_total A \<Longrightarrow> bi_total (set_rel A)"
   6.106 -by(simp add: bi_total_conv_left_right left_total_set_rel right_total_set_rel)
   6.107 +lemma bi_total_rel_set [transfer_rule]:
   6.108 +  "bi_total A \<Longrightarrow> bi_total (rel_set A)"
   6.109 +by(simp add: bi_total_conv_left_right left_total_rel_set right_total_rel_set)
   6.110  
   6.111 -lemma bi_unique_set_rel [transfer_rule]:
   6.112 -  "bi_unique A \<Longrightarrow> bi_unique (set_rel A)"
   6.113 -  unfolding bi_unique_def set_rel_def by fast
   6.114 +lemma bi_unique_rel_set [transfer_rule]:
   6.115 +  "bi_unique A \<Longrightarrow> bi_unique (rel_set A)"
   6.116 +  unfolding bi_unique_def rel_set_def by fast
   6.117  
   6.118  lemma set_invariant_commute [invariant_commute]:
   6.119 -  "set_rel (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)"
   6.120 -  unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast
   6.121 +  "rel_set (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)"
   6.122 +  unfolding fun_eq_iff rel_set_def Lifting.invariant_def Ball_def by fast
   6.123  
   6.124  subsection {* Quotient theorem for the Lifting package *}
   6.125  
   6.126  lemma Quotient_set[quot_map]:
   6.127    assumes "Quotient R Abs Rep T"
   6.128 -  shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
   6.129 +  shows "Quotient (rel_set R) (image Abs) (image Rep) (rel_set T)"
   6.130    using assms unfolding Quotient_alt_def4
   6.131 -  apply (simp add: set_rel_OO[symmetric])
   6.132 -  apply (simp add: set_rel_def, fast)
   6.133 +  apply (simp add: rel_set_OO[symmetric])
   6.134 +  apply (simp add: rel_set_def, fast)
   6.135    done
   6.136  
   6.137  subsection {* Transfer rules for the Transfer package *}
   6.138 @@ -104,143 +104,143 @@
   6.139  begin
   6.140  interpretation lifting_syntax .
   6.141  
   6.142 -lemma empty_transfer [transfer_rule]: "(set_rel A) {} {}"
   6.143 -  unfolding set_rel_def by simp
   6.144 +lemma empty_transfer [transfer_rule]: "(rel_set A) {} {}"
   6.145 +  unfolding rel_set_def by simp
   6.146  
   6.147  lemma insert_transfer [transfer_rule]:
   6.148 -  "(A ===> set_rel A ===> set_rel A) insert insert"
   6.149 -  unfolding fun_rel_def set_rel_def by auto
   6.150 +  "(A ===> rel_set A ===> rel_set A) insert insert"
   6.151 +  unfolding fun_rel_def rel_set_def by auto
   6.152  
   6.153  lemma union_transfer [transfer_rule]:
   6.154 -  "(set_rel A ===> set_rel A ===> set_rel A) union union"
   6.155 -  unfolding fun_rel_def set_rel_def by auto
   6.156 +  "(rel_set A ===> rel_set A ===> rel_set A) union union"
   6.157 +  unfolding fun_rel_def rel_set_def by auto
   6.158  
   6.159  lemma Union_transfer [transfer_rule]:
   6.160 -  "(set_rel (set_rel A) ===> set_rel A) Union Union"
   6.161 -  unfolding fun_rel_def set_rel_def by simp fast
   6.162 +  "(rel_set (rel_set A) ===> rel_set A) Union Union"
   6.163 +  unfolding fun_rel_def rel_set_def by simp fast
   6.164  
   6.165  lemma image_transfer [transfer_rule]:
   6.166 -  "((A ===> B) ===> set_rel A ===> set_rel B) image image"
   6.167 -  unfolding fun_rel_def set_rel_def by simp fast
   6.168 +  "((A ===> B) ===> rel_set A ===> rel_set B) image image"
   6.169 +  unfolding fun_rel_def rel_set_def by simp fast
   6.170  
   6.171  lemma UNION_transfer [transfer_rule]:
   6.172 -  "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) UNION UNION"
   6.173 +  "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
   6.174    unfolding SUP_def [abs_def] by transfer_prover
   6.175  
   6.176  lemma Ball_transfer [transfer_rule]:
   6.177 -  "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball"
   6.178 -  unfolding set_rel_def fun_rel_def by fast
   6.179 +  "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
   6.180 +  unfolding rel_set_def fun_rel_def by fast
   6.181  
   6.182  lemma Bex_transfer [transfer_rule]:
   6.183 -  "(set_rel A ===> (A ===> op =) ===> op =) Bex Bex"
   6.184 -  unfolding set_rel_def fun_rel_def by fast
   6.185 +  "(rel_set A ===> (A ===> op =) ===> op =) Bex Bex"
   6.186 +  unfolding rel_set_def fun_rel_def by fast
   6.187  
   6.188  lemma Pow_transfer [transfer_rule]:
   6.189 -  "(set_rel A ===> set_rel (set_rel A)) Pow Pow"
   6.190 -  apply (rule fun_relI, rename_tac X Y, rule set_relI)
   6.191 +  "(rel_set A ===> rel_set (rel_set A)) Pow Pow"
   6.192 +  apply (rule fun_relI, rename_tac X Y, rule rel_setI)
   6.193    apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp)
   6.194 -  apply (simp add: set_rel_def, fast)
   6.195 +  apply (simp add: rel_set_def, fast)
   6.196    apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp)
   6.197 -  apply (simp add: set_rel_def, fast)
   6.198 +  apply (simp add: rel_set_def, fast)
   6.199    done
   6.200  
   6.201 -lemma set_rel_transfer [transfer_rule]:
   6.202 -  "((A ===> B ===> op =) ===> set_rel A ===> set_rel B ===> op =)
   6.203 -    set_rel set_rel"
   6.204 -  unfolding fun_rel_def set_rel_def by fast
   6.205 +lemma rel_set_transfer [transfer_rule]:
   6.206 +  "((A ===> B ===> op =) ===> rel_set A ===> rel_set B ===> op =)
   6.207 +    rel_set rel_set"
   6.208 +  unfolding fun_rel_def rel_set_def by fast
   6.209  
   6.210  lemma SUPR_parametric [transfer_rule]:
   6.211 -  "(set_rel R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
   6.212 +  "(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
   6.213  proof(rule fun_relI)+
   6.214    fix A B f and g :: "'b \<Rightarrow> 'c"
   6.215 -  assume AB: "set_rel R A B"
   6.216 +  assume AB: "rel_set R A B"
   6.217      and fg: "(R ===> op =) f g"
   6.218    show "SUPR A f = SUPR B g"
   6.219 -    by(rule SUPR_eq)(auto 4 4 dest: set_relD1[OF AB] set_relD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
   6.220 +    by(rule SUPR_eq)(auto 4 4 dest: rel_setD1[OF AB] rel_setD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
   6.221  qed
   6.222  
   6.223  lemma bind_transfer [transfer_rule]:
   6.224 -  "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) Set.bind Set.bind"
   6.225 +  "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) Set.bind Set.bind"
   6.226  unfolding bind_UNION[abs_def] by transfer_prover
   6.227  
   6.228  subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
   6.229  
   6.230  lemma member_transfer [transfer_rule]:
   6.231    assumes "bi_unique A"
   6.232 -  shows "(A ===> set_rel A ===> op =) (op \<in>) (op \<in>)"
   6.233 -  using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
   6.234 +  shows "(A ===> rel_set A ===> op =) (op \<in>) (op \<in>)"
   6.235 +  using assms unfolding fun_rel_def rel_set_def bi_unique_def by fast
   6.236  
   6.237  lemma right_total_Collect_transfer[transfer_rule]:
   6.238    assumes "right_total A"
   6.239 -  shows "((A ===> op =) ===> set_rel A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect"
   6.240 -  using assms unfolding right_total_def set_rel_def fun_rel_def Domainp_iff by fast
   6.241 +  shows "((A ===> op =) ===> rel_set A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect"
   6.242 +  using assms unfolding right_total_def rel_set_def fun_rel_def Domainp_iff by fast
   6.243  
   6.244  lemma Collect_transfer [transfer_rule]:
   6.245    assumes "bi_total A"
   6.246 -  shows "((A ===> op =) ===> set_rel A) Collect Collect"
   6.247 -  using assms unfolding fun_rel_def set_rel_def bi_total_def by fast
   6.248 +  shows "((A ===> op =) ===> rel_set A) Collect Collect"
   6.249 +  using assms unfolding fun_rel_def rel_set_def bi_total_def by fast
   6.250  
   6.251  lemma inter_transfer [transfer_rule]:
   6.252    assumes "bi_unique A"
   6.253 -  shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter"
   6.254 -  using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
   6.255 +  shows "(rel_set A ===> rel_set A ===> rel_set A) inter inter"
   6.256 +  using assms unfolding fun_rel_def rel_set_def bi_unique_def by fast
   6.257  
   6.258  lemma Diff_transfer [transfer_rule]:
   6.259    assumes "bi_unique A"
   6.260 -  shows "(set_rel A ===> set_rel A ===> set_rel A) (op -) (op -)"
   6.261 -  using assms unfolding fun_rel_def set_rel_def bi_unique_def
   6.262 +  shows "(rel_set A ===> rel_set A ===> rel_set A) (op -) (op -)"
   6.263 +  using assms unfolding fun_rel_def rel_set_def bi_unique_def
   6.264    unfolding Ball_def Bex_def Diff_eq
   6.265    by (safe, simp, metis, simp, metis)
   6.266  
   6.267  lemma subset_transfer [transfer_rule]:
   6.268    assumes [transfer_rule]: "bi_unique A"
   6.269 -  shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)"
   6.270 +  shows "(rel_set A ===> rel_set A ===> op =) (op \<subseteq>) (op \<subseteq>)"
   6.271    unfolding subset_eq [abs_def] by transfer_prover
   6.272  
   6.273  lemma right_total_UNIV_transfer[transfer_rule]: 
   6.274    assumes "right_total A"
   6.275 -  shows "(set_rel A) (Collect (Domainp A)) UNIV"
   6.276 -  using assms unfolding right_total_def set_rel_def Domainp_iff by blast
   6.277 +  shows "(rel_set A) (Collect (Domainp A)) UNIV"
   6.278 +  using assms unfolding right_total_def rel_set_def Domainp_iff by blast
   6.279  
   6.280  lemma UNIV_transfer [transfer_rule]:
   6.281    assumes "bi_total A"
   6.282 -  shows "(set_rel A) UNIV UNIV"
   6.283 -  using assms unfolding set_rel_def bi_total_def by simp
   6.284 +  shows "(rel_set A) UNIV UNIV"
   6.285 +  using assms unfolding rel_set_def bi_total_def by simp
   6.286  
   6.287  lemma right_total_Compl_transfer [transfer_rule]:
   6.288    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
   6.289 -  shows "(set_rel A ===> set_rel A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus"
   6.290 +  shows "(rel_set A ===> rel_set A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus"
   6.291    unfolding Compl_eq [abs_def]
   6.292    by (subst Collect_conj_eq[symmetric]) transfer_prover
   6.293  
   6.294  lemma Compl_transfer [transfer_rule]:
   6.295    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
   6.296 -  shows "(set_rel A ===> set_rel A) uminus uminus"
   6.297 +  shows "(rel_set A ===> rel_set A) uminus uminus"
   6.298    unfolding Compl_eq [abs_def] by transfer_prover
   6.299  
   6.300  lemma right_total_Inter_transfer [transfer_rule]:
   6.301    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
   6.302 -  shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter"
   6.303 +  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter"
   6.304    unfolding Inter_eq[abs_def]
   6.305    by (subst Collect_conj_eq[symmetric]) transfer_prover
   6.306  
   6.307  lemma Inter_transfer [transfer_rule]:
   6.308    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
   6.309 -  shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter"
   6.310 +  shows "(rel_set (rel_set A) ===> rel_set A) Inter Inter"
   6.311    unfolding Inter_eq [abs_def] by transfer_prover
   6.312  
   6.313  lemma filter_transfer [transfer_rule]:
   6.314    assumes [transfer_rule]: "bi_unique A"
   6.315 -  shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter"
   6.316 -  unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast
   6.317 +  shows "((A ===> op=) ===> rel_set A ===> rel_set A) Set.filter Set.filter"
   6.318 +  unfolding Set.filter_def[abs_def] fun_rel_def rel_set_def by blast
   6.319  
   6.320 -lemma bi_unique_set_rel_lemma:
   6.321 -  assumes "bi_unique R" and "set_rel R X Y"
   6.322 +lemma bi_unique_rel_set_lemma:
   6.323 +  assumes "bi_unique R" and "rel_set R X Y"
   6.324    obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)"
   6.325  proof
   6.326    let ?f = "\<lambda>x. THE y. R x y"
   6.327    from assms show f: "\<forall>x\<in>X. R x (?f x)"
   6.328 -    apply (clarsimp simp add: set_rel_def)
   6.329 +    apply (clarsimp simp add: rel_set_def)
   6.330      apply (drule (1) bspec, clarify)
   6.331      apply (rule theI2, assumption)
   6.332      apply (simp add: bi_unique_def)
   6.333 @@ -248,13 +248,13 @@
   6.334      done
   6.335    from assms show "Y = image ?f X"
   6.336      apply safe
   6.337 -    apply (clarsimp simp add: set_rel_def)
   6.338 +    apply (clarsimp simp add: rel_set_def)
   6.339      apply (drule (1) bspec, clarify)
   6.340      apply (rule image_eqI)
   6.341      apply (rule the_equality [symmetric], assumption)
   6.342      apply (simp add: bi_unique_def)
   6.343      apply assumption
   6.344 -    apply (clarsimp simp add: set_rel_def)
   6.345 +    apply (clarsimp simp add: rel_set_def)
   6.346      apply (frule (1) bspec, clarify)
   6.347      apply (rule theI2, assumption)
   6.348      apply (clarsimp simp add: bi_unique_def)
   6.349 @@ -269,41 +269,41 @@
   6.350  qed
   6.351  
   6.352  lemma finite_transfer [transfer_rule]:
   6.353 -  "bi_unique A \<Longrightarrow> (set_rel A ===> op =) finite finite"
   6.354 -  by (rule fun_relI, erule (1) bi_unique_set_rel_lemma,
   6.355 +  "bi_unique A \<Longrightarrow> (rel_set A ===> op =) finite finite"
   6.356 +  by (rule fun_relI, erule (1) bi_unique_rel_set_lemma,
   6.357      auto dest: finite_imageD)
   6.358  
   6.359  lemma card_transfer [transfer_rule]:
   6.360 -  "bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card"
   6.361 -  by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image)
   6.362 +  "bi_unique A \<Longrightarrow> (rel_set A ===> op =) card card"
   6.363 +  by (rule fun_relI, erule (1) bi_unique_rel_set_lemma, simp add: card_image)
   6.364  
   6.365  lemma vimage_parametric [transfer_rule]:
   6.366    assumes [transfer_rule]: "bi_total A" "bi_unique B"
   6.367 -  shows "((A ===> B) ===> set_rel B ===> set_rel A) vimage vimage"
   6.368 +  shows "((A ===> B) ===> rel_set B ===> rel_set A) vimage vimage"
   6.369  unfolding vimage_def[abs_def] by transfer_prover
   6.370  
   6.371  lemma setsum_parametric [transfer_rule]:
   6.372    assumes "bi_unique A"
   6.373 -  shows "((A ===> op =) ===> set_rel A ===> op =) setsum setsum"
   6.374 +  shows "((A ===> op =) ===> rel_set A ===> op =) setsum setsum"
   6.375  proof(rule fun_relI)+
   6.376    fix f :: "'a \<Rightarrow> 'c" and g S T
   6.377    assume fg: "(A ===> op =) f g"
   6.378 -    and ST: "set_rel A S T"
   6.379 +    and ST: "rel_set A S T"
   6.380    show "setsum f S = setsum g T"
   6.381    proof(rule setsum_reindex_cong)
   6.382      let ?f = "\<lambda>t. THE s. A s t"
   6.383      show "S = ?f ` T"
   6.384 -      by(blast dest: set_relD1[OF ST] set_relD2[OF ST] bi_uniqueDl[OF assms] 
   6.385 +      by(blast dest: rel_setD1[OF ST] rel_setD2[OF ST] bi_uniqueDl[OF assms] 
   6.386             intro: rev_image_eqI the_equality[symmetric] subst[rotated, where P="\<lambda>x. x \<in> S"])
   6.387  
   6.388      show "inj_on ?f T"
   6.389      proof(rule inj_onI)
   6.390        fix t1 t2
   6.391        assume "t1 \<in> T" "t2 \<in> T" "?f t1 = ?f t2"
   6.392 -      from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: set_relD2)
   6.393 +      from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: rel_setD2)
   6.394        hence "?f t1 = s1" by(auto dest: bi_uniqueDl[OF assms])
   6.395        moreover
   6.396 -      from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: set_relD2)
   6.397 +      from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: rel_setD2)
   6.398        hence "?f t2 = s2" by(auto dest: bi_uniqueDl[OF assms])
   6.399        ultimately have "s1 = s2" using `?f t1 = ?f t2` by simp
   6.400        with `A s1 t1` `A s2 t2` show "t1 = t2" by(auto dest: bi_uniqueDr[OF assms])
   6.401 @@ -311,7 +311,7 @@
   6.402  
   6.403      fix t
   6.404      assume "t \<in> T"
   6.405 -    with ST obtain s where "A s t" "s \<in> S" by(auto dest: set_relD2)
   6.406 +    with ST obtain s where "A s t" "s \<in> S" by(auto dest: rel_setD2)
   6.407      hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
   6.408      moreover from fg `A s t` have "f s = g t" by(rule fun_relD)
   6.409      ultimately show "g t = f (?f t)" by simp
     7.1 --- a/src/HOL/List.thy	Thu Mar 06 14:25:55 2014 +0100
     7.2 +++ b/src/HOL/List.thy	Thu Mar 06 14:57:14 2014 +0100
     7.3 @@ -6734,7 +6734,7 @@
     7.4    by (rule fun_relI, erule list_all2_induct, auto)
     7.5  
     7.6  lemma set_transfer [transfer_rule]:
     7.7 -  "(list_all2 A ===> set_rel A) set set"
     7.8 +  "(list_all2 A ===> rel_set A) set set"
     7.9    unfolding set_rec[abs_def] by transfer_prover
    7.10  
    7.11  lemma map_rec: "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs"
    7.12 @@ -6864,7 +6864,7 @@
    7.13    done
    7.14  
    7.15  lemma sublist_transfer [transfer_rule]:
    7.16 -  "(list_all2 A ===> set_rel (op =) ===> list_all2 A) sublist sublist"
    7.17 +  "(list_all2 A ===> rel_set (op =) ===> list_all2 A) sublist sublist"
    7.18    unfolding sublist_def [abs_def] by transfer_prover
    7.19  
    7.20  lemma partition_transfer [transfer_rule]:
    7.21 @@ -6873,25 +6873,25 @@
    7.22    unfolding partition_def by transfer_prover
    7.23  
    7.24  lemma lists_transfer [transfer_rule]:
    7.25 -  "(set_rel A ===> set_rel (list_all2 A)) lists lists"
    7.26 -  apply (rule fun_relI, rule set_relI)
    7.27 +  "(rel_set A ===> rel_set (list_all2 A)) lists lists"
    7.28 +  apply (rule fun_relI, rule rel_setI)
    7.29    apply (erule lists.induct, simp)
    7.30 -  apply (simp only: set_rel_def list_all2_Cons1, metis lists.Cons)
    7.31 +  apply (simp only: rel_set_def list_all2_Cons1, metis lists.Cons)
    7.32    apply (erule lists.induct, simp)
    7.33 -  apply (simp only: set_rel_def list_all2_Cons2, metis lists.Cons)
    7.34 +  apply (simp only: rel_set_def list_all2_Cons2, metis lists.Cons)
    7.35    done
    7.36  
    7.37  lemma set_Cons_transfer [transfer_rule]:
    7.38 -  "(set_rel A ===> set_rel (list_all2 A) ===> set_rel (list_all2 A))
    7.39 +  "(rel_set A ===> rel_set (list_all2 A) ===> rel_set (list_all2 A))
    7.40      set_Cons set_Cons"
    7.41 -  unfolding fun_rel_def set_rel_def set_Cons_def
    7.42 +  unfolding fun_rel_def rel_set_def set_Cons_def
    7.43    apply safe
    7.44    apply (simp add: list_all2_Cons1, fast)
    7.45    apply (simp add: list_all2_Cons2, fast)
    7.46    done
    7.47  
    7.48  lemma listset_transfer [transfer_rule]:
    7.49 -  "(list_all2 (set_rel A) ===> set_rel (list_all2 A)) listset listset"
    7.50 +  "(list_all2 (rel_set A) ===> rel_set (list_all2 A)) listset listset"
    7.51    unfolding listset_def by transfer_prover
    7.52  
    7.53  lemma null_transfer [transfer_rule]:
     8.1 --- a/src/HOL/Topological_Spaces.thy	Thu Mar 06 14:25:55 2014 +0100
     8.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Mar 06 14:57:14 2014 +0100
     8.3 @@ -2497,19 +2497,19 @@
     8.4  by(fastforce simp add: filter_rel_eventually[abs_def] eventually_sup dest: fun_relD)
     8.5  
     8.6  lemma Sup_filter_parametric [transfer_rule]:
     8.7 -  "(set_rel (filter_rel A) ===> filter_rel A) Sup Sup"
     8.8 +  "(rel_set (filter_rel A) ===> filter_rel A) Sup Sup"
     8.9  proof(rule fun_relI)
    8.10    fix S T
    8.11 -  assume [transfer_rule]: "set_rel (filter_rel A) S T"
    8.12 +  assume [transfer_rule]: "rel_set (filter_rel A) S T"
    8.13    show "filter_rel A (Sup S) (Sup T)"
    8.14      by(simp add: filter_rel_eventually eventually_Sup) transfer_prover
    8.15  qed
    8.16  
    8.17  lemma principal_parametric [transfer_rule]:
    8.18 -  "(set_rel A ===> filter_rel A) principal principal"
    8.19 +  "(rel_set A ===> filter_rel A) principal principal"
    8.20  proof(rule fun_relI)
    8.21    fix S S'
    8.22 -  assume [transfer_rule]: "set_rel A S S'"
    8.23 +  assume [transfer_rule]: "rel_set A S S'"
    8.24    show "filter_rel A (principal S) (principal S')"
    8.25      by(simp add: filter_rel_eventually eventually_principal) transfer_prover
    8.26  qed
    8.27 @@ -2532,7 +2532,7 @@
    8.28  begin
    8.29  
    8.30  lemma Inf_filter_parametric [transfer_rule]:
    8.31 -  "(set_rel (filter_rel A) ===> filter_rel A) Inf Inf"
    8.32 +  "(rel_set (filter_rel A) ===> filter_rel A) Inf Inf"
    8.33  unfolding Inf_filter_def[abs_def] by transfer_prover
    8.34  
    8.35  lemma inf_filter_parametric [transfer_rule]:
     9.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Thu Mar 06 14:25:55 2014 +0100
     9.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Thu Mar 06 14:57:14 2014 +0100
     9.3 @@ -96,19 +96,19 @@
     9.4    unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
     9.5  
     9.6  lemma ZN_atMost [transfer_rule]:
     9.7 -  "(ZN ===> set_rel ZN) (atLeastAtMost 0) atMost"
     9.8 -  unfolding fun_rel_def ZN_def set_rel_def
     9.9 +  "(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"
    9.10 +  unfolding fun_rel_def ZN_def rel_set_def
    9.11    by (clarsimp simp add: Bex_def, arith)
    9.12  
    9.13  lemma ZN_atLeastAtMost [transfer_rule]:
    9.14 -  "(ZN ===> ZN ===> set_rel ZN) atLeastAtMost atLeastAtMost"
    9.15 -  unfolding fun_rel_def ZN_def set_rel_def
    9.16 +  "(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost"
    9.17 +  unfolding fun_rel_def ZN_def rel_set_def
    9.18    by (clarsimp simp add: Bex_def, arith)
    9.19  
    9.20  lemma ZN_setsum [transfer_rule]:
    9.21 -  "bi_unique A \<Longrightarrow> ((A ===> ZN) ===> set_rel A ===> ZN) setsum setsum"
    9.22 +  "bi_unique A \<Longrightarrow> ((A ===> ZN) ===> rel_set A ===> ZN) setsum setsum"
    9.23    apply (intro fun_relI)
    9.24 -  apply (erule (1) bi_unique_set_rel_lemma)
    9.25 +  apply (erule (1) bi_unique_rel_set_lemma)
    9.26    apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def)
    9.27    apply (rule setsum_cong2, simp)
    9.28    done