renamed 'fun_rel' to 'rel_fun'
authorblanchet
Thu Mar 06 15:40:33 2014 +0100 (2014-03-06)
changeset 55945e96383acecf9
parent 55944 7ab8f003fe41
child 55946 5163ed3a38f5
renamed 'fun_rel' to 'rel_fun'
NEWS
src/Doc/Datatypes/Datatypes.thy
src/HOL/BNF_Def.thy
src/HOL/BNF_FP_Base.thy
src/HOL/BNF_GFP.thy
src/HOL/BNF_LFP.thy
src/HOL/BNF_Util.thy
src/HOL/Basic_BNFs.thy
src/HOL/Code_Numeral.thy
src/HOL/Int.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Float.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Library/Quotient_Syntax.thy
src/HOL/Lifting.thy
src/HOL/Lifting_Option.thy
src/HOL/Lifting_Product.thy
src/HOL/Lifting_Set.thy
src/HOL/Lifting_Sum.thy
src/HOL/List.thy
src/HOL/Quotient.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Real.thy
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_util.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_util.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/transfer.ML
src/HOL/Topological_Spaces.thy
src/HOL/Transfer.thy
src/HOL/Word/Word.thy
src/HOL/ex/Transfer_Int_Nat.thy
     1.1 --- a/NEWS	Thu Mar 06 15:29:18 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 06 15:40:33 2014 +0100
     1.3 @@ -195,6 +195,7 @@
     1.4      map_pair ~> map_prod
     1.5      prod_rel ~> rel_prod
     1.6      sum_rel ~> rel_sum
     1.7 +    fun_rel ~> rel_fun
     1.8      set_rel ~> rel_set
     1.9      filter_rel ~> rel_filter
    1.10      fset_rel ~> rel_fset (in "Library/FSet.thy")
     2.1 --- a/src/Doc/Datatypes/Datatypes.thy	Thu Mar 06 15:29:18 2014 +0100
     2.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Thu Mar 06 15:40:33 2014 +0100
     2.3 @@ -2380,7 +2380,7 @@
     2.4      lift_definition
     2.5        rel_fn :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn \<Rightarrow> bool"
     2.6      is
     2.7 -      "fun_rel (op =)" .
     2.8 +      "rel_fun (op =)" .
     2.9  
    2.10  text {* \blankline *}
    2.11  
    2.12 @@ -2423,7 +2423,7 @@
    2.13      next
    2.14        fix R S
    2.15        show "rel_fn R OO rel_fn S \<le> rel_fn (R OO S)"
    2.16 -        by (rule, transfer) (auto simp add: fun_rel_def)
    2.17 +        by (rule, transfer) (auto simp add: rel_fun_def)
    2.18      next
    2.19        fix R
    2.20        show "rel_fn R =
    2.21 @@ -2431,7 +2431,7 @@
    2.22               BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
    2.23          unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
    2.24          apply transfer
    2.25 -        unfolding fun_rel_def subset_iff image_iff
    2.26 +        unfolding rel_fun_def subset_iff image_iff
    2.27          by auto (force, metis pair_collapse)
    2.28      qed
    2.29  
     3.1 --- a/src/HOL/BNF_Def.thy	Thu Mar 06 15:29:18 2014 +0100
     3.2 +++ b/src/HOL/BNF_Def.thy	Thu Mar 06 15:40:33 2014 +0100
     3.3 @@ -140,8 +140,8 @@
     3.4  lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
     3.5    unfolding vimage2p_def by -
     3.6  
     3.7 -lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)"
     3.8 -  unfolding fun_rel_def vimage2p_def by auto
     3.9 +lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
    3.10 +  unfolding rel_fun_def vimage2p_def by auto
    3.11  
    3.12  lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
    3.13    unfolding vimage2p_def convol_def by auto
     4.1 --- a/src/HOL/BNF_FP_Base.thy	Thu Mar 06 15:29:18 2014 +0100
     4.2 +++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 15:40:33 2014 +0100
     4.3 @@ -131,9 +131,9 @@
     4.4  lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x"
     4.5    unfolding case_sum_o_map_sum id_comp comp_id ..
     4.6  
     4.7 -lemma fun_rel_def_butlast:
     4.8 -  "fun_rel R (fun_rel S T) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
     4.9 -  unfolding fun_rel_def ..
    4.10 +lemma rel_fun_def_butlast:
    4.11 +  "rel_fun R (rel_fun S T) f g = (\<forall>x y. R x y \<longrightarrow> (rel_fun S T) (f x) (g y))"
    4.12 +  unfolding rel_fun_def ..
    4.13  
    4.14  lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
    4.15    by auto
     5.1 --- a/src/HOL/BNF_GFP.thy	Thu Mar 06 15:29:18 2014 +0100
     5.2 +++ b/src/HOL/BNF_GFP.thy	Thu Mar 06 15:40:33 2014 +0100
     5.3 @@ -233,11 +233,11 @@
     5.4  lemma image2pE: "\<lbrakk>image2p f g R fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
     5.5    unfolding image2p_def by blast
     5.6  
     5.7 -lemma fun_rel_iff_geq_image2p: "fun_rel R S f g = (image2p f g R \<le> S)"
     5.8 -  unfolding fun_rel_def image2p_def by auto
     5.9 +lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)"
    5.10 +  unfolding rel_fun_def image2p_def by auto
    5.11  
    5.12 -lemma fun_rel_image2p: "fun_rel R (image2p f g R) f g"
    5.13 -  unfolding fun_rel_def image2p_def by auto
    5.14 +lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
    5.15 +  unfolding rel_fun_def image2p_def by auto
    5.16  
    5.17  
    5.18  subsection {* Equivalence relations, quotients, and Hilbert's choice *}
     6.1 --- a/src/HOL/BNF_LFP.thy	Thu Mar 06 15:29:18 2014 +0100
     6.2 +++ b/src/HOL/BNF_LFP.thy	Thu Mar 06 15:40:33 2014 +0100
     6.3 @@ -244,14 +244,14 @@
     6.4    ultimately show P by (blast intro: assms(3))
     6.5  qed
     6.6  
     6.7 -lemma vimage2p_fun_rel: "fun_rel (vimage2p f g R) R f g"
     6.8 -  unfolding fun_rel_def vimage2p_def by auto
     6.9 +lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
    6.10 +  unfolding rel_fun_def vimage2p_def by auto
    6.11  
    6.12  lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
    6.13    unfolding vimage2p_def by auto
    6.14  
    6.15 -lemma id_transfer: "fun_rel A A id id"
    6.16 -  unfolding fun_rel_def by simp
    6.17 +lemma id_transfer: "rel_fun A A id id"
    6.18 +  unfolding rel_fun_def by simp
    6.19  
    6.20  lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
    6.21    by (rule ssubst)
     7.1 --- a/src/HOL/BNF_Util.thy	Thu Mar 06 15:29:18 2014 +0100
     7.2 +++ b/src/HOL/BNF_Util.thy	Thu Mar 06 15:40:33 2014 +0100
     7.3 @@ -13,19 +13,19 @@
     7.4  begin
     7.5  
     7.6  definition
     7.7 -  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
     7.8 +  rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
     7.9  where
    7.10 -  "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
    7.11 +  "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
    7.12  
    7.13 -lemma fun_relI [intro]:
    7.14 +lemma rel_funI [intro]:
    7.15    assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
    7.16 -  shows "fun_rel A B f g"
    7.17 -  using assms by (simp add: fun_rel_def)
    7.18 +  shows "rel_fun A B f g"
    7.19 +  using assms by (simp add: rel_fun_def)
    7.20  
    7.21 -lemma fun_relD:
    7.22 -  assumes "fun_rel A B f g" and "A x y"
    7.23 +lemma rel_funD:
    7.24 +  assumes "rel_fun A B f g" and "A x y"
    7.25    shows "B (f x) (g y)"
    7.26 -  using assms by (simp add: fun_rel_def)
    7.27 +  using assms by (simp add: rel_fun_def)
    7.28  
    7.29  definition collect where
    7.30  "collect F x = (\<Union>f \<in> F. f x)"
     8.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:29:18 2014 +0100
     8.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:40:33 2014 +0100
     8.3 @@ -163,7 +163,7 @@
     8.4    map: "op \<circ>"
     8.5    sets: range
     8.6    bd: "natLeq +c |UNIV :: 'a set|"
     8.7 -  rel: "fun_rel op ="
     8.8 +  rel: "rel_fun op ="
     8.9  proof
    8.10    fix f show "id \<circ> f = id f" by simp
    8.11  next
    8.12 @@ -193,13 +193,13 @@
    8.13    finally show "|range f| \<le>o natLeq +c ?U" .
    8.14  next
    8.15    fix R S
    8.16 -  show "fun_rel op = R OO fun_rel op = S \<le> fun_rel op = (R OO S)" by (auto simp: fun_rel_def)
    8.17 +  show "rel_fun op = R OO rel_fun op = S \<le> rel_fun op = (R OO S)" by (auto simp: rel_fun_def)
    8.18  next
    8.19    fix R
    8.20 -  show "fun_rel op = R =
    8.21 +  show "rel_fun op = R =
    8.22          (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
    8.23           Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
    8.24 -  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
    8.25 +  unfolding rel_fun_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
    8.26      comp_apply mem_Collect_eq split_beta bex_UNIV
    8.27    proof (safe, unfold fun_eq_iff[symmetric])
    8.28      fix x xa a b c xb y aa ba
     9.1 --- a/src/HOL/Code_Numeral.thy	Thu Mar 06 15:29:18 2014 +0100
     9.2 +++ b/src/HOL/Code_Numeral.thy	Thu Mar 06 15:40:33 2014 +0100
     9.3 @@ -76,27 +76,27 @@
     9.4  end
     9.5  
     9.6  lemma [transfer_rule]:
     9.7 -  "fun_rel HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
     9.8 +  "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
     9.9    by (unfold of_nat_def [abs_def]) transfer_prover
    9.10  
    9.11  lemma [transfer_rule]:
    9.12 -  "fun_rel HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
    9.13 +  "rel_fun HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
    9.14  proof -
    9.15 -  have "fun_rel HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
    9.16 +  have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
    9.17      by (unfold of_int_of_nat [abs_def]) transfer_prover
    9.18    then show ?thesis by (simp add: id_def)
    9.19  qed
    9.20  
    9.21  lemma [transfer_rule]:
    9.22 -  "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
    9.23 +  "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
    9.24  proof -
    9.25 -  have "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
    9.26 +  have "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
    9.27      by transfer_prover
    9.28    then show ?thesis by simp
    9.29  qed
    9.30  
    9.31  lemma [transfer_rule]:
    9.32 -  "fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    9.33 +  "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    9.34    by (unfold Num.sub_def [abs_def]) transfer_prover
    9.35  
    9.36  lemma int_of_integer_of_nat [simp]:
    9.37 @@ -192,11 +192,11 @@
    9.38  end
    9.39  
    9.40  lemma [transfer_rule]:
    9.41 -  "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    9.42 +  "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    9.43    by (unfold min_def [abs_def]) transfer_prover
    9.44  
    9.45  lemma [transfer_rule]:
    9.46 -  "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    9.47 +  "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    9.48    by (unfold max_def [abs_def]) transfer_prover
    9.49  
    9.50  lemma int_of_integer_min [simp]:
    9.51 @@ -249,7 +249,7 @@
    9.52    [simp, code_abbrev]: "Pos = numeral"
    9.53  
    9.54  lemma [transfer_rule]:
    9.55 -  "fun_rel HOL.eq pcr_integer numeral Pos"
    9.56 +  "rel_fun HOL.eq pcr_integer numeral Pos"
    9.57    by simp transfer_prover
    9.58  
    9.59  definition Neg :: "num \<Rightarrow> integer"
    9.60 @@ -257,7 +257,7 @@
    9.61    [simp, code_abbrev]: "Neg n = - Pos n"
    9.62  
    9.63  lemma [transfer_rule]:
    9.64 -  "fun_rel HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
    9.65 +  "rel_fun HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
    9.66    by (simp add: Neg_def [abs_def]) transfer_prover
    9.67  
    9.68  code_datatype "0::integer" Pos Neg
    9.69 @@ -680,17 +680,17 @@
    9.70  end
    9.71  
    9.72  lemma [transfer_rule]:
    9.73 -  "fun_rel HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
    9.74 +  "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
    9.75  proof -
    9.76 -  have "fun_rel HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
    9.77 +  have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
    9.78      by (unfold of_nat_def [abs_def]) transfer_prover
    9.79    then show ?thesis by (simp add: id_def)
    9.80  qed
    9.81  
    9.82  lemma [transfer_rule]:
    9.83 -  "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
    9.84 +  "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
    9.85  proof -
    9.86 -  have "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
    9.87 +  have "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
    9.88      by transfer_prover
    9.89    then show ?thesis by simp
    9.90  qed
    9.91 @@ -748,11 +748,11 @@
    9.92  end
    9.93  
    9.94  lemma [transfer_rule]:
    9.95 -  "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
    9.96 +  "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
    9.97    by (unfold min_def [abs_def]) transfer_prover
    9.98  
    9.99  lemma [transfer_rule]:
   9.100 -  "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   9.101 +  "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   9.102    by (unfold max_def [abs_def]) transfer_prover
   9.103  
   9.104  lemma nat_of_natural_min [simp]:
    10.1 --- a/src/HOL/Int.thy	Thu Mar 06 15:29:18 2014 +0100
    10.2 +++ b/src/HOL/Int.thy	Thu Mar 06 15:40:33 2014 +0100
    10.3 @@ -78,8 +78,8 @@
    10.4      simp add: one_int.abs_eq plus_int.abs_eq)
    10.5  
    10.6  lemma int_transfer [transfer_rule]:
    10.7 -  "(fun_rel (op =) cr_int) (\<lambda>n. (n, 0)) int"
    10.8 -  unfolding fun_rel_def cr_int_def int_def by simp
    10.9 +  "(rel_fun (op =) cr_int) (\<lambda>n. (n, 0)) int"
   10.10 +  unfolding rel_fun_def cr_int_def int_def by simp
   10.11  
   10.12  lemma int_diff_cases:
   10.13    obtains (diff) m n where "z = int m - int n"
    11.1 --- a/src/HOL/Library/FSet.thy	Thu Mar 06 15:29:18 2014 +0100
    11.2 +++ b/src/HOL/Library/FSet.thy	Thu Mar 06 15:40:33 2014 +0100
    11.3 @@ -878,99 +878,99 @@
    11.4  
    11.5  lemma finsert_transfer [transfer_rule]:
    11.6    "(A ===> rel_fset A ===> rel_fset A) finsert finsert"
    11.7 -  unfolding fun_rel_def rel_fset_alt_def by blast
    11.8 +  unfolding rel_fun_def rel_fset_alt_def by blast
    11.9  
   11.10  lemma funion_transfer [transfer_rule]:
   11.11    "(rel_fset A ===> rel_fset A ===> rel_fset A) funion funion"
   11.12 -  unfolding fun_rel_def rel_fset_alt_def by blast
   11.13 +  unfolding rel_fun_def rel_fset_alt_def by blast
   11.14  
   11.15  lemma ffUnion_transfer [transfer_rule]:
   11.16    "(rel_fset (rel_fset A) ===> rel_fset A) ffUnion ffUnion"
   11.17 -  unfolding fun_rel_def rel_fset_alt_def by transfer (simp, fast)
   11.18 +  unfolding rel_fun_def rel_fset_alt_def by transfer (simp, fast)
   11.19  
   11.20  lemma fimage_transfer [transfer_rule]:
   11.21    "((A ===> B) ===> rel_fset A ===> rel_fset B) fimage fimage"
   11.22 -  unfolding fun_rel_def rel_fset_alt_def by simp blast
   11.23 +  unfolding rel_fun_def rel_fset_alt_def by simp blast
   11.24  
   11.25  lemma fBall_transfer [transfer_rule]:
   11.26    "(rel_fset A ===> (A ===> op =) ===> op =) fBall fBall"
   11.27 -  unfolding rel_fset_alt_def fun_rel_def by blast
   11.28 +  unfolding rel_fset_alt_def rel_fun_def by blast
   11.29  
   11.30  lemma fBex_transfer [transfer_rule]:
   11.31    "(rel_fset A ===> (A ===> op =) ===> op =) fBex fBex"
   11.32 -  unfolding rel_fset_alt_def fun_rel_def by blast
   11.33 +  unfolding rel_fset_alt_def rel_fun_def by blast
   11.34  
   11.35  (* FIXME transfer doesn't work here *)
   11.36  lemma fPow_transfer [transfer_rule]:
   11.37    "(rel_fset A ===> rel_fset (rel_fset A)) fPow fPow"
   11.38 -  unfolding fun_rel_def
   11.39 -  using Pow_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred]
   11.40 +  unfolding rel_fun_def
   11.41 +  using Pow_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred]
   11.42    by blast
   11.43  
   11.44  lemma rel_fset_transfer [transfer_rule]:
   11.45    "((A ===> B ===> op =) ===> rel_fset A ===> rel_fset B ===> op =)
   11.46      rel_fset rel_fset"
   11.47 -  unfolding fun_rel_def
   11.48 -  using rel_set_transfer[unfolded fun_rel_def,rule_format, Transfer.transferred, where A = A and B = B]
   11.49 +  unfolding rel_fun_def
   11.50 +  using rel_set_transfer[unfolded rel_fun_def,rule_format, Transfer.transferred, where A = A and B = B]
   11.51    by simp
   11.52  
   11.53  lemma bind_transfer [transfer_rule]:
   11.54    "(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind"
   11.55 -  using assms unfolding fun_rel_def
   11.56 -  using bind_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   11.57 +  using assms unfolding rel_fun_def
   11.58 +  using bind_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
   11.59  
   11.60  text {* Rules requiring bi-unique, bi-total or right-total relations *}
   11.61  
   11.62  lemma fmember_transfer [transfer_rule]:
   11.63    assumes "bi_unique A"
   11.64    shows "(A ===> rel_fset A ===> op =) (op |\<in>|) (op |\<in>|)"
   11.65 -  using assms unfolding fun_rel_def rel_fset_alt_def bi_unique_def by metis
   11.66 +  using assms unfolding rel_fun_def rel_fset_alt_def bi_unique_def by metis
   11.67  
   11.68  lemma finter_transfer [transfer_rule]:
   11.69    assumes "bi_unique A"
   11.70    shows "(rel_fset A ===> rel_fset A ===> rel_fset A) finter finter"
   11.71 -  using assms unfolding fun_rel_def
   11.72 -  using inter_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   11.73 +  using assms unfolding rel_fun_def
   11.74 +  using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
   11.75  
   11.76  lemma fminus_transfer [transfer_rule]:
   11.77    assumes "bi_unique A"
   11.78    shows "(rel_fset A ===> rel_fset A ===> rel_fset A) (op |-|) (op |-|)"
   11.79 -  using assms unfolding fun_rel_def
   11.80 -  using Diff_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   11.81 +  using assms unfolding rel_fun_def
   11.82 +  using Diff_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
   11.83  
   11.84  lemma fsubset_transfer [transfer_rule]:
   11.85    assumes "bi_unique A"
   11.86    shows "(rel_fset A ===> rel_fset A ===> op =) (op |\<subseteq>|) (op |\<subseteq>|)"
   11.87 -  using assms unfolding fun_rel_def
   11.88 -  using subset_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   11.89 +  using assms unfolding rel_fun_def
   11.90 +  using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
   11.91  
   11.92  lemma fSup_transfer [transfer_rule]:
   11.93    "bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup"
   11.94 -  using assms unfolding fun_rel_def
   11.95 +  using assms unfolding rel_fun_def
   11.96    apply clarify
   11.97    apply transfer'
   11.98 -  using Sup_fset_transfer[unfolded fun_rel_def] by blast
   11.99 +  using Sup_fset_transfer[unfolded rel_fun_def] by blast
  11.100  
  11.101  (* FIXME: add right_total_fInf_transfer *)
  11.102  
  11.103  lemma fInf_transfer [transfer_rule]:
  11.104    assumes "bi_unique A" and "bi_total A"
  11.105    shows "(rel_set (rel_fset A) ===> rel_fset A) Inf Inf"
  11.106 -  using assms unfolding fun_rel_def
  11.107 +  using assms unfolding rel_fun_def
  11.108    apply clarify
  11.109    apply transfer'
  11.110 -  using Inf_fset_transfer[unfolded fun_rel_def] by blast
  11.111 +  using Inf_fset_transfer[unfolded rel_fun_def] by blast
  11.112  
  11.113  lemma ffilter_transfer [transfer_rule]:
  11.114    assumes "bi_unique A"
  11.115    shows "((A ===> op=) ===> rel_fset A ===> rel_fset A) ffilter ffilter"
  11.116 -  using assms unfolding fun_rel_def
  11.117 -  using Lifting_Set.filter_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
  11.118 +  using assms unfolding rel_fun_def
  11.119 +  using Lifting_Set.filter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
  11.120  
  11.121  lemma card_transfer [transfer_rule]:
  11.122    "bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard"
  11.123 -  using assms unfolding fun_rel_def
  11.124 -  using card_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
  11.125 +  using assms unfolding rel_fun_def
  11.126 +  using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
  11.127  
  11.128  end
  11.129  
    12.1 --- a/src/HOL/Library/Float.thy	Thu Mar 06 15:29:18 2014 +0100
    12.2 +++ b/src/HOL/Library/Float.thy	Thu Mar 06 15:40:33 2014 +0100
    12.3 @@ -223,15 +223,15 @@
    12.4    done
    12.5  
    12.6  lemma transfer_numeral [transfer_rule]:
    12.7 -  "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
    12.8 -  unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
    12.9 +  "rel_fun (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
   12.10 +  unfolding rel_fun_def float.pcr_cr_eq  cr_float_def by simp
   12.11  
   12.12  lemma float_neg_numeral[simp]: "real (- numeral x :: float) = - numeral x"
   12.13    by simp
   12.14  
   12.15  lemma transfer_neg_numeral [transfer_rule]:
   12.16 -  "fun_rel (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
   12.17 -  unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
   12.18 +  "rel_fun (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
   12.19 +  unfolding rel_fun_def float.pcr_cr_eq cr_float_def by simp
   12.20  
   12.21  lemma
   12.22    shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
    13.1 --- a/src/HOL/Library/Mapping.thy	Thu Mar 06 15:29:18 2014 +0100
    13.2 +++ b/src/HOL/Library/Mapping.thy	Thu Mar 06 15:40:33 2014 +0100
    13.3 @@ -33,7 +33,7 @@
    13.4  definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None"
    13.5  
    13.6  lemma [transfer_rule]: "(rel_option A ===> op=) equal_None equal_None" 
    13.7 -unfolding fun_rel_def rel_option_iff equal_None_def by (auto split: option.split)
    13.8 +unfolding rel_fun_def rel_option_iff equal_None_def by (auto split: option.split)
    13.9  
   13.10  lemma dom_transfer:
   13.11    assumes [transfer_rule]: "bi_total A"
   13.12 @@ -55,7 +55,7 @@
   13.13  lemma bulkload_transfer: 
   13.14    "(list_all2 A ===> op= ===> rel_option A) 
   13.15      (\<lambda>xs k. if k < length xs then Some (xs ! k) else None) (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)"
   13.16 -unfolding fun_rel_def 
   13.17 +unfolding rel_fun_def 
   13.18  apply clarsimp 
   13.19  apply (erule list_all2_induct) 
   13.20    apply simp 
    14.1 --- a/src/HOL/Library/Multiset.thy	Thu Mar 06 15:29:18 2014 +0100
    14.2 +++ b/src/HOL/Library/Multiset.thy	Thu Mar 06 15:40:33 2014 +0100
    14.3 @@ -2289,7 +2289,7 @@
    14.4  interpretation lifting_syntax .
    14.5  
    14.6  lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of"
    14.7 -  unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
    14.8 +  unfolding set_of_def pcr_multiset_def cr_multiset_def rel_fun_def by auto
    14.9  
   14.10  end
   14.11  
    15.1 --- a/src/HOL/Library/Quotient_Set.thy	Thu Mar 06 15:29:18 2014 +0100
    15.2 +++ b/src/HOL/Library/Quotient_Set.thy	Thu Mar 06 15:40:33 2014 +0100
    15.3 @@ -50,7 +50,7 @@
    15.4  lemma collect_rsp[quot_respect]:
    15.5    assumes "Quotient3 R Abs Rep"
    15.6    shows "((R ===> op =) ===> rel_vset R) Collect Collect"
    15.7 -  by (intro fun_relI) (simp add: fun_rel_def rel_vset_def)
    15.8 +  by (intro rel_funI) (simp add: rel_fun_def rel_vset_def)
    15.9  
   15.10  lemma collect_prs[quot_preserve]:
   15.11    assumes "Quotient3 R Abs Rep"
   15.12 @@ -61,7 +61,7 @@
   15.13  lemma union_rsp[quot_respect]:
   15.14    assumes "Quotient3 R Abs Rep"
   15.15    shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<union> op \<union>"
   15.16 -  by (intro fun_relI) (simp add: rel_vset_def)
   15.17 +  by (intro rel_funI) (simp add: rel_vset_def)
   15.18  
   15.19  lemma union_prs[quot_preserve]:
   15.20    assumes "Quotient3 R Abs Rep"
   15.21 @@ -72,7 +72,7 @@
   15.22  lemma diff_rsp[quot_respect]:
   15.23    assumes "Quotient3 R Abs Rep"
   15.24    shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op - op -"
   15.25 -  by (intro fun_relI) (simp add: rel_vset_def)
   15.26 +  by (intro rel_funI) (simp add: rel_vset_def)
   15.27  
   15.28  lemma diff_prs[quot_preserve]:
   15.29    assumes "Quotient3 R Abs Rep"
   15.30 @@ -83,7 +83,7 @@
   15.31  lemma inter_rsp[quot_respect]:
   15.32    assumes "Quotient3 R Abs Rep"
   15.33    shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<inter> op \<inter>"
   15.34 -  by (intro fun_relI) (auto simp add: rel_vset_def)
   15.35 +  by (intro rel_funI) (auto simp add: rel_vset_def)
   15.36  
   15.37  lemma inter_prs[quot_preserve]:
   15.38    assumes "Quotient3 R Abs Rep"
   15.39 @@ -98,6 +98,6 @@
   15.40  
   15.41  lemma mem_rsp[quot_respect]:
   15.42    shows "(R ===> rel_vset R ===> op =) op \<in> op \<in>"
   15.43 -  by (intro fun_relI) (simp add: rel_vset_def)
   15.44 +  by (intro rel_funI) (simp add: rel_vset_def)
   15.45  
   15.46  end
    16.1 --- a/src/HOL/Library/Quotient_Syntax.thy	Thu Mar 06 15:29:18 2014 +0100
    16.2 +++ b/src/HOL/Library/Quotient_Syntax.thy	Thu Mar 06 15:40:33 2014 +0100
    16.3 @@ -11,6 +11,6 @@
    16.4  notation
    16.5    rel_conj (infixr "OOO" 75) and
    16.6    map_fun (infixr "--->" 55) and
    16.7 -  fun_rel (infixr "===>" 55)
    16.8 +  rel_fun (infixr "===>" 55)
    16.9  
   16.10  end
    17.1 --- a/src/HOL/Lifting.thy	Thu Mar 06 15:29:18 2014 +0100
    17.2 +++ b/src/HOL/Lifting.thy	Thu Mar 06 15:40:33 2014 +0100
    17.3 @@ -52,7 +52,7 @@
    17.4    assumes [transfer_rule]: "right_total B"
    17.5    assumes [transfer_rule]: "bi_unique A"
    17.6    shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
    17.7 -using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def
    17.8 +using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
    17.9  by metis
   17.10  
   17.11  lemma bi_unique_iff: "bi_unique A = (right_unique A \<and> left_unique A)"
   17.12 @@ -69,7 +69,7 @@
   17.13  
   17.14  lemma left_total_fun:
   17.15    "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
   17.16 -  unfolding left_total_def fun_rel_def
   17.17 +  unfolding left_total_def rel_fun_def
   17.18    apply (rule allI, rename_tac f)
   17.19    apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
   17.20    apply clarify
   17.21 @@ -83,7 +83,7 @@
   17.22  
   17.23  lemma left_unique_fun:
   17.24    "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
   17.25 -  unfolding left_total_def left_unique_def fun_rel_def
   17.26 +  unfolding left_total_def left_unique_def rel_fun_def
   17.27    by (clarify, rule ext, fast)
   17.28  
   17.29  lemma left_total_eq: "left_total op=" unfolding left_total_def by blast
   17.30 @@ -242,7 +242,7 @@
   17.31    assumes 2: "Quotient R2 abs2 rep2 T2"
   17.32    shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
   17.33    using assms unfolding Quotient_alt_def2
   17.34 -  unfolding fun_rel_def fun_eq_iff map_fun_apply
   17.35 +  unfolding rel_fun_def fun_eq_iff map_fun_apply
   17.36    by (safe, metis+)
   17.37  
   17.38  lemma apply_rsp:
   17.39 @@ -250,12 +250,12 @@
   17.40    assumes q: "Quotient R1 Abs1 Rep1 T1"
   17.41    and     a: "(R1 ===> R2) f g" "R1 x y"
   17.42    shows "R2 (f x) (g y)"
   17.43 -  using a by (auto elim: fun_relE)
   17.44 +  using a by (auto elim: rel_funE)
   17.45  
   17.46  lemma apply_rsp':
   17.47    assumes a: "(R1 ===> R2) f g" "R1 x y"
   17.48    shows "R2 (f x) (g y)"
   17.49 -  using a by (auto elim: fun_relE)
   17.50 +  using a by (auto elim: rel_funE)
   17.51  
   17.52  lemma apply_rsp'':
   17.53    assumes "Quotient R Abs Rep T"
   17.54 @@ -296,12 +296,12 @@
   17.55    shows "x = y"
   17.56  using assms by (simp add: invariant_def)
   17.57  
   17.58 -lemma fun_rel_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
   17.59 -unfolding invariant_def fun_rel_def by auto
   17.60 +lemma rel_fun_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
   17.61 +unfolding invariant_def rel_fun_def by auto
   17.62  
   17.63 -lemma fun_rel_invariant_rel:
   17.64 +lemma rel_fun_invariant_rel:
   17.65    shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
   17.66 -by (auto simp add: invariant_def fun_rel_def)
   17.67 +by (auto simp add: invariant_def rel_fun_def)
   17.68  
   17.69  lemma invariant_same_args:
   17.70    shows "invariant P x x \<equiv> P x"
   17.71 @@ -376,7 +376,7 @@
   17.72    using 1 unfolding Quotient_alt_def right_total_def by metis
   17.73  
   17.74  lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)"
   17.75 -  using 1 unfolding Quotient_alt_def fun_rel_def by simp
   17.76 +  using 1 unfolding Quotient_alt_def rel_fun_def by simp
   17.77  
   17.78  lemma Quotient_abs_induct:
   17.79    assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
   17.80 @@ -395,7 +395,7 @@
   17.81    using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
   17.82  
   17.83  lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
   17.84 -  using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
   17.85 +  using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp
   17.86  
   17.87  lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
   17.88    using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
   17.89 @@ -432,7 +432,7 @@
   17.90    by blast
   17.91  
   17.92  lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
   17.93 -  unfolding fun_rel_def T_def by simp
   17.94 +  unfolding rel_fun_def T_def by simp
   17.95  
   17.96  end
   17.97  
   17.98 @@ -557,10 +557,10 @@
   17.99    assumes "A \<ge> C"
  17.100    assumes "B \<le> D"
  17.101    shows   "(A ===> B) \<le> (C ===> D)"
  17.102 -using assms unfolding fun_rel_def by blast
  17.103 +using assms unfolding rel_fun_def by blast
  17.104  
  17.105  lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))"
  17.106 -unfolding OO_def fun_rel_def by blast
  17.107 +unfolding OO_def rel_fun_def by blast
  17.108  
  17.109  lemma functional_relation: "right_unique R \<Longrightarrow> left_total R \<Longrightarrow> \<forall>x. \<exists>!y. R x y"
  17.110  unfolding right_unique_def left_total_def by blast
  17.111 @@ -573,7 +573,7 @@
  17.112  assumes 2: "right_unique R'" "left_total R'"
  17.113  shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S')) "
  17.114    using functional_relation[OF 2] functional_converse_relation[OF 1]
  17.115 -  unfolding fun_rel_def OO_def
  17.116 +  unfolding rel_fun_def OO_def
  17.117    apply clarify
  17.118    apply (subst all_comm)
  17.119    apply (subst all_conj_distrib[symmetric])
  17.120 @@ -585,7 +585,7 @@
  17.121  assumes 2: "left_unique S'" "right_total S'"
  17.122  shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S'))"
  17.123    using functional_converse_relation[OF 2] functional_relation[OF 1]
  17.124 -  unfolding fun_rel_def OO_def
  17.125 +  unfolding rel_fun_def OO_def
  17.126    apply clarify
  17.127    apply (subst all_comm)
  17.128    apply (subst all_conj_distrib[symmetric])
  17.129 @@ -599,7 +599,7 @@
  17.130    assumes "(R ===> op=) P P'"
  17.131    assumes "Domainp R = P''"
  17.132    shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
  17.133 -using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def
  17.134 +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def invariant_def
  17.135  fun_eq_iff by blast
  17.136  
  17.137  lemma composed_equiv_rel_eq_invariant:
  17.138 @@ -615,7 +615,7 @@
  17.139    assumes "(A ===> op=) P' P"
  17.140    shows "Domainp (A OO B) = P'"
  17.141  using assms
  17.142 -unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def fun_rel_def 
  17.143 +unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def 
  17.144  by (fast intro: fun_eq_iff)
  17.145  
  17.146  lemma pcr_Domainp_par:
  17.147 @@ -623,7 +623,7 @@
  17.148  assumes "Domainp A = P1"
  17.149  assumes "(A ===> op=) P2' P2"
  17.150  shows "Domainp (A OO B) = (inf P1 P2')"
  17.151 -using assms unfolding fun_rel_def Domainp_iff[abs_def] OO_def
  17.152 +using assms unfolding rel_fun_def Domainp_iff[abs_def] OO_def
  17.153  by (fast intro: fun_eq_iff)
  17.154  
  17.155  definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool"
    18.1 --- a/src/HOL/Lifting_Option.thy	Thu Mar 06 15:29:18 2014 +0100
    18.2 +++ b/src/HOL/Lifting_Option.thy	Thu Mar 06 15:40:33 2014 +0100
    18.3 @@ -86,11 +86,11 @@
    18.4    by (rule option.rel_inject)
    18.5  
    18.6  lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
    18.7 -  unfolding fun_rel_def by simp
    18.8 +  unfolding rel_fun_def by simp
    18.9  
   18.10  lemma case_option_transfer [transfer_rule]:
   18.11    "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
   18.12 -  unfolding fun_rel_def split_option_all by simp
   18.13 +  unfolding rel_fun_def split_option_all by simp
   18.14  
   18.15  lemma map_option_transfer [transfer_rule]:
   18.16    "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
   18.17 @@ -99,7 +99,7 @@
   18.18  lemma option_bind_transfer [transfer_rule]:
   18.19    "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
   18.20      Option.bind Option.bind"
   18.21 -  unfolding fun_rel_def split_option_all by simp
   18.22 +  unfolding rel_fun_def split_option_all by simp
   18.23  
   18.24  end
   18.25  
    19.1 --- a/src/HOL/Lifting_Product.thy	Thu Mar 06 15:29:18 2014 +0100
    19.2 +++ b/src/HOL/Lifting_Product.thy	Thu Mar 06 15:40:33 2014 +0100
    19.3 @@ -80,17 +80,17 @@
    19.4  interpretation lifting_syntax .
    19.5  
    19.6  lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
    19.7 -  unfolding fun_rel_def rel_prod_def by simp
    19.8 +  unfolding rel_fun_def rel_prod_def by simp
    19.9  
   19.10  lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
   19.11 -  unfolding fun_rel_def rel_prod_def by simp
   19.12 +  unfolding rel_fun_def rel_prod_def by simp
   19.13  
   19.14  lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
   19.15 -  unfolding fun_rel_def rel_prod_def by simp
   19.16 +  unfolding rel_fun_def rel_prod_def by simp
   19.17  
   19.18  lemma case_prod_transfer [transfer_rule]:
   19.19    "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
   19.20 -  unfolding fun_rel_def rel_prod_def by simp
   19.21 +  unfolding rel_fun_def rel_prod_def by simp
   19.22  
   19.23  lemma curry_transfer [transfer_rule]:
   19.24    "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
   19.25 @@ -104,7 +104,7 @@
   19.26  lemma rel_prod_transfer [transfer_rule]:
   19.27    "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
   19.28      rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
   19.29 -  unfolding fun_rel_def by auto
   19.30 +  unfolding rel_fun_def by auto
   19.31  
   19.32  end
   19.33  
    20.1 --- a/src/HOL/Lifting_Set.thy	Thu Mar 06 15:29:18 2014 +0100
    20.2 +++ b/src/HOL/Lifting_Set.thy	Thu Mar 06 15:40:33 2014 +0100
    20.3 @@ -109,19 +109,19 @@
    20.4  
    20.5  lemma insert_transfer [transfer_rule]:
    20.6    "(A ===> rel_set A ===> rel_set A) insert insert"
    20.7 -  unfolding fun_rel_def rel_set_def by auto
    20.8 +  unfolding rel_fun_def rel_set_def by auto
    20.9  
   20.10  lemma union_transfer [transfer_rule]:
   20.11    "(rel_set A ===> rel_set A ===> rel_set A) union union"
   20.12 -  unfolding fun_rel_def rel_set_def by auto
   20.13 +  unfolding rel_fun_def rel_set_def by auto
   20.14  
   20.15  lemma Union_transfer [transfer_rule]:
   20.16    "(rel_set (rel_set A) ===> rel_set A) Union Union"
   20.17 -  unfolding fun_rel_def rel_set_def by simp fast
   20.18 +  unfolding rel_fun_def rel_set_def by simp fast
   20.19  
   20.20  lemma image_transfer [transfer_rule]:
   20.21    "((A ===> B) ===> rel_set A ===> rel_set B) image image"
   20.22 -  unfolding fun_rel_def rel_set_def by simp fast
   20.23 +  unfolding rel_fun_def rel_set_def by simp fast
   20.24  
   20.25  lemma UNION_transfer [transfer_rule]:
   20.26    "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
   20.27 @@ -129,15 +129,15 @@
   20.28  
   20.29  lemma Ball_transfer [transfer_rule]:
   20.30    "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
   20.31 -  unfolding rel_set_def fun_rel_def by fast
   20.32 +  unfolding rel_set_def rel_fun_def by fast
   20.33  
   20.34  lemma Bex_transfer [transfer_rule]:
   20.35    "(rel_set A ===> (A ===> op =) ===> op =) Bex Bex"
   20.36 -  unfolding rel_set_def fun_rel_def by fast
   20.37 +  unfolding rel_set_def rel_fun_def by fast
   20.38  
   20.39  lemma Pow_transfer [transfer_rule]:
   20.40    "(rel_set A ===> rel_set (rel_set A)) Pow Pow"
   20.41 -  apply (rule fun_relI, rename_tac X Y, rule rel_setI)
   20.42 +  apply (rule rel_funI, rename_tac X Y, rule rel_setI)
   20.43    apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp)
   20.44    apply (simp add: rel_set_def, fast)
   20.45    apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp)
   20.46 @@ -147,16 +147,16 @@
   20.47  lemma rel_set_transfer [transfer_rule]:
   20.48    "((A ===> B ===> op =) ===> rel_set A ===> rel_set B ===> op =)
   20.49      rel_set rel_set"
   20.50 -  unfolding fun_rel_def rel_set_def by fast
   20.51 +  unfolding rel_fun_def rel_set_def by fast
   20.52  
   20.53  lemma SUPR_parametric [transfer_rule]:
   20.54    "(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
   20.55 -proof(rule fun_relI)+
   20.56 +proof(rule rel_funI)+
   20.57    fix A B f and g :: "'b \<Rightarrow> 'c"
   20.58    assume AB: "rel_set R A B"
   20.59      and fg: "(R ===> op =) f g"
   20.60    show "SUPR A f = SUPR B g"
   20.61 -    by(rule SUPR_eq)(auto 4 4 dest: rel_setD1[OF AB] rel_setD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
   20.62 +    by(rule SUPR_eq)(auto 4 4 dest: rel_setD1[OF AB] rel_setD2[OF AB] rel_funD[OF fg] intro: rev_bexI)
   20.63  qed
   20.64  
   20.65  lemma bind_transfer [transfer_rule]:
   20.66 @@ -168,27 +168,27 @@
   20.67  lemma member_transfer [transfer_rule]:
   20.68    assumes "bi_unique A"
   20.69    shows "(A ===> rel_set A ===> op =) (op \<in>) (op \<in>)"
   20.70 -  using assms unfolding fun_rel_def rel_set_def bi_unique_def by fast
   20.71 +  using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast
   20.72  
   20.73  lemma right_total_Collect_transfer[transfer_rule]:
   20.74    assumes "right_total A"
   20.75    shows "((A ===> op =) ===> rel_set A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect"
   20.76 -  using assms unfolding right_total_def rel_set_def fun_rel_def Domainp_iff by fast
   20.77 +  using assms unfolding right_total_def rel_set_def rel_fun_def Domainp_iff by fast
   20.78  
   20.79  lemma Collect_transfer [transfer_rule]:
   20.80    assumes "bi_total A"
   20.81    shows "((A ===> op =) ===> rel_set A) Collect Collect"
   20.82 -  using assms unfolding fun_rel_def rel_set_def bi_total_def by fast
   20.83 +  using assms unfolding rel_fun_def rel_set_def bi_total_def by fast
   20.84  
   20.85  lemma inter_transfer [transfer_rule]:
   20.86    assumes "bi_unique A"
   20.87    shows "(rel_set A ===> rel_set A ===> rel_set A) inter inter"
   20.88 -  using assms unfolding fun_rel_def rel_set_def bi_unique_def by fast
   20.89 +  using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast
   20.90  
   20.91  lemma Diff_transfer [transfer_rule]:
   20.92    assumes "bi_unique A"
   20.93    shows "(rel_set A ===> rel_set A ===> rel_set A) (op -) (op -)"
   20.94 -  using assms unfolding fun_rel_def rel_set_def bi_unique_def
   20.95 +  using assms unfolding rel_fun_def rel_set_def bi_unique_def
   20.96    unfolding Ball_def Bex_def Diff_eq
   20.97    by (safe, simp, metis, simp, metis)
   20.98  
   20.99 @@ -232,7 +232,7 @@
  20.100  lemma filter_transfer [transfer_rule]:
  20.101    assumes [transfer_rule]: "bi_unique A"
  20.102    shows "((A ===> op=) ===> rel_set A ===> rel_set A) Set.filter Set.filter"
  20.103 -  unfolding Set.filter_def[abs_def] fun_rel_def rel_set_def by blast
  20.104 +  unfolding Set.filter_def[abs_def] rel_fun_def rel_set_def by blast
  20.105  
  20.106  lemma bi_unique_rel_set_lemma:
  20.107    assumes "bi_unique R" and "rel_set R X Y"
  20.108 @@ -270,12 +270,12 @@
  20.109  
  20.110  lemma finite_transfer [transfer_rule]:
  20.111    "bi_unique A \<Longrightarrow> (rel_set A ===> op =) finite finite"
  20.112 -  by (rule fun_relI, erule (1) bi_unique_rel_set_lemma,
  20.113 +  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma,
  20.114      auto dest: finite_imageD)
  20.115  
  20.116  lemma card_transfer [transfer_rule]:
  20.117    "bi_unique A \<Longrightarrow> (rel_set A ===> op =) card card"
  20.118 -  by (rule fun_relI, erule (1) bi_unique_rel_set_lemma, simp add: card_image)
  20.119 +  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma, simp add: card_image)
  20.120  
  20.121  lemma vimage_parametric [transfer_rule]:
  20.122    assumes [transfer_rule]: "bi_total A" "bi_unique B"
  20.123 @@ -285,7 +285,7 @@
  20.124  lemma setsum_parametric [transfer_rule]:
  20.125    assumes "bi_unique A"
  20.126    shows "((A ===> op =) ===> rel_set A ===> op =) setsum setsum"
  20.127 -proof(rule fun_relI)+
  20.128 +proof(rule rel_funI)+
  20.129    fix f :: "'a \<Rightarrow> 'c" and g S T
  20.130    assume fg: "(A ===> op =) f g"
  20.131      and ST: "rel_set A S T"
  20.132 @@ -313,7 +313,7 @@
  20.133      assume "t \<in> T"
  20.134      with ST obtain s where "A s t" "s \<in> S" by(auto dest: rel_setD2)
  20.135      hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
  20.136 -    moreover from fg `A s t` have "f s = g t" by(rule fun_relD)
  20.137 +    moreover from fg `A s t` have "f s = g t" by(rule rel_funD)
  20.138      ultimately show "g t = f (?f t)" by simp
  20.139    qed
  20.140  qed
    21.1 --- a/src/HOL/Lifting_Sum.thy	Thu Mar 06 15:29:18 2014 +0100
    21.2 +++ b/src/HOL/Lifting_Sum.thy	Thu Mar 06 15:40:33 2014 +0100
    21.3 @@ -70,14 +70,14 @@
    21.4  interpretation lifting_syntax .
    21.5  
    21.6  lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
    21.7 -  unfolding fun_rel_def by simp
    21.8 +  unfolding rel_fun_def by simp
    21.9  
   21.10  lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
   21.11 -  unfolding fun_rel_def by simp
   21.12 +  unfolding rel_fun_def by simp
   21.13  
   21.14  lemma case_sum_transfer [transfer_rule]:
   21.15    "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
   21.16 -  unfolding fun_rel_def rel_sum_def by (simp split: sum.split)
   21.17 +  unfolding rel_fun_def rel_sum_def by (simp split: sum.split)
   21.18  
   21.19  end
   21.20  
    22.1 --- a/src/HOL/List.thy	Thu Mar 06 15:29:18 2014 +0100
    22.2 +++ b/src/HOL/List.thy	Thu Mar 06 15:40:33 2014 +0100
    22.3 @@ -6713,17 +6713,17 @@
    22.4  
    22.5  lemma Cons_transfer [transfer_rule]:
    22.6    "(A ===> list_all2 A ===> list_all2 A) Cons Cons"
    22.7 -  unfolding fun_rel_def by simp
    22.8 +  unfolding rel_fun_def by simp
    22.9  
   22.10  lemma case_list_transfer [transfer_rule]:
   22.11    "(B ===> (A ===> list_all2 A ===> B) ===> list_all2 A ===> B)
   22.12      case_list case_list"
   22.13 -  unfolding fun_rel_def by (simp split: list.split)
   22.14 +  unfolding rel_fun_def by (simp split: list.split)
   22.15  
   22.16  lemma rec_list_transfer [transfer_rule]:
   22.17    "(B ===> (A ===> list_all2 A ===> B ===> B) ===> list_all2 A ===> B)
   22.18      rec_list rec_list"
   22.19 -  unfolding fun_rel_def by (clarify, erule list_all2_induct, simp_all)
   22.20 +  unfolding rel_fun_def by (clarify, erule list_all2_induct, simp_all)
   22.21  
   22.22  lemma tl_transfer [transfer_rule]:
   22.23    "(list_all2 A ===> list_all2 A) tl tl"
   22.24 @@ -6731,7 +6731,7 @@
   22.25  
   22.26  lemma butlast_transfer [transfer_rule]:
   22.27    "(list_all2 A ===> list_all2 A) butlast butlast"
   22.28 -  by (rule fun_relI, erule list_all2_induct, auto)
   22.29 +  by (rule rel_funI, erule list_all2_induct, auto)
   22.30  
   22.31  lemma set_transfer [transfer_rule]:
   22.32    "(list_all2 A ===> rel_set A) set set"
   22.33 @@ -6836,7 +6836,7 @@
   22.34  lemma remdups_adj_transfer [transfer_rule]:
   22.35    assumes [transfer_rule]: "bi_unique A"
   22.36    shows "(list_all2 A ===> list_all2 A) remdups_adj remdups_adj"
   22.37 -  proof (rule fun_relI, erule list_all2_induct)
   22.38 +  proof (rule rel_funI, erule list_all2_induct)
   22.39    qed (auto simp: remdups_adj_Cons assms[unfolded bi_unique_def] split: list.splits)
   22.40  
   22.41  lemma replicate_transfer [transfer_rule]:
   22.42 @@ -6874,7 +6874,7 @@
   22.43  
   22.44  lemma lists_transfer [transfer_rule]:
   22.45    "(rel_set A ===> rel_set (list_all2 A)) lists lists"
   22.46 -  apply (rule fun_relI, rule rel_setI)
   22.47 +  apply (rule rel_funI, rule rel_setI)
   22.48    apply (erule lists.induct, simp)
   22.49    apply (simp only: rel_set_def list_all2_Cons1, metis lists.Cons)
   22.50    apply (erule lists.induct, simp)
   22.51 @@ -6884,7 +6884,7 @@
   22.52  lemma set_Cons_transfer [transfer_rule]:
   22.53    "(rel_set A ===> rel_set (list_all2 A) ===> rel_set (list_all2 A))
   22.54      set_Cons set_Cons"
   22.55 -  unfolding fun_rel_def rel_set_def set_Cons_def
   22.56 +  unfolding rel_fun_def rel_set_def set_Cons_def
   22.57    apply safe
   22.58    apply (simp add: list_all2_Cons1, fast)
   22.59    apply (simp add: list_all2_Cons2, fast)
   22.60 @@ -6896,7 +6896,7 @@
   22.61  
   22.62  lemma null_transfer [transfer_rule]:
   22.63    "(list_all2 A ===> op =) List.null List.null"
   22.64 -  unfolding fun_rel_def List.null_def by auto
   22.65 +  unfolding rel_fun_def List.null_def by auto
   22.66  
   22.67  lemma list_all_transfer [transfer_rule]:
   22.68    "((A ===> op =) ===> list_all2 A ===> op =) list_all list_all"
   22.69 @@ -6908,9 +6908,9 @@
   22.70  
   22.71  lemma splice_transfer [transfer_rule]:
   22.72    "(list_all2 A ===> list_all2 A ===> list_all2 A) splice splice"
   22.73 -  apply (rule fun_relI, erule list_all2_induct, simp add: fun_rel_def, simp)
   22.74 -  apply (rule fun_relI)
   22.75 -  apply (erule_tac xs=x in list_all2_induct, simp, simp add: fun_rel_def)
   22.76 +  apply (rule rel_funI, erule list_all2_induct, simp add: rel_fun_def, simp)
   22.77 +  apply (rule rel_funI)
   22.78 +  apply (erule_tac xs=x in list_all2_induct, simp, simp add: rel_fun_def)
   22.79    done
   22.80  
   22.81  lemma listsum_transfer[transfer_rule]:
    23.1 --- a/src/HOL/Quotient.thy	Thu Mar 06 15:29:18 2014 +0100
    23.2 +++ b/src/HOL/Quotient.thy	Thu Mar 06 15:40:33 2014 +0100
    23.3 @@ -146,7 +146,7 @@
    23.4      using q1 q2 by (simp add: Quotient3_def fun_eq_iff)
    23.5    moreover
    23.6    have "\<And>a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
    23.7 -    by (rule fun_relI)
    23.8 +    by (rule rel_funI)
    23.9        (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
   23.10          simp (no_asm) add: Quotient3_def, simp)
   23.11    
   23.12 @@ -157,17 +157,17 @@
   23.13          (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
   23.14    proof -
   23.15      
   23.16 -    have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding fun_rel_def
   23.17 +    have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding rel_fun_def
   23.18        using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
   23.19        by (metis (full_types) part_equivp_def)
   23.20 -    moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding fun_rel_def
   23.21 +    moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding rel_fun_def
   23.22        using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
   23.23        by (metis (full_types) part_equivp_def)
   23.24      moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 ---> abs2) r  = (rep1 ---> abs2) s"
   23.25 -      apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
   23.26 +      apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
   23.27      moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   23.28          (rep1 ---> abs2) r  = (rep1 ---> abs2) s) \<Longrightarrow> (R1 ===> R2) r s"
   23.29 -      apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 
   23.30 +      apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 
   23.31      by (metis map_fun_apply)
   23.32    
   23.33      ultimately show ?thesis by blast
   23.34 @@ -204,7 +204,7 @@
   23.35    assumes q: "Quotient3 R1 Abs1 Rep1"
   23.36    and     a: "(R1 ===> R2) f g" "R1 x y"
   23.37    shows "R2 (f x) (g y)"
   23.38 -  using a by (auto elim: fun_relE)
   23.39 +  using a by (auto elim: rel_funE)
   23.40  
   23.41  lemma apply_rspQ3'':
   23.42    assumes "Quotient3 R Abs Rep"
   23.43 @@ -261,7 +261,7 @@
   23.44    apply(rule iffI)
   23.45    apply(rule allI)
   23.46    apply(drule_tac x="\<lambda>y. f x" in bspec)
   23.47 -  apply(simp add: in_respects fun_rel_def)
   23.48 +  apply(simp add: in_respects rel_fun_def)
   23.49    apply(rule impI)
   23.50    using a equivp_reflp_symp_transp[of "R2"]
   23.51    apply (auto elim: equivpE reflpE)
   23.52 @@ -273,7 +273,7 @@
   23.53    apply(auto)
   23.54    apply(rule_tac x="\<lambda>y. f x" in bexI)
   23.55    apply(simp)
   23.56 -  apply(simp add: Respects_def in_respects fun_rel_def)
   23.57 +  apply(simp add: Respects_def in_respects rel_fun_def)
   23.58    apply(rule impI)
   23.59    using a equivp_reflp_symp_transp[of "R2"]
   23.60    apply (auto elim: equivpE reflpE)
   23.61 @@ -326,10 +326,10 @@
   23.62    assumes q: "Quotient3 R1 Abs1 Rep1"
   23.63    and     a: "(R1 ===> R2) f g"
   23.64    shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
   23.65 -  apply (auto simp add: Babs_def in_respects fun_rel_def)
   23.66 +  apply (auto simp add: Babs_def in_respects rel_fun_def)
   23.67    apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   23.68 -  using a apply (simp add: Babs_def fun_rel_def)
   23.69 -  apply (simp add: in_respects fun_rel_def)
   23.70 +  using a apply (simp add: Babs_def rel_fun_def)
   23.71 +  apply (simp add: in_respects rel_fun_def)
   23.72    using Quotient3_rel[OF q]
   23.73    by metis
   23.74  
   23.75 @@ -349,7 +349,7 @@
   23.76    shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
   23.77    apply(rule iffI)
   23.78    apply(simp_all only: babs_rsp[OF q])
   23.79 -  apply(auto simp add: Babs_def fun_rel_def)
   23.80 +  apply(auto simp add: Babs_def rel_fun_def)
   23.81    apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   23.82    apply(metis Babs_def)
   23.83    apply (simp add: in_respects)
   23.84 @@ -367,17 +367,17 @@
   23.85  lemma ball_rsp:
   23.86    assumes a: "(R ===> (op =)) f g"
   23.87    shows "Ball (Respects R) f = Ball (Respects R) g"
   23.88 -  using a by (auto simp add: Ball_def in_respects elim: fun_relE)
   23.89 +  using a by (auto simp add: Ball_def in_respects elim: rel_funE)
   23.90  
   23.91  lemma bex_rsp:
   23.92    assumes a: "(R ===> (op =)) f g"
   23.93    shows "(Bex (Respects R) f = Bex (Respects R) g)"
   23.94 -  using a by (auto simp add: Bex_def in_respects elim: fun_relE)
   23.95 +  using a by (auto simp add: Bex_def in_respects elim: rel_funE)
   23.96  
   23.97  lemma bex1_rsp:
   23.98    assumes a: "(R ===> (op =)) f g"
   23.99    shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
  23.100 -  using a by (auto elim: fun_relE simp add: Ex1_def in_respects) 
  23.101 +  using a by (auto elim: rel_funE simp add: Ex1_def in_respects) 
  23.102  
  23.103  (* 2 lemmas needed for cleaning of quantifiers *)
  23.104  lemma all_prs:
  23.105 @@ -440,7 +440,7 @@
  23.106  lemma bex1_rel_rsp:
  23.107    assumes a: "Quotient3 R absf repf"
  23.108    shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
  23.109 -  apply (simp add: fun_rel_def)
  23.110 +  apply (simp add: rel_fun_def)
  23.111    apply clarify
  23.112    apply rule
  23.113    apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
  23.114 @@ -519,7 +519,7 @@
  23.115  lemma quot_rel_rsp:
  23.116    assumes a: "Quotient3 R Abs Rep"
  23.117    shows "(R ===> R ===> op =) R R"
  23.118 -  apply(rule fun_relI)+
  23.119 +  apply(rule rel_funI)+
  23.120    apply(rule equals_rsp[OF a])
  23.121    apply(assumption)+
  23.122    done
  23.123 @@ -536,7 +536,7 @@
  23.124  lemma o_rsp:
  23.125    "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
  23.126    "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
  23.127 -  by (force elim: fun_relE)+
  23.128 +  by (force elim: rel_funE)+
  23.129  
  23.130  lemma cond_prs:
  23.131    assumes a: "Quotient3 R absf repf"
  23.132 @@ -563,7 +563,7 @@
  23.133  
  23.134  lemma let_rsp:
  23.135    shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
  23.136 -  by (force elim: fun_relE)
  23.137 +  by (force elim: rel_funE)
  23.138  
  23.139  lemma id_rsp:
  23.140    shows "(R ===> R) id id"
  23.141 @@ -759,7 +759,7 @@
  23.142  ML_file "Tools/Quotient/quotient_info.ML"
  23.143  setup Quotient_Info.setup
  23.144  
  23.145 -declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]]
  23.146 +declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
  23.147  
  23.148  lemmas [quot_thm] = fun_quotient3
  23.149  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
    24.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Thu Mar 06 15:29:18 2014 +0100
    24.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Thu Mar 06 15:40:33 2014 +0100
    24.3 @@ -403,7 +403,7 @@
    24.4  
    24.5  lemma Cons_rsp2 [quot_respect]:
    24.6    shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
    24.7 -  apply (auto intro!: fun_relI)
    24.8 +  apply (auto intro!: rel_funI)
    24.9    apply (rule_tac b="x # b" in relcomppI)
   24.10    apply auto
   24.11    apply (rule_tac b="x # ba" in relcomppI)
   24.12 @@ -459,24 +459,24 @@
   24.13  lemma compositional_rsp3:
   24.14    assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
   24.15    shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
   24.16 -  by (auto intro!: fun_relI)
   24.17 -     (metis (full_types) assms fun_relE relcomppI)
   24.18 +  by (auto intro!: rel_funI)
   24.19 +     (metis (full_types) assms rel_funE relcomppI)
   24.20  
   24.21  lemma append_rsp2 [quot_respect]:
   24.22    "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
   24.23    by (intro compositional_rsp3)
   24.24 -     (auto intro!: fun_relI simp add: append_rsp2_pre)
   24.25 +     (auto intro!: rel_funI simp add: append_rsp2_pre)
   24.26  
   24.27  lemma map_rsp2 [quot_respect]:
   24.28    "((op \<approx> ===> op \<approx>) ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) map map"
   24.29 -proof (auto intro!: fun_relI)
   24.30 +proof (auto intro!: rel_funI)
   24.31    fix f f' :: "'a list \<Rightarrow> 'b list"
   24.32    fix xa ya x y :: "'a list list"
   24.33    assume fs: "(op \<approx> ===> op \<approx>) f f'" and x: "list_all2 op \<approx> xa x" and xy: "set x = set y" and y: "list_all2 op \<approx> y ya"
   24.34    have a: "(list_all2 op \<approx>) (map f xa) (map f x)"
   24.35      using x
   24.36      by (induct xa x rule: list_induct2')
   24.37 -       (simp_all, metis fs fun_relE list_eq_def)
   24.38 +       (simp_all, metis fs rel_funE list_eq_def)
   24.39    have b: "set (map f x) = set (map f y)"
   24.40      using xy fs
   24.41      by (induct x y rule: list_induct2')
    25.1 --- a/src/HOL/Real.thy	Thu Mar 06 15:29:18 2014 +0100
    25.2 +++ b/src/HOL/Real.thy	Thu Mar 06 15:40:33 2014 +0100
    25.3 @@ -389,7 +389,7 @@
    25.4  lemma eq_Real:
    25.5    "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
    25.6    using real.rel_eq_transfer
    25.7 -  unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp
    25.8 +  unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp
    25.9  
   25.10  lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy"
   25.11  by (simp add: real.domain_eq realrel_def)
   25.12 @@ -445,13 +445,13 @@
   25.13    assumes X: "cauchy X" and Y: "cauchy Y"
   25.14    shows "Real X + Real Y = Real (\<lambda>n. X n + Y n)"
   25.15    using assms plus_real.transfer
   25.16 -  unfolding cr_real_eq fun_rel_def by simp
   25.17 +  unfolding cr_real_eq rel_fun_def by simp
   25.18  
   25.19  lemma minus_Real:
   25.20    assumes X: "cauchy X"
   25.21    shows "- Real X = Real (\<lambda>n. - X n)"
   25.22    using assms uminus_real.transfer
   25.23 -  unfolding cr_real_eq fun_rel_def by simp
   25.24 +  unfolding cr_real_eq rel_fun_def by simp
   25.25  
   25.26  lemma diff_Real:
   25.27    assumes X: "cauchy X" and Y: "cauchy Y"
   25.28 @@ -463,14 +463,14 @@
   25.29    assumes X: "cauchy X" and Y: "cauchy Y"
   25.30    shows "Real X * Real Y = Real (\<lambda>n. X n * Y n)"
   25.31    using assms times_real.transfer
   25.32 -  unfolding cr_real_eq fun_rel_def by simp
   25.33 +  unfolding cr_real_eq rel_fun_def by simp
   25.34  
   25.35  lemma inverse_Real:
   25.36    assumes X: "cauchy X"
   25.37    shows "inverse (Real X) =
   25.38      (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
   25.39    using assms inverse_real.transfer zero_real.transfer
   25.40 -  unfolding cr_real_eq fun_rel_def by (simp split: split_if_asm, metis)
   25.41 +  unfolding cr_real_eq rel_fun_def by (simp split: split_if_asm, metis)
   25.42  
   25.43  instance proof
   25.44    fix a b c :: real
   25.45 @@ -546,7 +546,7 @@
   25.46    assumes X: "cauchy X"
   25.47    shows "positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"
   25.48    using assms positive.transfer
   25.49 -  unfolding cr_real_eq fun_rel_def by simp
   25.50 +  unfolding cr_real_eq rel_fun_def by simp
   25.51  
   25.52  lemma positive_zero: "\<not> positive 0"
   25.53    by transfer auto
    26.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Mar 06 15:29:18 2014 +0100
    26.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Mar 06 15:40:33 2014 +0100
    26.3 @@ -1260,12 +1260,12 @@
    26.4  
    26.5          fun mk_map_transfer () =
    26.6            let
    26.7 -            val rels = map2 mk_fun_rel transfer_domRs transfer_ranRs;
    26.8 -            val rel = mk_fun_rel
    26.9 +            val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
   26.10 +            val rel = mk_rel_fun
   26.11                (Term.list_comb (mk_bnf_rel transfer_domRTs CA' CB1, transfer_domRs))
   26.12                (Term.list_comb (mk_bnf_rel transfer_ranRTs CB' CB2, transfer_ranRs));
   26.13              val concl = HOLogic.mk_Trueprop
   26.14 -              (fold_rev mk_fun_rel rels rel $ bnf_map_AsBs $ mk_bnf_map B1Ts B2Ts);
   26.15 +              (fold_rev mk_rel_fun rels rel $ bnf_map_AsBs $ mk_bnf_map B1Ts B2Ts);
   26.16            in
   26.17              Goal.prove_sorry lthy [] []
   26.18                (fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
    27.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Mar 06 15:29:18 2014 +0100
    27.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Mar 06 15:40:33 2014 +0100
    27.3 @@ -195,8 +195,8 @@
    27.4            @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
    27.5        set_maps;
    27.6    in
    27.7 -    REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN
    27.8 -    unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
    27.9 +    REPEAT_DETERM_N n (HEADGOAL (rtac @{thm rel_funI})) THEN
   27.10 +    unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
   27.11      HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
   27.12        rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
   27.13        REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt,
    28.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Mar 06 15:29:18 2014 +0100
    28.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Mar 06 15:40:33 2014 +0100
    28.3 @@ -502,9 +502,9 @@
    28.4      val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
    28.5      fun flip f x y = if fp = Greatest_FP then f y x else f x y;
    28.6  
    28.7 -    val arg_rels = map2 (flip mk_fun_rel) pre_relphis pre_phis;
    28.8 +    val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_phis;
    28.9      fun mk_transfer relphi pre_phi un_fold un_fold' =
   28.10 -      fold_rev mk_fun_rel arg_rels (flip mk_fun_rel relphi pre_phi) $ un_fold $ un_fold';
   28.11 +      fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold';
   28.12      val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds';
   28.13  
   28.14      val goal = fold_rev Logic.all (phis @ pre_phis)
    29.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Mar 06 15:29:18 2014 +0100
    29.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Mar 06 15:40:33 2014 +0100
    29.3 @@ -1088,16 +1088,16 @@
    29.4      val n = length map_transfers;
    29.5    in
    29.6      unfold_thms_tac ctxt
    29.7 -      @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
    29.8 -    unfold_thms_tac ctxt @{thms fun_rel_iff_geq_image2p} THEN
    29.9 +      @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
   29.10 +    unfold_thms_tac ctxt @{thms rel_fun_iff_geq_image2p} THEN
   29.11      HEADGOAL (EVERY'
   29.12        [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_coinduct,
   29.13        EVERY' (map (fn map_transfer => EVERY'
   29.14          [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
   29.15          SELECT_GOAL (unfold_thms_tac ctxt unfolds),
   29.16 -        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
   29.17 +        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
   29.18          REPEAT_DETERM_N m o rtac @{thm id_transfer},
   29.19 -        REPEAT_DETERM_N n o rtac @{thm fun_rel_image2p},
   29.20 +        REPEAT_DETERM_N n o rtac @{thm rel_fun_image2p},
   29.21          etac @{thm predicate2D}, etac @{thm image2pI}])
   29.22        map_transfers)])
   29.23    end;
    30.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Mar 06 15:29:18 2014 +0100
    30.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Mar 06 15:40:33 2014 +0100
    30.3 @@ -788,17 +788,17 @@
    30.4      val n = length map_transfers;
    30.5    in
    30.6      unfold_thms_tac ctxt
    30.7 -      @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
    30.8 -    unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
    30.9 +      @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
   30.10 +    unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
   30.11      HEADGOAL (EVERY'
   30.12        [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_induct,
   30.13        EVERY' (map (fn map_transfer => EVERY'
   30.14          [REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
   30.15          SELECT_GOAL (unfold_thms_tac ctxt folds),
   30.16          etac @{thm predicate2D_vimage2p},
   30.17 -        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
   30.18 +        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
   30.19          REPEAT_DETERM_N m o rtac @{thm id_transfer},
   30.20 -        REPEAT_DETERM_N n o rtac @{thm vimage2p_fun_rel},
   30.21 +        REPEAT_DETERM_N n o rtac @{thm vimage2p_rel_fun},
   30.22          atac])
   30.23        map_transfers)])
   30.24    end;
    31.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Thu Mar 06 15:29:18 2014 +0100
    31.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Mar 06 15:40:33 2014 +0100
    31.3 @@ -94,7 +94,7 @@
    31.4    val mk_cprod: term -> term -> term
    31.5    val mk_csum: term -> term -> term
    31.6    val mk_dir_image: term -> term -> term
    31.7 -  val mk_fun_rel: term -> term -> term
    31.8 +  val mk_rel_fun: term -> term -> term
    31.9    val mk_image: term -> term
   31.10    val mk_in: term list -> term list -> typ -> term
   31.11    val mk_leq: term -> term -> term
   31.12 @@ -438,11 +438,11 @@
   31.13    let val (T, U) = dest_funT (fastype_of f);
   31.14    in Const (@{const_name dir_image}, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end;
   31.15  
   31.16 -fun mk_fun_rel R S =
   31.17 +fun mk_rel_fun R S =
   31.18    let
   31.19      val ((RA, RB), RT) = `dest_pred2T (fastype_of R);
   31.20      val ((SA, SB), ST) = `dest_pred2T (fastype_of S);
   31.21 -  in Const (@{const_name fun_rel}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end;
   31.22 +  in Const (@{const_name rel_fun}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end;
   31.23  
   31.24  (*FIXME: "x"?*)
   31.25  (*(nth sets i) must be of type "T --> 'ai set"*)
    32.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Mar 06 15:29:18 2014 +0100
    32.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Mar 06 15:40:33 2014 +0100
    32.3 @@ -166,11 +166,11 @@
    32.4  fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
    32.5    | get_binder_types _ = []
    32.6  
    32.7 -fun get_binder_types_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = 
    32.8 +fun get_binder_types_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = 
    32.9      (T, V) :: get_binder_types_by_rel S (U, W)
   32.10    | get_binder_types_by_rel _ _ = []
   32.11  
   32.12 -fun get_body_type_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = 
   32.13 +fun get_body_type_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = 
   32.14      get_body_type_by_rel S (U, V)
   32.15    | get_body_type_by_rel _ (U, V)  = (U, V)
   32.16  
   32.17 @@ -270,8 +270,8 @@
   32.18        let
   32.19          val thy = Proof_Context.theory_of ctxt
   32.20          val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
   32.21 -        val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
   32.22 -        val rep_abs_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs_eq}
   32.23 +        val rel_fun = prove_rel ctxt rsp_thm (rty, qty)
   32.24 +        val rep_abs_thm = [quot_thm, rel_fun] MRSL @{thm Quotient_rep_abs_eq}
   32.25        in
   32.26          case mono_eq_prover ctxt (hd(prems_of rep_abs_thm)) of
   32.27            SOME mono_eq_thm =>
   32.28 @@ -311,7 +311,7 @@
   32.29            end
   32.30        in
   32.31          rep_abs_folded_unmapped_thm
   32.32 -        |> fold (fn _ => fn thm => thm RS @{thm fun_relD2}) ty_args
   32.33 +        |> fold (fn _ => fn thm => thm RS @{thm rel_funD2}) ty_args
   32.34          |> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm]))
   32.35        end
   32.36      
   32.37 @@ -505,11 +505,11 @@
   32.38      fun simp_arrows_conv ctm =
   32.39        let
   32.40          val unfold_conv = Conv.rewrs_conv 
   32.41 -          [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, 
   32.42 -            @{thm fun_rel_invariant_rel[THEN eq_reflection]},
   32.43 -            @{thm fun_rel_eq[THEN eq_reflection]},
   32.44 -            @{thm fun_rel_eq_rel[THEN eq_reflection]}, 
   32.45 -            @{thm fun_rel_def[THEN eq_reflection]}]
   32.46 +          [@{thm rel_fun_eq_invariant[THEN eq_reflection]}, 
   32.47 +            @{thm rel_fun_invariant_rel[THEN eq_reflection]},
   32.48 +            @{thm rel_fun_eq[THEN eq_reflection]},
   32.49 +            @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
   32.50 +            @{thm rel_fun_def[THEN eq_reflection]}]
   32.51          fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   32.52          val invariant_assms_tac_rules = @{thm left_unique_composition} :: 
   32.53              invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
   32.54 @@ -522,7 +522,7 @@
   32.55            (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
   32.56        in
   32.57          case (Thm.term_of ctm) of
   32.58 -          Const (@{const_name "fun_rel"}, _) $ _ $ _ => 
   32.59 +          Const (@{const_name "rel_fun"}, _) $ _ $ _ => 
   32.60              (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
   32.61            | _ => (invariant_commute_conv then_conv relator_eq_conv) ctm
   32.62        end
    33.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML	Thu Mar 06 15:29:18 2014 +0100
    33.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Thu Mar 06 15:40:33 2014 +0100
    33.3 @@ -27,7 +27,7 @@
    33.4    val same_type_constrs: typ * typ -> bool
    33.5    val Targs: typ -> typ list
    33.6    val Tname: typ -> string
    33.7 -  val is_fun_rel: term -> bool
    33.8 +  val is_rel_fun: term -> bool
    33.9    val relation_types: typ -> typ * typ
   33.10    val mk_HOL_eq: thm -> thm
   33.11    val safe_HOL_meta_eq: thm -> thm
   33.12 @@ -110,8 +110,8 @@
   33.13  fun Tname (Type (name, _)) = name
   33.14    | Tname _ = ""
   33.15  
   33.16 -fun is_fun_rel (Const (@{const_name "fun_rel"}, _) $ _ $ _) = true
   33.17 -  | is_fun_rel _ = false
   33.18 +fun is_rel_fun (Const (@{const_name "rel_fun"}, _) $ _ $ _) = true
   33.19 +  | is_rel_fun _ = false
   33.20  
   33.21  fun relation_types typ = 
   33.22    case strip_type typ of
    34.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 06 15:29:18 2014 +0100
    34.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 06 15:40:33 2014 +0100
    34.3 @@ -109,13 +109,13 @@
    34.4      fun simp_arrows_conv ctm =
    34.5        let
    34.6          val unfold_conv = Conv.rewrs_conv 
    34.7 -          [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]}, 
    34.8 -            @{thm fun_rel_def[THEN eq_reflection]}]
    34.9 +          [@{thm rel_fun_eq_invariant[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
   34.10 +            @{thm rel_fun_def[THEN eq_reflection]}]
   34.11          val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
   34.12          fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   34.13        in
   34.14          case (Thm.term_of ctm) of
   34.15 -          Const (@{const_name fun_rel}, _) $ _ $ _ => 
   34.16 +          Const (@{const_name rel_fun}, _) $ _ $ _ => 
   34.17              (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
   34.18            | _ => Conv.all_conv ctm
   34.19        end
    35.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Mar 06 15:29:18 2014 +0100
    35.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Mar 06 15:40:33 2014 +0100
    35.3 @@ -114,11 +114,11 @@
    35.4  fun ball_bex_range_simproc ctxt redex =
    35.5    case redex of
    35.6      (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
    35.7 -      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
    35.8 +      (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
    35.9          calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   35.10  
   35.11    | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
   35.12 -      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
   35.13 +      (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
   35.14          calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   35.15  
   35.16    | _ => NONE
   35.17 @@ -306,7 +306,7 @@
   35.18     The deterministic part:
   35.19      - remove lambdas from both sides
   35.20      - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
   35.21 -    - prove Ball/Bex relations using fun_relI
   35.22 +    - prove Ball/Bex relations using rel_funI
   35.23      - reflexivity of equality
   35.24      - prove equality of relations using equals_rsp
   35.25      - use user-supplied RSP theorems
   35.26 @@ -324,8 +324,8 @@
   35.27  fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
   35.28    (case bare_concl goal of
   35.29        (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
   35.30 -    (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
   35.31 -        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
   35.32 +    (Const (@{const_name rel_fun}, _) $ _ $ _) $ (Abs _) $ (Abs _)
   35.33 +        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
   35.34  
   35.35        (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
   35.36    | (Const (@{const_name HOL.eq},_) $
   35.37 @@ -334,10 +334,10 @@
   35.38          => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
   35.39  
   35.40        (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
   35.41 -  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   35.42 +  | (Const (@{const_name rel_fun}, _) $ _ $ _) $
   35.43        (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   35.44        (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   35.45 -        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
   35.46 +        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
   35.47  
   35.48        (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
   35.49    | Const (@{const_name HOL.eq},_) $
   35.50 @@ -346,12 +346,12 @@
   35.51          => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
   35.52  
   35.53        (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
   35.54 -  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   35.55 +  | (Const (@{const_name rel_fun}, _) $ _ $ _) $
   35.56        (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   35.57        (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   35.58 -        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
   35.59 +        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
   35.60  
   35.61 -  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   35.62 +  | (Const (@{const_name rel_fun}, _) $ _ $ _) $
   35.63        (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
   35.64          => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
   35.65  
   35.66 @@ -369,7 +369,7 @@
   35.67    | Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
   35.68  
   35.69       (* respectfulness of constants; in particular of a simple relation *)
   35.70 -  | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
   35.71 +  | _ $ (Const _) $ (Const _)  (* rel_fun, list_rel, etc but not equality *)
   35.72        => resolve_tac (Quotient_Info.rsp_rules ctxt) THEN_ALL_NEW quotient_tac ctxt
   35.73  
   35.74        (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
    36.1 --- a/src/HOL/Tools/transfer.ML	Thu Mar 06 15:29:18 2014 +0100
    36.2 +++ b/src/HOL/Tools/transfer.ML	Thu Mar 06 15:40:33 2014 +0100
    36.3 @@ -389,7 +389,7 @@
    36.4            val r2 = rel T2 U2
    36.5            val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
    36.6          in
    36.7 -          Const (@{const_name fun_rel}, rT) $ r1 $ r2
    36.8 +          Const (@{const_name rel_fun}, rT) $ r1 $ r2
    36.9          end
   36.10        | rel T U =
   36.11          let
   36.12 @@ -617,7 +617,7 @@
   36.13      val rule1 = transfer_rule_of_term ctxt false rhs
   36.14      val rules = get_transfer_raw ctxt
   36.15      val eq_rules = get_relator_eq_raw ctxt
   36.16 -    val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm fun_rel_eq[symmetric,THEN eq_reflection]}])
   36.17 +    val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])
   36.18    in
   36.19      EVERY
   36.20        [CONVERSION prep_conv i,
    37.1 --- a/src/HOL/Topological_Spaces.thy	Thu Mar 06 15:29:18 2014 +0100
    37.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Mar 06 15:40:33 2014 +0100
    37.3 @@ -2363,23 +2363,23 @@
    37.4    fix F G
    37.5    assume "rel_filter T F G"
    37.6    thus "filtermap Abs F = G" unfolding filter_eq_iff
    37.7 -    by(auto simp add: eventually_filtermap rel_filter_eventually * fun_relI del: iffI elim!: fun_relD)
    37.8 +    by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
    37.9  next
   37.10    from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
   37.11  
   37.12    fix F
   37.13    show "rel_filter T (filtermap Rep F) F" 
   37.14 -    by(auto elim: fun_relD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] fun_relI
   37.15 +    by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
   37.16              del: iffI simp add: eventually_filtermap rel_filter_eventually)
   37.17  qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
   37.18           fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
   37.19  
   37.20  lemma eventually_parametric [transfer_rule]:
   37.21    "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
   37.22 -by(simp add: fun_rel_def rel_filter_eventually)
   37.23 +by(simp add: rel_fun_def rel_filter_eventually)
   37.24  
   37.25  lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
   37.26 -by(auto simp add: rel_filter_eventually fun_rel_eq fun_eq_iff filter_eq_iff)
   37.27 +by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
   37.28  
   37.29  lemma rel_filter_mono [relator_mono]:
   37.30    "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
   37.31 @@ -2387,7 +2387,7 @@
   37.32  by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
   37.33  
   37.34  lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
   37.35 -by(auto simp add: rel_filter_eventually fun_eq_iff fun_rel_def)
   37.36 +by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
   37.37  
   37.38  lemma is_filter_parametric_aux:
   37.39    assumes "is_filter F"
   37.40 @@ -2427,11 +2427,11 @@
   37.41  lemma is_filter_parametric [transfer_rule]:
   37.42    "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
   37.43    \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
   37.44 -apply(rule fun_relI)
   37.45 +apply(rule rel_funI)
   37.46  apply(rule iffI)
   37.47   apply(erule (3) is_filter_parametric_aux)
   37.48  apply(erule is_filter_parametric_aux[where A="conversep A"])
   37.49 -apply(auto simp add: fun_rel_def)
   37.50 +apply(auto simp add: rel_fun_def)
   37.51  done
   37.52  
   37.53  lemma left_total_rel_filter [reflexivity_rule]:
   37.54 @@ -2490,15 +2490,15 @@
   37.55  by(simp add: rel_filter_eventually All_transfer)
   37.56  
   37.57  lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
   37.58 -by(simp add: rel_filter_eventually fun_rel_def)
   37.59 +by(simp add: rel_filter_eventually rel_fun_def)
   37.60  
   37.61  lemma sup_filter_parametric [transfer_rule]:
   37.62    "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
   37.63 -by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: fun_relD)
   37.64 +by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
   37.65  
   37.66  lemma Sup_filter_parametric [transfer_rule]:
   37.67    "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
   37.68 -proof(rule fun_relI)
   37.69 +proof(rule rel_funI)
   37.70    fix S T
   37.71    assume [transfer_rule]: "rel_set (rel_filter A) S T"
   37.72    show "rel_filter A (Sup S) (Sup T)"
   37.73 @@ -2507,7 +2507,7 @@
   37.74  
   37.75  lemma principal_parametric [transfer_rule]:
   37.76    "(rel_set A ===> rel_filter A) principal principal"
   37.77 -proof(rule fun_relI)
   37.78 +proof(rule rel_funI)
   37.79    fix S S'
   37.80    assume [transfer_rule]: "rel_set A S S'"
   37.81    show "rel_filter A (principal S) (principal S')"
   37.82 @@ -2537,7 +2537,7 @@
   37.83  
   37.84  lemma inf_filter_parametric [transfer_rule]:
   37.85    "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
   37.86 -proof(intro fun_relI)+
   37.87 +proof(intro rel_funI)+
   37.88    fix F F' G G'
   37.89    assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
   37.90    have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
    38.1 --- a/src/HOL/Transfer.thy	Thu Mar 06 15:29:18 2014 +0100
    38.2 +++ b/src/HOL/Transfer.thy	Thu Mar 06 15:40:33 2014 +0100
    38.3 @@ -13,7 +13,7 @@
    38.4  
    38.5  locale lifting_syntax
    38.6  begin
    38.7 -  notation fun_rel (infixr "===>" 55)
    38.8 +  notation rel_fun (infixr "===>" 55)
    38.9    notation map_fun (infixr "--->" 55)
   38.10  end
   38.11  
   38.12 @@ -21,21 +21,21 @@
   38.13  begin
   38.14  interpretation lifting_syntax .
   38.15  
   38.16 -lemma fun_relD2:
   38.17 -  assumes "fun_rel A B f g" and "A x x"
   38.18 +lemma rel_funD2:
   38.19 +  assumes "rel_fun A B f g" and "A x x"
   38.20    shows "B (f x) (g x)"
   38.21 -  using assms by (rule fun_relD)
   38.22 +  using assms by (rule rel_funD)
   38.23  
   38.24 -lemma fun_relE:
   38.25 -  assumes "fun_rel A B f g" and "A x y"
   38.26 +lemma rel_funE:
   38.27 +  assumes "rel_fun A B f g" and "A x y"
   38.28    obtains "B (f x) (g y)"
   38.29 -  using assms by (simp add: fun_rel_def)
   38.30 +  using assms by (simp add: rel_fun_def)
   38.31  
   38.32 -lemmas fun_rel_eq = fun.rel_eq
   38.33 +lemmas rel_fun_eq = fun.rel_eq
   38.34  
   38.35 -lemma fun_rel_eq_rel:
   38.36 -shows "fun_rel (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
   38.37 -  by (simp add: fun_rel_def)
   38.38 +lemma rel_fun_eq_rel:
   38.39 +shows "rel_fun (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
   38.40 +  by (simp add: rel_fun_def)
   38.41  
   38.42  
   38.43  subsection {* Transfer method *}
   38.44 @@ -98,12 +98,12 @@
   38.45  lemma Rel_app:
   38.46    assumes "Rel (A ===> B) f g" and "Rel A x y"
   38.47    shows "Rel B (f x) (g y)"
   38.48 -  using assms unfolding Rel_def fun_rel_def by fast
   38.49 +  using assms unfolding Rel_def rel_fun_def by fast
   38.50  
   38.51  lemma Rel_abs:
   38.52    assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
   38.53    shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
   38.54 -  using assms unfolding Rel_def fun_rel_def by fast
   38.55 +  using assms unfolding Rel_def rel_fun_def by fast
   38.56  
   38.57  end
   38.58  
   38.59 @@ -112,7 +112,7 @@
   38.60  
   38.61  declare refl [transfer_rule]
   38.62  
   38.63 -declare fun_rel_eq [relator_eq]
   38.64 +declare rel_fun_eq [relator_eq]
   38.65  
   38.66  hide_const (open) Rel
   38.67  
   38.68 @@ -131,7 +131,7 @@
   38.69  lemma Domainp_prod_fun_eq[transfer_domain_rule]:
   38.70    assumes "Domainp T = P"
   38.71    shows "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. P (f x))"
   38.72 -by (auto intro: choice simp: assms[symmetric] Domainp_iff fun_rel_def fun_eq_iff)
   38.73 +by (auto intro: choice simp: assms[symmetric] Domainp_iff rel_fun_def fun_eq_iff)
   38.74  
   38.75  subsection {* Predicates on relations, i.e. ``class constraints'' *}
   38.76  
   38.77 @@ -163,7 +163,7 @@
   38.78  
   38.79  lemma right_total_alt_def:
   38.80    "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
   38.81 -  unfolding right_total_def fun_rel_def
   38.82 +  unfolding right_total_def rel_fun_def
   38.83    apply (rule iffI, fast)
   38.84    apply (rule allI)
   38.85    apply (drule_tac x="\<lambda>x. True" in spec)
   38.86 @@ -173,11 +173,11 @@
   38.87  
   38.88  lemma right_unique_alt_def:
   38.89    "right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)"
   38.90 -  unfolding right_unique_def fun_rel_def by auto
   38.91 +  unfolding right_unique_def rel_fun_def by auto
   38.92  
   38.93  lemma bi_total_alt_def:
   38.94    "bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All"
   38.95 -  unfolding bi_total_def fun_rel_def
   38.96 +  unfolding bi_total_def rel_fun_def
   38.97    apply (rule iffI, fast)
   38.98    apply safe
   38.99    apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec)
  38.100 @@ -190,7 +190,7 @@
  38.101  
  38.102  lemma bi_unique_alt_def:
  38.103    "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
  38.104 -  unfolding bi_unique_def fun_rel_def by auto
  38.105 +  unfolding bi_unique_def rel_fun_def by auto
  38.106  
  38.107  lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
  38.108  by(auto simp add: bi_unique_def)
  38.109 @@ -234,7 +234,7 @@
  38.110  
  38.111  lemma right_total_fun [transfer_rule]:
  38.112    "\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
  38.113 -  unfolding right_total_def fun_rel_def
  38.114 +  unfolding right_total_def rel_fun_def
  38.115    apply (rule allI, rename_tac g)
  38.116    apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
  38.117    apply clarify
  38.118 @@ -248,12 +248,12 @@
  38.119  
  38.120  lemma right_unique_fun [transfer_rule]:
  38.121    "\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
  38.122 -  unfolding right_total_def right_unique_def fun_rel_def
  38.123 +  unfolding right_total_def right_unique_def rel_fun_def
  38.124    by (clarify, rule ext, fast)
  38.125  
  38.126  lemma bi_total_fun [transfer_rule]:
  38.127    "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
  38.128 -  unfolding bi_total_def fun_rel_def
  38.129 +  unfolding bi_total_def rel_fun_def
  38.130    apply safe
  38.131    apply (rename_tac f)
  38.132    apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
  38.133 @@ -277,7 +277,7 @@
  38.134  
  38.135  lemma bi_unique_fun [transfer_rule]:
  38.136    "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
  38.137 -  unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff
  38.138 +  unfolding bi_total_def bi_unique_def rel_fun_def fun_eq_iff
  38.139    by (safe, metis, fast)
  38.140  
  38.141  
  38.142 @@ -288,7 +288,7 @@
  38.143    shows "((A ===> op =) ===> op =)
  38.144      (transfer_bforall (Domainp A)) transfer_forall"
  38.145    using assms unfolding right_total_def
  38.146 -  unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff
  38.147 +  unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff
  38.148    by metis
  38.149  
  38.150  text {* Transfer rules using implication instead of equality on booleans. *}
  38.151 @@ -299,7 +299,7 @@
  38.152    "right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall"
  38.153    "bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall"
  38.154    "bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
  38.155 -  unfolding transfer_forall_def rev_implies_def fun_rel_def right_total_def bi_total_def
  38.156 +  unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def
  38.157    by metis+
  38.158  
  38.159  lemma transfer_implies_transfer [transfer_rule]:
  38.160 @@ -312,7 +312,7 @@
  38.161    "(implies     ===> op =        ===> rev_implies) transfer_implies transfer_implies"
  38.162    "(op =        ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
  38.163    "(op =        ===> op =        ===> rev_implies) transfer_implies transfer_implies"
  38.164 -  unfolding transfer_implies_def rev_implies_def fun_rel_def by auto
  38.165 +  unfolding transfer_implies_def rev_implies_def rel_fun_def by auto
  38.166  
  38.167  lemma eq_imp_transfer [transfer_rule]:
  38.168    "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
  38.169 @@ -321,42 +321,42 @@
  38.170  lemma eq_transfer [transfer_rule]:
  38.171    assumes "bi_unique A"
  38.172    shows "(A ===> A ===> op =) (op =) (op =)"
  38.173 -  using assms unfolding bi_unique_def fun_rel_def by auto
  38.174 +  using assms unfolding bi_unique_def rel_fun_def by auto
  38.175  
  38.176  lemma right_total_Ex_transfer[transfer_rule]:
  38.177    assumes "right_total A"
  38.178    shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
  38.179 -using assms unfolding right_total_def Bex_def fun_rel_def Domainp_iff[abs_def]
  38.180 +using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def]
  38.181  by blast
  38.182  
  38.183  lemma right_total_All_transfer[transfer_rule]:
  38.184    assumes "right_total A"
  38.185    shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All"
  38.186 -using assms unfolding right_total_def Ball_def fun_rel_def Domainp_iff[abs_def]
  38.187 +using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
  38.188  by blast
  38.189  
  38.190  lemma All_transfer [transfer_rule]:
  38.191    assumes "bi_total A"
  38.192    shows "((A ===> op =) ===> op =) All All"
  38.193 -  using assms unfolding bi_total_def fun_rel_def by fast
  38.194 +  using assms unfolding bi_total_def rel_fun_def by fast
  38.195  
  38.196  lemma Ex_transfer [transfer_rule]:
  38.197    assumes "bi_total A"
  38.198    shows "((A ===> op =) ===> op =) Ex Ex"
  38.199 -  using assms unfolding bi_total_def fun_rel_def by fast
  38.200 +  using assms unfolding bi_total_def rel_fun_def by fast
  38.201  
  38.202  lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
  38.203 -  unfolding fun_rel_def by simp
  38.204 +  unfolding rel_fun_def by simp
  38.205  
  38.206  lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
  38.207 -  unfolding fun_rel_def by simp
  38.208 +  unfolding rel_fun_def by simp
  38.209  
  38.210  lemma id_transfer [transfer_rule]: "(A ===> A) id id"
  38.211 -  unfolding fun_rel_def by simp
  38.212 +  unfolding rel_fun_def by simp
  38.213  
  38.214  lemma comp_transfer [transfer_rule]:
  38.215    "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
  38.216 -  unfolding fun_rel_def by simp
  38.217 +  unfolding rel_fun_def by simp
  38.218  
  38.219  lemma fun_upd_transfer [transfer_rule]:
  38.220    assumes [transfer_rule]: "bi_unique A"
  38.221 @@ -365,11 +365,11 @@
  38.222  
  38.223  lemma case_nat_transfer [transfer_rule]:
  38.224    "(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat"
  38.225 -  unfolding fun_rel_def by (simp split: nat.split)
  38.226 +  unfolding rel_fun_def by (simp split: nat.split)
  38.227  
  38.228  lemma rec_nat_transfer [transfer_rule]:
  38.229    "(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat"
  38.230 -  unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
  38.231 +  unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
  38.232  
  38.233  lemma funpow_transfer [transfer_rule]:
  38.234    "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
  38.235 @@ -409,7 +409,7 @@
  38.236    "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
  38.237    "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
  38.238    "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
  38.239 -using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def fun_rel_def 
  38.240 +using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def 
  38.241  by fast+
  38.242  
  38.243  lemma right_unique_transfer [transfer_rule]:
  38.244 @@ -417,7 +417,7 @@
  38.245    assumes [transfer_rule]: "right_total B"
  38.246    assumes [transfer_rule]: "bi_unique B"
  38.247    shows "((A ===> B ===> op=) ===> implies) right_unique right_unique"
  38.248 -using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def
  38.249 +using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
  38.250  by metis
  38.251  
  38.252  end
    39.1 --- a/src/HOL/Word/Word.thy	Thu Mar 06 15:29:18 2014 +0100
    39.2 +++ b/src/HOL/Word/Word.thy	Thu Mar 06 15:40:33 2014 +0100
    39.3 @@ -193,9 +193,9 @@
    39.4  text {* TODO: The next lemma could be generated automatically. *}
    39.5  
    39.6  lemma uint_transfer [transfer_rule]:
    39.7 -  "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
    39.8 +  "(rel_fun pcr_word op =) (bintrunc (len_of TYPE('a)))
    39.9      (uint :: 'a::len0 word \<Rightarrow> int)"
   39.10 -  unfolding fun_rel_def word.pcr_cr_eq cr_word_def
   39.11 +  unfolding rel_fun_def word.pcr_cr_eq cr_word_def
   39.12    by (simp add: no_bintr_alt1 uint_word_of_int)
   39.13  
   39.14  
   39.15 @@ -651,9 +651,9 @@
   39.16  declare word_neg_numeral_alt [symmetric, code_abbrev]
   39.17  
   39.18  lemma word_numeral_transfer [transfer_rule]:
   39.19 -  "(fun_rel op = pcr_word) numeral numeral"
   39.20 -  "(fun_rel op = pcr_word) (- numeral) (- numeral)"
   39.21 -  apply (simp_all add: fun_rel_def word.pcr_cr_eq cr_word_def)
   39.22 +  "(rel_fun op = pcr_word) numeral numeral"
   39.23 +  "(rel_fun op = pcr_word) (- numeral) (- numeral)"
   39.24 +  apply (simp_all add: rel_fun_def word.pcr_cr_eq cr_word_def)
   39.25    using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by blast+
   39.26  
   39.27  lemma uint_bintrunc [simp]:
   39.28 @@ -2295,9 +2295,9 @@
   39.29    by (simp add: word_ubin.eq_norm nth_bintr)
   39.30  
   39.31  lemma word_test_bit_transfer [transfer_rule]:
   39.32 -  "(fun_rel pcr_word (fun_rel op = op =))
   39.33 +  "(rel_fun pcr_word (rel_fun op = op =))
   39.34      (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
   39.35 -  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by simp
   39.36 +  unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp
   39.37  
   39.38  lemma word_ops_nth_size:
   39.39    "n < size (x::'a::len0 word) \<Longrightarrow> 
    40.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Thu Mar 06 15:29:18 2014 +0100
    40.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Thu Mar 06 15:40:33 2014 +0100
    40.3 @@ -37,79 +37,79 @@
    40.4    unfolding ZN_def by simp
    40.5  
    40.6  lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)"
    40.7 -  unfolding fun_rel_def ZN_def by simp
    40.8 +  unfolding rel_fun_def ZN_def by simp
    40.9  
   40.10  lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
   40.11 -  unfolding fun_rel_def ZN_def by (simp add: int_mult)
   40.12 +  unfolding rel_fun_def ZN_def by (simp add: int_mult)
   40.13  
   40.14  lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
   40.15 -  unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int)
   40.16 +  unfolding rel_fun_def ZN_def tsub_def by (simp add: zdiff_int)
   40.17  
   40.18  lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
   40.19 -  unfolding fun_rel_def ZN_def by (simp add: int_power)
   40.20 +  unfolding rel_fun_def ZN_def by (simp add: int_power)
   40.21  
   40.22  lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
   40.23 -  unfolding fun_rel_def ZN_def by simp
   40.24 +  unfolding rel_fun_def ZN_def by simp
   40.25  
   40.26  lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int"
   40.27 -  unfolding fun_rel_def ZN_def by simp
   40.28 +  unfolding rel_fun_def ZN_def by simp
   40.29  
   40.30  lemma ZN_All [transfer_rule]:
   40.31    "((ZN ===> op =) ===> op =) (Ball {0..}) All"
   40.32 -  unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
   40.33 +  unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int)
   40.34  
   40.35  lemma ZN_transfer_forall [transfer_rule]:
   40.36    "((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall"
   40.37    unfolding transfer_forall_def transfer_bforall_def
   40.38 -  unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
   40.39 +  unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int)
   40.40  
   40.41  lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
   40.42 -  unfolding fun_rel_def ZN_def Bex_def atLeast_iff
   40.43 +  unfolding rel_fun_def ZN_def Bex_def atLeast_iff
   40.44    by (metis zero_le_imp_eq_int zero_zle_int)
   40.45  
   40.46  lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
   40.47 -  unfolding fun_rel_def ZN_def by simp
   40.48 +  unfolding rel_fun_def ZN_def by simp
   40.49  
   40.50  lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)"
   40.51 -  unfolding fun_rel_def ZN_def by simp
   40.52 +  unfolding rel_fun_def ZN_def by simp
   40.53  
   40.54  lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)"
   40.55 -  unfolding fun_rel_def ZN_def by simp
   40.56 +  unfolding rel_fun_def ZN_def by simp
   40.57  
   40.58  lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc"
   40.59 -  unfolding fun_rel_def ZN_def by simp
   40.60 +  unfolding rel_fun_def ZN_def by simp
   40.61  
   40.62  lemma ZN_numeral [transfer_rule]:
   40.63    "(op = ===> ZN) numeral numeral"
   40.64 -  unfolding fun_rel_def ZN_def by simp
   40.65 +  unfolding rel_fun_def ZN_def by simp
   40.66  
   40.67  lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
   40.68 -  unfolding fun_rel_def ZN_def by (simp add: zdvd_int)
   40.69 +  unfolding rel_fun_def ZN_def by (simp add: zdvd_int)
   40.70  
   40.71  lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
   40.72 -  unfolding fun_rel_def ZN_def by (simp add: zdiv_int)
   40.73 +  unfolding rel_fun_def ZN_def by (simp add: zdiv_int)
   40.74  
   40.75  lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
   40.76 -  unfolding fun_rel_def ZN_def by (simp add: zmod_int)
   40.77 +  unfolding rel_fun_def ZN_def by (simp add: zmod_int)
   40.78  
   40.79  lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
   40.80 -  unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
   40.81 +  unfolding rel_fun_def ZN_def by (simp add: transfer_int_nat_gcd)
   40.82  
   40.83  lemma ZN_atMost [transfer_rule]:
   40.84    "(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"
   40.85 -  unfolding fun_rel_def ZN_def rel_set_def
   40.86 +  unfolding rel_fun_def ZN_def rel_set_def
   40.87    by (clarsimp simp add: Bex_def, arith)
   40.88  
   40.89  lemma ZN_atLeastAtMost [transfer_rule]:
   40.90    "(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost"
   40.91 -  unfolding fun_rel_def ZN_def rel_set_def
   40.92 +  unfolding rel_fun_def ZN_def rel_set_def
   40.93    by (clarsimp simp add: Bex_def, arith)
   40.94  
   40.95  lemma ZN_setsum [transfer_rule]:
   40.96    "bi_unique A \<Longrightarrow> ((A ===> ZN) ===> rel_set A ===> ZN) setsum setsum"
   40.97 -  apply (intro fun_relI)
   40.98 +  apply (intro rel_funI)
   40.99    apply (erule (1) bi_unique_rel_set_lemma)
  40.100 -  apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def)
  40.101 +  apply (simp add: setsum.reindex int_setsum ZN_def rel_fun_def)
  40.102    apply (rule setsum_cong2, simp)
  40.103    done
  40.104