1.1 --- a/src/HOL/Library/Glbs.thy	Thu Dec 05 17:52:12 2013 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,79 +0,0 @@
     1.4 -(* Author: Amine Chaieb, University of Cambridge *)
     1.5 -
     1.6 -header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
     1.7 -
     1.8 -theory Glbs
     1.9 -imports Lubs
    1.10 -begin
    1.11 -
    1.12 -definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
    1.13 -  where "greatestP P x = (P x \<and> Collect P *<=  x)"
    1.14 -
    1.15 -definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
    1.16 -  where "isLb R S x = (x <=* S \<and> x: R)"
    1.17 -
    1.18 -definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
    1.19 -  where "isGlb R S x = greatestP (isLb R S) x"
    1.20 -
    1.21 -definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
    1.22 -  where "lbs R S = Collect (isLb R S)"
    1.23 -
    1.24 -
    1.25 -subsection {* Rules about the Operators @{term greatestP}, @{term isLb}
    1.26 -  and @{term isGlb} *}
    1.27 -
    1.28 -lemma leastPD1: "greatestP P x \<Longrightarrow> P x"
    1.29 -  by (simp add: greatestP_def)
    1.30 -
    1.31 -lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
    1.32 -  by (simp add: greatestP_def)
    1.33 -
    1.34 -lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
    1.35 -  by (blast dest!: greatestPD2 setleD)
    1.36 -
    1.37 -lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
    1.38 -  by (simp add: isGlb_def isLb_def greatestP_def)
    1.39 -
    1.40 -lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
    1.41 -  by (simp add: isGlb_def isLb_def greatestP_def)
    1.42 -
    1.43 -lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
    1.44 -  unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
    1.45 -
    1.46 -lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
    1.47 -  by (blast dest!: isGlbD1 setgeD)
    1.48 -
    1.49 -lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
    1.50 -  by (simp add: isGlb_def)
    1.51 -
    1.52 -lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
    1.53 -  by (simp add: isGlb_def)
    1.54 -
    1.55 -lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
    1.56 -  by (simp add: isGlb_def greatestP_def)
    1.57 -
    1.58 -lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
    1.59 -  by (simp add: isLb_def setge_def)
    1.60 -
    1.61 -lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
    1.62 -  by (simp add: isLb_def)
    1.63 -
    1.64 -lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
    1.65 -  by (simp add: isLb_def)
    1.66 -
    1.67 -lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
    1.68 -  by (simp add: isLb_def)
    1.69 -
    1.70 -lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
    1.71 -  unfolding isGlb_def by (blast intro!: greatestPD3)
    1.72 -
    1.73 -lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
    1.74 -  unfolding lbs_def isGlb_def by (rule greatestPD2)
    1.75 -
    1.76 -lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
    1.77 -  apply (frule isGlb_isLb)
    1.78 -  apply (frule_tac x = y in isGlb_isLb)
    1.79 -  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
    1.80 -  done
    1.81 -
    1.82 -end