src/HOL/Library/Glbs.thy
author wenzelm
Thu Feb 16 22:54:40 2012 +0100 (2012-02-16)
changeset 46509 c4b2ec379fdd
parent 30661 54858c8ad226
child 51342 763c6872bd10
permissions -rw-r--r--
more symbols;
misc tuning;
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 \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
wenzelm@46509
    10
  where "greatestP P x = (P x \<and> Collect P *<=  x)"
chaieb@29838
    11
wenzelm@46509
    12
definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
wenzelm@46509
    13
  where "isLb R S x = (x <=* S \<and> x: R)"
chaieb@29838
    14
wenzelm@46509
    15
definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
wenzelm@46509
    16
  where "isGlb R S x = greatestP (isLb R S) x"
chaieb@29838
    17
wenzelm@46509
    18
definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> '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 \<Longrightarrow> P x"
wenzelm@46509
    26
  by (simp add: greatestP_def)
chaieb@29838
    27
wenzelm@46509
    28
lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
wenzelm@46509
    29
  by (simp add: greatestP_def)
chaieb@29838
    30
wenzelm@46509
    31
lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
wenzelm@46509
    32
  by (blast dest!: greatestPD2 setleD)
chaieb@29838
    33
wenzelm@46509
    34
lemma isGlbD1: "isGlb R S x \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
wenzelm@46509
    44
  by (blast dest!: isGlbD1 setgeD)
chaieb@29838
    45
wenzelm@46509
    46
lemma isGlbD3: "isGlb R S x \<Longrightarrow> 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 \<Longrightarrow> isGlb R S x"
wenzelm@46509
    50
  by (simp add: isGlb_def)
chaieb@29838
    51
wenzelm@46509
    52
lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> 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 \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
wenzelm@46509
    56
  by (simp add: isLb_def setge_def)
chaieb@29838
    57
wenzelm@46509
    58
lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
wenzelm@46509
    59
  by (simp add: isLb_def)
chaieb@29838
    60
wenzelm@46509
    61
lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
wenzelm@46509
    62
  by (simp add: isLb_def)
chaieb@29838
    63
wenzelm@46509
    64
lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> 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 \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
wenzelm@46509
    68
  unfolding isGlb_def by (blast intro!: greatestPD3)
chaieb@29838
    69
wenzelm@46509
    70
lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
wenzelm@46509
    71
  unfolding lbs_def isGlb_def by (rule greatestPD2)
chaieb@29838
    72
chaieb@29838
    73
end