src/HOL/Lubs.thy
author haftmann
Wed Dec 03 15:58:44 2008 +0100 (2008-12-03)
changeset 28952 15a4b2cf8c34
parent 27368 src/HOL/Real/Lubs.thy@9f90ac19e32b
child 29654 24e73987bfe2
permissions -rw-r--r--
made repository layout more coherent with logical distribution structure; stripped some $Id$s
paulson@5078
     1
(*  Title       : Lubs.thy
paulson@7219
     2
    ID          : $Id$
paulson@5078
     3
    Author      : Jacques D. Fleuriot
paulson@5078
     4
    Copyright   : 1998  University of Cambridge
paulson@14368
     5
*)
paulson@5078
     6
paulson@14368
     7
header{*Definitions of Upper Bounds and Least Upper Bounds*}
paulson@5078
     8
nipkow@15131
     9
theory Lubs
haftmann@27368
    10
imports Plain
nipkow@15131
    11
begin
paulson@5078
    12
paulson@14368
    13
text{*Thanks to suggestions by James Margetson*}
paulson@5078
    14
wenzelm@19765
    15
definition
wenzelm@21404
    16
  setle :: "['a set, 'a::ord] => bool"  (infixl "*<=" 70) where
wenzelm@19765
    17
  "S *<= x = (ALL y: S. y <= x)"
paulson@14368
    18
wenzelm@21404
    19
definition
wenzelm@21404
    20
  setge :: "['a::ord, 'a set] => bool"  (infixl "<=*" 70) where
wenzelm@19765
    21
  "x <=* S = (ALL y: S. x <= y)"
paulson@14368
    22
wenzelm@21404
    23
definition
wenzelm@21404
    24
  leastP      :: "['a =>bool,'a::ord] => bool" where
wenzelm@19765
    25
  "leastP P x = (P x & x <=* Collect P)"
paulson@5078
    26
wenzelm@21404
    27
definition
wenzelm@21404
    28
  isUb        :: "['a set, 'a set, 'a::ord] => bool" where
wenzelm@19765
    29
  "isUb R S x = (S *<= x & x: R)"
wenzelm@14653
    30
wenzelm@21404
    31
definition
wenzelm@21404
    32
  isLub       :: "['a set, 'a set, 'a::ord] => bool" where
wenzelm@19765
    33
  "isLub R S x = leastP (isUb R S) x"
paulson@5078
    34
wenzelm@21404
    35
definition
wenzelm@21404
    36
  ubs         :: "['a set, 'a::ord set] => 'a set" where
wenzelm@19765
    37
  "ubs R S = Collect (isUb R S)"
paulson@5078
    38
paulson@14368
    39
paulson@14368
    40
paulson@14368
    41
subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}
paulson@14368
    42
paulson@14368
    43
lemma setleI: "ALL y: S. y <= x ==> S *<= x"
paulson@14368
    44
by (simp add: setle_def)
paulson@14368
    45
paulson@14368
    46
lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
paulson@14368
    47
by (simp add: setle_def)
paulson@14368
    48
paulson@14368
    49
lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
paulson@14368
    50
by (simp add: setge_def)
paulson@14368
    51
paulson@14368
    52
lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
paulson@14368
    53
by (simp add: setge_def)
paulson@14368
    54
paulson@14368
    55
paulson@14368
    56
subsection{*Rules about the Operators @{term leastP}, @{term ub}
paulson@14368
    57
    and @{term lub}*}
paulson@14368
    58
paulson@14368
    59
lemma leastPD1: "leastP P x ==> P x"
paulson@14368
    60
by (simp add: leastP_def)
paulson@14368
    61
paulson@14368
    62
lemma leastPD2: "leastP P x ==> x <=* Collect P"
paulson@14368
    63
by (simp add: leastP_def)
paulson@14368
    64
paulson@14368
    65
lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
paulson@14368
    66
by (blast dest!: leastPD2 setgeD)
paulson@14368
    67
paulson@14368
    68
lemma isLubD1: "isLub R S x ==> S *<= x"
paulson@14368
    69
by (simp add: isLub_def isUb_def leastP_def)
paulson@14368
    70
paulson@14368
    71
lemma isLubD1a: "isLub R S x ==> x: R"
paulson@14368
    72
by (simp add: isLub_def isUb_def leastP_def)
paulson@14368
    73
paulson@14368
    74
lemma isLub_isUb: "isLub R S x ==> isUb R S x"
paulson@14368
    75
apply (simp add: isUb_def)
paulson@14368
    76
apply (blast dest: isLubD1 isLubD1a)
paulson@14368
    77
done
paulson@14368
    78
paulson@14368
    79
lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x"
paulson@14368
    80
by (blast dest!: isLubD1 setleD)
paulson@14368
    81
paulson@14368
    82
lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
paulson@14368
    83
by (simp add: isLub_def)
paulson@14368
    84
paulson@14368
    85
lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
paulson@14368
    86
by (simp add: isLub_def)
paulson@14368
    87
paulson@14368
    88
lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"
paulson@14368
    89
by (simp add: isLub_def leastP_def)
paulson@5078
    90
paulson@14368
    91
lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x"
paulson@14368
    92
by (simp add: isUb_def setle_def)
paulson@14368
    93
paulson@14368
    94
lemma isUbD2: "isUb R S x ==> S *<= x"
paulson@14368
    95
by (simp add: isUb_def)
paulson@14368
    96
paulson@14368
    97
lemma isUbD2a: "isUb R S x ==> x: R"
paulson@14368
    98
by (simp add: isUb_def)
paulson@14368
    99
paulson@14368
   100
lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x"
paulson@14368
   101
by (simp add: isUb_def)
paulson@14368
   102
paulson@14368
   103
lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y"
paulson@14368
   104
apply (simp add: isLub_def)
paulson@14368
   105
apply (blast intro!: leastPD3)
paulson@14368
   106
done
paulson@14368
   107
paulson@14368
   108
lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S"
paulson@14368
   109
apply (simp add: ubs_def isLub_def)
paulson@14368
   110
apply (erule leastPD2)
paulson@14368
   111
done
paulson@5078
   112
paulson@14368
   113
end