# HG changeset patch
# User blanchet
# Date 1394109409 -3600
# Node ID 12ee2c407dadb48eb787192b3efa9f00d48a04b0
# Parent  68c5104d2204c1ab99f3a9373c1a89c4e25eb65f
renamed 'fset_rel' to 'rel_fset'

diff -r 68c5104d2204 -r 12ee2c407dad NEWS
--- a/NEWS	Thu Mar 06 13:36:48 2014 +0100
+++ b/NEWS	Thu Mar 06 13:36:49 2014 +0100
@@ -190,8 +190,10 @@
     the.simps ~> option.sel
   INCOMPATIBILITY.
 
-* The following map function has been renamed:
+* The following map functions and relators have been renamed:
     map_sum ~> sum_map
+    map_pair ~> prod_map
+    fset_rel ~> rel_fset
 
 * New theory:
     Cardinals/Ordinal_Arithmetic.thy
diff -r 68c5104d2204 -r 12ee2c407dad src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
--- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 13:36:48 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 13:36:49 2014 +0100
@@ -61,8 +61,8 @@
 by (metis Node_root_cont assms)
 
 lemma set_rel_cont:
-"set_rel \<chi> (cont tr1) (cont tr2) = fset_rel \<chi> (ccont tr1) (ccont tr2)"
-unfolding cont_def comp_def fset_rel_fset ..
+"set_rel \<chi> (cont tr1) (cont tr2) = rel_fset \<chi> (ccont tr1) (ccont tr2)"
+unfolding cont_def comp_def rel_fset_fset ..
 
 lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]:
 assumes phi: "\<phi> tr1 tr2" and
diff -r 68c5104d2204 -r 12ee2c407dad src/HOL/BNF_Examples/TreeFsetI.thy
--- a/src/HOL/BNF_Examples/TreeFsetI.thy	Thu Mar 06 13:36:48 2014 +0100
+++ b/src/HOL/BNF_Examples/TreeFsetI.thy	Thu Mar 06 13:36:49 2014 +0100
@@ -20,6 +20,6 @@
 "sub (tmap f t) = fimage (tmap f) (sub t)"
 
 lemma "tmap (f o g) x = tmap f (tmap g x)"
-  by (coinduction arbitrary: x) (auto simp: fset_rel_alt)
+  by (coinduction arbitrary: x) (auto simp: rel_fset_alt)
 
 end
diff -r 68c5104d2204 -r 12ee2c407dad src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Thu Mar 06 13:36:48 2014 +0100
+++ b/src/HOL/Library/FSet.thy	Thu Mar 06 13:36:49 2014 +0100
@@ -762,23 +762,23 @@
 
 subsubsection {* Relator and predicator properties *}
 
-lift_definition fset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is set_rel
+lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is set_rel
 parametric set_rel_transfer .
 
-lemma fset_rel_alt_def: "fset_rel R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y) 
+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) 
   \<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
 apply (rule ext)+
 apply transfer'
 apply (subst set_rel_def[unfolded fun_eq_iff]) 
 by blast
 
-lemma fset_rel_conversep: "fset_rel (conversep R) = conversep (fset_rel R)"
-  unfolding fset_rel_alt_def by auto
+lemma rel_fset_conversep: "rel_fset (conversep R) = conversep (rel_fset R)"
+  unfolding rel_fset_alt_def by auto
 
-lemmas fset_rel_eq [relator_eq] = set_rel_eq[Transfer.transferred]
+lemmas rel_fset_eq [relator_eq] = set_rel_eq[Transfer.transferred]
 
-lemma fset_rel_mono[relator_mono]: "A \<le> B \<Longrightarrow> fset_rel A \<le> fset_rel B"
-unfolding fset_rel_alt_def by blast
+lemma rel_fset_mono[relator_mono]: "A \<le> B \<Longrightarrow> rel_fset A \<le> rel_fset B"
+unfolding rel_fset_alt_def by blast
 
 lemma finite_set_rel:
   assumes fin: "finite X" "finite Z"
