boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
--- a/NEWS Sat Jun 11 17:40:52 2016 +0200
+++ b/NEWS Sat Jun 11 16:22:42 2016 +0200
@@ -132,6 +132,14 @@
*** HOL ***
+* Abstract locales semigroup, abel_semigroup, semilattice,
+semilattice_neutr, ordering, ordering_top, semilattice_order,
+semilattice_neutr_order, comm_monoid_set, semilattice_set,
+semilattice_neutr_set, semilattice_order_set, semilattice_order_neutr_set
+monoid_list, comm_monoid_list, comm_monoid_list_set, comm_monoid_mset,
+comm_monoid_fun use boldified syntax uniformly that does not clash
+with corresponding global syntax. INCOMPATIBILITY.
+
* Conventional syntax "%(). t" for unit abstractions. Slight syntactic
INCOMPATIBILITY.
--- a/src/HOL/Groups.thy Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Groups.thy Sat Jun 11 16:22:42 2016 +0200
@@ -42,17 +42,17 @@
\<close>
locale semigroup =
- fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
- assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
+ fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^bold>*" 70)
+ assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)"
locale abel_semigroup = semigroup +
- assumes commute [ac_simps]: "a * b = b * a"
+ assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a"
begin
lemma left_commute [ac_simps]:
- "b * (a * c) = a * (b * c)"
+ "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)"
proof -
- have "(b * a) * c = (a * b) * c"
+ have "(b \<^bold>* a) \<^bold>* c = (a \<^bold>* b) \<^bold>* c"
by (simp only: commute)
then show ?thesis
by (simp only: assoc)
@@ -61,13 +61,13 @@
end
locale monoid = semigroup +
- fixes z :: 'a ("1")
- assumes left_neutral [simp]: "1 * a = a"
- assumes right_neutral [simp]: "a * 1 = a"
+ fixes z :: 'a ("\<^bold>1")
+ assumes left_neutral [simp]: "\<^bold>1 \<^bold>* a = a"
+ assumes right_neutral [simp]: "a \<^bold>* \<^bold>1 = a"
locale comm_monoid = abel_semigroup +
- fixes z :: 'a ("1")
- assumes comm_neutral: "a * 1 = a"
+ fixes z :: 'a ("\<^bold>1")
+ assumes comm_neutral: "a \<^bold>* \<^bold>1 = a"
begin
sublocale monoid
--- a/src/HOL/Groups_Big.thy Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Groups_Big.thy Sat Jun 11 16:22:42 2016 +0200
@@ -11,9 +11,6 @@
subsection \<open>Generic monoid operation over a set\<close>
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
locale comm_monoid_set = comm_monoid
begin
@@ -25,24 +22,24 @@
definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
where
- eq_fold: "F g A = Finite_Set.fold (f \<circ> g) 1 A"
+ eq_fold: "F g A = Finite_Set.fold (f \<circ> g) \<^bold>1 A"
lemma infinite [simp]:
- "\<not> finite A \<Longrightarrow> F g A = 1"
+ "\<not> finite A \<Longrightarrow> F g A = \<^bold>1"
by (simp add: eq_fold)
lemma empty [simp]:
- "F g {} = 1"
+ "F g {} = \<^bold>1"
by (simp add: eq_fold)
lemma insert [simp]:
assumes "finite A" and "x \<notin> A"
- shows "F g (insert x A) = g x * F g A"
+ shows "F g (insert x A) = g x \<^bold>* F g A"
using assms by (simp add: eq_fold)
lemma remove:
assumes "finite A" and "x \<in> A"
- shows "F g A = g x * F g (A - {x})"
+ shows "F g A = g x \<^bold>* F g (A - {x})"
proof -
from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
by (auto dest: mk_disjoint_insert)
@@ -52,21 +49,21 @@
lemma insert_remove:
assumes "finite A"
- shows "F g (insert x A) = g x * F g (A - {x})"
+ shows "F g (insert x A) = g x \<^bold>* F g (A - {x})"
using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
lemma neutral:
- assumes "\<forall>x\<in>A. g x = 1"
- shows "F g A = 1"
+ assumes "\<forall>x\<in>A. g x = \<^bold>1"
+ shows "F g A = \<^bold>1"
using assms by (induct A rule: infinite_finite_induct) simp_all
lemma neutral_const [simp]:
- "F (\<lambda>_. 1) A = 1"
+ "F (\<lambda>_. \<^bold>1) A = \<^bold>1"
by (simp add: neutral)
lemma union_inter:
assumes "finite A" and "finite B"
- shows "F g (A \<union> B) * F g (A \<inter> B) = F g A * F g B"
+ shows "F g (A \<union> B) \<^bold>* F g (A \<inter> B) = F g A \<^bold>* F g B"
\<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
using assms proof (induct A)
case empty then show ?case by simp
@@ -77,19 +74,19 @@
corollary union_inter_neutral:
assumes "finite A" and "finite B"
- and I0: "\<forall>x \<in> A \<inter> B. g x = 1"
- shows "F g (A \<union> B) = F g A * F g B"
+ and I0: "\<forall>x \<in> A \<inter> B. g x = \<^bold>1"
+ shows "F g (A \<union> B) = F g A \<^bold>* F g B"
using assms by (simp add: union_inter [symmetric] neutral)
corollary union_disjoint:
assumes "finite A" and "finite B"
assumes "A \<inter> B = {}"
- shows "F g (A \<union> B) = F g A * F g B"
+ shows "F g (A \<union> B) = F g A \<^bold>* F g B"
using assms by (simp add: union_inter_neutral)
lemma union_diff2:
assumes "finite A" and "finite B"
- shows "F g (A \<union> B) = F g (A - B) * F g (B - A) * F g (A \<inter> B)"
+ shows "F g (A \<union> B) = F g (A - B) \<^bold>* F g (B - A) \<^bold>* F g (A \<inter> B)"
proof -
have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
by auto
@@ -98,12 +95,12 @@
lemma subset_diff:
assumes "B \<subseteq> A" and "finite A"
- shows "F g A = F g (A - B) * F g B"
+ shows "F g A = F g (A - B) \<^bold>* F g B"
proof -
from assms have "finite (A - B)" by auto
moreover from assms have "finite B" by (rule finite_subset)
moreover from assms have "(A - B) \<inter> B = {}" by auto
- ultimately have "F g (A - B \<union> B) = F g (A - B) * F g B" by (rule union_disjoint)
+ ultimately have "F g (A - B \<union> B) = F g (A - B) \<^bold>* F g B" by (rule union_disjoint)
moreover from assms have "A \<union> B = A" by auto
ultimately show ?thesis by simp
qed
@@ -114,10 +111,10 @@
using assms by (induct A) (simp_all add: insert_Diff_if)
lemma not_neutral_contains_not_neutral:
- assumes "F g A \<noteq> z"
- obtains a where "a \<in> A" and "g a \<noteq> z"
+ assumes "F g A \<noteq> \<^bold>1"
+ obtains a where "a \<in> A" and "g a \<noteq> \<^bold>1"
proof -
- from assms have "\<exists>a\<in>A. g a \<noteq> z"
+ from assms have "\<exists>a\<in>A. g a \<noteq> \<^bold>1"
proof (induct A rule: infinite_finite_induct)
case (insert a A)
then show ?case by simp (rule, simp)
@@ -180,7 +177,7 @@
qed (auto dest: finite_UnionD intro: infinite)
lemma distrib:
- "F (\<lambda>x. g x * h x) A = F g A * F h A"
+ "F (\<lambda>x. g x \<^bold>* h x) A = F g A \<^bold>* F h A"
by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
lemma Sigma:
@@ -197,14 +194,14 @@
done
lemma related:
- assumes Re: "R 1 1"
- and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)"
+ assumes Re: "R \<^bold>1 \<^bold>1"
+ and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 \<^bold>* y1) (x2 \<^bold>* y2)"
and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
shows "R (F h S) (F g S)"
using fS by (rule finite_subset_induct) (insert assms, auto)
lemma mono_neutral_cong_left:
- assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
+ assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = \<^bold>1"
and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
proof-
have eq: "T = S \<union> (T - S)" using \<open>S \<subseteq> T\<close> by blast
@@ -216,16 +213,16 @@
qed
lemma mono_neutral_cong_right:
- "\<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>
+ "\<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>
\<Longrightarrow> F g T = F h S"
by (auto intro!: mono_neutral_cong_left [symmetric])
lemma mono_neutral_left:
- "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
+ "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = \<^bold>1 \<rbrakk> \<Longrightarrow> F g S = F g T"
by (blast intro: mono_neutral_cong_left)
lemma mono_neutral_right:
- "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
+ "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = \<^bold>1 \<rbrakk> \<Longrightarrow> F g T = F g S"
by (blast intro!: mono_neutral_left [symmetric])
lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T"
@@ -275,10 +272,10 @@
lemma reindex_nontrivial:
assumes "finite A"
- 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"
+ 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"
shows "F g (h ` A) = F (g \<circ> h) A"
proof (subst reindex_bij_betw_not_neutral [symmetric])
- show "bij_betw h (A - {x \<in> A. (g \<circ> h) x = 1}) (h ` A - h ` {x \<in> A. (g \<circ> h) x = 1})"
+ 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})"
using nz by (auto intro!: inj_onI simp: bij_betw_def)
qed (insert \<open>finite A\<close>, auto)
@@ -307,11 +304,11 @@
lemma delta:
assumes fS: "finite S"
- shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
+ shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
proof-
- let ?f = "(\<lambda>k. if k=a then b k else 1)"
+ let ?f = "(\<lambda>k. if k=a then b k else \<^bold>1)"
{ assume a: "a \<notin> S"
- hence "\<forall>k\<in>S. ?f k = 1" by simp
+ hence "\<forall>k\<in>S. ?f k = \<^bold>1" by simp
hence ?thesis using a by simp }
moreover
{ assume a: "a \<in> S"
@@ -320,7 +317,7 @@
have eq: "S = ?A \<union> ?B" using a by blast
have dj: "?A \<inter> ?B = {}" by simp
from fS have fAB: "finite ?A" "finite ?B" by auto
- have "F ?f S = F ?f ?A * F ?f ?B"
+ have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
by simp
then have ?thesis using a by simp }
@@ -329,14 +326,14 @@
lemma delta':
assumes fS: "finite S"
- shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
+ shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
using delta [OF fS, of a b, symmetric] by (auto intro: cong)
lemma If_cases:
fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
assumes fA: "finite A"
shows "F (\<lambda>x. if P x then h x else g x) A =
- F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
+ F h (A \<inter> {x. P x}) \<^bold>* F g (A \<inter> - {x. P x})"
proof -
have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}"
"(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
@@ -363,10 +360,10 @@
lemma inter_restrict:
assumes "finite A"
- shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else 1) A"
+ shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else \<^bold>1) A"
proof -
- let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else 1"
- have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else 1) = 1"
+ let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else \<^bold>1"
+ have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else \<^bold>1) = \<^bold>1"
by simp
moreover have "A \<inter> B \<subseteq> A" by blast
ultimately have "F ?g (A \<inter> B) = F ?g A" using \<open>finite A\<close>
@@ -375,12 +372,12 @@
qed
lemma inter_filter:
- "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else 1) A"
+ "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else \<^bold>1) A"
by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def)
lemma Union_comp:
assumes "\<forall>A \<in> B. finite A"
- 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"
+ 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"
shows "F g (\<Union>B) = (F \<circ> F) g B"
using assms proof (induct B rule: infinite_finite_induct)
case (infinite A)
@@ -391,9 +388,9 @@
next
case (insert A B)
then have "finite A" "finite B" "finite (\<Union>B)" "A \<notin> B"
- and "\<forall>x\<in>A \<inter> \<Union>B. g x = 1"
+ and "\<forall>x\<in>A \<inter> \<Union>B. g x = \<^bold>1"
and H: "F g (\<Union>B) = (F o F) g B" by auto
- then have "F g (A \<union> \<Union>B) = F g A * F g (\<Union>B)"
+ then have "F g (A \<union> \<Union>B) = F g A \<^bold>* F g (\<Union>B)"
by (simp add: union_inter_neutral)
with \<open>finite B\<close> \<open>A \<notin> B\<close> show ?case
by (simp add: H)
@@ -412,7 +409,7 @@
lemma Plus:
fixes A :: "'b set" and B :: "'c set"
assumes fin: "finite A" "finite B"
- shows "F g (A <+> B) = F (g \<circ> Inl) A * F (g \<circ> Inr) B"
+ shows "F g (A <+> B) = F (g \<circ> Inl) A \<^bold>* F (g \<circ> Inr) B"
proof -
have "A <+> B = Inl ` A \<union> Inr ` B" by auto
moreover from fin have "finite (Inl ` A :: ('b + 'c) set)" "finite (Inr ` B :: ('b + 'c) set)"
@@ -427,7 +424,7 @@
lemma same_carrier:
assumes "finite C"
assumes subset: "A \<subseteq> C" "B \<subseteq> C"
- assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
+ assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = \<^bold>1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = \<^bold>1"
shows "F g A = F h B \<longleftrightarrow> F g C = F h C"
proof -
from \<open>finite C\<close> subset have
@@ -437,12 +434,12 @@
from subset have [simp]: "B - (C - B) = B" by auto
from subset have "C = A \<union> (C - A)" by auto
then have "F g C = F g (A \<union> (C - A))" by simp
- also have "\<dots> = F g (A - (C - A)) * F g (C - A - A) * F g (A \<inter> (C - A))"
+ also have "\<dots> = F g (A - (C - A)) \<^bold>* F g (C - A - A) \<^bold>* F g (A \<inter> (C - A))"
using \<open>finite A\<close> \<open>finite (C - A)\<close> by (simp only: union_diff2)
finally have P: "F g C = F g A" using trivial by simp
from subset have "C = B \<union> (C - B)" by auto
then have "F h C = F h (B \<union> (C - B))" by simp
- also have "\<dots> = F h (B - (C - B)) * F h (C - B - B) * F h (B \<inter> (C - B))"
+ also have "\<dots> = F h (B - (C - B)) \<^bold>* F h (C - B - B) \<^bold>* F h (B \<inter> (C - B))"
using \<open>finite B\<close> \<open>finite (C - B)\<close> by (simp only: union_diff2)
finally have Q: "F h C = F h B" using trivial by simp
from P Q show ?thesis by simp
@@ -451,16 +448,13 @@
lemma same_carrierI:
assumes "finite C"
assumes subset: "A \<subseteq> C" "B \<subseteq> C"
- assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
+ assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = \<^bold>1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = \<^bold>1"
assumes "F g C = F h C"
shows "F g A = F h B"
using assms same_carrier [of C A B] by simp
end
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
subsection \<open>Generalized summation over a set\<close>
--- a/src/HOL/Groups_List.thy Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Groups_List.thy Sat Jun 11 16:22:42 2016 +0200
@@ -6,26 +6,23 @@
imports List
begin
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
locale monoid_list = monoid
begin
definition F :: "'a list \<Rightarrow> 'a"
where
- eq_foldr [code]: "F xs = foldr f xs 1"
+ eq_foldr [code]: "F xs = foldr f xs \<^bold>1"
lemma Nil [simp]:
- "F [] = 1"
+ "F [] = \<^bold>1"
by (simp add: eq_foldr)
lemma Cons [simp]:
- "F (x # xs) = x * F xs"
+ "F (x # xs) = x \<^bold>* F xs"
by (simp add: eq_foldr)
lemma append [simp]:
- "F (xs @ ys) = F xs * F ys"
+ "F (xs @ ys) = F xs \<^bold>* F ys"
by (induct xs) (simp_all add: assoc)
end
@@ -52,9 +49,6 @@
end
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
subsection \<open>List summation\<close>
--- a/src/HOL/Lattices.thy Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Lattices.thy Sat Jun 11 16:22:42 2016 +0200
@@ -16,17 +16,14 @@
undesired effects may occur due to interpretation.
\<close>
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
locale semilattice = abel_semigroup +
- assumes idem [simp]: "a * a = a"
+ assumes idem [simp]: "a \<^bold>* a = a"
begin
-lemma left_idem [simp]: "a * (a * b) = a * b"
+lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
by (simp add: assoc [symmetric])
-lemma right_idem [simp]: "(a * b) * b = a * b"
+lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
by (simp add: assoc)
end
@@ -34,109 +31,109 @@
locale semilattice_neutr = semilattice + comm_monoid
locale semilattice_order = semilattice +
- fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
- and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
- assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
- and strict_order_iff: "a \<prec> b \<longleftrightarrow> a = a * b \<and> a \<noteq> b"
+ fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50)
+ and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50)
+ assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b"
+ and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b"
begin
lemma orderI:
- "a = a * b \<Longrightarrow> a \<preceq> b"
+ "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b"
by (simp add: order_iff)
lemma orderE:
- assumes "a \<preceq> b"
- obtains "a = a * b"
+ assumes "a \<^bold>\<le> b"
+ obtains "a = a \<^bold>* b"
using assms by (unfold order_iff)
sublocale ordering less_eq less
proof
fix a b
- show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
+ show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b"
by (simp add: order_iff strict_order_iff)
next
fix a
- show "a \<preceq> a"
+ show "a \<^bold>\<le> a"
by (simp add: order_iff)
next
fix a b
- assume "a \<preceq> b" "b \<preceq> a"
- then have "a = a * b" "a * b = b"
+ assume "a \<^bold>\<le> b" "b \<^bold>\<le> a"
+ then have "a = a \<^bold>* b" "a \<^bold>* b = b"
by (simp_all add: order_iff commute)
then show "a = b" by simp
next
fix a b c
- assume "a \<preceq> b" "b \<preceq> c"
- then have "a = a * b" "b = b * c"
+ assume "a \<^bold>\<le> b" "b \<^bold>\<le> c"
+ then have "a = a \<^bold>* b" "b = b \<^bold>* c"
by (simp_all add: order_iff commute)
- then have "a = a * (b * c)"
+ then have "a = a \<^bold>* (b \<^bold>* c)"
by simp
- then have "a = (a * b) * c"
+ then have "a = (a \<^bold>* b) \<^bold>* c"
by (simp add: assoc)
- with \<open>a = a * b\<close> [symmetric] have "a = a * c" by simp
- then show "a \<preceq> c" by (rule orderI)
+ with \<open>a = a \<^bold>* b\<close> [symmetric] have "a = a \<^bold>* c" by simp
+ then show "a \<^bold>\<le> c" by (rule orderI)
qed
lemma cobounded1 [simp]:
- "a * b \<preceq> a"
+ "a \<^bold>* b \<^bold>\<le> a"
by (simp add: order_iff commute)
lemma cobounded2 [simp]:
- "a * b \<preceq> b"
+ "a \<^bold>* b \<^bold>\<le> b"
by (simp add: order_iff)
lemma boundedI:
- assumes "a \<preceq> b" and "a \<preceq> c"
- shows "a \<preceq> b * c"
+ assumes "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
+ shows "a \<^bold>\<le> b \<^bold>* c"
proof (rule orderI)
- from assms obtain "a * b = a" and "a * c = a" by (auto elim!: orderE)
- then show "a = a * (b * c)" by (simp add: assoc [symmetric])
+ from assms obtain "a \<^bold>* b = a" and "a \<^bold>* c = a" by (auto elim!: orderE)
+ then show "a = a \<^bold>* (b \<^bold>* c)" by (simp add: assoc [symmetric])
qed
lemma boundedE:
- assumes "a \<preceq> b * c"
- obtains "a \<preceq> b" and "a \<preceq> c"
+ assumes "a \<^bold>\<le> b \<^bold>* c"
+ obtains "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
using assms by (blast intro: trans cobounded1 cobounded2)
lemma bounded_iff [simp]:
- "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c"
+ "a \<^bold>\<le> b \<^bold>* c \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<^bold>\<le> c"
by (blast intro: boundedI elim: boundedE)
lemma strict_boundedE:
- assumes "a \<prec> b * c"
- obtains "a \<prec> b" and "a \<prec> c"
+ assumes "a \<^bold>< b \<^bold>* c"
+ obtains "a \<^bold>< b" and "a \<^bold>< c"
using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+
lemma coboundedI1:
- "a \<preceq> c \<Longrightarrow> a * b \<preceq> c"
+ "a \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
by (rule trans) auto
lemma coboundedI2:
- "b \<preceq> c \<Longrightarrow> a * b \<preceq> c"
+ "b \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
by (rule trans) auto
lemma strict_coboundedI1:
- "a \<prec> c \<Longrightarrow> a * b \<prec> c"
+ "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
using irrefl
by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order elim: strict_boundedE)
lemma strict_coboundedI2:
- "b \<prec> c \<Longrightarrow> a * b \<prec> c"
+ "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
using strict_coboundedI1 [of b c a] by (simp add: commute)
-lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d"
+lemma mono: "a \<^bold>\<le> c \<Longrightarrow> b \<^bold>\<le> d \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c \<^bold>* d"
by (blast intro: boundedI coboundedI1 coboundedI2)
-lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
+lemma absorb1: "a \<^bold>\<le> b \<Longrightarrow> a \<^bold>* b = a"
by (rule antisym) (auto simp add: refl)
-lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
+lemma absorb2: "b \<^bold>\<le> a \<Longrightarrow> a \<^bold>* b = b"
by (rule antisym) (auto simp add: refl)
-lemma absorb_iff1: "a \<preceq> b \<longleftrightarrow> a * b = a"
+lemma absorb_iff1: "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>* b = a"
using order_iff by auto
-lemma absorb_iff2: "b \<preceq> a \<longleftrightarrow> a * b = b"
+lemma absorb_iff2: "b \<^bold>\<le> a \<longleftrightarrow> a \<^bold>* b = b"
using order_iff by (auto simp add: commute)
end
@@ -144,14 +141,11 @@
locale semilattice_neutr_order = semilattice_neutr + semilattice_order
begin
-sublocale ordering_top less_eq less 1
+sublocale ordering_top less_eq less "\<^bold>1"
by standard (simp add: order_iff)
end
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
subsection \<open>Syntactic infimum and supremum operations\<close>
--- a/src/HOL/Lattices_Big.thy Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Lattices_Big.thy Sat Jun 11 16:22:42 2016 +0200
@@ -11,10 +11,6 @@
subsection \<open>Generic lattice operations over a set\<close>
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
-
subsubsection \<open>Without neutral element\<close>
locale semilattice_set = semilattice
@@ -48,20 +44,20 @@
lemma insert_not_elem:
assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
- shows "F (insert x A) = x * F A"
+ shows "F (insert x A) = x \<^bold>* F A"
proof -
from \<open>A \<noteq> {}\<close> obtain b where "b \<in> A" by blast
then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
with \<open>finite A\<close> and \<open>x \<notin> A\<close>
have "finite (insert x B)" and "b \<notin> insert x B" by auto
- then have "F (insert b (insert x B)) = x * F (insert b B)"
+ then have "F (insert b (insert x B)) = x \<^bold>* F (insert b B)"
by (simp add: eq_fold)
then show ?thesis by (simp add: * insert_commute)
qed
lemma in_idem:
assumes "finite A" and "x \<in> A"
- shows "x * F A = F A"
+ shows "x \<^bold>* F A = F A"
proof -
from assms have "A \<noteq> {}" by auto
with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
@@ -70,17 +66,17 @@
lemma insert [simp]:
assumes "finite A" and "A \<noteq> {}"
- shows "F (insert x A) = x * F A"
+ shows "F (insert x A) = x \<^bold>* F A"
using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
lemma union:
assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
- shows "F (A \<union> B) = F A * F B"
+ shows "F (A \<union> B) = F A \<^bold>* F B"
using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
lemma remove:
assumes "finite A" and "x \<in> A"
- shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
+ shows "F A = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
proof -
from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
with assms show ?thesis by simp
@@ -88,19 +84,19 @@
lemma insert_remove:
assumes "finite A"
- shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
+ shows "F (insert x A) = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
lemma subset:
assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
- shows "F B * F A = F A"
+ shows "F B \<^bold>* F A = F A"
proof -
from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
qed
lemma closed:
- assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
+ assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
shows "F A \<in> A"
using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
case singleton then show ?case by simp
@@ -109,17 +105,17 @@
qed
lemma hom_commute:
- assumes hom: "\<And>x y. h (x * y) = h x * h y"
+ assumes hom: "\<And>x y. h (x \<^bold>* y) = h x \<^bold>* h y"
and N: "finite N" "N \<noteq> {}"
shows "h (F N) = F (h ` N)"
using N proof (induct rule: finite_ne_induct)
case singleton thus ?case by simp
next
case (insert n N)
- then have "h (F (insert n N)) = h (n * F N)" by simp
- also have "\<dots> = h n * h (F N)" by (rule hom)
+ then have "h (F (insert n N)) = h (n \<^bold>* F N)" by simp
+ also have "\<dots> = h n \<^bold>* h (F N)" by (rule hom)
also have "h (F N) = F (h ` N)" by (rule insert)
- also have "h n * \<dots> = F (insert (h n) (h ` N))"
+ also have "h n \<^bold>* \<dots> = F (insert (h n) (h ` N))"
using insert by simp
also have "insert (h n) (h ` N) = h ` insert n N" by simp
finally show ?case .
@@ -135,25 +131,25 @@
lemma bounded_iff:
assumes "finite A" and "A \<noteq> {}"
- shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
+ shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
lemma boundedI:
assumes "finite A"
assumes "A \<noteq> {}"
- assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
- shows "x \<preceq> F A"
+ assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
+ shows "x \<^bold>\<le> F A"
using assms by (simp add: bounded_iff)
lemma boundedE:
- assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
- obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
+ assumes "finite A" and "A \<noteq> {}" and "x \<^bold>\<le> F A"
+ obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
using assms by (simp add: bounded_iff)
lemma coboundedI:
assumes "finite A"
and "a \<in> A"
- shows "F A \<preceq> a"
+ shows "F A \<^bold>\<le> a"
proof -
from assms have "A \<noteq> {}" by auto
from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
@@ -168,15 +164,15 @@
lemma antimono:
assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
- shows "F B \<preceq> F A"
+ shows "F B \<^bold>\<le> F A"
proof (cases "A = B")
case True then show ?thesis by (simp add: refl)
next
case False
have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
then have "F B = F (A \<union> (B - A))" by simp
- also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
- also have "\<dots> \<preceq> F A" by simp
+ also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
+ also have "\<dots> \<^bold>\<le> F A" by simp
finally show ?thesis .
qed
@@ -193,24 +189,24 @@
definition F :: "'a set \<Rightarrow> 'a"
where
- eq_fold: "F A = Finite_Set.fold f 1 A"
+ eq_fold: "F A = Finite_Set.fold f \<^bold>1 A"
lemma infinite [simp]:
- "\<not> finite A \<Longrightarrow> F A = 1"
+ "\<not> finite A \<Longrightarrow> F A = \<^bold>1"
by (simp add: eq_fold)
lemma empty [simp]:
- "F {} = 1"
+ "F {} = \<^bold>1"
by (simp add: eq_fold)
lemma insert [simp]:
assumes "finite A"
- shows "F (insert x A) = x * F A"
+ shows "F (insert x A) = x \<^bold>* F A"
using assms by (simp add: eq_fold)
lemma in_idem:
assumes "finite A" and "x \<in> A"
- shows "x * F A = F A"
+ shows "x \<^bold>* F A = F A"
proof -
from assms have "A \<noteq> {}" by auto
with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
@@ -219,12 +215,12 @@
lemma union:
assumes "finite A" and "finite B"
- shows "F (A \<union> B) = F A * F B"
+ shows "F (A \<union> B) = F A \<^bold>* F B"
using assms by (induct A) (simp_all add: ac_simps)
lemma remove:
assumes "finite A" and "x \<in> A"
- shows "F A = x * F (A - {x})"
+ shows "F A = x \<^bold>* F (A - {x})"
proof -
from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
with assms show ?thesis by simp
@@ -232,19 +228,19 @@
lemma insert_remove:
assumes "finite A"
- shows "F (insert x A) = x * F (A - {x})"
+ shows "F (insert x A) = x \<^bold>* F (A - {x})"
using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
lemma subset:
assumes "finite A" and "B \<subseteq> A"
- shows "F B * F A = F A"
+ shows "F B \<^bold>* F A = F A"
proof -
from assms have "finite B" by (auto dest: finite_subset)
with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
qed
lemma closed:
- assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
+ assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
shows "F A \<in> A"
using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
case singleton then show ?case by simp
@@ -259,24 +255,24 @@
lemma bounded_iff:
assumes "finite A"
- shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
+ shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
using assms by (induct A) (simp_all add: bounded_iff)
lemma boundedI:
assumes "finite A"
- assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
- shows "x \<preceq> F A"
+ assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
+ shows "x \<^bold>\<le> F A"
using assms by (simp add: bounded_iff)
lemma boundedE:
- assumes "finite A" and "x \<preceq> F A"
- obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
+ assumes "finite A" and "x \<^bold>\<le> F A"
+ obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
using assms by (simp add: bounded_iff)
lemma coboundedI:
assumes "finite A"
and "a \<in> A"
- shows "F A \<preceq> a"
+ shows "F A \<^bold>\<le> a"
proof -
from assms have "A \<noteq> {}" by auto
from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
@@ -291,23 +287,20 @@
lemma antimono:
assumes "A \<subseteq> B" and "finite B"
- shows "F B \<preceq> F A"
+ shows "F B \<^bold>\<le> F A"
proof (cases "A = B")
case True then show ?thesis by (simp add: refl)
next
case False
have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
then have "F B = F (A \<union> (B - A))" by simp
- also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
- also have "\<dots> \<preceq> F A" by simp
+ also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
+ also have "\<dots> \<^bold>\<le> F A" by simp
finally show ?thesis .
qed
end
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
subsection \<open>Lattice operations on finite sets\<close>
--- a/src/HOL/Library/Groups_Big_Fun.thy Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Sat Jun 11 16:22:42 2016 +0200
@@ -9,21 +9,18 @@
subsection \<open>Abstract product\<close>
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
locale comm_monoid_fun = comm_monoid
begin
definition G :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
where
- expand_set: "G g = comm_monoid_set.F f 1 g {a. g a \<noteq> 1}"
+ expand_set: "G g = comm_monoid_set.F f \<^bold>1 g {a. g a \<noteq> \<^bold>1}"
-interpretation F: comm_monoid_set f 1
+interpretation F: comm_monoid_set f "\<^bold>1"
..
lemma expand_superset:
- assumes "finite A" and "{a. g a \<noteq> 1} \<subseteq> A"
+ assumes "finite A" and "{a. g a \<noteq> \<^bold>1} \<subseteq> A"
shows "G g = F.F g A"
apply (simp add: expand_set)
apply (rule F.same_carrierI [of A])
@@ -32,7 +29,7 @@
lemma conditionalize:
assumes "finite A"
- shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else 1)"
+ shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else \<^bold>1)"
using assms
apply (simp add: expand_set)
apply (rule F.same_carrierI [of A])
@@ -40,29 +37,29 @@
done
lemma neutral [simp]:
- "G (\<lambda>a. 1) = 1"
+ "G (\<lambda>a. \<^bold>1) = \<^bold>1"
by (simp add: expand_set)
lemma update [simp]:
- assumes "finite {a. g a \<noteq> 1}"
- assumes "g a = 1"
- shows "G (g(a := b)) = b * G g"
-proof (cases "b = 1")
- case True with \<open>g a = 1\<close> show ?thesis
+ assumes "finite {a. g a \<noteq> \<^bold>1}"
+ assumes "g a = \<^bold>1"
+ shows "G (g(a := b)) = b \<^bold>* G g"
+proof (cases "b = \<^bold>1")
+ case True with \<open>g a = \<^bold>1\<close> show ?thesis
by (simp add: expand_set) (rule F.cong, auto)
next
case False
- moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> 1} = insert a {a. g a \<noteq> 1}"
+ moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> \<^bold>1} = insert a {a. g a \<noteq> \<^bold>1}"
by auto
- moreover from \<open>g a = 1\<close> have "a \<notin> {a. g a \<noteq> 1}"
+ moreover from \<open>g a = \<^bold>1\<close> have "a \<notin> {a. g a \<noteq> \<^bold>1}"
by simp
- 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}"
- by (rule F.cong) (auto simp add: \<open>g a = 1\<close>)
- ultimately show ?thesis using \<open>finite {a. g a \<noteq> 1}\<close> by (simp add: expand_set)
+ 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}"
+ by (rule F.cong) (auto simp add: \<open>g a = \<^bold>1\<close>)
+ ultimately show ?thesis using \<open>finite {a. g a \<noteq> \<^bold>1}\<close> by (simp add: expand_set)
qed
lemma infinite [simp]:
- "\<not> finite {a. g a \<noteq> 1} \<Longrightarrow> G g = 1"
+ "\<not> finite {a. g a \<noteq> \<^bold>1} \<Longrightarrow> G g = \<^bold>1"
by (simp add: expand_set)
lemma cong:
@@ -76,8 +73,8 @@
using assms by (fact cong)
lemma not_neutral_obtains_not_neutral:
- assumes "G g \<noteq> 1"
- obtains a where "g a \<noteq> 1"
+ assumes "G g \<noteq> \<^bold>1"
+ obtains a where "g a \<noteq> \<^bold>1"
using assms by (auto elim: F.not_neutral_contains_not_neutral simp add: expand_set)
lemma reindex_cong:
@@ -87,59 +84,59 @@
proof -
from assms have unfold: "h = g \<circ> l" by simp
from \<open>bij l\<close> have "inj l" by (rule bij_is_inj)
- then have "inj_on l {a. h a \<noteq> 1}" by (rule subset_inj_on) simp
- moreover from \<open>bij l\<close> have "{a. g a \<noteq> 1} = l ` {a. h a \<noteq> 1}"
+ then have "inj_on l {a. h a \<noteq> \<^bold>1}" by (rule subset_inj_on) simp
+ moreover from \<open>bij l\<close> have "{a. g a \<noteq> \<^bold>1} = l ` {a. h a \<noteq> \<^bold>1}"
by (auto simp add: image_Collect unfold elim: bij_pointE)
- moreover have "\<And>x. x \<in> {a. h a \<noteq> 1} \<Longrightarrow> g (l x) = h x"
+ moreover have "\<And>x. x \<in> {a. h a \<noteq> \<^bold>1} \<Longrightarrow> g (l x) = h x"
by (simp add: unfold)
- ultimately have "F.F g {a. g a \<noteq> 1} = F.F h {a. h a \<noteq> 1}"
+ ultimately have "F.F g {a. g a \<noteq> \<^bold>1} = F.F h {a. h a \<noteq> \<^bold>1}"
by (rule F.reindex_cong)
then show ?thesis by (simp add: expand_set)
qed
lemma distrib:
- assumes "finite {a. g a \<noteq> 1}" and "finite {a. h a \<noteq> 1}"
- shows "G (\<lambda>a. g a * h a) = G g * G h"
+ assumes "finite {a. g a \<noteq> \<^bold>1}" and "finite {a. h a \<noteq> \<^bold>1}"
+ shows "G (\<lambda>a. g a \<^bold>* h a) = G g \<^bold>* G h"
proof -
- from assms have "finite ({a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1})" by simp
- moreover have "{a. g a * h a \<noteq> 1} \<subseteq> {a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"
+ from assms have "finite ({a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1})" by simp
+ 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}"
by auto (drule sym, simp)
ultimately show ?thesis
using assms
- by (simp add: expand_superset [of "{a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"] F.distrib)
+ by (simp add: expand_superset [of "{a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1}"] F.distrib)
qed
lemma commute:
assumes "finite C"
- 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")
+ 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")
shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
proof -
from \<open>finite C\<close> subset
- have "finite ({a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1})"
+ have "finite ({a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1})"
by (rule rev_finite_subset)
then have fins:
- "finite {b. \<exists>a. g a b \<noteq> 1}" "finite {a. \<exists>b. g a b \<noteq> 1}"
+ "finite {b. \<exists>a. g a b \<noteq> \<^bold>1}" "finite {a. \<exists>b. g a b \<noteq> \<^bold>1}"
by (auto simp add: finite_cartesian_product_iff)
- have subsets: "\<And>a. {b. g a b \<noteq> 1} \<subseteq> {b. \<exists>a. g a b \<noteq> 1}"
- "\<And>b. {a. g a b \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
- "{a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1} \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
- "{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}"
+ have subsets: "\<And>a. {b. g a b \<noteq> \<^bold>1} \<subseteq> {b. \<exists>a. g a b \<noteq> \<^bold>1}"
+ "\<And>b. {a. g a b \<noteq> \<^bold>1} \<subseteq> {a. \<exists>b. g a b \<noteq> \<^bold>1}"
+ "{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}"
+ "{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}"
by (auto elim: F.not_neutral_contains_not_neutral)
from F.commute have
- "F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1} =
- 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}" .
- with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) =
- G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> 1})"
- by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
- expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
+ "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} =
+ 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}" .
+ with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) =
+ G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> \<^bold>1})"
+ by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> \<^bold>1}"]
+ expand_superset [of "{a. \<exists>b. g a b \<noteq> \<^bold>1}"])
with subsets fins show ?thesis
- by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
- expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
+ by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> \<^bold>1}"]
+ expand_superset [of "{a. \<exists>b. g a b \<noteq> \<^bold>1}"])
qed
lemma cartesian_product:
assumes "finite C"
- 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")
+ 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")
shows "G (\<lambda>a. G (g a)) = G (\<lambda>(a, b). g a b)"
proof -
from subset \<open>finite C\<close> have fin_prod: "finite (?A \<times> ?B)"
@@ -147,7 +144,7 @@
from fin_prod have "finite ?A" and "finite ?B"
by (auto simp add: finite_cartesian_product_iff)
have *: "G (\<lambda>a. G (g a)) =
- (F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1})"
+ (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})"
apply (subst expand_superset [of "?B"])
apply (rule \<open>finite ?B\<close>)
apply auto
@@ -157,9 +154,9 @@
apply (erule F.not_neutral_contains_not_neutral)
apply auto
done
- have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> ?A \<times> ?B"
+ have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> ?A \<times> ?B"
by auto
- with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> C"
+ with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> C"
by blast
show ?thesis
apply (simp add: *)
@@ -176,12 +173,12 @@
lemma cartesian_product2:
assumes fin: "finite D"
- 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")
+ 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")
shows "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>(a, b, c). g a b c)"
proof -
have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
by (auto intro!: bijI injI simp add: image_def)
- 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"
+ 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"
by auto (insert subset, blast)
with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
by (rule cartesian_product)
@@ -193,27 +190,24 @@
qed
lemma delta [simp]:
- "G (\<lambda>b. if b = a then g b else 1) = g a"
+ "G (\<lambda>b. if b = a then g b else \<^bold>1) = g a"
proof -
- have "{b. (if b = a then g b else 1) \<noteq> 1} \<subseteq> {a}" by auto
+ have "{b. (if b = a then g b else \<^bold>1) \<noteq> \<^bold>1} \<subseteq> {a}" by auto
then show ?thesis by (simp add: expand_superset [of "{a}"])
qed
lemma delta' [simp]:
- "G (\<lambda>b. if a = b then g b else 1) = g a"
+ "G (\<lambda>b. if a = b then g b else \<^bold>1) = g a"
proof -
- have "(\<lambda>b. if a = b then g b else 1) = (\<lambda>b. if b = a then g b else 1)"
+ have "(\<lambda>b. if a = b then g b else \<^bold>1) = (\<lambda>b. if b = a then g b else \<^bold>1)"
by (simp add: fun_eq_iff)
- then have "G (\<lambda>b. if a = b then g b else 1) = G (\<lambda>b. if b = a then g b else 1)"
+ 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)"
by (simp cong del: strong_cong)
then show ?thesis by simp
qed
end
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
subsection \<open>Concrete sum\<close>
@@ -339,4 +333,3 @@
qed
end
-
--- a/src/HOL/Library/Multiset.thy Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Jun 11 16:22:42 2016 +0200
@@ -1562,16 +1562,13 @@
subsection \<open>Big operators\<close>
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
locale comm_monoid_mset = comm_monoid
begin
definition F :: "'a multiset \<Rightarrow> 'a"
- where eq_fold: "F M = fold_mset f 1 M"
-
-lemma empty [simp]: "F {#} = 1"
+ where eq_fold: "F M = fold_mset f \<^bold>1 M"
+
+lemma empty [simp]: "F {#} = \<^bold>1"
by (simp add: eq_fold)
lemma singleton [simp]: "F {#x#} = x"
@@ -1581,7 +1578,7 @@
show ?thesis by (simp add: eq_fold)
qed
-lemma union [simp]: "F (M + N) = F M * F N"
+lemma union [simp]: "F (M + N) = F M \<^bold>* F N"
proof -
interpret comp_fun_commute f
by standard (simp add: fun_eq_iff left_commute)
@@ -1599,9 +1596,6 @@
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)"
by (induct NN) auto
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
context comm_monoid_add
begin
--- a/src/HOL/Orderings.thy Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Orderings.thy Sat Jun 11 16:22:42 2016 +0200
@@ -15,71 +15,71 @@
subsection \<open>Abstract ordering\<close>
locale ordering =
- fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
- and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
- assumes strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
- assumes refl: "a \<preceq> a" \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
- and antisym: "a \<preceq> b \<Longrightarrow> b \<preceq> a \<Longrightarrow> a = b"
- and trans: "a \<preceq> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<preceq> c"
+ fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50)
+ and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50)
+ assumes strict_iff_order: "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b"
+ assumes refl: "a \<^bold>\<le> a" \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
+ and antisym: "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>\<le> a \<Longrightarrow> a = b"
+ and trans: "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>\<le> c \<Longrightarrow> a \<^bold>\<le> c"
begin
lemma strict_implies_order:
- "a \<prec> b \<Longrightarrow> a \<preceq> b"
+ "a \<^bold>< b \<Longrightarrow> a \<^bold>\<le> b"
by (simp add: strict_iff_order)
lemma strict_implies_not_eq:
- "a \<prec> b \<Longrightarrow> a \<noteq> b"
+ "a \<^bold>< b \<Longrightarrow> a \<noteq> b"
by (simp add: strict_iff_order)
lemma not_eq_order_implies_strict:
- "a \<noteq> b \<Longrightarrow> a \<preceq> b \<Longrightarrow> a \<prec> b"
+ "a \<noteq> b \<Longrightarrow> a \<^bold>\<le> b \<Longrightarrow> a \<^bold>< b"
by (simp add: strict_iff_order)
lemma order_iff_strict:
- "a \<preceq> b \<longleftrightarrow> a \<prec> b \<or> a = b"
+ "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>< b \<or> a = b"
by (auto simp add: strict_iff_order refl)
lemma irrefl: \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
- "\<not> a \<prec> a"
+ "\<not> a \<^bold>< a"
by (simp add: strict_iff_order)
lemma asym:
- "a \<prec> b \<Longrightarrow> b \<prec> a \<Longrightarrow> False"
+ "a \<^bold>< b \<Longrightarrow> b \<^bold>< a \<Longrightarrow> False"
by (auto simp add: strict_iff_order intro: antisym)
lemma strict_trans1:
- "a \<preceq> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
+ "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
by (auto simp add: strict_iff_order intro: trans antisym)
lemma strict_trans2:
- "a \<prec> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<prec> c"
+ "a \<^bold>< b \<Longrightarrow> b \<^bold>\<le> c \<Longrightarrow> a \<^bold>< c"
by (auto simp add: strict_iff_order intro: trans antisym)
lemma strict_trans:
- "a \<prec> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
+ "a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
by (auto intro: strict_trans1 strict_implies_order)
end
locale ordering_top = ordering +
- fixes top :: "'a"
- assumes extremum [simp]: "a \<preceq> top"
+ fixes top :: "'a" ("\<^bold>\<top>")
+ assumes extremum [simp]: "a \<^bold>\<le> \<^bold>\<top>"
begin
lemma extremum_uniqueI:
- "top \<preceq> a \<Longrightarrow> a = top"
+ "\<^bold>\<top> \<^bold>\<le> a \<Longrightarrow> a = \<^bold>\<top>"
by (rule antisym) auto
lemma extremum_unique:
- "top \<preceq> a \<longleftrightarrow> a = top"
+ "\<^bold>\<top> \<^bold>\<le> a \<longleftrightarrow> a = \<^bold>\<top>"
by (auto intro: antisym)
lemma extremum_strict [simp]:
- "\<not> (top \<prec> a)"
+ "\<not> (\<^bold>\<top> \<^bold>< a)"
using extremum [of a] by (auto simp add: order_iff_strict intro: asym irrefl)
lemma not_eq_extremum:
- "a \<noteq> top \<longleftrightarrow> a \<prec> top"
+ "a \<noteq> \<^bold>\<top> \<longleftrightarrow> a \<^bold>< \<^bold>\<top>"
by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum)
end