src/HOL/Library/Glbs.thy
 author wenzelm Wed Mar 04 23:52:47 2009 +0100 (2009-03-04) changeset 30267 171b3bd93c90 parent 29838 a562ca0c408d child 30661 54858c8ad226 permissions -rw-r--r--
removed old/broken CVS Ids;
 chaieb@29838 ` 1` ```(* Title: Glbs ``` chaieb@29838 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` chaieb@29838 ` 3` ```*) ``` chaieb@29838 ` 4` chaieb@29838 ` 5` ```header{*Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs*} ``` chaieb@29838 ` 6` chaieb@29838 ` 7` ```theory Glbs ``` chaieb@29838 ` 8` ```imports Lubs ``` chaieb@29838 ` 9` ```begin ``` chaieb@29838 ` 10` chaieb@29838 ` 11` ```definition ``` chaieb@29838 ` 12` ``` greatestP :: "['a =>bool,'a::ord] => bool" where ``` chaieb@29838 ` 13` ``` "greatestP P x = (P x & Collect P *<= x)" ``` chaieb@29838 ` 14` chaieb@29838 ` 15` ```definition ``` chaieb@29838 ` 16` ``` isLb :: "['a set, 'a set, 'a::ord] => bool" where ``` chaieb@29838 ` 17` ``` "isLb R S x = (x <=* S & x: R)" ``` chaieb@29838 ` 18` chaieb@29838 ` 19` ```definition ``` chaieb@29838 ` 20` ``` isGlb :: "['a set, 'a set, 'a::ord] => bool" where ``` chaieb@29838 ` 21` ``` "isGlb R S x = greatestP (isLb R S) x" ``` chaieb@29838 ` 22` chaieb@29838 ` 23` ```definition ``` chaieb@29838 ` 24` ``` lbs :: "['a set, 'a::ord set] => 'a set" where ``` chaieb@29838 ` 25` ``` "lbs R S = Collect (isLb R S)" ``` chaieb@29838 ` 26` chaieb@29838 ` 27` ```subsection{*Rules about the Operators @{term greatestP}, @{term isLb} ``` chaieb@29838 ` 28` ``` and @{term isGlb}*} ``` chaieb@29838 ` 29` chaieb@29838 ` 30` ```lemma leastPD1: "greatestP P x ==> P x" ``` chaieb@29838 ` 31` ```by (simp add: greatestP_def) ``` chaieb@29838 ` 32` chaieb@29838 ` 33` ```lemma greatestPD2: "greatestP P x ==> Collect P *<= x" ``` chaieb@29838 ` 34` ```by (simp add: greatestP_def) ``` chaieb@29838 ` 35` chaieb@29838 ` 36` ```lemma greatestPD3: "[| greatestP P x; y: Collect P |] ==> x >= y" ``` chaieb@29838 ` 37` ```by (blast dest!: greatestPD2 setleD) ``` chaieb@29838 ` 38` chaieb@29838 ` 39` ```lemma isGlbD1: "isGlb R S x ==> x <=* S" ``` chaieb@29838 ` 40` ```by (simp add: isGlb_def isLb_def greatestP_def) ``` chaieb@29838 ` 41` chaieb@29838 ` 42` ```lemma isGlbD1a: "isGlb R S x ==> x: R" ``` chaieb@29838 ` 43` ```by (simp add: isGlb_def isLb_def greatestP_def) ``` chaieb@29838 ` 44` chaieb@29838 ` 45` ```lemma isGlb_isLb: "isGlb R S x ==> isLb R S x" ``` chaieb@29838 ` 46` ```apply (simp add: isLb_def) ``` chaieb@29838 ` 47` ```apply (blast dest: isGlbD1 isGlbD1a) ``` chaieb@29838 ` 48` ```done ``` chaieb@29838 ` 49` chaieb@29838 ` 50` ```lemma isGlbD2: "[| isGlb R S x; y : S |] ==> y >= x" ``` chaieb@29838 ` 51` ```by (blast dest!: isGlbD1 setgeD) ``` chaieb@29838 ` 52` chaieb@29838 ` 53` ```lemma isGlbD3: "isGlb R S x ==> greatestP(isLb R S) x" ``` chaieb@29838 ` 54` ```by (simp add: isGlb_def) ``` chaieb@29838 ` 55` chaieb@29838 ` 56` ```lemma isGlbI1: "greatestP(isLb R S) x ==> isGlb R S x" ``` chaieb@29838 ` 57` ```by (simp add: isGlb_def) ``` chaieb@29838 ` 58` chaieb@29838 ` 59` ```lemma isGlbI2: "[| isLb R S x; Collect (isLb R S) *<= x |] ==> isGlb R S x" ``` chaieb@29838 ` 60` ```by (simp add: isGlb_def greatestP_def) ``` chaieb@29838 ` 61` chaieb@29838 ` 62` ```lemma isLbD: "[| isLb R S x; y : S |] ==> y >= x" ``` chaieb@29838 ` 63` ```by (simp add: isLb_def setge_def) ``` chaieb@29838 ` 64` chaieb@29838 ` 65` ```lemma isLbD2: "isLb R S x ==> x <=* S " ``` chaieb@29838 ` 66` ```by (simp add: isLb_def) ``` chaieb@29838 ` 67` chaieb@29838 ` 68` ```lemma isLbD2a: "isLb R S x ==> x: R" ``` chaieb@29838 ` 69` ```by (simp add: isLb_def) ``` chaieb@29838 ` 70` chaieb@29838 ` 71` ```lemma isLbI: "[| x <=* S ; x: R |] ==> isLb R S x" ``` chaieb@29838 ` 72` ```by (simp add: isLb_def) ``` chaieb@29838 ` 73` chaieb@29838 ` 74` ```lemma isGlb_le_isLb: "[| isGlb R S x; isLb R S y |] ==> x >= y" ``` chaieb@29838 ` 75` ```apply (simp add: isGlb_def) ``` chaieb@29838 ` 76` ```apply (blast intro!: greatestPD3) ``` chaieb@29838 ` 77` ```done ``` chaieb@29838 ` 78` chaieb@29838 ` 79` ```lemma isGlb_ubs: "isGlb R S x ==> lbs R S *<= x" ``` chaieb@29838 ` 80` ```apply (simp add: lbs_def isGlb_def) ``` chaieb@29838 ` 81` ```apply (erule greatestPD2) ``` chaieb@29838 ` 82` ```done ``` chaieb@29838 ` 83` chaieb@29838 ` 84` ```end ```