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