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