haftmann@30661: (* Author: Amine Chaieb, University of Cambridge *)
chaieb@29838: 
haftmann@30661: header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
chaieb@29838: 
chaieb@29838: theory Glbs
chaieb@29838: imports Lubs
chaieb@29838: begin
chaieb@29838: 
wenzelm@46509: definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
wenzelm@46509:   where "greatestP P x = (P x \<and> Collect P *<=  x)"
chaieb@29838: 
wenzelm@46509: definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
wenzelm@46509:   where "isLb R S x = (x <=* S \<and> x: R)"
chaieb@29838: 
wenzelm@46509: definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
wenzelm@46509:   where "isGlb R S x = greatestP (isLb R S) x"
chaieb@29838: 
wenzelm@46509: definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
wenzelm@46509:   where "lbs R S = Collect (isLb R S)"
wenzelm@46509: 
chaieb@29838: 
wenzelm@46509: subsection {* Rules about the Operators @{term greatestP}, @{term isLb}
wenzelm@46509:   and @{term isGlb} *}
chaieb@29838: 
wenzelm@46509: lemma leastPD1: "greatestP P x \<Longrightarrow> P x"
wenzelm@46509:   by (simp add: greatestP_def)
chaieb@29838: 
wenzelm@46509: lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
wenzelm@46509:   by (simp add: greatestP_def)
chaieb@29838: 
wenzelm@46509: lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
wenzelm@46509:   by (blast dest!: greatestPD2 setleD)
chaieb@29838: 
wenzelm@46509: lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
wenzelm@46509:   by (simp add: isGlb_def isLb_def greatestP_def)
chaieb@29838: 
wenzelm@46509: lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
wenzelm@46509:   by (simp add: isGlb_def isLb_def greatestP_def)
chaieb@29838: 
wenzelm@46509: lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
wenzelm@46509:   unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
chaieb@29838: 
wenzelm@46509: lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
wenzelm@46509:   by (blast dest!: isGlbD1 setgeD)
chaieb@29838: 
wenzelm@46509: lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
wenzelm@46509:   by (simp add: isGlb_def)
chaieb@29838: 
wenzelm@46509: lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
wenzelm@46509:   by (simp add: isGlb_def)
chaieb@29838: 
wenzelm@46509: lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
wenzelm@46509:   by (simp add: isGlb_def greatestP_def)
chaieb@29838: 
wenzelm@46509: lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
wenzelm@46509:   by (simp add: isLb_def setge_def)
chaieb@29838: 
wenzelm@46509: lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
wenzelm@46509:   by (simp add: isLb_def)
chaieb@29838: 
wenzelm@46509: lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
wenzelm@46509:   by (simp add: isLb_def)
chaieb@29838: 
wenzelm@46509: lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
wenzelm@46509:   by (simp add: isLb_def)
chaieb@29838: 
wenzelm@46509: lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
wenzelm@46509:   unfolding isGlb_def by (blast intro!: greatestPD3)
chaieb@29838: 
wenzelm@46509: lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
wenzelm@46509:   unfolding lbs_def isGlb_def by (rule greatestPD2)
chaieb@29838: 
chaieb@29838: end