src/HOL/Library/Glbs.thy
 author Andreas Lochbihler Fri Sep 20 10:09:16 2013 +0200 (2013-09-20) changeset 53745 788730ab7da4 parent 51342 763c6872bd10 permissions -rw-r--r--
prefer Code.abort over code_abort
 haftmann@30661 ` 1` ```(* Author: Amine Chaieb, University of Cambridge *) ``` chaieb@29838 ` 2` haftmann@30661 ` 3` ```header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *} ``` chaieb@29838 ` 4` chaieb@29838 ` 5` ```theory Glbs ``` chaieb@29838 ` 6` ```imports Lubs ``` chaieb@29838 ` 7` ```begin ``` chaieb@29838 ` 8` wenzelm@46509 ` 9` ```definition greatestP :: "('a \ bool) \ 'a::ord \ bool" ``` wenzelm@46509 ` 10` ``` where "greatestP P x = (P x \ Collect P *<= x)" ``` chaieb@29838 ` 11` wenzelm@46509 ` 12` ```definition isLb :: "'a set \ 'a set \ 'a::ord \ bool" ``` wenzelm@46509 ` 13` ``` where "isLb R S x = (x <=* S \ x: R)" ``` chaieb@29838 ` 14` wenzelm@46509 ` 15` ```definition isGlb :: "'a set \ 'a set \ 'a::ord \ bool" ``` wenzelm@46509 ` 16` ``` where "isGlb R S x = greatestP (isLb R S) x" ``` chaieb@29838 ` 17` wenzelm@46509 ` 18` ```definition lbs :: "'a set \ 'a::ord set \ 'a set" ``` wenzelm@46509 ` 19` ``` where "lbs R S = Collect (isLb R S)" ``` wenzelm@46509 ` 20` chaieb@29838 ` 21` wenzelm@46509 ` 22` ```subsection {* Rules about the Operators @{term greatestP}, @{term isLb} ``` wenzelm@46509 ` 23` ``` and @{term isGlb} *} ``` chaieb@29838 ` 24` wenzelm@46509 ` 25` ```lemma leastPD1: "greatestP P x \ P x" ``` wenzelm@46509 ` 26` ``` by (simp add: greatestP_def) ``` chaieb@29838 ` 27` wenzelm@46509 ` 28` ```lemma greatestPD2: "greatestP P x \ Collect P *<= x" ``` wenzelm@46509 ` 29` ``` by (simp add: greatestP_def) ``` chaieb@29838 ` 30` wenzelm@46509 ` 31` ```lemma greatestPD3: "greatestP P x \ y: Collect P \ x \ y" ``` wenzelm@46509 ` 32` ``` by (blast dest!: greatestPD2 setleD) ``` chaieb@29838 ` 33` wenzelm@46509 ` 34` ```lemma isGlbD1: "isGlb R S x \ x <=* S" ``` wenzelm@46509 ` 35` ``` by (simp add: isGlb_def isLb_def greatestP_def) ``` chaieb@29838 ` 36` wenzelm@46509 ` 37` ```lemma isGlbD1a: "isGlb R S x \ x: R" ``` wenzelm@46509 ` 38` ``` by (simp add: isGlb_def isLb_def greatestP_def) ``` chaieb@29838 ` 39` wenzelm@46509 ` 40` ```lemma isGlb_isLb: "isGlb R S x \ isLb R S x" ``` wenzelm@46509 ` 41` ``` unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a) ``` chaieb@29838 ` 42` wenzelm@46509 ` 43` ```lemma isGlbD2: "isGlb R S x \ y : S \ y \ x" ``` wenzelm@46509 ` 44` ``` by (blast dest!: isGlbD1 setgeD) ``` chaieb@29838 ` 45` wenzelm@46509 ` 46` ```lemma isGlbD3: "isGlb R S x \ greatestP (isLb R S) x" ``` wenzelm@46509 ` 47` ``` by (simp add: isGlb_def) ``` chaieb@29838 ` 48` wenzelm@46509 ` 49` ```lemma isGlbI1: "greatestP (isLb R S) x \ isGlb R S x" ``` wenzelm@46509 ` 50` ``` by (simp add: isGlb_def) ``` chaieb@29838 ` 51` wenzelm@46509 ` 52` ```lemma isGlbI2: "isLb R S x \ Collect (isLb R S) *<= x \ isGlb R S x" ``` wenzelm@46509 ` 53` ``` by (simp add: isGlb_def greatestP_def) ``` chaieb@29838 ` 54` wenzelm@46509 ` 55` ```lemma isLbD: "isLb R S x \ y : S \ y \ x" ``` wenzelm@46509 ` 56` ``` by (simp add: isLb_def setge_def) ``` chaieb@29838 ` 57` wenzelm@46509 ` 58` ```lemma isLbD2: "isLb R S x \ x <=* S " ``` wenzelm@46509 ` 59` ``` by (simp add: isLb_def) ``` chaieb@29838 ` 60` wenzelm@46509 ` 61` ```lemma isLbD2a: "isLb R S x \ x: R" ``` wenzelm@46509 ` 62` ``` by (simp add: isLb_def) ``` chaieb@29838 ` 63` wenzelm@46509 ` 64` ```lemma isLbI: "x <=* S \ x: R \ isLb R S x" ``` wenzelm@46509 ` 65` ``` by (simp add: isLb_def) ``` chaieb@29838 ` 66` wenzelm@46509 ` 67` ```lemma isGlb_le_isLb: "isGlb R S x \ isLb R S y \ x \ y" ``` wenzelm@46509 ` 68` ``` unfolding isGlb_def by (blast intro!: greatestPD3) ``` chaieb@29838 ` 69` wenzelm@46509 ` 70` ```lemma isGlb_ubs: "isGlb R S x \ lbs R S *<= x" ``` wenzelm@46509 ` 71` ``` unfolding lbs_def isGlb_def by (rule greatestPD2) ``` chaieb@29838 ` 72` hoelzl@51342 ` 73` ```lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)" ``` hoelzl@51342 ` 74` ``` apply (frule isGlb_isLb) ``` hoelzl@51342 ` 75` ``` apply (frule_tac x = y in isGlb_isLb) ``` hoelzl@51342 ` 76` ``` apply (blast intro!: order_antisym dest!: isGlb_le_isLb) ``` hoelzl@51342 ` 77` ``` done ``` hoelzl@51342 ` 78` chaieb@29838 ` 79` ```end ```