boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
authorhaftmann
Sat Jun 11 16:22:42 2016 +0200 (2016-06-11)
changeset 632909ac558ab0906
parent 63289 26134a00d060
child 63291 b1d7950285cf
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
NEWS
src/HOL/Groups.thy
src/HOL/Groups_Big.thy
src/HOL/Groups_List.thy
src/HOL/Lattices.thy
src/HOL/Lattices_Big.thy
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/Library/Multiset.thy
src/HOL/Orderings.thy
     1.1 --- a/NEWS	Sat Jun 11 17:40:52 2016 +0200
     1.2 +++ b/NEWS	Sat Jun 11 16:22:42 2016 +0200
     1.3 @@ -132,6 +132,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Abstract locales semigroup, abel_semigroup, semilattice,
     1.8 +semilattice_neutr, ordering, ordering_top, semilattice_order,
     1.9 +semilattice_neutr_order, comm_monoid_set, semilattice_set,
    1.10 +semilattice_neutr_set, semilattice_order_set, semilattice_order_neutr_set
    1.11 +monoid_list, comm_monoid_list, comm_monoid_list_set, comm_monoid_mset,
    1.12 +comm_monoid_fun use boldified syntax uniformly that does not clash
    1.13 +with corresponding global syntax.  INCOMPATIBILITY.
    1.14 +
    1.15  * Conventional syntax "%(). t" for unit abstractions.  Slight syntactic
    1.16  INCOMPATIBILITY.
    1.17  
     2.1 --- a/src/HOL/Groups.thy	Sat Jun 11 17:40:52 2016 +0200
     2.2 +++ b/src/HOL/Groups.thy	Sat Jun 11 16:22:42 2016 +0200
     2.3 @@ -42,17 +42,17 @@
     2.4  \<close>
     2.5  
     2.6  locale semigroup =
     2.7 -  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
     2.8 -  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
     2.9 +  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^bold>*" 70)
    2.10 +  assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)"
    2.11  
    2.12  locale abel_semigroup = semigroup +
    2.13 -  assumes commute [ac_simps]: "a * b = b * a"
    2.14 +  assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a"
    2.15  begin
    2.16  
    2.17  lemma left_commute [ac_simps]:
    2.18 -  "b * (a * c) = a * (b * c)"
    2.19 +  "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)"
    2.20  proof -
    2.21 -  have "(b * a) * c = (a * b) * c"
    2.22 +  have "(b \<^bold>* a) \<^bold>* c = (a \<^bold>* b) \<^bold>* c"
    2.23      by (simp only: commute)
    2.24    then show ?thesis
    2.25      by (simp only: assoc)
    2.26 @@ -61,13 +61,13 @@
    2.27  end
    2.28  
    2.29  locale monoid = semigroup +
    2.30 -  fixes z :: 'a ("1")
    2.31 -  assumes left_neutral [simp]: "1 * a = a"
    2.32 -  assumes right_neutral [simp]: "a * 1 = a"
    2.33 +  fixes z :: 'a ("\<^bold>1")
    2.34 +  assumes left_neutral [simp]: "\<^bold>1 \<^bold>* a = a"
    2.35 +  assumes right_neutral [simp]: "a \<^bold>* \<^bold>1 = a"
    2.36  
    2.37  locale comm_monoid = abel_semigroup +
    2.38 -  fixes z :: 'a ("1")
    2.39 -  assumes comm_neutral: "a * 1 = a"
    2.40 +  fixes z :: 'a ("\<^bold>1")
    2.41 +  assumes comm_neutral: "a \<^bold>* \<^bold>1 = a"
    2.42  begin
    2.43  
    2.44  sublocale monoid
     3.1 --- a/src/HOL/Groups_Big.thy	Sat Jun 11 17:40:52 2016 +0200
     3.2 +++ b/src/HOL/Groups_Big.thy	Sat Jun 11 16:22:42 2016 +0200
     3.3 @@ -11,9 +11,6 @@
     3.4  
     3.5  subsection \<open>Generic monoid operation over a set\<close>
     3.6  
     3.7 -no_notation times (infixl "*" 70)
     3.8 -no_notation Groups.one ("1")
     3.9 -
    3.10  locale comm_monoid_set = comm_monoid
    3.11  begin
    3.12  
    3.13 @@ -25,24 +22,24 @@
    3.14  
    3.15  definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    3.16  where
    3.17 -  eq_fold: "F g A = Finite_Set.fold (f \<circ> g) 1 A"
    3.18 +  eq_fold: "F g A = Finite_Set.fold (f \<circ> g) \<^bold>1 A"
    3.19  
    3.20  lemma infinite [simp]:
    3.21 -  "\<not> finite A \<Longrightarrow> F g A = 1"
    3.22 +  "\<not> finite A \<Longrightarrow> F g A = \<^bold>1"
    3.23    by (simp add: eq_fold)
    3.24  
    3.25  lemma empty [simp]:
    3.26 -  "F g {} = 1"
    3.27 +  "F g {} = \<^bold>1"
    3.28    by (simp add: eq_fold)
    3.29  
    3.30  lemma insert [simp]:
    3.31    assumes "finite A" and "x \<notin> A"
    3.32 -  shows "F g (insert x A) = g x * F g A"
    3.33 +  shows "F g (insert x A) = g x \<^bold>* F g A"
    3.34    using assms by (simp add: eq_fold)
    3.35  
    3.36  lemma remove:
    3.37    assumes "finite A" and "x \<in> A"
    3.38 -  shows "F g A = g x * F g (A - {x})"
    3.39 +  shows "F g A = g x \<^bold>* F g (A - {x})"
    3.40  proof -
    3.41    from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
    3.42      by (auto dest: mk_disjoint_insert)
    3.43 @@ -52,21 +49,21 @@
    3.44  
    3.45  lemma insert_remove:
    3.46    assumes "finite A"
    3.47 -  shows "F g (insert x A) = g x * F g (A - {x})"
    3.48 +  shows "F g (insert x A) = g x \<^bold>* F g (A - {x})"
    3.49    using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
    3.50  
    3.51  lemma neutral:
    3.52 -  assumes "\<forall>x\<in>A. g x = 1"
    3.53 -  shows "F g A = 1"
    3.54 +  assumes "\<forall>x\<in>A. g x = \<^bold>1"
    3.55 +  shows "F g A = \<^bold>1"
    3.56    using assms by (induct A rule: infinite_finite_induct) simp_all
    3.57  
    3.58  lemma neutral_const [simp]:
    3.59 -  "F (\<lambda>_. 1) A = 1"
    3.60 +  "F (\<lambda>_. \<^bold>1) A = \<^bold>1"
    3.61    by (simp add: neutral)
    3.62  
    3.63  lemma union_inter:
    3.64    assumes "finite A" and "finite B"
    3.65 -  shows "F g (A \<union> B) * F g (A \<inter> B) = F g A * F g B"
    3.66 +  shows "F g (A \<union> B) \<^bold>* F g (A \<inter> B) = F g A \<^bold>* F g B"
    3.67    \<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
    3.68  using assms proof (induct A)
    3.69    case empty then show ?case by simp
    3.70 @@ -77,19 +74,19 @@
    3.71  
    3.72  corollary union_inter_neutral:
    3.73    assumes "finite A" and "finite B"
    3.74 -  and I0: "\<forall>x \<in> A \<inter> B. g x = 1"
    3.75 -  shows "F g (A \<union> B) = F g A * F g B"
    3.76 +  and I0: "\<forall>x \<in> A \<inter> B. g x = \<^bold>1"
    3.77 +  shows "F g (A \<union> B) = F g A \<^bold>* F g B"
    3.78    using assms by (simp add: union_inter [symmetric] neutral)
    3.79  
    3.80  corollary union_disjoint:
    3.81    assumes "finite A" and "finite B"
    3.82    assumes "A \<inter> B = {}"
    3.83 -  shows "F g (A \<union> B) = F g A * F g B"
    3.84 +  shows "F g (A \<union> B) = F g A \<^bold>* F g B"
    3.85    using assms by (simp add: union_inter_neutral)
    3.86  
    3.87  lemma union_diff2:
    3.88    assumes "finite A" and "finite B"
    3.89 -  shows "F g (A \<union> B) = F g (A - B) * F g (B - A) * F g (A \<inter> B)"
    3.90 +  shows "F g (A \<union> B) = F g (A - B) \<^bold>* F g (B - A) \<^bold>* F g (A \<inter> B)"
    3.91  proof -
    3.92    have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
    3.93      by auto
    3.94 @@ -98,12 +95,12 @@
    3.95  
    3.96  lemma subset_diff:
    3.97    assumes "B \<subseteq> A" and "finite A"
    3.98 -  shows "F g A = F g (A - B) * F g B"
    3.99 +  shows "F g A = F g (A - B) \<^bold>* F g B"
   3.100  proof -
   3.101    from assms have "finite (A - B)" by auto
   3.102    moreover from assms have "finite B" by (rule finite_subset)
   3.103    moreover from assms have "(A - B) \<inter> B = {}" by auto
   3.104 -  ultimately have "F g (A - B \<union> B) = F g (A - B) * F g B" by (rule union_disjoint)
   3.105 +  ultimately have "F g (A - B \<union> B) = F g (A - B) \<^bold>* F g B" by (rule union_disjoint)
   3.106    moreover from assms have "A \<union> B = A" by auto
   3.107    ultimately show ?thesis by simp
   3.108  qed
   3.109 @@ -114,10 +111,10 @@
   3.110    using assms by (induct A) (simp_all add: insert_Diff_if)
   3.111  
   3.112  lemma not_neutral_contains_not_neutral:
   3.113 -  assumes "F g A \<noteq> z"
   3.114 -  obtains a where "a \<in> A" and "g a \<noteq> z"
   3.115 +  assumes "F g A \<noteq> \<^bold>1"
   3.116 +  obtains a where "a \<in> A" and "g a \<noteq> \<^bold>1"
   3.117  proof -
   3.118 -  from assms have "\<exists>a\<in>A. g a \<noteq> z"
   3.119 +  from assms have "\<exists>a\<in>A. g a \<noteq> \<^bold>1"
   3.120    proof (induct A rule: infinite_finite_induct)
   3.121      case (insert a A)
   3.122      then show ?case by simp (rule, simp)
   3.123 @@ -180,7 +177,7 @@
   3.124  qed (auto dest: finite_UnionD intro: infinite)
   3.125  
   3.126  lemma distrib:
   3.127 -  "F (\<lambda>x. g x * h x) A = F g A * F h A"
   3.128 +  "F (\<lambda>x. g x \<^bold>* h x) A = F g A \<^bold>* F h A"
   3.129    by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
   3.130  
   3.131  lemma Sigma:
   3.132 @@ -197,14 +194,14 @@
   3.133  done
   3.134  
   3.135  lemma related:
   3.136 -  assumes Re: "R 1 1"
   3.137 -  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)"
   3.138 +  assumes Re: "R \<^bold>1 \<^bold>1"
   3.139 +  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 \<^bold>* y1) (x2 \<^bold>* y2)"
   3.140    and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   3.141    shows "R (F h S) (F g S)"
   3.142    using fS by (rule finite_subset_induct) (insert assms, auto)
   3.143  
   3.144  lemma mono_neutral_cong_left:
   3.145 -  assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
   3.146 +  assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = \<^bold>1"
   3.147    and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
   3.148  proof-
   3.149    have eq: "T = S \<union> (T - S)" using \<open>S \<subseteq> T\<close> by blast
   3.150 @@ -216,16 +213,16 @@
   3.151  qed
   3.152  
   3.153  lemma mono_neutral_cong_right:
   3.154 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk>
   3.155 +  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = \<^bold>1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk>
   3.156     \<Longrightarrow> F g T = F h S"
   3.157    by (auto intro!: mono_neutral_cong_left [symmetric])
   3.158  
   3.159  lemma mono_neutral_left:
   3.160 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
   3.161 +  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = \<^bold>1 \<rbrakk> \<Longrightarrow> F g S = F g T"
   3.162    by (blast intro: mono_neutral_cong_left)
   3.163  
   3.164  lemma mono_neutral_right:
   3.165 -  "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
   3.166 +  "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = \<^bold>1 \<rbrakk> \<Longrightarrow> F g T = F g S"
   3.167    by (blast intro!: mono_neutral_left [symmetric])
   3.168  
   3.169  lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T"
   3.170 @@ -275,10 +272,10 @@
   3.171  
   3.172  lemma reindex_nontrivial:
   3.173    assumes "finite A"
   3.174 -  and nz: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> h x = h y \<Longrightarrow> g (h x) = 1"
   3.175 +  and nz: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> h x = h y \<Longrightarrow> g (h x) = \<^bold>1"
   3.176    shows "F g (h ` A) = F (g \<circ> h) A"
   3.177  proof (subst reindex_bij_betw_not_neutral [symmetric])
   3.178 -  show "bij_betw h (A - {x \<in> A. (g \<circ> h) x = 1}) (h ` A - h ` {x \<in> A. (g \<circ> h) x = 1})"
   3.179 +  show "bij_betw h (A - {x \<in> A. (g \<circ> h) x = \<^bold>1}) (h ` A - h ` {x \<in> A. (g \<circ> h) x = \<^bold>1})"
   3.180      using nz by (auto intro!: inj_onI simp: bij_betw_def)
   3.181  qed (insert \<open>finite A\<close>, auto)
   3.182  
   3.183 @@ -307,11 +304,11 @@
   3.184  
   3.185  lemma delta:
   3.186    assumes fS: "finite S"
   3.187 -  shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
   3.188 +  shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
   3.189  proof-
   3.190 -  let ?f = "(\<lambda>k. if k=a then b k else 1)"
   3.191 +  let ?f = "(\<lambda>k. if k=a then b k else \<^bold>1)"
   3.192    { assume a: "a \<notin> S"
   3.193 -    hence "\<forall>k\<in>S. ?f k = 1" by simp
   3.194 +    hence "\<forall>k\<in>S. ?f k = \<^bold>1" by simp
   3.195      hence ?thesis  using a by simp }
   3.196    moreover
   3.197    { assume a: "a \<in> S"
   3.198 @@ -320,7 +317,7 @@
   3.199      have eq: "S = ?A \<union> ?B" using a by blast
   3.200      have dj: "?A \<inter> ?B = {}" by simp
   3.201      from fS have fAB: "finite ?A" "finite ?B" by auto
   3.202 -    have "F ?f S = F ?f ?A * F ?f ?B"
   3.203 +    have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
   3.204        using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
   3.205        by simp
   3.206      then have ?thesis using a by simp }
   3.207 @@ -329,14 +326,14 @@
   3.208  
   3.209  lemma delta':
   3.210    assumes fS: "finite S"
   3.211 -  shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
   3.212 +  shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
   3.213    using delta [OF fS, of a b, symmetric] by (auto intro: cong)
   3.214  
   3.215  lemma If_cases:
   3.216    fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   3.217    assumes fA: "finite A"
   3.218    shows "F (\<lambda>x. if P x then h x else g x) A =
   3.219 -    F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
   3.220 +    F h (A \<inter> {x. P x}) \<^bold>* F g (A \<inter> - {x. P x})"
   3.221  proof -
   3.222    have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}"
   3.223            "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
   3.224 @@ -363,10 +360,10 @@
   3.225  
   3.226  lemma inter_restrict:
   3.227    assumes "finite A"
   3.228 -  shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else 1) A"
   3.229 +  shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else \<^bold>1) A"
   3.230  proof -
   3.231 -  let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else 1"
   3.232 -  have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else 1) = 1"
   3.233 +  let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else \<^bold>1"
   3.234 +  have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else \<^bold>1) = \<^bold>1"
   3.235     by simp
   3.236    moreover have "A \<inter> B \<subseteq> A" by blast
   3.237    ultimately have "F ?g (A \<inter> B) = F ?g A" using \<open>finite A\<close>
   3.238 @@ -375,12 +372,12 @@
   3.239  qed
   3.240  
   3.241  lemma inter_filter:
   3.242 -  "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else 1) A"
   3.243 +  "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else \<^bold>1) A"
   3.244    by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def)
   3.245  
   3.246  lemma Union_comp:
   3.247    assumes "\<forall>A \<in> B. finite A"
   3.248 -    and "\<And>A1 A2 x. A1 \<in> B \<Longrightarrow> A2 \<in> B  \<Longrightarrow> A1 \<noteq> A2 \<Longrightarrow> x \<in> A1 \<Longrightarrow> x \<in> A2 \<Longrightarrow> g x = 1"
   3.249 +    and "\<And>A1 A2 x. A1 \<in> B \<Longrightarrow> A2 \<in> B  \<Longrightarrow> A1 \<noteq> A2 \<Longrightarrow> x \<in> A1 \<Longrightarrow> x \<in> A2 \<Longrightarrow> g x = \<^bold>1"
   3.250    shows "F g (\<Union>B) = (F \<circ> F) g B"
   3.251  using assms proof (induct B rule: infinite_finite_induct)
   3.252    case (infinite A)
   3.253 @@ -391,9 +388,9 @@
   3.254  next
   3.255    case (insert A B)
   3.256    then have "finite A" "finite B" "finite (\<Union>B)" "A \<notin> B"
   3.257 -    and "\<forall>x\<in>A \<inter> \<Union>B. g x = 1"
   3.258 +    and "\<forall>x\<in>A \<inter> \<Union>B. g x = \<^bold>1"
   3.259      and H: "F g (\<Union>B) = (F o F) g B" by auto
   3.260 -  then have "F g (A \<union> \<Union>B) = F g A * F g (\<Union>B)"
   3.261 +  then have "F g (A \<union> \<Union>B) = F g A \<^bold>* F g (\<Union>B)"
   3.262      by (simp add: union_inter_neutral)
   3.263    with \<open>finite B\<close> \<open>A \<notin> B\<close> show ?case
   3.264      by (simp add: H)
   3.265 @@ -412,7 +409,7 @@
   3.266  lemma Plus:
   3.267    fixes A :: "'b set" and B :: "'c set"
   3.268    assumes fin: "finite A" "finite B"
   3.269 -  shows "F g (A <+> B) = F (g \<circ> Inl) A * F (g \<circ> Inr) B"
   3.270 +  shows "F g (A <+> B) = F (g \<circ> Inl) A \<^bold>* F (g \<circ> Inr) B"
   3.271  proof -
   3.272    have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   3.273    moreover from fin have "finite (Inl ` A :: ('b + 'c) set)" "finite (Inr ` B :: ('b + 'c) set)"
   3.274 @@ -427,7 +424,7 @@
   3.275  lemma same_carrier:
   3.276    assumes "finite C"
   3.277    assumes subset: "A \<subseteq> C" "B \<subseteq> C"
   3.278 -  assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
   3.279 +  assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = \<^bold>1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = \<^bold>1"
   3.280    shows "F g A = F h B \<longleftrightarrow> F g C = F h C"
   3.281  proof -
   3.282    from \<open>finite C\<close> subset have
   3.283 @@ -437,12 +434,12 @@
   3.284    from subset have [simp]: "B - (C - B) = B" by auto
   3.285    from subset have "C = A \<union> (C - A)" by auto
   3.286    then have "F g C = F g (A \<union> (C - A))" by simp
   3.287 -  also have "\<dots> = F g (A - (C - A)) * F g (C - A - A) * F g (A \<inter> (C - A))"
   3.288 +  also have "\<dots> = F g (A - (C - A)) \<^bold>* F g (C - A - A) \<^bold>* F g (A \<inter> (C - A))"
   3.289      using \<open>finite A\<close> \<open>finite (C - A)\<close> by (simp only: union_diff2)
   3.290    finally have P: "F g C = F g A" using trivial by simp
   3.291    from subset have "C = B \<union> (C - B)" by auto
   3.292    then have "F h C = F h (B \<union> (C - B))" by simp
   3.293 -  also have "\<dots> = F h (B - (C - B)) * F h (C - B - B) * F h (B \<inter> (C - B))"
   3.294 +  also have "\<dots> = F h (B - (C - B)) \<^bold>* F h (C - B - B) \<^bold>* F h (B \<inter> (C - B))"
   3.295      using \<open>finite B\<close> \<open>finite (C - B)\<close> by (simp only: union_diff2)
   3.296    finally have Q: "F h C = F h B" using trivial by simp
   3.297    from P Q show ?thesis by simp
   3.298 @@ -451,16 +448,13 @@
   3.299  lemma same_carrierI:
   3.300    assumes "finite C"
   3.301    assumes subset: "A \<subseteq> C" "B \<subseteq> C"
   3.302 -  assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
   3.303 +  assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = \<^bold>1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = \<^bold>1"
   3.304    assumes "F g C = F h C"
   3.305    shows "F g A = F h B"
   3.306    using assms same_carrier [of C A B] by simp
   3.307  
   3.308  end
   3.309  
   3.310 -notation times (infixl "*" 70)
   3.311 -notation Groups.one ("1")
   3.312 -
   3.313  
   3.314  subsection \<open>Generalized summation over a set\<close>
   3.315  
     4.1 --- a/src/HOL/Groups_List.thy	Sat Jun 11 17:40:52 2016 +0200
     4.2 +++ b/src/HOL/Groups_List.thy	Sat Jun 11 16:22:42 2016 +0200
     4.3 @@ -6,26 +6,23 @@
     4.4  imports List
     4.5  begin
     4.6  
     4.7 -no_notation times (infixl "*" 70)
     4.8 -no_notation Groups.one ("1")
     4.9 - 
    4.10  locale monoid_list = monoid
    4.11  begin
    4.12   
    4.13  definition F :: "'a list \<Rightarrow> 'a"
    4.14  where
    4.15 -  eq_foldr [code]: "F xs = foldr f xs 1"
    4.16 +  eq_foldr [code]: "F xs = foldr f xs \<^bold>1"
    4.17   
    4.18  lemma Nil [simp]:
    4.19 -  "F [] = 1"
    4.20 +  "F [] = \<^bold>1"
    4.21    by (simp add: eq_foldr)
    4.22   
    4.23  lemma Cons [simp]:
    4.24 -  "F (x # xs) = x * F xs"
    4.25 +  "F (x # xs) = x \<^bold>* F xs"
    4.26    by (simp add: eq_foldr)
    4.27   
    4.28  lemma append [simp]:
    4.29 -  "F (xs @ ys) = F xs * F ys"
    4.30 +  "F (xs @ ys) = F xs \<^bold>* F ys"
    4.31    by (induct xs) (simp_all add: assoc)
    4.32   
    4.33  end
    4.34 @@ -52,9 +49,6 @@
    4.35  
    4.36  end
    4.37  
    4.38 -notation times (infixl "*" 70)
    4.39 -notation Groups.one ("1")
    4.40 -
    4.41  
    4.42  subsection \<open>List summation\<close>
    4.43  
     5.1 --- a/src/HOL/Lattices.thy	Sat Jun 11 17:40:52 2016 +0200
     5.2 +++ b/src/HOL/Lattices.thy	Sat Jun 11 16:22:42 2016 +0200
     5.3 @@ -16,17 +16,14 @@
     5.4    undesired effects may occur due to interpretation.
     5.5  \<close>
     5.6  
     5.7 -no_notation times (infixl "*" 70)
     5.8 -no_notation Groups.one ("1")
     5.9 -
    5.10  locale semilattice = abel_semigroup +
    5.11 -  assumes idem [simp]: "a * a = a"
    5.12 +  assumes idem [simp]: "a \<^bold>* a = a"
    5.13  begin
    5.14  
    5.15 -lemma left_idem [simp]: "a * (a * b) = a * b"
    5.16 +lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
    5.17  by (simp add: assoc [symmetric])
    5.18  
    5.19 -lemma right_idem [simp]: "(a * b) * b = a * b"
    5.20 +lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
    5.21  by (simp add: assoc)
    5.22  
    5.23  end
    5.24 @@ -34,109 +31,109 @@
    5.25  locale semilattice_neutr = semilattice + comm_monoid
    5.26  
    5.27  locale semilattice_order = semilattice +
    5.28 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
    5.29 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
    5.30 -  assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
    5.31 -    and strict_order_iff: "a \<prec> b \<longleftrightarrow> a = a * b \<and> a \<noteq> b"
    5.32 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50)
    5.33 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50)
    5.34 +  assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b"
    5.35 +    and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b"
    5.36  begin
    5.37  
    5.38  lemma orderI:
    5.39 -  "a = a * b \<Longrightarrow> a \<preceq> b"
    5.40 +  "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b"
    5.41    by (simp add: order_iff)
    5.42  
    5.43  lemma orderE:
    5.44 -  assumes "a \<preceq> b"
    5.45 -  obtains "a = a * b"
    5.46 +  assumes "a \<^bold>\<le> b"
    5.47 +  obtains "a = a \<^bold>* b"
    5.48    using assms by (unfold order_iff)
    5.49  
    5.50  sublocale ordering less_eq less
    5.51  proof
    5.52    fix a b
    5.53 -  show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    5.54 +  show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b"
    5.55      by (simp add: order_iff strict_order_iff)
    5.56  next
    5.57    fix a
    5.58 -  show "a \<preceq> a"
    5.59 +  show "a \<^bold>\<le> a"
    5.60      by (simp add: order_iff)
    5.61  next
    5.62    fix a b
    5.63 -  assume "a \<preceq> b" "b \<preceq> a"
    5.64 -  then have "a = a * b" "a * b = b"
    5.65 +  assume "a \<^bold>\<le> b" "b \<^bold>\<le> a"
    5.66 +  then have "a = a \<^bold>* b" "a \<^bold>* b = b"
    5.67      by (simp_all add: order_iff commute)
    5.68    then show "a = b" by simp
    5.69  next
    5.70    fix a b c
    5.71 -  assume "a \<preceq> b" "b \<preceq> c"
    5.72 -  then have "a = a * b" "b = b * c"
    5.73 +  assume "a \<^bold>\<le> b" "b \<^bold>\<le> c"
    5.74 +  then have "a = a \<^bold>* b" "b = b \<^bold>* c"
    5.75      by (simp_all add: order_iff commute)
    5.76 -  then have "a = a * (b * c)"
    5.77 +  then have "a = a \<^bold>* (b \<^bold>* c)"
    5.78      by simp
    5.79 -  then have "a = (a * b) * c"
    5.80 +  then have "a = (a \<^bold>* b) \<^bold>* c"
    5.81      by (simp add: assoc)
    5.82 -  with \<open>a = a * b\<close> [symmetric] have "a = a * c" by simp
    5.83 -  then show "a \<preceq> c" by (rule orderI)
    5.84 +  with \<open>a = a \<^bold>* b\<close> [symmetric] have "a = a \<^bold>* c" by simp
    5.85 +  then show "a \<^bold>\<le> c" by (rule orderI)
    5.86  qed
    5.87  
    5.88  lemma cobounded1 [simp]:
    5.89 -  "a * b \<preceq> a"
    5.90 +  "a \<^bold>* b \<^bold>\<le> a"
    5.91    by (simp add: order_iff commute)  
    5.92  
    5.93  lemma cobounded2 [simp]:
    5.94 -  "a * b \<preceq> b"
    5.95 +  "a \<^bold>* b \<^bold>\<le> b"
    5.96    by (simp add: order_iff)
    5.97  
    5.98  lemma boundedI:
    5.99 -  assumes "a \<preceq> b" and "a \<preceq> c"
   5.100 -  shows "a \<preceq> b * c"
   5.101 +  assumes "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
   5.102 +  shows "a \<^bold>\<le> b \<^bold>* c"
   5.103  proof (rule orderI)
   5.104 -  from assms obtain "a * b = a" and "a * c = a" by (auto elim!: orderE)
   5.105 -  then show "a = a * (b * c)" by (simp add: assoc [symmetric])
   5.106 +  from assms obtain "a \<^bold>* b = a" and "a \<^bold>* c = a" by (auto elim!: orderE)
   5.107 +  then show "a = a \<^bold>* (b \<^bold>* c)" by (simp add: assoc [symmetric])
   5.108  qed
   5.109  
   5.110  lemma boundedE:
   5.111 -  assumes "a \<preceq> b * c"
   5.112 -  obtains "a \<preceq> b" and "a \<preceq> c"
   5.113 +  assumes "a \<^bold>\<le> b \<^bold>* c"
   5.114 +  obtains "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
   5.115    using assms by (blast intro: trans cobounded1 cobounded2)
   5.116  
   5.117  lemma bounded_iff [simp]:
   5.118 -  "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c"
   5.119 +  "a \<^bold>\<le> b \<^bold>* c \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<^bold>\<le> c"
   5.120    by (blast intro: boundedI elim: boundedE)
   5.121  
   5.122  lemma strict_boundedE:
   5.123 -  assumes "a \<prec> b * c"
   5.124 -  obtains "a \<prec> b" and "a \<prec> c"
   5.125 +  assumes "a \<^bold>< b \<^bold>* c"
   5.126 +  obtains "a \<^bold>< b" and "a \<^bold>< c"
   5.127    using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+
   5.128  
   5.129  lemma coboundedI1:
   5.130 -  "a \<preceq> c \<Longrightarrow> a * b \<preceq> c"
   5.131 +  "a \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
   5.132    by (rule trans) auto
   5.133  
   5.134  lemma coboundedI2:
   5.135 -  "b \<preceq> c \<Longrightarrow> a * b \<preceq> c"
   5.136 +  "b \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
   5.137    by (rule trans) auto
   5.138  
   5.139  lemma strict_coboundedI1:
   5.140 -  "a \<prec> c \<Longrightarrow> a * b \<prec> c"
   5.141 +  "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
   5.142    using irrefl
   5.143      by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order elim: strict_boundedE)
   5.144  
   5.145  lemma strict_coboundedI2:
   5.146 -  "b \<prec> c \<Longrightarrow> a * b \<prec> c"
   5.147 +  "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
   5.148    using strict_coboundedI1 [of b c a] by (simp add: commute)
   5.149  
   5.150 -lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d"
   5.151 +lemma mono: "a \<^bold>\<le> c \<Longrightarrow> b \<^bold>\<le> d \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c \<^bold>* d"
   5.152    by (blast intro: boundedI coboundedI1 coboundedI2)
   5.153  
   5.154 -lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
   5.155 +lemma absorb1: "a \<^bold>\<le> b \<Longrightarrow> a \<^bold>* b = a"
   5.156    by (rule antisym) (auto simp add: refl)
   5.157  
   5.158 -lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
   5.159 +lemma absorb2: "b \<^bold>\<le> a \<Longrightarrow> a \<^bold>* b = b"
   5.160    by (rule antisym) (auto simp add: refl)
   5.161  
   5.162 -lemma absorb_iff1: "a \<preceq> b \<longleftrightarrow> a * b = a"
   5.163 +lemma absorb_iff1: "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>* b = a"
   5.164    using order_iff by auto
   5.165  
   5.166 -lemma absorb_iff2: "b \<preceq> a \<longleftrightarrow> a * b = b"
   5.167 +lemma absorb_iff2: "b \<^bold>\<le> a \<longleftrightarrow> a \<^bold>* b = b"
   5.168    using order_iff by (auto simp add: commute)
   5.169  
   5.170  end
   5.171 @@ -144,14 +141,11 @@
   5.172  locale semilattice_neutr_order = semilattice_neutr + semilattice_order
   5.173  begin
   5.174  
   5.175 -sublocale ordering_top less_eq less 1
   5.176 +sublocale ordering_top less_eq less "\<^bold>1"
   5.177    by standard (simp add: order_iff)
   5.178  
   5.179  end
   5.180  
   5.181 -notation times (infixl "*" 70)
   5.182 -notation Groups.one ("1")
   5.183 -
   5.184  
   5.185  subsection \<open>Syntactic infimum and supremum operations\<close>
   5.186  
     6.1 --- a/src/HOL/Lattices_Big.thy	Sat Jun 11 17:40:52 2016 +0200
     6.2 +++ b/src/HOL/Lattices_Big.thy	Sat Jun 11 16:22:42 2016 +0200
     6.3 @@ -11,10 +11,6 @@
     6.4  
     6.5  subsection \<open>Generic lattice operations over a set\<close>
     6.6  
     6.7 -no_notation times (infixl "*" 70)
     6.8 -no_notation Groups.one ("1")
     6.9 -
    6.10 -
    6.11  subsubsection \<open>Without neutral element\<close>
    6.12  
    6.13  locale semilattice_set = semilattice
    6.14 @@ -48,20 +44,20 @@
    6.15  
    6.16  lemma insert_not_elem:
    6.17    assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
    6.18 -  shows "F (insert x A) = x * F A"
    6.19 +  shows "F (insert x A) = x \<^bold>* F A"
    6.20  proof -
    6.21    from \<open>A \<noteq> {}\<close> obtain b where "b \<in> A" by blast
    6.22    then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
    6.23    with \<open>finite A\<close> and \<open>x \<notin> A\<close>
    6.24      have "finite (insert x B)" and "b \<notin> insert x B" by auto
    6.25 -  then have "F (insert b (insert x B)) = x * F (insert b B)"
    6.26 +  then have "F (insert b (insert x B)) = x \<^bold>* F (insert b B)"
    6.27      by (simp add: eq_fold)
    6.28    then show ?thesis by (simp add: * insert_commute)
    6.29  qed
    6.30  
    6.31  lemma in_idem:
    6.32    assumes "finite A" and "x \<in> A"
    6.33 -  shows "x * F A = F A"
    6.34 +  shows "x \<^bold>* F A = F A"
    6.35  proof -
    6.36    from assms have "A \<noteq> {}" by auto
    6.37    with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
    6.38 @@ -70,17 +66,17 @@
    6.39  
    6.40  lemma insert [simp]:
    6.41    assumes "finite A" and "A \<noteq> {}"
    6.42 -  shows "F (insert x A) = x * F A"
    6.43 +  shows "F (insert x A) = x \<^bold>* F A"
    6.44    using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
    6.45  
    6.46  lemma union:
    6.47    assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
    6.48 -  shows "F (A \<union> B) = F A * F B"
    6.49 +  shows "F (A \<union> B) = F A \<^bold>* F B"
    6.50    using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
    6.51  
    6.52  lemma remove:
    6.53    assumes "finite A" and "x \<in> A"
    6.54 -  shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
    6.55 +  shows "F A = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
    6.56  proof -
    6.57    from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
    6.58    with assms show ?thesis by simp
    6.59 @@ -88,19 +84,19 @@
    6.60  
    6.61  lemma insert_remove:
    6.62    assumes "finite A"
    6.63 -  shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
    6.64 +  shows "F (insert x A) = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
    6.65    using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
    6.66  
    6.67  lemma subset:
    6.68    assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
    6.69 -  shows "F B * F A = F A"
    6.70 +  shows "F B \<^bold>* F A = F A"
    6.71  proof -
    6.72    from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
    6.73    with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
    6.74  qed
    6.75  
    6.76  lemma closed:
    6.77 -  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
    6.78 +  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
    6.79    shows "F A \<in> A"
    6.80  using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
    6.81    case singleton then show ?case by simp
    6.82 @@ -109,17 +105,17 @@
    6.83  qed
    6.84  
    6.85  lemma hom_commute:
    6.86 -  assumes hom: "\<And>x y. h (x * y) = h x * h y"
    6.87 +  assumes hom: "\<And>x y. h (x \<^bold>* y) = h x \<^bold>* h y"
    6.88    and N: "finite N" "N \<noteq> {}"
    6.89    shows "h (F N) = F (h ` N)"
    6.90  using N proof (induct rule: finite_ne_induct)
    6.91    case singleton thus ?case by simp
    6.92  next
    6.93    case (insert n N)
    6.94 -  then have "h (F (insert n N)) = h (n * F N)" by simp
    6.95 -  also have "\<dots> = h n * h (F N)" by (rule hom)
    6.96 +  then have "h (F (insert n N)) = h (n \<^bold>* F N)" by simp
    6.97 +  also have "\<dots> = h n \<^bold>* h (F N)" by (rule hom)
    6.98    also have "h (F N) = F (h ` N)" by (rule insert)
    6.99 -  also have "h n * \<dots> = F (insert (h n) (h ` N))"
   6.100 +  also have "h n \<^bold>* \<dots> = F (insert (h n) (h ` N))"
   6.101      using insert by simp
   6.102    also have "insert (h n) (h ` N) = h ` insert n N" by simp
   6.103    finally show ?case .
   6.104 @@ -135,25 +131,25 @@
   6.105  
   6.106  lemma bounded_iff:
   6.107    assumes "finite A" and "A \<noteq> {}"
   6.108 -  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
   6.109 +  shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
   6.110    using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
   6.111  
   6.112  lemma boundedI:
   6.113    assumes "finite A"
   6.114    assumes "A \<noteq> {}"
   6.115 -  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   6.116 -  shows "x \<preceq> F A"
   6.117 +  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
   6.118 +  shows "x \<^bold>\<le> F A"
   6.119    using assms by (simp add: bounded_iff)
   6.120  
   6.121  lemma boundedE:
   6.122 -  assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
   6.123 -  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   6.124 +  assumes "finite A" and "A \<noteq> {}" and "x \<^bold>\<le> F A"
   6.125 +  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
   6.126    using assms by (simp add: bounded_iff)
   6.127  
   6.128  lemma coboundedI:
   6.129    assumes "finite A"
   6.130      and "a \<in> A"
   6.131 -  shows "F A \<preceq> a"
   6.132 +  shows "F A \<^bold>\<le> a"
   6.133  proof -
   6.134    from assms have "A \<noteq> {}" by auto
   6.135    from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
   6.136 @@ -168,15 +164,15 @@
   6.137  
   6.138  lemma antimono:
   6.139    assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
   6.140 -  shows "F B \<preceq> F A"
   6.141 +  shows "F B \<^bold>\<le> F A"
   6.142  proof (cases "A = B")
   6.143    case True then show ?thesis by (simp add: refl)
   6.144  next
   6.145    case False
   6.146    have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
   6.147    then have "F B = F (A \<union> (B - A))" by simp
   6.148 -  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   6.149 -  also have "\<dots> \<preceq> F A" by simp
   6.150 +  also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   6.151 +  also have "\<dots> \<^bold>\<le> F A" by simp
   6.152    finally show ?thesis .
   6.153  qed
   6.154  
   6.155 @@ -193,24 +189,24 @@
   6.156  
   6.157  definition F :: "'a set \<Rightarrow> 'a"
   6.158  where
   6.159 -  eq_fold: "F A = Finite_Set.fold f 1 A"
   6.160 +  eq_fold: "F A = Finite_Set.fold f \<^bold>1 A"
   6.161  
   6.162  lemma infinite [simp]:
   6.163 -  "\<not> finite A \<Longrightarrow> F A = 1"
   6.164 +  "\<not> finite A \<Longrightarrow> F A = \<^bold>1"
   6.165    by (simp add: eq_fold)
   6.166  
   6.167  lemma empty [simp]:
   6.168 -  "F {} = 1"
   6.169 +  "F {} = \<^bold>1"
   6.170    by (simp add: eq_fold)
   6.171  
   6.172  lemma insert [simp]:
   6.173    assumes "finite A"
   6.174 -  shows "F (insert x A) = x * F A"
   6.175 +  shows "F (insert x A) = x \<^bold>* F A"
   6.176    using assms by (simp add: eq_fold)
   6.177  
   6.178  lemma in_idem:
   6.179    assumes "finite A" and "x \<in> A"
   6.180 -  shows "x * F A = F A"
   6.181 +  shows "x \<^bold>* F A = F A"
   6.182  proof -
   6.183    from assms have "A \<noteq> {}" by auto
   6.184    with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
   6.185 @@ -219,12 +215,12 @@
   6.186  
   6.187  lemma union:
   6.188    assumes "finite A" and "finite B"
   6.189 -  shows "F (A \<union> B) = F A * F B"
   6.190 +  shows "F (A \<union> B) = F A \<^bold>* F B"
   6.191    using assms by (induct A) (simp_all add: ac_simps)
   6.192  
   6.193  lemma remove:
   6.194    assumes "finite A" and "x \<in> A"
   6.195 -  shows "F A = x * F (A - {x})"
   6.196 +  shows "F A = x \<^bold>* F (A - {x})"
   6.197  proof -
   6.198    from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
   6.199    with assms show ?thesis by simp
   6.200 @@ -232,19 +228,19 @@
   6.201  
   6.202  lemma insert_remove:
   6.203    assumes "finite A"
   6.204 -  shows "F (insert x A) = x * F (A - {x})"
   6.205 +  shows "F (insert x A) = x \<^bold>* F (A - {x})"
   6.206    using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
   6.207  
   6.208  lemma subset:
   6.209    assumes "finite A" and "B \<subseteq> A"
   6.210 -  shows "F B * F A = F A"
   6.211 +  shows "F B \<^bold>* F A = F A"
   6.212  proof -
   6.213    from assms have "finite B" by (auto dest: finite_subset)
   6.214    with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
   6.215  qed
   6.216  
   6.217  lemma closed:
   6.218 -  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
   6.219 +  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
   6.220    shows "F A \<in> A"
   6.221  using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
   6.222    case singleton then show ?case by simp
   6.223 @@ -259,24 +255,24 @@
   6.224  
   6.225  lemma bounded_iff:
   6.226    assumes "finite A"
   6.227 -  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
   6.228 +  shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
   6.229    using assms by (induct A) (simp_all add: bounded_iff)
   6.230  
   6.231  lemma boundedI:
   6.232    assumes "finite A"
   6.233 -  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   6.234 -  shows "x \<preceq> F A"
   6.235 +  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
   6.236 +  shows "x \<^bold>\<le> F A"
   6.237    using assms by (simp add: bounded_iff)
   6.238  
   6.239  lemma boundedE:
   6.240 -  assumes "finite A" and "x \<preceq> F A"
   6.241 -  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   6.242 +  assumes "finite A" and "x \<^bold>\<le> F A"
   6.243 +  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
   6.244    using assms by (simp add: bounded_iff)
   6.245  
   6.246  lemma coboundedI:
   6.247    assumes "finite A"
   6.248      and "a \<in> A"
   6.249 -  shows "F A \<preceq> a"
   6.250 +  shows "F A \<^bold>\<le> a"
   6.251  proof -
   6.252    from assms have "A \<noteq> {}" by auto
   6.253    from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
   6.254 @@ -291,23 +287,20 @@
   6.255  
   6.256  lemma antimono:
   6.257    assumes "A \<subseteq> B" and "finite B"
   6.258 -  shows "F B \<preceq> F A"
   6.259 +  shows "F B \<^bold>\<le> F A"
   6.260  proof (cases "A = B")
   6.261    case True then show ?thesis by (simp add: refl)
   6.262  next
   6.263    case False
   6.264    have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
   6.265    then have "F B = F (A \<union> (B - A))" by simp
   6.266 -  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   6.267 -  also have "\<dots> \<preceq> F A" by simp
   6.268 +  also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   6.269 +  also have "\<dots> \<^bold>\<le> F A" by simp
   6.270    finally show ?thesis .
   6.271  qed
   6.272  
   6.273  end
   6.274  
   6.275 -notation times (infixl "*" 70)
   6.276 -notation Groups.one ("1")
   6.277 -
   6.278  
   6.279  subsection \<open>Lattice operations on finite sets\<close>
   6.280  
     7.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Sat Jun 11 17:40:52 2016 +0200
     7.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sat Jun 11 16:22:42 2016 +0200
     7.3 @@ -9,21 +9,18 @@
     7.4  
     7.5  subsection \<open>Abstract product\<close>
     7.6  
     7.7 -no_notation times (infixl "*" 70)
     7.8 -no_notation Groups.one ("1")
     7.9 -
    7.10  locale comm_monoid_fun = comm_monoid
    7.11  begin
    7.12  
    7.13  definition G :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    7.14  where
    7.15 -  expand_set: "G g = comm_monoid_set.F f 1 g {a. g a \<noteq> 1}"
    7.16 +  expand_set: "G g = comm_monoid_set.F f \<^bold>1 g {a. g a \<noteq> \<^bold>1}"
    7.17  
    7.18 -interpretation F: comm_monoid_set f 1
    7.19 +interpretation F: comm_monoid_set f "\<^bold>1"
    7.20    ..
    7.21  
    7.22  lemma expand_superset:
    7.23 -  assumes "finite A" and "{a. g a \<noteq> 1} \<subseteq> A"
    7.24 +  assumes "finite A" and "{a. g a \<noteq> \<^bold>1} \<subseteq> A"
    7.25    shows "G g = F.F g A"
    7.26    apply (simp add: expand_set)
    7.27    apply (rule F.same_carrierI [of A])
    7.28 @@ -32,7 +29,7 @@
    7.29  
    7.30  lemma conditionalize:
    7.31    assumes "finite A"
    7.32 -  shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else 1)"
    7.33 +  shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else \<^bold>1)"
    7.34    using assms
    7.35    apply (simp add: expand_set)
    7.36    apply (rule F.same_carrierI [of A])
    7.37 @@ -40,29 +37,29 @@
    7.38    done
    7.39  
    7.40  lemma neutral [simp]:
    7.41 -  "G (\<lambda>a. 1) = 1"
    7.42 +  "G (\<lambda>a. \<^bold>1) = \<^bold>1"
    7.43    by (simp add: expand_set)
    7.44  
    7.45  lemma update [simp]:
    7.46 -  assumes "finite {a. g a \<noteq> 1}"
    7.47 -  assumes "g a = 1"
    7.48 -  shows "G (g(a := b)) = b * G g"
    7.49 -proof (cases "b = 1")
    7.50 -  case True with \<open>g a = 1\<close> show ?thesis
    7.51 +  assumes "finite {a. g a \<noteq> \<^bold>1}"
    7.52 +  assumes "g a = \<^bold>1"
    7.53 +  shows "G (g(a := b)) = b \<^bold>* G g"
    7.54 +proof (cases "b = \<^bold>1")
    7.55 +  case True with \<open>g a = \<^bold>1\<close> show ?thesis
    7.56      by (simp add: expand_set) (rule F.cong, auto)
    7.57  next
    7.58    case False
    7.59 -  moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> 1} = insert a {a. g a \<noteq> 1}"
    7.60 +  moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> \<^bold>1} = insert a {a. g a \<noteq> \<^bold>1}"
    7.61      by auto
    7.62 -  moreover from \<open>g a = 1\<close> have "a \<notin> {a. g a \<noteq> 1}"
    7.63 +  moreover from \<open>g a = \<^bold>1\<close> have "a \<notin> {a. g a \<noteq> \<^bold>1}"
    7.64      by simp
    7.65 -  moreover have "F.F (\<lambda>a'. if a' = a then b else g a') {a. g a \<noteq> 1} = F.F g {a. g a \<noteq> 1}"
    7.66 -    by (rule F.cong) (auto simp add: \<open>g a = 1\<close>)
    7.67 -  ultimately show ?thesis using \<open>finite {a. g a \<noteq> 1}\<close> by (simp add: expand_set)
    7.68 +  moreover have "F.F (\<lambda>a'. if a' = a then b else g a') {a. g a \<noteq> \<^bold>1} = F.F g {a. g a \<noteq> \<^bold>1}"
    7.69 +    by (rule F.cong) (auto simp add: \<open>g a = \<^bold>1\<close>)
    7.70 +  ultimately show ?thesis using \<open>finite {a. g a \<noteq> \<^bold>1}\<close> by (simp add: expand_set)
    7.71  qed
    7.72  
    7.73  lemma infinite [simp]:
    7.74 -  "\<not> finite {a. g a \<noteq> 1} \<Longrightarrow> G g = 1"
    7.75 +  "\<not> finite {a. g a \<noteq> \<^bold>1} \<Longrightarrow> G g = \<^bold>1"
    7.76    by (simp add: expand_set)
    7.77  
    7.78  lemma cong:
    7.79 @@ -76,8 +73,8 @@
    7.80    using assms by (fact cong)
    7.81  
    7.82  lemma not_neutral_obtains_not_neutral:
    7.83 -  assumes "G g \<noteq> 1"
    7.84 -  obtains a where "g a \<noteq> 1"
    7.85 +  assumes "G g \<noteq> \<^bold>1"
    7.86 +  obtains a where "g a \<noteq> \<^bold>1"
    7.87    using assms by (auto elim: F.not_neutral_contains_not_neutral simp add: expand_set)
    7.88  
    7.89  lemma reindex_cong:
    7.90 @@ -87,59 +84,59 @@
    7.91  proof -
    7.92    from assms have unfold: "h = g \<circ> l" by simp
    7.93    from \<open>bij l\<close> have "inj l" by (rule bij_is_inj)
    7.94 -  then have "inj_on l {a. h a \<noteq> 1}" by (rule subset_inj_on) simp
    7.95 -  moreover from \<open>bij l\<close> have "{a. g a \<noteq> 1} = l ` {a. h a \<noteq> 1}"
    7.96 +  then have "inj_on l {a. h a \<noteq> \<^bold>1}" by (rule subset_inj_on) simp
    7.97 +  moreover from \<open>bij l\<close> have "{a. g a \<noteq> \<^bold>1} = l ` {a. h a \<noteq> \<^bold>1}"
    7.98      by (auto simp add: image_Collect unfold elim: bij_pointE)
    7.99 -  moreover have "\<And>x. x \<in> {a. h a \<noteq> 1} \<Longrightarrow> g (l x) = h x"
   7.100 +  moreover have "\<And>x. x \<in> {a. h a \<noteq> \<^bold>1} \<Longrightarrow> g (l x) = h x"
   7.101      by (simp add: unfold)
   7.102 -  ultimately have "F.F g {a. g a \<noteq> 1} = F.F h {a. h a \<noteq> 1}"
   7.103 +  ultimately have "F.F g {a. g a \<noteq> \<^bold>1} = F.F h {a. h a \<noteq> \<^bold>1}"
   7.104      by (rule F.reindex_cong)
   7.105    then show ?thesis by (simp add: expand_set)
   7.106  qed
   7.107  
   7.108  lemma distrib:
   7.109 -  assumes "finite {a. g a \<noteq> 1}" and "finite {a. h a \<noteq> 1}"
   7.110 -  shows "G (\<lambda>a. g a * h a) = G g * G h"
   7.111 +  assumes "finite {a. g a \<noteq> \<^bold>1}" and "finite {a. h a \<noteq> \<^bold>1}"
   7.112 +  shows "G (\<lambda>a. g a \<^bold>* h a) = G g \<^bold>* G h"
   7.113  proof -
   7.114 -  from assms have "finite ({a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1})" by simp
   7.115 -  moreover have "{a. g a * h a \<noteq> 1} \<subseteq> {a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"
   7.116 +  from assms have "finite ({a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1})" by simp
   7.117 +  moreover have "{a. g a \<^bold>* h a \<noteq> \<^bold>1} \<subseteq> {a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1}"
   7.118      by auto (drule sym, simp)
   7.119    ultimately show ?thesis
   7.120      using assms
   7.121 -    by (simp add: expand_superset [of "{a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"] F.distrib)
   7.122 +    by (simp add: expand_superset [of "{a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1}"] F.distrib)
   7.123  qed
   7.124  
   7.125  lemma commute:
   7.126    assumes "finite C"
   7.127 -  assumes subset: "{a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
   7.128 +  assumes subset: "{a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
   7.129    shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
   7.130  proof -
   7.131    from \<open>finite C\<close> subset
   7.132 -    have "finite ({a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1})"
   7.133 +    have "finite ({a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1})"
   7.134      by (rule rev_finite_subset)
   7.135    then have fins:
   7.136 -    "finite {b. \<exists>a. g a b \<noteq> 1}" "finite {a. \<exists>b. g a b \<noteq> 1}"
   7.137 +    "finite {b. \<exists>a. g a b \<noteq> \<^bold>1}" "finite {a. \<exists>b. g a b \<noteq> \<^bold>1}"
   7.138      by (auto simp add: finite_cartesian_product_iff)
   7.139 -  have subsets: "\<And>a. {b. g a b \<noteq> 1} \<subseteq> {b. \<exists>a. g a b \<noteq> 1}"
   7.140 -    "\<And>b. {a. g a b \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
   7.141 -    "{a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1} \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
   7.142 -    "{a. F.F (\<lambda>aa. g aa a) {a. \<exists>b. g a b \<noteq> 1} \<noteq> 1} \<subseteq> {b. \<exists>a. g a b \<noteq> 1}"
   7.143 +  have subsets: "\<And>a. {b. g a b \<noteq> \<^bold>1} \<subseteq> {b. \<exists>a. g a b \<noteq> \<^bold>1}"
   7.144 +    "\<And>b. {a. g a b \<noteq> \<^bold>1} \<subseteq> {a. \<exists>b. g a b \<noteq> \<^bold>1}"
   7.145 +    "{a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1} \<noteq> \<^bold>1} \<subseteq> {a. \<exists>b. g a b \<noteq> \<^bold>1}"
   7.146 +    "{a. F.F (\<lambda>aa. g aa a) {a. \<exists>b. g a b \<noteq> \<^bold>1} \<noteq> \<^bold>1} \<subseteq> {b. \<exists>a. g a b \<noteq> \<^bold>1}"
   7.147      by (auto elim: F.not_neutral_contains_not_neutral)
   7.148    from F.commute have
   7.149 -    "F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1} =
   7.150 -      F.F (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> 1}) {b. \<exists>a. g a b \<noteq> 1}" .
   7.151 -  with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) =
   7.152 -    G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> 1})"
   7.153 -    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
   7.154 -      expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
   7.155 +    "F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) {a. \<exists>b. g a b \<noteq> \<^bold>1} =
   7.156 +      F.F (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> \<^bold>1}) {b. \<exists>a. g a b \<noteq> \<^bold>1}" .
   7.157 +  with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) =
   7.158 +    G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> \<^bold>1})"
   7.159 +    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> \<^bold>1}"]
   7.160 +      expand_superset [of "{a. \<exists>b. g a b \<noteq> \<^bold>1}"])
   7.161    with subsets fins show ?thesis
   7.162 -    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
   7.163 -      expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
   7.164 +    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> \<^bold>1}"]
   7.165 +      expand_superset [of "{a. \<exists>b. g a b \<noteq> \<^bold>1}"])
   7.166  qed
   7.167  
   7.168  lemma cartesian_product:
   7.169    assumes "finite C"
   7.170 -  assumes subset: "{a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
   7.171 +  assumes subset: "{a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
   7.172    shows "G (\<lambda>a. G (g a)) = G (\<lambda>(a, b). g a b)"
   7.173  proof -
   7.174    from subset \<open>finite C\<close> have fin_prod: "finite (?A \<times> ?B)"
   7.175 @@ -147,7 +144,7 @@
   7.176    from fin_prod have "finite ?A" and "finite ?B"
   7.177      by (auto simp add: finite_cartesian_product_iff)
   7.178    have *: "G (\<lambda>a. G (g a)) =
   7.179 -    (F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1})"
   7.180 +    (F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) {a. \<exists>b. g a b \<noteq> \<^bold>1})"
   7.181      apply (subst expand_superset [of "?B"])
   7.182      apply (rule \<open>finite ?B\<close>)
   7.183      apply auto
   7.184 @@ -157,9 +154,9 @@
   7.185      apply (erule F.not_neutral_contains_not_neutral)
   7.186      apply auto
   7.187      done
   7.188 -  have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> ?A \<times> ?B"
   7.189 +  have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> ?A \<times> ?B"
   7.190      by auto
   7.191 -  with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> C"
   7.192 +  with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> C"
   7.193      by blast
   7.194    show ?thesis
   7.195      apply (simp add: *)
   7.196 @@ -176,12 +173,12 @@
   7.197  
   7.198  lemma cartesian_product2:
   7.199    assumes fin: "finite D"
   7.200 -  assumes subset: "{(a, b). \<exists>c. g a b c \<noteq> 1} \<times> {c. \<exists>a b. g a b c \<noteq> 1} \<subseteq> D" (is "?AB \<times> ?C \<subseteq> D")
   7.201 +  assumes subset: "{(a, b). \<exists>c. g a b c \<noteq> \<^bold>1} \<times> {c. \<exists>a b. g a b c \<noteq> \<^bold>1} \<subseteq> D" (is "?AB \<times> ?C \<subseteq> D")
   7.202    shows "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>(a, b, c). g a b c)"
   7.203  proof -
   7.204    have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
   7.205      by (auto intro!: bijI injI simp add: image_def)
   7.206 -  have "{p. \<exists>c. g (fst p) (snd p) c \<noteq> 1} \<times> {c. \<exists>p. g (fst p) (snd p) c \<noteq> 1} \<subseteq> D"
   7.207 +  have "{p. \<exists>c. g (fst p) (snd p) c \<noteq> \<^bold>1} \<times> {c. \<exists>p. g (fst p) (snd p) c \<noteq> \<^bold>1} \<subseteq> D"
   7.208      by auto (insert subset, blast)
   7.209    with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
   7.210      by (rule cartesian_product)
   7.211 @@ -193,27 +190,24 @@
   7.212  qed
   7.213  
   7.214  lemma delta [simp]:
   7.215 -  "G (\<lambda>b. if b = a then g b else 1) = g a"
   7.216 +  "G (\<lambda>b. if b = a then g b else \<^bold>1) = g a"
   7.217  proof -
   7.218 -  have "{b. (if b = a then g b else 1) \<noteq> 1} \<subseteq> {a}" by auto
   7.219 +  have "{b. (if b = a then g b else \<^bold>1) \<noteq> \<^bold>1} \<subseteq> {a}" by auto
   7.220    then show ?thesis by (simp add: expand_superset [of "{a}"])
   7.221  qed
   7.222  
   7.223  lemma delta' [simp]:
   7.224 -  "G (\<lambda>b. if a = b then g b else 1) = g a"
   7.225 +  "G (\<lambda>b. if a = b then g b else \<^bold>1) = g a"
   7.226  proof -
   7.227 -  have "(\<lambda>b. if a = b then g b else 1) = (\<lambda>b. if b = a then g b else 1)"
   7.228 +  have "(\<lambda>b. if a = b then g b else \<^bold>1) = (\<lambda>b. if b = a then g b else \<^bold>1)"
   7.229      by (simp add: fun_eq_iff)
   7.230 -  then have "G (\<lambda>b. if a = b then g b else 1) = G (\<lambda>b. if b = a then g b else 1)"
   7.231 +  then have "G (\<lambda>b. if a = b then g b else \<^bold>1) = G (\<lambda>b. if b = a then g b else \<^bold>1)"
   7.232      by (simp cong del: strong_cong)
   7.233    then show ?thesis by simp
   7.234  qed
   7.235  
   7.236  end
   7.237  
   7.238 -notation times (infixl "*" 70)
   7.239 -notation Groups.one ("1")
   7.240 -
   7.241  
   7.242  subsection \<open>Concrete sum\<close>
   7.243  
   7.244 @@ -339,4 +333,3 @@
   7.245  qed
   7.246  
   7.247  end
   7.248 -
     8.1 --- a/src/HOL/Library/Multiset.thy	Sat Jun 11 17:40:52 2016 +0200
     8.2 +++ b/src/HOL/Library/Multiset.thy	Sat Jun 11 16:22:42 2016 +0200
     8.3 @@ -1562,16 +1562,13 @@
     8.4  
     8.5  subsection \<open>Big operators\<close>
     8.6  
     8.7 -no_notation times (infixl "*" 70)
     8.8 -no_notation Groups.one ("1")
     8.9 -
    8.10  locale comm_monoid_mset = comm_monoid
    8.11  begin
    8.12  
    8.13  definition F :: "'a multiset \<Rightarrow> 'a"
    8.14 -  where eq_fold: "F M = fold_mset f 1 M"
    8.15 -
    8.16 -lemma empty [simp]: "F {#} = 1"
    8.17 +  where eq_fold: "F M = fold_mset f \<^bold>1 M"
    8.18 +
    8.19 +lemma empty [simp]: "F {#} = \<^bold>1"
    8.20    by (simp add: eq_fold)
    8.21  
    8.22  lemma singleton [simp]: "F {#x#} = x"
    8.23 @@ -1581,7 +1578,7 @@
    8.24    show ?thesis by (simp add: eq_fold)
    8.25  qed
    8.26  
    8.27 -lemma union [simp]: "F (M + N) = F M * F N"
    8.28 +lemma union [simp]: "F (M + N) = F M \<^bold>* F N"
    8.29  proof -
    8.30    interpret comp_fun_commute f
    8.31      by standard (simp add: fun_eq_iff left_commute)
    8.32 @@ -1599,9 +1596,6 @@
    8.33  lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
    8.34    by (induct NN) auto
    8.35  
    8.36 -notation times (infixl "*" 70)
    8.37 -notation Groups.one ("1")
    8.38 -
    8.39  context comm_monoid_add
    8.40  begin
    8.41  
     9.1 --- a/src/HOL/Orderings.thy	Sat Jun 11 17:40:52 2016 +0200
     9.2 +++ b/src/HOL/Orderings.thy	Sat Jun 11 16:22:42 2016 +0200
     9.3 @@ -15,71 +15,71 @@
     9.4  subsection \<open>Abstract ordering\<close>
     9.5  
     9.6  locale ordering =
     9.7 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
     9.8 -   and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
     9.9 -  assumes strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    9.10 -  assumes refl: "a \<preceq> a" \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
    9.11 -    and antisym: "a \<preceq> b \<Longrightarrow> b \<preceq> a \<Longrightarrow> a = b"
    9.12 -    and trans: "a \<preceq> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<preceq> c"
    9.13 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50)
    9.14 +   and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50)
    9.15 +  assumes strict_iff_order: "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b"
    9.16 +  assumes refl: "a \<^bold>\<le> a" \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
    9.17 +    and antisym: "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>\<le> a \<Longrightarrow> a = b"
    9.18 +    and trans: "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>\<le> c \<Longrightarrow> a \<^bold>\<le> c"
    9.19  begin
    9.20  
    9.21  lemma strict_implies_order:
    9.22 -  "a \<prec> b \<Longrightarrow> a \<preceq> b"
    9.23 +  "a \<^bold>< b \<Longrightarrow> a \<^bold>\<le> b"
    9.24    by (simp add: strict_iff_order)
    9.25  
    9.26  lemma strict_implies_not_eq:
    9.27 -  "a \<prec> b \<Longrightarrow> a \<noteq> b"
    9.28 +  "a \<^bold>< b \<Longrightarrow> a \<noteq> b"
    9.29    by (simp add: strict_iff_order)
    9.30  
    9.31  lemma not_eq_order_implies_strict:
    9.32 -  "a \<noteq> b \<Longrightarrow> a \<preceq> b \<Longrightarrow> a \<prec> b"
    9.33 +  "a \<noteq> b \<Longrightarrow> a \<^bold>\<le> b \<Longrightarrow> a \<^bold>< b"
    9.34    by (simp add: strict_iff_order)
    9.35  
    9.36  lemma order_iff_strict:
    9.37 -  "a \<preceq> b \<longleftrightarrow> a \<prec> b \<or> a = b"
    9.38 +  "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>< b \<or> a = b"
    9.39    by (auto simp add: strict_iff_order refl)
    9.40  
    9.41  lemma irrefl: \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
    9.42 -  "\<not> a \<prec> a"
    9.43 +  "\<not> a \<^bold>< a"
    9.44    by (simp add: strict_iff_order)
    9.45  
    9.46  lemma asym:
    9.47 -  "a \<prec> b \<Longrightarrow> b \<prec> a \<Longrightarrow> False"
    9.48 +  "a \<^bold>< b \<Longrightarrow> b \<^bold>< a \<Longrightarrow> False"
    9.49    by (auto simp add: strict_iff_order intro: antisym)
    9.50  
    9.51  lemma strict_trans1:
    9.52 -  "a \<preceq> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
    9.53 +  "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
    9.54    by (auto simp add: strict_iff_order intro: trans antisym)
    9.55  
    9.56  lemma strict_trans2:
    9.57 -  "a \<prec> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<prec> c"
    9.58 +  "a \<^bold>< b \<Longrightarrow> b \<^bold>\<le> c \<Longrightarrow> a \<^bold>< c"
    9.59    by (auto simp add: strict_iff_order intro: trans antisym)
    9.60  
    9.61  lemma strict_trans:
    9.62 -  "a \<prec> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
    9.63 +  "a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
    9.64    by (auto intro: strict_trans1 strict_implies_order)
    9.65  
    9.66  end
    9.67  
    9.68  locale ordering_top = ordering +
    9.69 -  fixes top :: "'a"
    9.70 -  assumes extremum [simp]: "a \<preceq> top"
    9.71 +  fixes top :: "'a"  ("\<^bold>\<top>")
    9.72 +  assumes extremum [simp]: "a \<^bold>\<le> \<^bold>\<top>"
    9.73  begin
    9.74  
    9.75  lemma extremum_uniqueI:
    9.76 -  "top \<preceq> a \<Longrightarrow> a = top"
    9.77 +  "\<^bold>\<top> \<^bold>\<le> a \<Longrightarrow> a = \<^bold>\<top>"
    9.78    by (rule antisym) auto
    9.79  
    9.80  lemma extremum_unique:
    9.81 -  "top \<preceq> a \<longleftrightarrow> a = top"
    9.82 +  "\<^bold>\<top> \<^bold>\<le> a \<longleftrightarrow> a = \<^bold>\<top>"
    9.83    by (auto intro: antisym)
    9.84  
    9.85  lemma extremum_strict [simp]:
    9.86 -  "\<not> (top \<prec> a)"
    9.87 +  "\<not> (\<^bold>\<top> \<^bold>< a)"
    9.88    using extremum [of a] by (auto simp add: order_iff_strict intro: asym irrefl)
    9.89  
    9.90  lemma not_eq_extremum:
    9.91 -  "a \<noteq> top \<longleftrightarrow> a \<prec> top"
    9.92 +  "a \<noteq> \<^bold>\<top> \<longleftrightarrow> a \<^bold>< \<^bold>\<top>"
    9.93    by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum)
    9.94  
    9.95  end