@@ -806,27 +806,27 @@
   ultimately show ?thesis by metis
 qed
 
-lemma fset_rel_OO[relator_distr]: "fset_rel R OO fset_rel S = fset_rel (R OO S)"
+lemma rel_fset_OO[relator_distr]: "rel_fset R OO rel_fset S = rel_fset (R OO S)"
 apply (rule ext)+
 by transfer (auto intro: finite_set_rel set_rel_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
 
 lemma Domainp_fset[relator_domain]:
   assumes "Domainp T = P"
-  shows "Domainp (fset_rel T) = (\<lambda>A. fBall A P)"
+  shows "Domainp (rel_fset T) = (\<lambda>A. fBall A P)"
 proof -
   from assms obtain f where f: "\<forall>x\<in>Collect P. T x (f x)"
     unfolding Domainp_iff[abs_def]
     apply atomize_elim
     by (subst bchoice_iff[symmetric]) auto
   from assms f show ?thesis
-    unfolding fun_eq_iff fset_rel_alt_def Domainp_iff
+    unfolding fun_eq_iff rel_fset_alt_def Domainp_iff
     apply clarify
     apply (rule iffI)
       apply blast
     by (rename_tac A, rule_tac x="f |`| A" in exI, blast)
 qed
 
-lemma right_total_fset_rel[transfer_rule]: "right_total A \<Longrightarrow> right_total (fset_rel A)"
+lemma right_total_rel_fset[transfer_rule]: "right_total A \<Longrightarrow> right_total (rel_fset A)"
 unfolding right_total_def 
 apply transfer
 apply (subst(asm) choice_iff)
@@ -834,7 +834,7 @@
 apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
 by (auto simp add: set_rel_def)
 
-lemma left_total_fset_rel[reflexivity_rule]: "left_total A \<Longrightarrow> left_total (fset_rel A)"
+lemma left_total_rel_fset[reflexivity_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
 unfolding left_total_def 
 apply transfer
 apply (subst(asm) choice_iff)
@@ -842,16 +842,16 @@
 apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
 by (auto simp add: set_rel_def)
 
-lemmas right_unique_fset_rel[transfer_rule] = right_unique_set_rel[Transfer.transferred]
-lemmas left_unique_fset_rel[reflexivity_rule] = left_unique_set_rel[Transfer.transferred]
+lemmas right_unique_rel_fset[transfer_rule] = right_unique_set_rel[Transfer.transferred]
+lemmas left_unique_rel_fset[reflexivity_rule] = left_unique_set_rel[Transfer.transferred]
 
-thm right_unique_fset_rel left_unique_fset_rel
+thm right_unique_rel_fset left_unique_rel_fset
 
-lemma bi_unique_fset_rel[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (fset_rel A)"
-by (auto intro: right_unique_fset_rel left_unique_fset_rel iff: bi_unique_iff)
+lemma bi_unique_rel_fset[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_fset A)"
+by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_iff)
 
-lemma bi_total_fset_rel[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (fset_rel A)"
-by (auto intro: right_total_fset_rel left_total_fset_rel iff: bi_total_iff)
+lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
+by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff)
 
 lemmas fset_invariant_commute [invariant_commute] = set_invariant_commute[Transfer.transferred]
 
@@ -860,9 +860,9 @@
 
 lemma Quotient_fset_map[quot_map]:
   assumes "Quotient R Abs Rep T"
-  shows "Quotient (fset_rel R) (fimage Abs) (fimage Rep) (fset_rel T)"
+  shows "Quotient (rel_fset R) (fimage Abs) (fimage Rep) (rel_fset T)"
   using assms unfolding Quotient_alt_def4
-  by (simp add: fset_rel_OO[symmetric] fset_rel_conversep) (simp add: fset_rel_alt_def, blast)
+  by (simp add: rel_fset_OO[symmetric] rel_fset_conversep) (simp add: rel_fset_alt_def, blast)
 
 
 subsubsection {* Transfer rules for the Transfer package *}
@@ -877,45 +877,45 @@
 lemmas fempty_transfer [transfer_rule] = empty_transfer[Transfer.transferred]
 
 lemma finsert_transfer [transfer_rule]:
-  "(A ===> fset_rel A ===> fset_rel A) finsert finsert"
-  unfolding fun_rel_def fset_rel_alt_def by blast
+  "(A ===> rel_fset A ===> rel_fset A) finsert finsert"
+  unfolding fun_rel_def rel_fset_alt_def by blast
 
 lemma funion_transfer [transfer_rule]:
-  "(fset_rel A ===> fset_rel A ===> fset_rel A) funion funion"
-  unfolding fun_rel_def fset_rel_alt_def by blast
+  "(rel_fset A ===> rel_fset A ===> rel_fset A) funion funion"
+  unfolding fun_rel_def rel_fset_alt_def by blast
 
 lemma ffUnion_transfer [transfer_rule]:
-  "(fset_rel (fset_rel A) ===> fset_rel A) ffUnion ffUnion"
-  unfolding fun_rel_def fset_rel_alt_def by transfer (simp, fast)
+  "(rel_fset (rel_fset A) ===> rel_fset A) ffUnion ffUnion"
+  unfolding fun_rel_def rel_fset_alt_def by transfer (simp, fast)
 
 lemma fimage_transfer [transfer_rule]:
-  "((A ===> B) ===> fset_rel A ===> fset_rel B) fimage fimage"
-  unfolding fun_rel_def fset_rel_alt_def by simp blast
+  "((A ===> B) ===> rel_fset A ===> rel_fset B) fimage fimage"
+  unfolding fun_rel_def rel_fset_alt_def by simp blast
 
 lemma fBall_transfer [transfer_rule]:
-  "(fset_rel A ===> (A ===> op =) ===> op =) fBall fBall"
-  unfolding fset_rel_alt_def fun_rel_def by blast
+  "(rel_fset A ===> (A ===> op =) ===> op =) fBall fBall"
+  unfolding rel_fset_alt_def fun_rel_def by blast
 
 lemma fBex_transfer [transfer_rule]:
-  "(fset_rel A ===> (A ===> op =) ===> op =) fBex fBex"
-  unfolding fset_rel_alt_def fun_rel_def by blast
+  "(rel_fset A ===> (A ===> op =) ===> op =) fBex fBex"
+  unfolding rel_fset_alt_def fun_rel_def by blast
 
 (* FIXME transfer doesn't work here *)
 lemma fPow_transfer [transfer_rule]:
-  "(fset_rel A ===> fset_rel (fset_rel A)) fPow fPow"
+  "(rel_fset A ===> rel_fset (rel_fset A)) fPow fPow"
   unfolding fun_rel_def
   using Pow_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred]
   by blast
 
-lemma fset_rel_transfer [transfer_rule]:
-  "((A ===> B ===> op =) ===> fset_rel A ===> fset_rel B ===> op =)
-    fset_rel fset_rel"
+lemma rel_fset_transfer [transfer_rule]:
+  "((A ===> B ===> op =) ===> rel_fset A ===> rel_fset B ===> op =)
+    rel_fset rel_fset"
   unfolding fun_rel_def
   using set_rel_transfer[unfolded fun_rel_def,rule_format, Transfer.transferred, where A = A and B = B]
   by simp
 
 lemma bind_transfer [transfer_rule]:
-  "(fset_rel A ===> (A ===> fset_rel B) ===> fset_rel B) fbind fbind"
+  "(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind"
   using assms unfolding fun_rel_def
   using bind_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
 
@@ -923,29 +923,29 @@
 
 lemma fmember_transfer [transfer_rule]:
   assumes "bi_unique A"
-  shows "(A ===> fset_rel A ===> op =) (op |\<in>|) (op |\<in>|)"
-  using assms unfolding fun_rel_def fset_rel_alt_def bi_unique_def by metis
+  shows "(A ===> rel_fset A ===> op =) (op |\<in>|) (op |\<in>|)"
+  using assms unfolding fun_rel_def rel_fset_alt_def bi_unique_def by metis
 
 lemma finter_transfer [transfer_rule]:
   assumes "bi_unique A"
-  shows "(fset_rel A ===> fset_rel A ===> fset_rel A) finter finter"
+  shows "(rel_fset A ===> rel_fset A ===> rel_fset A) finter finter"
   using assms unfolding fun_rel_def
   using inter_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
 
 lemma fminus_transfer [transfer_rule]:
   assumes "bi_unique A"
-  shows "(fset_rel A ===> fset_rel A ===> fset_rel A) (op |-|) (op |-|)"
+  shows "(rel_fset A ===> rel_fset A ===> rel_fset A) (op |-|) (op |-|)"
   using assms unfolding fun_rel_def
   using Diff_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
 
 lemma fsubset_transfer [transfer_rule]:
   assumes "bi_unique A"
-  shows "(fset_rel A ===> fset_rel A ===> op =) (op |\<subseteq>|) (op |\<subseteq>|)"
+  shows "(rel_fset A ===> rel_fset A ===> op =) (op |\<subseteq>|) (op |\<subseteq>|)"
   using assms unfolding fun_rel_def
   using subset_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
 
 lemma fSup_transfer [transfer_rule]:
-  "bi_unique A \<Longrightarrow> (set_rel (fset_rel A) ===> fset_rel A) Sup Sup"
+  "bi_unique A \<Longrightarrow> (set_rel (rel_fset A) ===> rel_fset A) Sup Sup"
   using assms unfolding fun_rel_def
   apply clarify
   apply transfer'
@@ -955,7 +955,7 @@
 
 lemma fInf_transfer [transfer_rule]:
   assumes "bi_unique A" and "bi_total A"
-  shows "(set_rel (fset_rel A) ===> fset_rel A) Inf Inf"
+  shows "(set_rel (rel_fset A) ===> rel_fset A) Inf Inf"
   using assms unfolding fun_rel_def
   apply clarify
   apply transfer'
@@ -963,12 +963,12 @@
 
 lemma ffilter_transfer [transfer_rule]:
   assumes "bi_unique A"
-  shows "((A ===> op=) ===> fset_rel A ===> fset_rel A) ffilter ffilter"
+  shows "((A ===> op=) ===> rel_fset A ===> rel_fset A) ffilter ffilter"
   using assms unfolding fun_rel_def
   using Lifting_Set.filter_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
 
 lemma card_transfer [transfer_rule]:
-  "bi_unique A \<Longrightarrow> (fset_rel A ===> op =) fcard fcard"
+  "bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard"
   using assms unfolding fun_rel_def
   using card_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
 
@@ -984,8 +984,8 @@
 includes fset.lifting
 begin
 
-lemma fset_rel_alt:
-  "fset_rel 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)"
+lemma rel_fset_alt:
+  "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)"
 by transfer (simp add: set_rel_def)
 
 lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
@@ -994,7 +994,7 @@
 apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
 .
 
-lemma fset_rel_aux:
+lemma rel_fset_aux:
 "(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
  ((BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
   BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
@@ -1023,7 +1023,7 @@
   sets: fset 
   bd: natLeq
   wits: "{||}"
-  rel: fset_rel
+  rel: rel_fset
 apply -
           apply transfer' apply simp
          apply transfer' apply force
@@ -1032,12 +1032,12 @@
       apply (rule natLeq_card_order)
      apply (rule natLeq_cinfinite)
     apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
-   apply (fastforce simp: fset_rel_alt)
- apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) 
+   apply (fastforce simp: rel_fset_alt)
+ apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt rel_fset_aux) 
 apply transfer apply simp
 done
 
-lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
+lemma rel_fset_fset: "set_rel \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2"
   by transfer (rule refl)
 
 end