renamed 'sum_rel' to 'rel_sum'
authorblanchet
Thu Mar 06 15:25:21 2014 +0100 (2014-03-06)
changeset 559435c2df04e97d1
parent 55942 c2d96043de4b
child 55944 7ab8f003fe41
renamed 'sum_rel' to 'rel_sum'
NEWS
src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy
src/HOL/BNF_Examples/Process.thy
src/HOL/Basic_BNFs.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Lifting_Sum.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/NEWS	Thu Mar 06 15:14:09 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 06 15:25:21 2014 +0100
     1.3 @@ -193,6 +193,7 @@
     1.4  * The following map functions and relators have been renamed:
     1.5      sum_map ~> map_sum
     1.6      map_pair ~> map_prod
     1.7 +    sum_rel ~> rel_sum
     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/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 15:14:09 2014 +0100
     2.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 15:25:21 2014 +0100
     2.3 @@ -67,7 +67,7 @@
     2.4  lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]:
     2.5  assumes phi: "\<phi> tr1 tr2" and
     2.6  Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
     2.7 -                  root tr1 = root tr2 \<and> rel_set (sum_rel op = \<phi>) (cont tr1) (cont tr2)"
     2.8 +                  root tr1 = root tr2 \<and> rel_set (rel_sum op = \<phi>) (cont tr1) (cont tr2)"
     2.9  shows "tr1 = tr2"
    2.10  using phi apply(elim dtree.coinduct)
    2.11  apply(rule Lift[unfolded rel_set_cont]) .
     3.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy	Thu Mar 06 15:14:09 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy	Thu Mar 06 15:25:21 2014 +0100
     3.3 @@ -67,10 +67,10 @@
     3.4  
     3.5  subsection{* Structural Coinduction Proofs *}
     3.6  
     3.7 -lemma rel_set_sum_rel_eq[simp]:
     3.8 -"rel_set (sum_rel (op =) \<phi>) A1 A2 \<longleftrightarrow>
     3.9 +lemma rel_set_rel_sum_eq[simp]:
    3.10 +"rel_set (rel_sum (op =) \<phi>) A1 A2 \<longleftrightarrow>
    3.11   Inl -` A1 = Inl -` A2 \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
    3.12 -unfolding rel_set_sum_rel rel_set_eq ..
    3.13 +unfolding rel_set_rel_sum rel_set_eq ..
    3.14  
    3.15  (* Detailed proofs of commutativity and associativity: *)
    3.16  theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1"
    3.17 @@ -79,7 +79,7 @@
    3.18    {fix trA trB
    3.19     assume "?\<theta> trA trB" hence "trA = trB"
    3.20     apply (induct rule: dtree_coinduct)
    3.21 -   unfolding rel_set_sum_rel rel_set_eq unfolding rel_set_def proof safe
    3.22 +   unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe
    3.23       fix tr1 tr2  show "root (tr1 \<parallel> tr2) = root (tr2 \<parallel> tr1)"
    3.24       unfolding root_par by (rule Nplus_comm)
    3.25     next
    3.26 @@ -114,7 +114,7 @@
    3.27    {fix trA trB
    3.28     assume "?\<theta> trA trB" hence "trA = trB"
    3.29     apply (induct rule: dtree_coinduct)
    3.30 -   unfolding rel_set_sum_rel rel_set_eq unfolding rel_set_def proof safe
    3.31 +   unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe
    3.32       fix tr1 tr2 tr3  show "root ((tr1 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))"
    3.33       unfolding root_par by (rule Nplus_assoc)
    3.34     next
     4.1 --- a/src/HOL/BNF_Examples/Process.thy	Thu Mar 06 15:14:09 2014 +0100
     4.2 +++ b/src/HOL/BNF_Examples/Process.thy	Thu Mar 06 15:25:21 2014 +0100
     4.3 @@ -23,7 +23,7 @@
     4.4  
     4.5  declare
     4.6    rel_pre_process_def[simp]
     4.7 -  sum_rel_def[simp]
     4.8 +  rel_sum_def[simp]
     4.9    prod_rel_def[simp]
    4.10  
    4.11  (* Constructors versus discriminators *)
     5.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:14:09 2014 +0100
     5.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:25:21 2014 +0100
     5.3 @@ -22,26 +22,26 @@
     5.4  lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
     5.5  
     5.6  definition
     5.7 -   sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
     5.8 +   rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
     5.9  where
    5.10 -   "sum_rel R1 R2 x y =
    5.11 +   "rel_sum R1 R2 x y =
    5.12       (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    5.13       | (Inr x, Inr y) \<Rightarrow> R2 x y
    5.14       | _ \<Rightarrow> False)"
    5.15  
    5.16 -lemma sum_rel_simps[simp]:
    5.17 -  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    5.18 -  "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    5.19 -  "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    5.20 -  "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    5.21 -  unfolding sum_rel_def by simp_all
    5.22 +lemma rel_sum_simps[simp]:
    5.23 +  "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    5.24 +  "rel_sum R1 R2 (Inl a1) (Inr b2) = False"
    5.25 +  "rel_sum R1 R2 (Inr a2) (Inl b1) = False"
    5.26 +  "rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    5.27 +  unfolding rel_sum_def by simp_all
    5.28  
    5.29  bnf "'a + 'b"
    5.30    map: map_sum
    5.31    sets: setl setr
    5.32    bd: natLeq
    5.33    wits: Inl Inr
    5.34 -  rel: sum_rel
    5.35 +  rel: rel_sum
    5.36  proof -
    5.37    show "map_sum id id = id" by (rule map_sum.id)
    5.38  next
    5.39 @@ -84,14 +84,14 @@
    5.40      by (simp add: setr_def split: sum.split)
    5.41  next
    5.42    fix R1 R2 S1 S2
    5.43 -  show "sum_rel R1 R2 OO sum_rel S1 S2 \<le> sum_rel (R1 OO S1) (R2 OO S2)"
    5.44 -    by (auto simp: sum_rel_def split: sum.splits)
    5.45 +  show "rel_sum R1 R2 OO rel_sum S1 S2 \<le> rel_sum (R1 OO S1) (R2 OO S2)"
    5.46 +    by (auto simp: rel_sum_def split: sum.splits)
    5.47  next
    5.48    fix R S
    5.49 -  show "sum_rel R S =
    5.50 +  show "rel_sum R S =
    5.51          (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
    5.52          Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
    5.53 -  unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    5.54 +  unfolding setl_def setr_def rel_sum_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    5.55    by (fastforce split: sum.splits)
    5.56  qed (auto simp: sum_set_defs)
    5.57  
     6.1 --- a/src/HOL/Library/FSet.thy	Thu Mar 06 15:14:09 2014 +0100
     6.2 +++ b/src/HOL/Library/FSet.thy	Thu Mar 06 15:25:21 2014 +0100
     6.3 @@ -1049,34 +1049,34 @@
     6.4  
     6.5  (* Set vs. sum relators: *)
     6.6  
     6.7 -lemma rel_set_sum_rel[simp]: 
     6.8 -"rel_set (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow> 
     6.9 +lemma rel_set_rel_sum[simp]: 
    6.10 +"rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow> 
    6.11   rel_set \<chi> (Inl -` A1) (Inl -` A2) \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
    6.12  (is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
    6.13  proof safe
    6.14    assume L: "?L"
    6.15    show ?Rl unfolding rel_set_def Bex_def vimage_eq proof safe
    6.16      fix l1 assume "Inl l1 \<in> A1"
    6.17 -    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2"
    6.18 +    then obtain a2 where a2: "a2 \<in> A2" and "rel_sum \<chi> \<phi> (Inl l1) a2"
    6.19      using L unfolding rel_set_def by auto
    6.20      then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto)
    6.21      thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto
    6.22    next
    6.23      fix l2 assume "Inl l2 \<in> A2"
    6.24 -    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)"
    6.25 +    then obtain a1 where a1: "a1 \<in> A1" and "rel_sum \<chi> \<phi> a1 (Inl l2)"
    6.26      using L unfolding rel_set_def by auto
    6.27      then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto)
    6.28      thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto
    6.29    qed
    6.30    show ?Rr unfolding rel_set_def Bex_def vimage_eq proof safe
    6.31      fix r1 assume "Inr r1 \<in> A1"
    6.32 -    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2"
    6.33 +    then obtain a2 where a2: "a2 \<in> A2" and "rel_sum \<chi> \<phi> (Inr r1) a2"
    6.34      using L unfolding rel_set_def by auto
    6.35      then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto)
    6.36      thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto
    6.37    next
    6.38      fix r2 assume "Inr r2 \<in> A2"
    6.39 -    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)"
    6.40 +    then obtain a1 where a1: "a1 \<in> A1" and "rel_sum \<chi> \<phi> a1 (Inr r2)"
    6.41      using L unfolding rel_set_def by auto
    6.42      then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto)
    6.43      thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto
    6.44 @@ -1085,7 +1085,7 @@
    6.45    assume Rl: "?Rl" and Rr: "?Rr"
    6.46    show ?L unfolding rel_set_def Bex_def vimage_eq proof safe
    6.47      fix a1 assume a1: "a1 \<in> A1"
    6.48 -    show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2"
    6.49 +    show "\<exists> a2. a2 \<in> A2 \<and> rel_sum \<chi> \<phi> a1 a2"
    6.50      proof(cases a1)
    6.51        case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2"
    6.52        using Rl a1 unfolding rel_set_def by blast
    6.53 @@ -1097,7 +1097,7 @@
    6.54      qed
    6.55    next
    6.56      fix a2 assume a2: "a2 \<in> A2"
    6.57 -    show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2"
    6.58 +    show "\<exists> a1. a1 \<in> A1 \<and> rel_sum \<chi> \<phi> a1 a2"
    6.59      proof(cases a2)
    6.60        case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2"
    6.61        using Rl a2 unfolding rel_set_def by blast
     7.1 --- a/src/HOL/Library/Quotient_Sum.thy	Thu Mar 06 15:14:09 2014 +0100
     7.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Thu Mar 06 15:25:21 2014 +0100
     7.3 @@ -10,61 +10,61 @@
     7.4  
     7.5  subsection {* Rules for the Quotient package *}
     7.6  
     7.7 -lemma sum_rel_map1:
     7.8 -  "sum_rel R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
     7.9 -  by (simp add: sum_rel_def split: sum.split)
    7.10 +lemma rel_sum_map1:
    7.11 +  "rel_sum R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> rel_sum (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
    7.12 +  by (simp add: rel_sum_def split: sum.split)
    7.13  
    7.14 -lemma sum_rel_map2:
    7.15 -  "sum_rel R1 R2 x (map_sum f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
    7.16 -  by (simp add: sum_rel_def split: sum.split)
    7.17 +lemma rel_sum_map2:
    7.18 +  "rel_sum R1 R2 x (map_sum f1 f2 y) \<longleftrightarrow> rel_sum (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
    7.19 +  by (simp add: rel_sum_def split: sum.split)
    7.20  
    7.21  lemma map_sum_id [id_simps]:
    7.22    "map_sum id id = id"
    7.23    by (simp add: id_def map_sum.identity fun_eq_iff)
    7.24  
    7.25 -lemma sum_rel_eq [id_simps]:
    7.26 -  "sum_rel (op =) (op =) = (op =)"
    7.27 -  by (simp add: sum_rel_def fun_eq_iff split: sum.split)
    7.28 +lemma rel_sum_eq [id_simps]:
    7.29 +  "rel_sum (op =) (op =) = (op =)"
    7.30 +  by (simp add: rel_sum_def fun_eq_iff split: sum.split)
    7.31  
    7.32 -lemma reflp_sum_rel:
    7.33 -  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    7.34 -  unfolding reflp_def split_sum_all sum_rel_simps by fast
    7.35 +lemma reflp_rel_sum:
    7.36 +  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (rel_sum R1 R2)"
    7.37 +  unfolding reflp_def split_sum_all rel_sum_simps by fast
    7.38  
    7.39  lemma sum_symp:
    7.40 -  "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    7.41 -  unfolding symp_def split_sum_all sum_rel_simps by fast
    7.42 +  "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (rel_sum R1 R2)"
    7.43 +  unfolding symp_def split_sum_all rel_sum_simps by fast
    7.44  
    7.45  lemma sum_transp:
    7.46 -  "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
    7.47 -  unfolding transp_def split_sum_all sum_rel_simps by fast
    7.48 +  "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (rel_sum R1 R2)"
    7.49 +  unfolding transp_def split_sum_all rel_sum_simps by fast
    7.50  
    7.51  lemma sum_equivp [quot_equiv]:
    7.52 -  "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    7.53 -  by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE)
    7.54 +  "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (rel_sum R1 R2)"
    7.55 +  by (blast intro: equivpI reflp_rel_sum sum_symp sum_transp elim: equivpE)
    7.56  
    7.57  lemma sum_quotient [quot_thm]:
    7.58    assumes q1: "Quotient3 R1 Abs1 Rep1"
    7.59    assumes q2: "Quotient3 R2 Abs2 Rep2"
    7.60 -  shows "Quotient3 (sum_rel R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2)"
    7.61 +  shows "Quotient3 (rel_sum R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2)"
    7.62    apply (rule Quotient3I)
    7.63 -  apply (simp_all add: map_sum.compositionality comp_def map_sum.identity sum_rel_eq sum_rel_map1 sum_rel_map2
    7.64 +  apply (simp_all add: map_sum.compositionality comp_def map_sum.identity rel_sum_eq rel_sum_map1 rel_sum_map2
    7.65      Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
    7.66    using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
    7.67 -  apply (simp add: sum_rel_def comp_def split: sum.split)
    7.68 +  apply (simp add: rel_sum_def comp_def split: sum.split)
    7.69    done
    7.70  
    7.71 -declare [[mapQ3 sum = (sum_rel, sum_quotient)]]
    7.72 +declare [[mapQ3 sum = (rel_sum, sum_quotient)]]
    7.73  
    7.74  lemma sum_Inl_rsp [quot_respect]:
    7.75    assumes q1: "Quotient3 R1 Abs1 Rep1"
    7.76    assumes q2: "Quotient3 R2 Abs2 Rep2"
    7.77 -  shows "(R1 ===> sum_rel R1 R2) Inl Inl"
    7.78 +  shows "(R1 ===> rel_sum R1 R2) Inl Inl"
    7.79    by auto
    7.80  
    7.81  lemma sum_Inr_rsp [quot_respect]:
    7.82    assumes q1: "Quotient3 R1 Abs1 Rep1"
    7.83    assumes q2: "Quotient3 R2 Abs2 Rep2"
    7.84 -  shows "(R2 ===> sum_rel R1 R2) Inr Inr"
    7.85 +  shows "(R2 ===> rel_sum R1 R2) Inr Inr"
    7.86    by auto
    7.87  
    7.88  lemma sum_Inl_prs [quot_preserve]:
     8.1 --- a/src/HOL/Lifting_Sum.thy	Thu Mar 06 15:14:09 2014 +0100
     8.2 +++ b/src/HOL/Lifting_Sum.thy	Thu Mar 06 15:25:21 2014 +0100
     8.3 @@ -12,54 +12,54 @@
     8.4  
     8.5  abbreviation (input) "sum_pred \<equiv> case_sum"
     8.6  
     8.7 -lemmas sum_rel_eq[relator_eq] = sum.rel_eq
     8.8 -lemmas sum_rel_mono[relator_mono] = sum.rel_mono
     8.9 +lemmas rel_sum_eq[relator_eq] = sum.rel_eq
    8.10 +lemmas rel_sum_mono[relator_mono] = sum.rel_mono
    8.11  
    8.12 -lemma sum_rel_OO[relator_distr]:
    8.13 -  "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
    8.14 -  by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split)
    8.15 +lemma rel_sum_OO[relator_distr]:
    8.16 +  "(rel_sum A B) OO (rel_sum C D) = rel_sum (A OO C) (B OO D)"
    8.17 +  by (rule ext)+ (auto simp add: rel_sum_def OO_def split_sum_ex split: sum.split)
    8.18  
    8.19  lemma Domainp_sum[relator_domain]:
    8.20    assumes "Domainp R1 = P1"
    8.21    assumes "Domainp R2 = P2"
    8.22 -  shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
    8.23 +  shows "Domainp (rel_sum R1 R2) = (sum_pred P1 P2)"
    8.24  using assms
    8.25  by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
    8.26  
    8.27 -lemma left_total_sum_rel[reflexivity_rule]:
    8.28 -  "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
    8.29 +lemma left_total_rel_sum[reflexivity_rule]:
    8.30 +  "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (rel_sum R1 R2)"
    8.31    using assms unfolding left_total_def split_sum_all split_sum_ex by simp
    8.32  
    8.33 -lemma left_unique_sum_rel [reflexivity_rule]:
    8.34 -  "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)"
    8.35 +lemma left_unique_rel_sum [reflexivity_rule]:
    8.36 +  "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (rel_sum R1 R2)"
    8.37    using assms unfolding left_unique_def split_sum_all by simp
    8.38  
    8.39 -lemma right_total_sum_rel [transfer_rule]:
    8.40 -  "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
    8.41 +lemma right_total_rel_sum [transfer_rule]:
    8.42 +  "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (rel_sum R1 R2)"
    8.43    unfolding right_total_def split_sum_all split_sum_ex by simp
    8.44  
    8.45 -lemma right_unique_sum_rel [transfer_rule]:
    8.46 -  "right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (sum_rel R1 R2)"
    8.47 +lemma right_unique_rel_sum [transfer_rule]:
    8.48 +  "right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (rel_sum R1 R2)"
    8.49    unfolding right_unique_def split_sum_all by simp
    8.50  
    8.51 -lemma bi_total_sum_rel [transfer_rule]:
    8.52 -  "bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (sum_rel R1 R2)"
    8.53 +lemma bi_total_rel_sum [transfer_rule]:
    8.54 +  "bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (rel_sum R1 R2)"
    8.55    using assms unfolding bi_total_def split_sum_all split_sum_ex by simp
    8.56  
    8.57 -lemma bi_unique_sum_rel [transfer_rule]:
    8.58 -  "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
    8.59 +lemma bi_unique_rel_sum [transfer_rule]:
    8.60 +  "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (rel_sum R1 R2)"
    8.61    using assms unfolding bi_unique_def split_sum_all by simp
    8.62  
    8.63  lemma sum_invariant_commute [invariant_commute]: 
    8.64 -  "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
    8.65 -  by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_def split: sum.split)
    8.66 +  "rel_sum (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
    8.67 +  by (auto simp add: fun_eq_iff Lifting.invariant_def rel_sum_def split: sum.split)
    8.68  
    8.69  subsection {* Quotient theorem for the Lifting package *}
    8.70  
    8.71  lemma Quotient_sum[quot_map]:
    8.72    assumes "Quotient R1 Abs1 Rep1 T1"
    8.73    assumes "Quotient R2 Abs2 Rep2 T2"
    8.74 -  shows "Quotient (sum_rel R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2) (sum_rel T1 T2)"
    8.75 +  shows "Quotient (rel_sum R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2) (rel_sum T1 T2)"
    8.76    using assms unfolding Quotient_alt_def
    8.77    by (simp add: split_sum_all)
    8.78  
    8.79 @@ -69,15 +69,15 @@
    8.80  begin
    8.81  interpretation lifting_syntax .
    8.82  
    8.83 -lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
    8.84 +lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
    8.85    unfolding fun_rel_def by simp
    8.86  
    8.87 -lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr"
    8.88 +lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
    8.89    unfolding fun_rel_def by simp
    8.90  
    8.91  lemma case_sum_transfer [transfer_rule]:
    8.92 -  "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) case_sum case_sum"
    8.93 -  unfolding fun_rel_def sum_rel_def by (simp split: sum.split)
    8.94 +  "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
    8.95 +  unfolding fun_rel_def rel_sum_def by (simp split: sum.split)
    8.96  
    8.97  end
    8.98  
     9.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 15:14:09 2014 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 15:25:21 2014 +0100
     9.3 @@ -42,7 +42,7 @@
     9.4    @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
     9.5        Union_Un_distrib image_iff o_apply map_prod_simp
     9.6        mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
     9.7 -val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply};
     9.8 +val sum_prod_thms_rel = @{thms prod_rel_apply rel_sum_simps id_apply};
     9.9  
    9.10  fun hhf_concl_conv cv ctxt ct =
    9.11    (case Thm.term_of ct of