1.1 --- a/src/HOL/BNF/Examples/Koenig.thy	Tue Nov 19 10:05:53 2013 +0100
     1.2 +++ b/src/HOL/BNF/Examples/Koenig.thy	Tue Nov 19 14:11:26 2013 +0100
     1.3 @@ -12,44 +12,33 @@
     1.4  imports TreeFI Stream
     1.5  begin
     1.6  
     1.7 -(* selectors for streams *)
     1.8 -lemma shd_def': "shd as = fst (stream_dtor as)"
     1.9 -apply (case_tac as)
    1.10 -apply (auto simp add: shd_def)
    1.11 -by (simp add: Stream_def stream.dtor_ctor)
    1.12 -
    1.13 -lemma stl_def': "stl as = snd (stream_dtor as)"
    1.14 -apply (case_tac as)
    1.15 -apply (auto simp add: stl_def)
    1.16 -by (simp add: Stream_def stream.dtor_ctor)
    1.17 -
    1.18  (* infinite trees: *)
    1.19  coinductive infiniteTr where
    1.20 -"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
    1.21 +"\<lbrakk>tr' \<in> set_listF (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
    1.22  
    1.23  lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
    1.24  assumes *: "phi tr" and
    1.25 -**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'"
    1.26 +**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> set_listF (sub tr). phi tr' \<or> infiniteTr tr'"
    1.27  shows "infiniteTr tr"
    1.28  using assms by (elim infiniteTr.coinduct) blast
    1.29  
    1.30  lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
    1.31  assumes *: "phi tr" and
    1.32 -**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'"
    1.33 +**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> set_listF (sub tr). phi tr'"
    1.34  shows "infiniteTr tr"
    1.35  using assms by (elim infiniteTr.coinduct) blast
    1.36  
    1.37  lemma infiniteTr_sub[simp]:
    1.38 -"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
    1.39 +"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> set_listF (sub tr). infiniteTr tr')"
    1.40  by (erule infiniteTr.cases) blast
    1.41  
    1.42  primcorec konigPath where
    1.43    "shd (konigPath t) = lab t"
    1.44 -| "stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
    1.45 +| "stl (konigPath t) = konigPath (SOME tr. tr \<in> set_listF (sub t) \<and> infiniteTr tr)"
    1.46  
    1.47  (* proper paths in trees: *)
    1.48  coinductive properPath where
    1.49 -"\<lbrakk>shd as = lab tr; tr' \<in> listF_set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
    1.50 +"\<lbrakk>shd as = lab tr; tr' \<in> set_listF (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
    1.51   properPath as tr"
    1.52  
    1.53  lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]:
    1.54 @@ -57,7 +46,7 @@
    1.55  **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
    1.56  ***: "\<And> as tr.
    1.57           phi as tr \<Longrightarrow>
    1.58 -         \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    1.59 +         \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    1.60  shows "properPath as tr"
    1.61  using assms by (elim properPath.coinduct) blast
    1.62  
    1.63 @@ -66,7 +55,7 @@
    1.64  **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
    1.65  ***: "\<And> as tr.
    1.66           phi as tr \<Longrightarrow>
    1.67 -         \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr'"
    1.68 +         \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr'"
    1.69  shows "properPath as tr"
    1.70  using properPath_strong_coind[of phi, OF * **] *** by blast
    1.71  
    1.72 @@ -76,7 +65,7 @@
    1.73  
    1.74  lemma properPath_sub:
    1.75  "properPath as tr \<Longrightarrow>
    1.76 - \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    1.77 + \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    1.78  by (erule properPath.cases) blast
    1.79  
    1.80  (* prove the following by coinduction *)
    1.81 @@ -88,10 +77,10 @@
    1.82     assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
    1.83     proof (coinduction arbitrary: tr as rule: properPath_coind)
    1.84       case (sub tr as)
    1.85 -     let ?t = "SOME t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'"
    1.86 -     from sub have "\<exists>t' \<in> listF_set (sub tr). infiniteTr t'" by simp
    1.87 -     then have "\<exists>t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'" by blast
    1.88 -     then have "?t \<in> listF_set (sub tr) \<and> infiniteTr ?t" by (rule someI_ex)
    1.89 +     let ?t = "SOME t'. t' \<in> set_listF (sub tr) \<and> infiniteTr t'"
    1.90 +     from sub have "\<exists>t' \<in> set_listF (sub tr). infiniteTr t'" by simp
    1.91 +     then have "\<exists>t'. t' \<in> set_listF (sub tr) \<and> infiniteTr t'" by blast
    1.92 +     then have "?t \<in> set_listF (sub tr) \<and> infiniteTr ?t" by (rule someI_ex)
    1.93       moreover have "stl (konigPath tr) = konigPath ?t" by simp
    1.94       ultimately show ?case using sub by blast
    1.95     qed simp

     2.1 --- a/src/HOL/BNF/Examples/ListF.thy	Tue Nov 19 10:05:53 2013 +0100
     2.2 +++ b/src/HOL/BNF/Examples/ListF.thy	Tue Nov 19 14:11:26 2013 +0100
     2.3 @@ -62,7 +62,7 @@
     2.4    "i < lengthh xs \<Longrightarrow> nthh (mapF f xs) i = f (nthh xs i)"
     2.5    by (induct rule: nthh.induct) auto
     2.6  
     2.7 -lemma nthh_listF_set[simp]: "i < lengthh xs \<Longrightarrow> nthh xs i \<in> listF_set xs"
     2.8 +lemma nthh_listF_set[simp]: "i < lengthh xs \<Longrightarrow> nthh xs i \<in> set_listF xs"
     2.9    by (induct rule: nthh.induct) auto
    2.10  
    2.11  lemma NilF_iff[iff]: "(lengthh xs = 0) = (xs = NilF)"
    2.12 @@ -105,7 +105,7 @@
    2.13  qed simp
    2.14  
    2.15  lemma list_set_nthh[simp]:
    2.16 -  "(x \<in> listF_set xs) \<Longrightarrow> (\<exists>i < lengthh xs. nthh xs i = x)"
    2.17 +  "(x \<in> set_listF xs) \<Longrightarrow> (\<exists>i < lengthh xs. nthh xs i = x)"
    2.18    by (induct xs) (auto, induct rule: nthh.induct, auto)
    2.19  
    2.20  end

     3.1 --- a/src/HOL/BNF/Examples/Process.thy	Tue Nov 19 10:05:53 2013 +0100
     3.2 +++ b/src/HOL/BNF/Examples/Process.thy	Tue Nov 19 14:11:26 2013 +0100
     3.3 @@ -22,7 +22,7 @@
     3.4  subsection {* Basic properties *}
     3.5  
     3.6  declare
     3.7 -  pre_process_rel_def[simp]
     3.8 +  rel_pre_process_def[simp]
     3.9    sum_rel_def[simp]
    3.10    prod_rel_def[simp]
    3.11  

     4.1 --- a/src/HOL/BNF/More_BNFs.thy	Tue Nov 19 10:05:53 2013 +0100
     4.2 +++ b/src/HOL/BNF/More_BNFs.thy	Tue Nov 19 14:11:26 2013 +0100
     4.3 @@ -909,18 +909,18 @@
     4.4  by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
     4.5    intro: mmap_cong wpull_mmap)
     4.6  
     4.7 -inductive multiset_rel' where
     4.8 -Zero: "multiset_rel' R {#} {#}"
     4.9 +inductive rel_multiset' where
    4.10 +Zero: "rel_multiset' R {#} {#}"
    4.11  |
    4.12 -Plus: "\<lbrakk>R a b; multiset_rel' R M N\<rbrakk> \<Longrightarrow> multiset_rel' R (M + {#a#}) (N + {#b#})"
    4.13 +Plus: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"
    4.14  
    4.15 -lemma multiset_map_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> M = {#}"
    4.16 +lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> M = {#}"
    4.17  by (metis image_is_empty multiset.set_map set_of_eq_empty_iff)
    4.18  
    4.19 -lemma multiset_map_Zero[simp]: "mmap f {#} = {#}" by simp
    4.20 +lemma map_multiset_Zero[simp]: "mmap f {#} = {#}" by simp
    4.21  
    4.22 -lemma multiset_rel_Zero: "multiset_rel R {#} {#}"
    4.23 -unfolding multiset_rel_def Grp_def by auto
    4.24 +lemma rel_multiset_Zero: "rel_multiset R {#} {#}"
    4.25 +unfolding rel_multiset_def Grp_def by auto
    4.26  
    4.27  declare multiset.count[simp]
    4.28  declare Abs_multiset_inverse[simp]
    4.29 @@ -928,7 +928,7 @@
    4.30  declare union_preserves_multiset[simp]
    4.31  
    4.32  
    4.33 -lemma multiset_map_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2"
    4.34 +lemma map_multiset_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2"
    4.35  proof (intro multiset_eqI, transfer fixing: f)
    4.36    fix x :: 'a and M1 M2 :: "'b \<Rightarrow> nat"
    4.37    assume "M1 \<in> multiset" "M2 \<in> multiset"
    4.38 @@ -941,12 +941,12 @@
    4.39      by (auto simp: setsum.distrib[symmetric])
    4.40  qed
    4.41  
    4.42 -lemma multiset_map_singl[simp]: "mmap f {#a#} = {#f a#}"
    4.43 +lemma map_multiset_singl[simp]: "mmap f {#a#} = {#f a#}"
    4.44    by transfer auto
    4.45  
    4.46 -lemma multiset_rel_Plus:
    4.47 -assumes ab: "R a b" and MN: "multiset_rel R M N"
    4.48 -shows "multiset_rel R (M + {#a#}) (N + {#b#})"
    4.49 +lemma rel_multiset_Plus:
    4.50 +assumes ab: "R a b" and MN: "rel_multiset R M N"
    4.51 +shows "rel_multiset R (M + {#a#}) (N + {#b#})"
    4.52  proof-
    4.53    {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
    4.54     hence "\<exists>ya. mmap fst y + {#a#} = mmap fst ya \<and>
    4.55 @@ -956,13 +956,13 @@
    4.56    }
    4.57    thus ?thesis
    4.58    using assms
    4.59 -  unfolding multiset_rel_def Grp_def by force
    4.60 +  unfolding rel_multiset_def Grp_def by force
    4.61  qed
    4.62  
    4.63 -lemma multiset_rel'_imp_multiset_rel:
    4.64 -"multiset_rel' R M N \<Longrightarrow> multiset_rel R M N"
    4.65 -apply(induct rule: multiset_rel'.induct)
    4.66 -using multiset_rel_Zero multiset_rel_Plus by auto
    4.67 +lemma rel_multiset'_imp_rel_multiset:
    4.68 +"rel_multiset' R M N \<Longrightarrow> rel_multiset R M N"
    4.69 +apply(induct rule: rel_multiset'.induct)
    4.70 +using rel_multiset_Zero rel_multiset_Plus by auto
    4.71  
    4.72  lemma mcard_mmap[simp]: "mcard (mmap f M) = mcard M"
    4.73  proof -
    4.74 @@ -994,10 +994,10 @@
    4.75    then show ?thesis unfolding mcard_unfold_setsum A_def by transfer
    4.76  qed
    4.77  
    4.78 -lemma multiset_rel_mcard:
    4.79 -assumes "multiset_rel R M N"
    4.80 +lemma rel_multiset_mcard:
    4.81 +assumes "rel_multiset R M N"
    4.82  shows "mcard M = mcard N"
    4.83 -using assms unfolding multiset_rel_def Grp_def by auto
    4.84 +using assms unfolding rel_multiset_def Grp_def by auto
    4.85  
    4.86  lemma multiset_induct2[case_names empty addL addR]:
    4.87  assumes empty: "P {#} {#}"
    4.88 @@ -1052,67 +1052,67 @@
    4.89  qed
    4.90  
    4.91  lemma msed_rel_invL:
    4.92 -assumes "multiset_rel R (M + {#a#}) N"
    4.93 -shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> multiset_rel R M N1"
    4.94 +assumes "rel_multiset R (M + {#a#}) N"
    4.95 +shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_multiset R M N1"
    4.96  proof-
    4.97    obtain K where KM: "mmap fst K = M + {#a#}"
    4.98    and KN: "mmap snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
    4.99    using assms
   4.100 -  unfolding multiset_rel_def Grp_def by auto
   4.101 +  unfolding rel_multiset_def Grp_def by auto
   4.102    obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
   4.103    and K1M: "mmap fst K1 = M" using msed_map_invR[OF KM] by auto
   4.104    obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "mmap snd K1 = N1"
   4.105    using msed_map_invL[OF KN[unfolded K]] by auto
   4.106    have Rab: "R a (snd ab)" using sK a unfolding K by auto
   4.107 -  have "multiset_rel R M N1" using sK K1M K1N1
   4.108 -  unfolding K multiset_rel_def Grp_def by auto
   4.109 +  have "rel_multiset R M N1" using sK K1M K1N1
   4.110 +  unfolding K rel_multiset_def Grp_def by auto
   4.111    thus ?thesis using N Rab by auto
   4.112  qed
   4.113  
   4.114  lemma msed_rel_invR:
   4.115 -assumes "multiset_rel R M (N + {#b#})"
   4.116 -shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> multiset_rel R M1 N"
   4.117 +assumes "rel_multiset R M (N + {#b#})"
   4.118 +shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_multiset R M1 N"
   4.119  proof-
   4.120    obtain K where KN: "mmap snd K = N + {#b#}"
   4.121    and KM: "mmap fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   4.122    using assms
   4.123 -  unfolding multiset_rel_def Grp_def by auto
   4.124 +  unfolding rel_multiset_def Grp_def by auto
   4.125    obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
   4.126    and K1N: "mmap snd K1 = N" using msed_map_invR[OF KN] by auto
   4.127    obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "mmap fst K1 = M1"
   4.128    using msed_map_invL[OF KM[unfolded K]] by auto
   4.129    have Rab: "R (fst ab) b" using sK b unfolding K by auto
   4.130 -  have "multiset_rel R M1 N" using sK K1N K1M1
   4.131 -  unfolding K multiset_rel_def Grp_def by auto
   4.132 +  have "rel_multiset R M1 N" using sK K1N K1M1
   4.133 +  unfolding K rel_multiset_def Grp_def by auto
   4.134    thus ?thesis using M Rab by auto
   4.135  qed
   4.136  
   4.137 -lemma multiset_rel_imp_multiset_rel':
   4.138 -assumes "multiset_rel R M N"
   4.139 -shows "multiset_rel' R M N"
   4.140 +lemma rel_multiset_imp_rel_multiset':
   4.141 +assumes "rel_multiset R M N"
   4.142 +shows "rel_multiset' R M N"
   4.143  using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
   4.144    case (less M)
   4.145 -  have c: "mcard M = mcard N" using multiset_rel_mcard[OF less.prems] .
   4.146 +  have c: "mcard M = mcard N" using rel_multiset_mcard[OF less.prems] .
   4.147    show ?case
   4.148    proof(cases "M = {#}")
   4.149      case True hence "N = {#}" using c by simp
   4.150 -    thus ?thesis using True multiset_rel'.Zero by auto
   4.151 +    thus ?thesis using True rel_multiset'.Zero by auto
   4.152    next
   4.153      case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
   4.154 -    obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "multiset_rel R M1 N1"
   4.155 +    obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_multiset R M1 N1"
   4.156      using msed_rel_invL[OF less.prems[unfolded M]] by auto
   4.157 -    have "multiset_rel' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
   4.158 -    thus ?thesis using multiset_rel'.Plus[of R a b, OF R] unfolding M N by simp
   4.159 +    have "rel_multiset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
   4.160 +    thus ?thesis using rel_multiset'.Plus[of R a b, OF R] unfolding M N by simp
   4.161    qed
   4.162  qed
   4.163  
   4.164 -lemma multiset_rel_multiset_rel':
   4.165 -"multiset_rel R M N = multiset_rel' R M N"
   4.166 -using  multiset_rel_imp_multiset_rel' multiset_rel'_imp_multiset_rel by auto
   4.167 +lemma rel_multiset_rel_multiset':
   4.168 +"rel_multiset R M N = rel_multiset' R M N"
   4.169 +using  rel_multiset_imp_rel_multiset' rel_multiset'_imp_rel_multiset by auto
   4.170  
   4.171 -(* The main end product for multiset_rel: inductive characterization *)
   4.172 -theorems multiset_rel_induct[case_names empty add, induct pred: multiset_rel] =
   4.173 -         multiset_rel'.induct[unfolded multiset_rel_multiset_rel'[symmetric]]
   4.174 +(* The main end product for rel_multiset: inductive characterization *)
   4.175 +theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] =
   4.176 +         rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]]
   4.177  
   4.178  
   4.179  
   4.180 @@ -1183,5 +1183,4 @@
   4.181    qed
   4.182  qed
   4.183  
   4.184 -
   4.185  end

     5.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Tue Nov 19 10:05:53 2013 +0100
     5.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Tue Nov 19 14:11:26 2013 +0100
     5.3 @@ -678,7 +678,7 @@
     5.4  
     5.5      val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
     5.6  
     5.7 -    fun mk_suffix_binding suf = Binding.suffix_name ("_" ^ suf) bnf_b;
     5.8 +    fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
     5.9  
    5.10      fun maybe_define user_specified (b, rhs) lthy =
    5.11        let
    5.12 @@ -703,7 +703,7 @@
    5.13        lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
    5.14  
    5.15      val map_bind_def =
    5.16 -      (fn () => def_qualify (if Binding.is_empty map_b then mk_suffix_binding mapN else map_b),
    5.17 +      (fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b),
    5.18           map_rhs);
    5.19      val set_binds_defs =
    5.20        let
    5.21 @@ -711,10 +711,10 @@
    5.22            (case try (nth set_bs) (i - 1) of
    5.23              SOME b => if Binding.is_empty b then get_b else K b
    5.24            | NONE => get_b) #> def_qualify;
    5.25 -        val bs = if live = 1 then [set_name 1 (fn () => mk_suffix_binding setN)]
    5.26 -          else map (fn i => set_name i (fn () => mk_suffix_binding (mk_setN i))) (1 upto live);
    5.27 +        val bs = if live = 1 then [set_name 1 (fn () => mk_prefix_binding setN)]
    5.28 +          else map (fn i => set_name i (fn () => mk_prefix_binding (mk_setN i))) (1 upto live);
    5.29        in bs ~~ set_rhss end;
    5.30 -    val bd_bind_def = (fn () => def_qualify (mk_suffix_binding bdN), bd_rhs);
    5.31 +    val bd_bind_def = (fn () => def_qualify (mk_prefix_binding bdN), bd_rhs);
    5.32  
    5.33      val ((((bnf_map_term, raw_map_def),
    5.34        (bnf_set_terms, raw_set_defs)),
    5.35 @@ -861,7 +861,7 @@
    5.36        | SOME raw_rel => prep_term no_defs_lthy raw_rel);
    5.37  
    5.38      val rel_bind_def =
    5.39 -      (fn () => def_qualify (if Binding.is_empty rel_b then mk_suffix_binding relN else rel_b),
    5.40 +      (fn () => def_qualify (if Binding.is_empty rel_b then mk_prefix_binding relN else rel_b),
    5.41           rel_rhs);
    5.42  
    5.43      val wit_rhss =
    5.44 @@ -873,8 +873,8 @@
    5.45      val nwits = length wit_rhss;
    5.46      val wit_binds_defs =
    5.47        let
    5.48 -        val bs = if nwits = 1 then [fn () => def_qualify (mk_suffix_binding witN)]
    5.49 -          else map (fn i => fn () => def_qualify (mk_suffix_binding (mk_witN i))) (1 upto nwits);
    5.50 +        val bs = if nwits = 1 then [fn () => def_qualify (mk_prefix_binding witN)]
    5.51 +          else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits);
    5.52        in bs ~~ wit_rhss end;
    5.53  
    5.54      val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =