src/HOL/Lattices.thy

 (*  Title:      HOL/Lattices.thy
     Author:     Tobias Nipkow
 *)
 
-section {* Abstract lattices *}
+section \<open>Abstract lattices\<close>
 
 theory Lattices
 imports Groups
 begin
 
-subsection {* Abstract semilattice *}
-
-text {*
+subsection \<open>Abstract semilattice\<close>
+
+text \<open>
   These locales provide a basic structure for interpretation into
   bigger structures;  extensions require careful thinking, otherwise
   undesired effects may occur due to interpretation.
-*}
+\<close>
 
 no_notation times (infixl "*" 70)
 no_notation Groups.one ("1")
 
 locale semilattice = abel_semigroup +

     by (simp_all add: order_iff commute)
   then have "a = a * (b * c)"
     by simp
   then have "a = (a * b) * c"
     by (simp add: assoc)
-  with `a = a * b` [symmetric] have "a = a * c" by simp
+  with \<open>a = a * b\<close> [symmetric] have "a = a * c" by simp
   then show "a \<preceq> c" by (rule orderI)
 qed
 
 lemma cobounded1 [simp]:
   "a * b \<preceq> a"

 
 notation times (infixl "*" 70)
 notation Groups.one ("1")
 
 
-subsection {* Syntactic infimum and supremum operations *}
+subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class inf =
   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
 
 class sup = 
   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
 
 
-subsection {* Concrete lattices *}
+subsection \<open>Concrete lattices\<close>
 
 notation
   less_eq  (infix "\<sqsubseteq>" 50) and
   less  (infix "\<sqsubset>" 50)
 

   assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
   and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
 begin
 
-text {* Dual lattice *}
+text \<open>Dual lattice\<close>
 
 lemma dual_semilattice:
   "class.semilattice_inf sup greater_eq greater"
 by (rule class.semilattice_inf.intro, rule dual_order)
   (unfold_locales, simp_all add: sup_least)

 end
 
 class lattice = semilattice_inf + semilattice_sup
 
 
-subsubsection {* Intro and elim rules*}
+subsubsection \<open>Intro and elim rules\<close>
 
 context semilattice_inf
 begin
 
 lemma le_infI1:

   by (auto simp add: mono_def intro: Lattices.sup_least)
 
 end
 
 
-subsubsection {* Equational laws *}
+subsubsection \<open>Equational laws\<close>
 
 context semilattice_inf
 begin
 
 sublocale inf!: semilattice inf

 
 lemmas inf_sup_aci = inf_aci sup_aci
 
 lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
 
-text{* Towards distributivity *}
+text\<open>Towards distributivity\<close>
 
 lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
 lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
-text{* If you have one of them, you have them all. *}
+text\<open>If you have one of them, you have them all.\<close>
 
 lemma distrib_imp1:
 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
 proof-

   finally show ?thesis .
 qed
 
 end
 
-subsubsection {* Strict order *}
+subsubsection \<open>Strict order\<close>
 
 context semilattice_inf
 begin
 
 lemma less_infI1:

   by (rule semilattice_inf.less_infI2)
 
 end
 
 
-subsection {* Distributive lattices *}
+subsection \<open>Distributive lattices\<close>
 
 class distrib_lattice = lattice +
   assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
 
 context distrib_lattice

   sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
 
 end
 
 
-subsection {* Bounded lattices and boolean algebras *}
+subsection \<open>Bounded lattices and boolean algebras\<close>
 
 class bounded_semilattice_inf_top = semilattice_inf + order_top
 begin
 
 sublocale inf_top!: semilattice_neutr inf top

 qed
 
 end
 
 
-subsection {* @{text "min/max"} as special case of lattice *}
+subsection \<open>@{text "min/max"} as special case of lattice\<close>
 
 context linorder
 begin
 
 sublocale min!: semilattice_order min less_eq less

 
 lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   by (auto intro: antisym simp add: max_def fun_eq_iff)
 
 
-subsection {* Uniqueness of inf and sup *}
+subsection \<open>Uniqueness of inf and sup\<close>
 
 lemma (in semilattice_inf) inf_unique:
   fixes f (infixl "\<triangle>" 70)
   assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"

   have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
   show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
 qed
 
 
-subsection {* Lattice on @{typ bool} *}
+subsection \<open>Lattice on @{typ bool}\<close>
 
 instantiation bool :: boolean_algebra
 begin
 
 definition

 lemma sup_boolE:
   "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   by auto
 
 
-subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
+subsection \<open>Lattice on @{typ "_ \<Rightarrow> _"}\<close>
 
 instantiation "fun" :: (type, semilattice_sup) semilattice_sup
 begin
 
 definition

 
 instance "fun" :: (type, boolean_algebra) boolean_algebra proof
 qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
 
 
-subsection {* Lattice on unary and binary predicates *}
+subsection \<open>Lattice on unary and binary predicates\<close>
 
 lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
   by (simp add: inf_fun_def)
 
 lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"

   by (simp add: sup_fun_def) iprover
 
 lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   by (simp add: sup_fun_def) iprover
 
-text {*
+text \<open>
   \medskip Classical introduction rule: no commitment to @{text A} vs
   @{text B}.
-*}
+\<close>
 
 lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   by (auto simp add: sup_fun_def)
 
 lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"