src/HOL/Lattices.thy
 changeset 22737 d87ccbcc2702 parent 22548 6ce4bddf3bcb child 22916 8caf6da610e2
```     1.1 --- a/src/HOL/Lattices.thy	Fri Apr 20 11:21:34 2007 +0200
1.2 +++ b/src/HOL/Lattices.thy	Fri Apr 20 11:21:35 2007 +0200
1.3 @@ -13,18 +13,20 @@
1.4
1.5  text{*
1.6    This theory of lattices only defines binary sup and inf
1.7 -  operations. The extension to (finite) sets is done in theories @{text FixedPoint}
1.8 -  and @{text Finite_Set}.
1.9 +  operations. The extension to (finite) sets is done in theories
1.10 +  @{text FixedPoint} and @{text Finite_Set}.
1.11  *}
1.12
1.13  class lower_semilattice = order +
1.14    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
1.15 -  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
1.16 +  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
1.17 +  and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
1.18    and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
1.19
1.20  class upper_semilattice = order +
1.21    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
1.22 -  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
1.23 +  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
1.24 +  and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
1.25    and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
1.26
1.27  class lattice = lower_semilattice + upper_semilattice
1.28 @@ -251,28 +253,28 @@
1.29
1.30  subsection {* Uniqueness of inf and sup *}
1.31
1.32 -lemma inf_unique:
1.33 +lemma (in lower_semilattice) inf_unique:
1.34    fixes f (infixl "\<triangle>" 70)
1.35 -  assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
1.36 -  and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
1.37 -  shows "inf x y = f x y"
1.38 +  assumes le1: "\<And>x y. x \<triangle> y \<^loc>\<le> x" and le2: "\<And>x y. x \<triangle> y \<^loc>\<le> y"
1.39 +  and greatest: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z"
1.40 +  shows "x \<sqinter> y = x \<triangle> y"
1.41  proof (rule antisym)
1.42 -  show "x \<triangle> y \<le> inf x y" by (rule le_infI) (rule le1 le2)
1.43 +  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1 le2)
1.44  next
1.45 -  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
1.46 -  show "inf x y \<le> x \<triangle> y" by (rule leI) simp_all
1.47 +  have leI: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z" by (blast intro: greatest)
1.48 +  show "x \<sqinter> y \<^loc>\<le> x \<triangle> y" by (rule leI) simp_all
1.49  qed
1.50
1.51 -lemma sup_unique:
1.52 +lemma (in upper_semilattice) sup_unique:
1.53    fixes f (infixl "\<nabla>" 70)
1.54 -  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
1.55 -  and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
1.56 -  shows "sup x y = f x y"
1.57 +  assumes ge1 [simp]: "\<And>x y. x \<^loc>\<le> x \<nabla> y" and ge2: "\<And>x y. y \<^loc>\<le> x \<nabla> y"
1.58 +  and least: "\<And>x y z. y \<^loc>\<le> x \<Longrightarrow> z \<^loc>\<le> x \<Longrightarrow> y \<nabla> z \<^loc>\<le> x"
1.59 +  shows "x \<squnion> y = x \<nabla> y"
1.60  proof (rule antisym)
1.61 -  show "sup x y \<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
1.62 +  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
1.63  next
1.64 -  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
1.65 -  show "x \<nabla> y \<le> sup x y" by (rule leI) simp_all
1.66 +  have leI: "\<And>x y z. x \<^loc>\<le> z \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<nabla> y \<^loc>\<le> z" by (blast intro: least)
1.67 +  show "x \<nabla> y \<^loc>\<le> x \<squnion> y" by (rule leI) simp_all
1.68  qed
1.69
1.70
```