renamed 'prod_rel' to 'rel_prod'
authorblanchet
Thu Mar 06 15:29:18 2014 +0100 (2014-03-06)
changeset 559447ab8f003fe41
parent 55943 5c2df04e97d1
child 55945 e96383acecf9
renamed 'prod_rel' to 'rel_prod'
NEWS
src/Doc/IsarRef/HOL_Specific.thy
src/HOL/BNF_Examples/Process.thy
src/HOL/Basic_BNFs.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Lifting_Product.thy
src/HOL/List.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/NEWS	Thu Mar 06 15:25:21 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 06 15:29:18 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 +    prod_rel ~> rel_prod
     1.8      sum_rel ~> rel_sum
     1.9      set_rel ~> rel_set
    1.10      filter_rel ~> rel_filter
     2.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Thu Mar 06 15:25:21 2014 +0100
     2.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Thu Mar 06 15:29:18 2014 +0100
     2.3 @@ -1565,7 +1565,7 @@
     2.4      using the same attribute. For example:
     2.5  
     2.6      @{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\
     2.7 -    @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (prod_rel A B)"}
     2.8 +    @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)"}
     2.9  
    2.10    \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
    2.11      of rules, which specify a domain of a transfer relation by a predicate.
     3.1 --- a/src/HOL/BNF_Examples/Process.thy	Thu Mar 06 15:25:21 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/Process.thy	Thu Mar 06 15:29:18 2014 +0100
     3.3 @@ -24,7 +24,7 @@
     3.4  declare
     3.5    rel_pre_process_def[simp]
     3.6    rel_sum_def[simp]
     3.7 -  prod_rel_def[simp]
     3.8 +  rel_prod_def[simp]
     3.9  
    3.10  (* Constructors versus discriminators *)
    3.11  theorem isAction_isChoice:
     4.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:25:21 2014 +0100
     4.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:29:18 2014 +0100
     4.3 @@ -104,19 +104,19 @@
     4.4  lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
     4.5  
     4.6  definition
     4.7 -  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
     4.8 +  rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
     4.9  where
    4.10 -  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    4.11 +  "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    4.12  
    4.13 -lemma prod_rel_apply [simp]:
    4.14 -  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    4.15 -  by (simp add: prod_rel_def)
    4.16 +lemma rel_prod_apply [simp]:
    4.17 +  "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    4.18 +  by (simp add: rel_prod_def)
    4.19  
    4.20  bnf "'a \<times> 'b"
    4.21    map: map_prod
    4.22    sets: fsts snds
    4.23    bd: natLeq
    4.24 -  rel: prod_rel
    4.25 +  rel: rel_prod
    4.26  proof (unfold prod_set_defs)
    4.27    show "map_prod id id = id" by (rule map_prod.id)
    4.28  next
    4.29 @@ -149,13 +149,13 @@
    4.30      by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
    4.31  next
    4.32    fix R1 R2 S1 S2
    4.33 -  show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
    4.34 +  show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> rel_prod (R1 OO S1) (R2 OO S2)" by auto
    4.35  next
    4.36    fix R S
    4.37 -  show "prod_rel R S =
    4.38 +  show "rel_prod R S =
    4.39          (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
    4.40          Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
    4.41 -  unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    4.42 +  unfolding prod_set_defs rel_prod_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    4.43    by auto
    4.44  qed
    4.45  
     5.1 --- a/src/HOL/Library/Mapping.thy	Thu Mar 06 15:25:21 2014 +0100
     5.2 +++ b/src/HOL/Library/Mapping.thy	Thu Mar 06 15:29:18 2014 +0100
     5.3 @@ -43,7 +43,7 @@
     5.4  
     5.5  lemma map_of_transfer [transfer_rule]:
     5.6    assumes [transfer_rule]: "bi_unique R1"
     5.7 -  shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
     5.8 +  shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
     5.9  unfolding map_of_def by transfer_prover
    5.10  
    5.11  lemma tabulate_transfer: 
     6.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu Mar 06 15:25:21 2014 +0100
     6.2 +++ b/src/HOL/Library/Quotient_Product.thy	Thu Mar 06 15:29:18 2014 +0100
     6.3 @@ -14,20 +14,20 @@
     6.4    shows "map_prod id id = id"
     6.5    by (simp add: fun_eq_iff)
     6.6  
     6.7 -lemma prod_rel_eq [id_simps]:
     6.8 -  shows "prod_rel (op =) (op =) = (op =)"
     6.9 +lemma rel_prod_eq [id_simps]:
    6.10 +  shows "rel_prod (op =) (op =) = (op =)"
    6.11    by (simp add: fun_eq_iff)
    6.12  
    6.13  lemma prod_equivp [quot_equiv]:
    6.14    assumes "equivp R1"
    6.15    assumes "equivp R2"
    6.16 -  shows "equivp (prod_rel R1 R2)"
    6.17 +  shows "equivp (rel_prod R1 R2)"
    6.18    using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
    6.19  
    6.20  lemma prod_quotient [quot_thm]:
    6.21    assumes "Quotient3 R1 Abs1 Rep1"
    6.22    assumes "Quotient3 R2 Abs2 Rep2"
    6.23 -  shows "Quotient3 (prod_rel R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2)"
    6.24 +  shows "Quotient3 (rel_prod R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2)"
    6.25    apply (rule Quotient3I)
    6.26    apply (simp add: map_prod.compositionality comp_def map_prod.identity
    6.27       Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)])
    6.28 @@ -36,12 +36,12 @@
    6.29    apply (auto simp add: split_paired_all)
    6.30    done
    6.31  
    6.32 -declare [[mapQ3 prod = (prod_rel, prod_quotient)]]
    6.33 +declare [[mapQ3 prod = (rel_prod, prod_quotient)]]
    6.34  
    6.35  lemma Pair_rsp [quot_respect]:
    6.36    assumes q1: "Quotient3 R1 Abs1 Rep1"
    6.37    assumes q2: "Quotient3 R2 Abs2 Rep2"
    6.38 -  shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
    6.39 +  shows "(R1 ===> R2 ===> rel_prod R1 R2) Pair Pair"
    6.40    by (rule Pair_transfer)
    6.41  
    6.42  lemma Pair_prs [quot_preserve]:
    6.43 @@ -55,7 +55,7 @@
    6.44  lemma fst_rsp [quot_respect]:
    6.45    assumes "Quotient3 R1 Abs1 Rep1"
    6.46    assumes "Quotient3 R2 Abs2 Rep2"
    6.47 -  shows "(prod_rel R1 R2 ===> R1) fst fst"
    6.48 +  shows "(rel_prod R1 R2 ===> R1) fst fst"
    6.49    by auto
    6.50  
    6.51  lemma fst_prs [quot_preserve]:
    6.52 @@ -67,7 +67,7 @@
    6.53  lemma snd_rsp [quot_respect]:
    6.54    assumes "Quotient3 R1 Abs1 Rep1"
    6.55    assumes "Quotient3 R2 Abs2 Rep2"
    6.56 -  shows "(prod_rel R1 R2 ===> R2) snd snd"
    6.57 +  shows "(rel_prod R1 R2 ===> R2) snd snd"
    6.58    by auto
    6.59  
    6.60  lemma snd_prs [quot_preserve]:
    6.61 @@ -77,7 +77,7 @@
    6.62    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
    6.63  
    6.64  lemma split_rsp [quot_respect]:
    6.65 -  shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
    6.66 +  shows "((R1 ===> R2 ===> (op =)) ===> (rel_prod R1 R2) ===> (op =)) split split"
    6.67    by (rule case_prod_transfer)
    6.68  
    6.69  lemma split_prs [quot_preserve]:
    6.70 @@ -88,18 +88,18 @@
    6.71  
    6.72  lemma [quot_respect]:
    6.73    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
    6.74 -  prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
    6.75 -  by (rule prod_rel_transfer)
    6.76 +  rel_prod R2 R1 ===> rel_prod R2 R1 ===> op =) rel_prod rel_prod"
    6.77 +  by (rule rel_prod_transfer)
    6.78  
    6.79  lemma [quot_preserve]:
    6.80    assumes q1: "Quotient3 R1 abs1 rep1"
    6.81    and     q2: "Quotient3 R2 abs2 rep2"
    6.82    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
    6.83 -  map_prod rep1 rep2 ---> map_prod rep1 rep2 ---> id) prod_rel = prod_rel"
    6.84 +  map_prod rep1 rep2 ---> map_prod rep1 rep2 ---> id) rel_prod = rel_prod"
    6.85    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
    6.86  
    6.87  lemma [quot_preserve]:
    6.88 -  shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
    6.89 +  shows"(rel_prod ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
    6.90    (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))"
    6.91    by simp
    6.92  
     7.1 --- a/src/HOL/Lifting_Product.thy	Thu Mar 06 15:25:21 2014 +0100
     7.2 +++ b/src/HOL/Lifting_Product.thy	Thu Mar 06 15:29:18 2014 +0100
     7.3 @@ -17,60 +17,60 @@
     7.4    "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
     7.5    by (simp add: prod_pred_def)
     7.6  
     7.7 -lemmas prod_rel_eq[relator_eq] = prod.rel_eq
     7.8 -lemmas prod_rel_mono[relator_mono] = prod.rel_mono
     7.9 +lemmas rel_prod_eq[relator_eq] = prod.rel_eq
    7.10 +lemmas rel_prod_mono[relator_mono] = prod.rel_mono
    7.11  
    7.12 -lemma prod_rel_OO[relator_distr]:
    7.13 -  "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
    7.14 -by (rule ext)+ (auto simp: prod_rel_def OO_def)
    7.15 +lemma rel_prod_OO[relator_distr]:
    7.16 +  "(rel_prod A B) OO (rel_prod C D) = rel_prod (A OO C) (B OO D)"
    7.17 +by (rule ext)+ (auto simp: rel_prod_def OO_def)
    7.18  
    7.19  lemma Domainp_prod[relator_domain]:
    7.20    assumes "Domainp T1 = P1"
    7.21    assumes "Domainp T2 = P2"
    7.22 -  shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
    7.23 -using assms unfolding prod_rel_def prod_pred_def by blast
    7.24 +  shows "Domainp (rel_prod T1 T2) = (prod_pred P1 P2)"
    7.25 +using assms unfolding rel_prod_def prod_pred_def by blast
    7.26  
    7.27 -lemma left_total_prod_rel [reflexivity_rule]:
    7.28 +lemma left_total_rel_prod [reflexivity_rule]:
    7.29    assumes "left_total R1"
    7.30    assumes "left_total R2"
    7.31 -  shows "left_total (prod_rel R1 R2)"
    7.32 -  using assms unfolding left_total_def prod_rel_def by auto
    7.33 +  shows "left_total (rel_prod R1 R2)"
    7.34 +  using assms unfolding left_total_def rel_prod_def by auto
    7.35  
    7.36 -lemma left_unique_prod_rel [reflexivity_rule]:
    7.37 +lemma left_unique_rel_prod [reflexivity_rule]:
    7.38    assumes "left_unique R1" and "left_unique R2"
    7.39 -  shows "left_unique (prod_rel R1 R2)"
    7.40 -  using assms unfolding left_unique_def prod_rel_def by auto
    7.41 +  shows "left_unique (rel_prod R1 R2)"
    7.42 +  using assms unfolding left_unique_def rel_prod_def by auto
    7.43  
    7.44 -lemma right_total_prod_rel [transfer_rule]:
    7.45 +lemma right_total_rel_prod [transfer_rule]:
    7.46    assumes "right_total R1" and "right_total R2"
    7.47 -  shows "right_total (prod_rel R1 R2)"
    7.48 -  using assms unfolding right_total_def prod_rel_def by auto
    7.49 +  shows "right_total (rel_prod R1 R2)"
    7.50 +  using assms unfolding right_total_def rel_prod_def by auto
    7.51  
    7.52 -lemma right_unique_prod_rel [transfer_rule]:
    7.53 +lemma right_unique_rel_prod [transfer_rule]:
    7.54    assumes "right_unique R1" and "right_unique R2"
    7.55 -  shows "right_unique (prod_rel R1 R2)"
    7.56 -  using assms unfolding right_unique_def prod_rel_def by auto
    7.57 +  shows "right_unique (rel_prod R1 R2)"
    7.58 +  using assms unfolding right_unique_def rel_prod_def by auto
    7.59  
    7.60 -lemma bi_total_prod_rel [transfer_rule]:
    7.61 +lemma bi_total_rel_prod [transfer_rule]:
    7.62    assumes "bi_total R1" and "bi_total R2"
    7.63 -  shows "bi_total (prod_rel R1 R2)"
    7.64 -  using assms unfolding bi_total_def prod_rel_def by auto
    7.65 +  shows "bi_total (rel_prod R1 R2)"
    7.66 +  using assms unfolding bi_total_def rel_prod_def by auto
    7.67  
    7.68 -lemma bi_unique_prod_rel [transfer_rule]:
    7.69 +lemma bi_unique_rel_prod [transfer_rule]:
    7.70    assumes "bi_unique R1" and "bi_unique R2"
    7.71 -  shows "bi_unique (prod_rel R1 R2)"
    7.72 -  using assms unfolding bi_unique_def prod_rel_def by auto
    7.73 +  shows "bi_unique (rel_prod R1 R2)"
    7.74 +  using assms unfolding bi_unique_def rel_prod_def by auto
    7.75  
    7.76  lemma prod_invariant_commute [invariant_commute]: 
    7.77 -  "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
    7.78 -  by (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) blast
    7.79 +  "rel_prod (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
    7.80 +  by (simp add: fun_eq_iff rel_prod_def prod_pred_def Lifting.invariant_def) blast
    7.81  
    7.82  subsection {* Quotient theorem for the Lifting package *}
    7.83  
    7.84  lemma Quotient_prod[quot_map]:
    7.85    assumes "Quotient R1 Abs1 Rep1 T1"
    7.86    assumes "Quotient R2 Abs2 Rep2 T2"
    7.87 -  shows "Quotient (prod_rel R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2) (prod_rel T1 T2)"
    7.88 +  shows "Quotient (rel_prod R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2) (rel_prod T1 T2)"
    7.89    using assms unfolding Quotient_alt_def by auto
    7.90  
    7.91  subsection {* Transfer rules for the Transfer package *}
    7.92 @@ -79,31 +79,31 @@
    7.93  begin
    7.94  interpretation lifting_syntax .
    7.95  
    7.96 -lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
    7.97 -  unfolding fun_rel_def prod_rel_def by simp
    7.98 +lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
    7.99 +  unfolding fun_rel_def rel_prod_def by simp
   7.100  
   7.101 -lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst"
   7.102 -  unfolding fun_rel_def prod_rel_def by simp
   7.103 +lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
   7.104 +  unfolding fun_rel_def rel_prod_def by simp
   7.105  
   7.106 -lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
   7.107 -  unfolding fun_rel_def prod_rel_def by simp
   7.108 +lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
   7.109 +  unfolding fun_rel_def rel_prod_def by simp
   7.110  
   7.111  lemma case_prod_transfer [transfer_rule]:
   7.112 -  "((A ===> B ===> C) ===> prod_rel A B ===> C) case_prod case_prod"
   7.113 -  unfolding fun_rel_def prod_rel_def by simp
   7.114 +  "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
   7.115 +  unfolding fun_rel_def rel_prod_def by simp
   7.116  
   7.117  lemma curry_transfer [transfer_rule]:
   7.118 -  "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
   7.119 +  "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
   7.120    unfolding curry_def by transfer_prover
   7.121  
   7.122  lemma map_prod_transfer [transfer_rule]:
   7.123 -  "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
   7.124 +  "((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D)
   7.125      map_prod map_prod"
   7.126    unfolding map_prod_def [abs_def] by transfer_prover
   7.127  
   7.128 -lemma prod_rel_transfer [transfer_rule]:
   7.129 +lemma rel_prod_transfer [transfer_rule]:
   7.130    "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
   7.131 -    prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel"
   7.132 +    rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
   7.133    unfolding fun_rel_def by auto
   7.134  
   7.135  end
     8.1 --- a/src/HOL/List.thy	Thu Mar 06 15:25:21 2014 +0100
     8.2 +++ b/src/HOL/List.thy	Thu Mar 06 15:29:18 2014 +0100
     8.3 @@ -6793,11 +6793,11 @@
     8.4    unfolding dropWhile_def by transfer_prover
     8.5  
     8.6  lemma zip_transfer [transfer_rule]:
     8.7 -  "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) zip zip"
     8.8 +  "(list_all2 A ===> list_all2 B ===> list_all2 (rel_prod A B)) zip zip"
     8.9    unfolding zip_def by transfer_prover
    8.10  
    8.11  lemma product_transfer [transfer_rule]:
    8.12 -  "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) List.product List.product"
    8.13 +  "(list_all2 A ===> list_all2 B ===> list_all2 (rel_prod A B)) List.product List.product"
    8.14    unfolding List.product_def by transfer_prover
    8.15  
    8.16  lemma product_lists_transfer [transfer_rule]:
    8.17 @@ -6868,7 +6868,7 @@
    8.18    unfolding sublist_def [abs_def] by transfer_prover
    8.19  
    8.20  lemma partition_transfer [transfer_rule]:
    8.21 -  "((A ===> op =) ===> list_all2 A ===> prod_rel (list_all2 A) (list_all2 A))
    8.22 +  "((A ===> op =) ===> list_all2 A ===> rel_prod (list_all2 A) (list_all2 A))
    8.23      partition partition"
    8.24    unfolding partition_def by transfer_prover
    8.25  
     9.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 15:25:21 2014 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 15:29:18 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 rel_sum_simps id_apply};
     9.8 +val sum_prod_thms_rel = @{thms rel_prod_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