# Theory Lubs

Up to index of Isabelle/HOL/HOL-Complex

theory Lubs
imports Main
begin

    (*  Title       : Lubs.thy
        ID          : $Id: Lubs.thy,v 1.8 2004/08/18 09:10:05 nipkow Exp $
        Author      : Jacques D. Fleuriot
        Copyright   : 1998  University of Cambridge
    *)

    header{*Definitions of Upper Bounds and Least Upper Bounds*}

    theory Lubs
    imports Main
    begin

    text{*Thanks to suggestions by James Margetson*}

    constdefs

      setle :: "['a set, 'a::ord] => bool"     (infixl "*<=" 70)
        "S *<= x    == (ALL y: S. y <= x)"

      setge :: "['a::ord, 'a set] => bool"     (infixl "<=*" 70)
        "x <=* S    == (ALL y: S. x <= y)"

      leastP      :: "['a =>bool,'a::ord] => bool"
        "leastP P x == (P x & x <=* Collect P)"

      isUb        :: "['a set, 'a set, 'a::ord] => bool"
        "isUb R S x   == S *<= x & x: R"

      isLub       :: "['a set, 'a set, 'a::ord] => bool"
        "isLub R S x  == leastP (isUb R S) x"

      ubs         :: "['a set, 'a::ord set] => 'a set"
        "ubs R S      == Collect (isUb R S)"

    subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}

    lemma setleI: "ALL y: S. y <= x ==> S *<= x"
    by (simp add: setle_def)

    lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
    by (simp add: setle_def)

    lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
    by (simp add: setge_def)

    lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
    by (simp add: setge_def)

    subsection{*Rules about the Operators @{term leastP}, @{term ub}
        and @{term lub}*}

    lemma leastPD1: "leastP P x ==> P x"
    by (simp add: leastP_def)

    lemma leastPD2: "leastP P x ==> x <=* Collect P"
    by (simp add: leastP_def)

    lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
    by (blast dest!: leastPD2 setgeD)

    lemma isLubD1: "isLub R S x ==> S *<= x"
    by (simp add: isLub_def isUb_def leastP_def)

    lemma isLubD1a: "isLub R S x ==> x: R"
    by (simp add: isLub_def isUb_def leastP_def)

    lemma isLub_isUb: "isLub R S x ==> isUb R S x"
    apply (simp add: isUb_def)
    apply (blast dest: isLubD1 isLubD1a)
    done

    lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x"
    by (blast dest!: isLubD1 setleD)

    lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
    by (simp add: isLub_def)

    lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
    by (simp add: isLub_def)

    lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"
    by (simp add: isLub_def leastP_def)

    lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x"
    by (simp add: isUb_def setle_def)

    lemma isUbD2: "isUb R S x ==> S *<= x"
    by (simp add: isUb_def)

    lemma isUbD2a: "isUb R S x ==> x: R"
    by (simp add: isUb_def)

    lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x"
    by (simp add: isUb_def)

    lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y"
    apply (simp add: isLub_def)
    apply (blast intro!: leastPD3)
    done

    lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S"
    apply (simp add: ubs_def isLub_def)
    apply (erule leastPD2)
    done

    ML
    {*
    val setle_def = thm "setle_def";
    val setge_def = thm "setge_def";
    val leastP_def = thm "leastP_def";
    val isLub_def = thm "isLub_def";
    val isUb_def = thm "isUb_def";
    val ubs_def = thm "ubs_def";

    val setleI = thm "setleI";
    val setleD = thm "setleD";
    val setgeI = thm "setgeI";
    val setgeD = thm "setgeD";
    val leastPD1 = thm "leastPD1";
    val leastPD2 = thm "leastPD2";
    val leastPD3 = thm "leastPD3";
    val isLubD1 = thm "isLubD1";
    val isLubD1a = thm "isLubD1a";
    val isLub_isUb = thm "isLub_isUb";
    val isLubD2 = thm "isLubD2";
    val isLubD3 = thm "isLubD3";
    val isLubI1 = thm "isLubI1";
    val isLubI2 = thm "isLubI2";
    val isUbD = thm "isUbD";
    val isUbD2 = thm "isUbD2";
    val isUbD2a = thm "isUbD2a";
    val isUbI = thm "isUbI";
    val isLub_le_isUb = thm "isLub_le_isUb";
    val isLub_ubs = thm "isLub_ubs";
    *}

    end

### Rules for the Relations @{text "*<="} and @{text "<=*"}

lemma setleI:

      ∀y∈S. y ≤ x ==> S *<= x

lemma setleD:

      [| S *<= x; y ∈ S |] ==> y ≤ x

lemma setgeI:

      ∀y∈S. x ≤ y ==> x <=* S

lemma setgeD:

      [| x <=* S; y ∈ S |] ==> x ≤ y

### Rules about the Operators @{term leastP}, @{term ub} and @{term lub}

lemma leastPD1:

      leastP P x ==> P x

lemma leastPD2:

      leastP P x ==> x <=* Collect P

lemma leastPD3:

      [| leastP P x; y ∈ Collect P |] ==> x ≤ y

lemma isLubD1:

      isLub R S x ==> S *<= x

lemma isLubD1a:

      isLub R S x ==> x ∈ R

lemma isLub_isUb:

      isLub R S x ==> isUb R S x

lemma isLubD2:

      [| isLub R S x; y ∈ S |] ==> y ≤ x

lemma isLubD3:

      isLub R S x ==> leastP (isUb R S) x

lemma isLubI1:

      leastP (isUb R S) x ==> isLub R S x

lemma isLubI2:

      [| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x

lemma isUbD:

      [| isUb R S x; y ∈ S |] ==> y ≤ x

lemma isUbD2:

      isUb R S x ==> S *<= x

lemma isUbD2a:

      isUb R S x ==> x ∈ R

lemma isUbI:

      [| S *<= x; x ∈ R |] ==> isUb R S x

lemma isLub_le_isUb:

      [| isLub R S x; isUb R S y |] ==> x ≤ y

lemma isLub_ubs:

      isLub R S x ==> x <=* ubs R S