--- a/src/HOL/Algebra/Lattice.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Lattice.thy Sat Oct 10 16:26:23 2015 +0200
@@ -9,9 +9,9 @@
imports Congruence
begin
-section {* Orders and Lattices *}
+section \<open>Orders and Lattices\<close>
-subsection {* Partial Orders *}
+subsection \<open>Partial Orders\<close>
record 'a gorder = "'a eq_object" +
le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
@@ -32,7 +32,7 @@
where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
-subsubsection {* The order relation *}
+subsubsection \<open>The order relation\<close>
context weak_partial_order
begin
@@ -103,7 +103,7 @@
using assms unfolding lless_def by (blast dest: le_trans intro: sym)
-subsubsection {* Upper and lower bounds of a set *}
+subsubsection \<open>Upper and lower bounds of a set\<close>
definition
Upper :: "[_, 'a set] => 'a set"
@@ -276,7 +276,7 @@
qed
-subsubsection {* Least and greatest, as predicate *}
+subsubsection \<open>Least and greatest, as predicate\<close>
definition
least :: "[_, 'a, 'a set] => bool"
@@ -286,8 +286,8 @@
greatest :: "[_, 'a, 'a set] => bool"
where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
-text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
- .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
+text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l
+ .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
lemma least_closed [intro, simp]:
"least L l A ==> l \<in> carrier L"
@@ -310,8 +310,8 @@
"[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
by (unfold least_def) (auto dest: sym)
-text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for
- @{term "A {.=} A'"} *}
+text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for
+ @{term "A {.=} A'"}\<close>
lemma (in weak_partial_order) least_Upper_cong_l:
assumes "x .= x'"
@@ -367,8 +367,8 @@
greatest L x A = greatest L x' A"
by (unfold greatest_def) (auto dest: sym)
-text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for
- @{term "A {.=} A'"} *}
+text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for
+ @{term "A {.=} A'"}\<close>
lemma (in weak_partial_order) greatest_Lower_cong_l:
assumes "x .= x'"
@@ -402,7 +402,7 @@
shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
by (unfold greatest_def) blast
-text {* Supremum and infimum *}
+text \<open>Supremum and infimum\<close>
definition
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
@@ -421,7 +421,7 @@
where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
-subsection {* Lattices *}
+subsection \<open>Lattices\<close>
locale weak_upper_semilattice = weak_partial_order +
assumes sup_of_two_exists:
@@ -434,7 +434,7 @@
locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
-subsubsection {* Supremum *}
+subsubsection \<open>Supremum\<close>
lemma (in weak_upper_semilattice) joinI:
"[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
@@ -507,7 +507,7 @@
unfolding sup_def
by (rule someI2) (auto intro: sup_of_singletonI)
-text {* Condition on @{text A}: supremum exists. *}
+text \<open>Condition on @{text A}: supremum exists.\<close>
lemma (in weak_upper_semilattice) sup_insertI:
"[| !!s. least L s (Upper L (insert x A)) ==> P s;
@@ -638,7 +638,7 @@
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
proof (rule finite_sup_insertI)
- -- {* The textbook argument in Jacobson I, p 457 *}
+ -- \<open>The textbook argument in Jacobson I, p 457\<close>
fix s
assume sup: "least L s (Upper L {x, y, z})"
show "x \<squnion> (y \<squnion> z) .= s"
@@ -652,7 +652,7 @@
qed (simp_all add: L least_closed [OF sup])
qed (simp_all add: L)
-text {* Commutativity holds for @{text "="}. *}
+text \<open>Commutativity holds for @{text "="}.\<close>
lemma join_comm:
fixes L (structure)
@@ -673,7 +673,7 @@
qed
-subsubsection {* Infimum *}
+subsubsection \<open>Infimum\<close>
lemma (in weak_lower_semilattice) meetI:
"[| !!i. greatest L i (Lower L {x, y}) ==> P i;
@@ -747,7 +747,7 @@
unfolding inf_def
by (rule someI2) (auto intro: inf_of_singletonI)
-text {* Condition on @{text A}: infimum exists. *}
+text \<open>Condition on @{text A}: infimum exists.\<close>
lemma (in weak_lower_semilattice) inf_insertI:
"[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
@@ -879,7 +879,7 @@
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
proof (rule finite_inf_insertI)
- txt {* The textbook argument in Jacobson I, p 457 *}
+ txt \<open>The textbook argument in Jacobson I, p 457\<close>
fix i
assume inf: "greatest L i (Lower L {x, y, z})"
show "x \<sqinter> (y \<sqinter> z) .= i"
@@ -911,19 +911,19 @@
qed
-subsection {* Total Orders *}
+subsection \<open>Total Orders\<close>
locale weak_total_order = weak_partial_order +
assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
-text {* Introduction rule: the usual definition of total order *}
+text \<open>Introduction rule: the usual definition of total order\<close>
lemma (in weak_partial_order) weak_total_orderI:
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
shows "weak_total_order L"
by standard (rule total)
-text {* Total orders are lattices. *}
+text \<open>Total orders are lattices.\<close>
sublocale weak_total_order < weak: weak_lattice
proof
@@ -969,7 +969,7 @@
qed
-subsection {* Complete Lattices *}
+subsection \<open>Complete Lattices\<close>
locale weak_complete_lattice = weak_lattice +
assumes sup_exists:
@@ -977,7 +977,7 @@
and inf_exists:
"[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
-text {* Introduction rule: the usual definition of complete lattice *}
+text \<open>Introduction rule: the usual definition of complete lattice\<close>
lemma (in weak_partial_order) weak_complete_latticeI:
assumes sup_exists:
@@ -1034,7 +1034,7 @@
"\<bottom> \<in> carrier L"
by (unfold bottom_def) simp
-text {* Jacobson: Theorem 8.1 *}
+text \<open>Jacobson: Theorem 8.1\<close>
lemma Lower_empty [simp]:
"Lower L {} = carrier L"
@@ -1090,7 +1090,7 @@
(* TODO: prove dual version *)
-subsection {* Orders and Lattices where @{text eq} is the Equality *}
+subsection \<open>Orders and Lattices where @{text eq} is the Equality\<close>
locale partial_order = weak_partial_order +
assumes eq_is_equal: "op .= = op ="
@@ -1115,7 +1115,7 @@
end
-text {* Least and greatest, as predicate *}
+text \<open>Least and greatest, as predicate\<close>
lemma (in partial_order) least_unique:
"[| least L x A; least L y A |] ==> x = y"
@@ -1126,7 +1126,7 @@
using weak_greatest_unique unfolding eq_is_equal .
-text {* Lattices *}
+text \<open>Lattices\<close>
locale upper_semilattice = partial_order +
assumes sup_of_two_exists:
@@ -1145,7 +1145,7 @@
locale lattice = upper_semilattice + lower_semilattice
-text {* Supremum *}
+text \<open>Supremum\<close>
declare (in partial_order) weak_sup_of_singleton [simp del]
@@ -1164,7 +1164,7 @@
using weak_join_assoc L unfolding eq_is_equal .
-text {* Infimum *}
+text \<open>Infimum\<close>
declare (in partial_order) weak_inf_of_singleton [simp del]
@@ -1172,7 +1172,7 @@
"x \<in> carrier L ==> \<Sqinter>{x} = x"
using weak_inf_of_singleton unfolding eq_is_equal .
-text {* Condition on @{text A}: infimum exists. *}
+text \<open>Condition on @{text A}: infimum exists.\<close>
lemma (in lower_semilattice) meet_assoc_lemma:
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
@@ -1185,7 +1185,7 @@
using weak_meet_assoc L unfolding eq_is_equal .
-text {* Total Orders *}
+text \<open>Total Orders\<close>
locale total_order = partial_order +
assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
@@ -1193,20 +1193,20 @@
sublocale total_order < weak: weak_total_order
by standard (rule total_order_total)
-text {* Introduction rule: the usual definition of total order *}
+text \<open>Introduction rule: the usual definition of total order\<close>
lemma (in partial_order) total_orderI:
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
shows "total_order L"
by standard (rule total)
-text {* Total orders are lattices. *}
+text \<open>Total orders are lattices.\<close>
sublocale total_order < weak: lattice
by standard (auto intro: sup_of_two_exists inf_of_two_exists)
-text {* Complete lattices *}
+text \<open>Complete lattices\<close>
locale complete_lattice = lattice +
assumes sup_exists:
@@ -1217,7 +1217,7 @@
sublocale complete_lattice < weak: weak_complete_lattice
by standard (auto intro: sup_exists inf_exists)
-text {* Introduction rule: the usual definition of complete lattice *}
+text \<open>Introduction rule: the usual definition of complete lattice\<close>
lemma (in partial_order) complete_latticeI:
assumes sup_exists:
@@ -1273,9 +1273,9 @@
(* TODO: prove dual version *)
-subsection {* Examples *}
+subsection \<open>Examples\<close>
-subsubsection {* The Powerset of a Set is a Complete Lattice *}
+subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
theorem powerset_is_complete_lattice:
"complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
@@ -1293,13 +1293,13 @@
fix B
assume "B \<subseteq> carrier ?L"
then have "greatest ?L (\<Inter>B \<inter> A) (Lower ?L B)"
- txt {* @{term "\<Inter>B"} is not the infimum of @{term B}:
- @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}! *}
+ txt \<open>@{term "\<Inter>B"} is not the infimum of @{term B}:
+ @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}!\<close>
by (fastforce intro!: greatest_LowerI simp: Lower_def)
then show "EX i. greatest ?L i (Lower ?L B)" ..
qed
-text {* An other example, that of the lattice of subgroups of a group,
- can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
+text \<open>An other example, that of the lattice of subgroups of a group,
+ can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
end