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: chaieb@29838: definition chaieb@29838: greatestP :: "['a =>bool,'a::ord] => bool" where chaieb@29838: "greatestP P x = (P x & Collect P *<= x)" chaieb@29838: chaieb@29838: definition chaieb@29838: isLb :: "['a set, 'a set, 'a::ord] => bool" where chaieb@29838: "isLb R S x = (x <=* S & x: R)" chaieb@29838: chaieb@29838: definition chaieb@29838: isGlb :: "['a set, 'a set, 'a::ord] => bool" where chaieb@29838: "isGlb R S x = greatestP (isLb R S) x" chaieb@29838: chaieb@29838: definition chaieb@29838: lbs :: "['a set, 'a::ord set] => 'a set" where chaieb@29838: "lbs R S = Collect (isLb R S)" chaieb@29838: chaieb@29838: subsection{*Rules about the Operators @{term greatestP}, @{term isLb} chaieb@29838: and @{term isGlb}*} chaieb@29838: chaieb@29838: lemma leastPD1: "greatestP P x ==> P x" chaieb@29838: by (simp add: greatestP_def) chaieb@29838: chaieb@29838: lemma greatestPD2: "greatestP P x ==> Collect P *<= x" chaieb@29838: by (simp add: greatestP_def) chaieb@29838: chaieb@29838: lemma greatestPD3: "[| greatestP P x; y: Collect P |] ==> x >= y" chaieb@29838: by (blast dest!: greatestPD2 setleD) chaieb@29838: chaieb@29838: lemma isGlbD1: "isGlb R S x ==> x <=* S" chaieb@29838: by (simp add: isGlb_def isLb_def greatestP_def) chaieb@29838: chaieb@29838: lemma isGlbD1a: "isGlb R S x ==> x: R" chaieb@29838: by (simp add: isGlb_def isLb_def greatestP_def) chaieb@29838: chaieb@29838: lemma isGlb_isLb: "isGlb R S x ==> isLb R S x" chaieb@29838: apply (simp add: isLb_def) chaieb@29838: apply (blast dest: isGlbD1 isGlbD1a) chaieb@29838: done chaieb@29838: chaieb@29838: lemma isGlbD2: "[| isGlb R S x; y : S |] ==> y >= x" chaieb@29838: by (blast dest!: isGlbD1 setgeD) chaieb@29838: chaieb@29838: lemma isGlbD3: "isGlb R S x ==> greatestP(isLb R S) x" chaieb@29838: by (simp add: isGlb_def) chaieb@29838: chaieb@29838: lemma isGlbI1: "greatestP(isLb R S) x ==> isGlb R S x" chaieb@29838: by (simp add: isGlb_def) chaieb@29838: chaieb@29838: lemma isGlbI2: "[| isLb R S x; Collect (isLb R S) *<= x |] ==> isGlb R S x" chaieb@29838: by (simp add: isGlb_def greatestP_def) chaieb@29838: chaieb@29838: lemma isLbD: "[| isLb R S x; y : S |] ==> y >= x" chaieb@29838: by (simp add: isLb_def setge_def) chaieb@29838: chaieb@29838: lemma isLbD2: "isLb R S x ==> x <=* S " chaieb@29838: by (simp add: isLb_def) chaieb@29838: chaieb@29838: lemma isLbD2a: "isLb R S x ==> x: R" chaieb@29838: by (simp add: isLb_def) chaieb@29838: chaieb@29838: lemma isLbI: "[| x <=* S ; x: R |] ==> isLb R S x" chaieb@29838: by (simp add: isLb_def) chaieb@29838: chaieb@29838: lemma isGlb_le_isLb: "[| isGlb R S x; isLb R S y |] ==> x >= y" chaieb@29838: apply (simp add: isGlb_def) chaieb@29838: apply (blast intro!: greatestPD3) chaieb@29838: done chaieb@29838: chaieb@29838: lemma isGlb_ubs: "isGlb R S x ==> lbs R S *<= x" chaieb@29838: apply (simp add: lbs_def isGlb_def) chaieb@29838: apply (erule greatestPD2) chaieb@29838: done chaieb@29838: chaieb@29838: end