src/HOL/Algebra/Lattice.thy

 
 theory Lattice
 imports Congruence
 begin
 
-section {* Orders and Lattices *}
-
-subsection {* Partial Orders *}
+section \<open>Orders and Lattices\<close>
+
+subsection \<open>Partial Orders\<close>
 
 record 'a gorder = "'a eq_object" +
   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
 
 locale weak_partial_order = equivalence L for L (structure) +

 definition
   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
   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
 
 lemma le_cong_l [intro, trans]:

     and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
   shows "a \<sqsubset> c"
   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"
   where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
 

   also note aa'[symmetric]
   finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
 qed
 
 
-subsubsection {* Least and greatest, as predicate *}
+subsubsection \<open>Least and greatest, as predicate\<close>
 
 definition
   least :: "[_, 'a, 'a set] => bool"
   where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
 
 definition
   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"
   by (unfold least_def) fast
 

 
 lemma (in weak_partial_order) least_cong:
   "[| 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'"
     and "x \<in> carrier L" "x' \<in> carrier L"
     and "A \<subseteq> carrier L"

 lemma (in weak_partial_order) greatest_cong:
   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
   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'"
     and "x \<in> carrier L" "x' \<in> carrier L"
     and "A \<subseteq> carrier L" (* unneccessary with current Lower *)

 lemma greatest_Lower_below:
   fixes L (structure)
   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)
   where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
 

 definition
   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   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:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 

     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
 
 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 |]
   ==> P (x \<squnion> y)"
 proof (unfold join_def sup_def)

 lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
   "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
   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;
   least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   ==> P (\<Squnion>(insert x A))"

 
 lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
   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"
   proof (rule weak_le_antisym)
     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"

     by (erule_tac least_le)
       (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
   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)
   shows "x \<squnion> y = y \<squnion> x"
   by (unfold join_def) (simp add: insert_commute)

   also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
   finally show ?thesis by (simp add: L)
 qed
 
 
-subsubsection {* Infimum *}
+subsubsection \<open>Infimum\<close>
 
 lemma (in weak_lower_semilattice) meetI:
   "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
   x \<in> carrier L; y \<in> carrier L |]
   ==> P (x \<sqinter> y)"

 lemma (in weak_partial_order) inf_of_singleton_closed:
   "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
   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;
   greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
   ==> P (\<Sqinter>(insert x A))"

 
 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
   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"
   proof (rule weak_le_antisym)
     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"

   also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
   finally show ?thesis by (simp add: L)
 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
   fix x y
   assume L: "x \<in> carrier L"  "y \<in> carrier L"

     ultimately show ?thesis by blast
   qed
 qed
 
 
-subsection {* Complete Lattices *}
+subsection \<open>Complete Lattices\<close>
 
 locale weak_complete_lattice = weak_lattice +
   assumes sup_exists:
     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
     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:
     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
     and inf_exists:

 
 lemma (in weak_complete_lattice) bottom_closed [simp, intro]:
   "\<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"
   by (unfold Lower_def) simp
 

 qed
 
 (* 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 ="
 begin
 

   using assms unfolding lless_eq by auto
 
 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"
   using weak_least_unique unfolding eq_is_equal .
 
 lemma (in partial_order) greatest_unique:
   "[| greatest L x A; greatest L y A |] ==> x = y"
   using weak_greatest_unique unfolding eq_is_equal .
 
 
-text {* Lattices *}
+text \<open>Lattices\<close>
 
 locale upper_semilattice = partial_order +
   assumes sup_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 

   by standard (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
 
 
-text {* Supremum *}
+text \<open>Supremum\<close>
 
 declare (in partial_order) weak_sup_of_singleton [simp del]
 
 lemma (in partial_order) sup_of_singleton [simp]:
   "x \<in> carrier L ==> \<Squnion>{x} = x"

   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   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]
 
 lemma (in partial_order) inf_of_singleton [simp]:
   "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"
   shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
   using weak_meet_assoc_lemma L unfolding eq_is_equal .

   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   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"
 
 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:
     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
     and inf_exists:
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
 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:
     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
     and inf_exists:

 qed
 
 (* TODO: prove dual version *)
 
 
-subsection {* Examples *}
-
-subsubsection {* The Powerset of a Set is a Complete Lattice *}
+subsection \<open>Examples\<close>
+
+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>"
   (is "complete_lattice ?L")
 proof (rule partial_order.complete_latticeI)

   then show "EX s. least ?L s (Upper ?L B)" ..
 next
   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