src/HOL/Real/Lubs.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 15131 c69542757a4d child 19765 dfe940911617 permissions -rw-r--r--
import -> imports
```     1 (*  Title       : Lubs.thy
```
```     2     ID          : \$Id\$
```
```     3     Author      : Jacques D. Fleuriot
```
```     4     Copyright   : 1998  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header{*Definitions of Upper Bounds and Least Upper Bounds*}
```
```     8
```
```     9 theory Lubs
```
```    10 imports Main
```
```    11 begin
```
```    12
```
```    13 text{*Thanks to suggestions by James Margetson*}
```
```    14
```
```    15 constdefs
```
```    16
```
```    17   setle :: "['a set, 'a::ord] => bool"     (infixl "*<=" 70)
```
```    18     "S *<= x    == (ALL y: S. y <= x)"
```
```    19
```
```    20   setge :: "['a::ord, 'a set] => bool"     (infixl "<=*" 70)
```
```    21     "x <=* S    == (ALL y: S. x <= y)"
```
```    22
```
```    23   leastP      :: "['a =>bool,'a::ord] => bool"
```
```    24     "leastP P x == (P x & x <=* Collect P)"
```
```    25
```
```    26   isUb        :: "['a set, 'a set, 'a::ord] => bool"
```
```    27     "isUb R S x   == S *<= x & x: R"
```
```    28
```
```    29   isLub       :: "['a set, 'a set, 'a::ord] => bool"
```
```    30     "isLub R S x  == leastP (isUb R S) x"
```
```    31
```
```    32   ubs         :: "['a set, 'a::ord set] => 'a set"
```
```    33     "ubs R S      == Collect (isUb R S)"
```
```    34
```
```    35
```
```    36
```
```    37 subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}
```
```    38
```
```    39 lemma setleI: "ALL y: S. y <= x ==> S *<= x"
```
```    40 by (simp add: setle_def)
```
```    41
```
```    42 lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
```
```    43 by (simp add: setle_def)
```
```    44
```
```    45 lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
```
```    46 by (simp add: setge_def)
```
```    47
```
```    48 lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
```
```    49 by (simp add: setge_def)
```
```    50
```
```    51
```
```    52 subsection{*Rules about the Operators @{term leastP}, @{term ub}
```
```    53     and @{term lub}*}
```
```    54
```
```    55 lemma leastPD1: "leastP P x ==> P x"
```
```    56 by (simp add: leastP_def)
```
```    57
```
```    58 lemma leastPD2: "leastP P x ==> x <=* Collect P"
```
```    59 by (simp add: leastP_def)
```
```    60
```
```    61 lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
```
```    62 by (blast dest!: leastPD2 setgeD)
```
```    63
```
```    64 lemma isLubD1: "isLub R S x ==> S *<= x"
```
```    65 by (simp add: isLub_def isUb_def leastP_def)
```
```    66
```
```    67 lemma isLubD1a: "isLub R S x ==> x: R"
```
```    68 by (simp add: isLub_def isUb_def leastP_def)
```
```    69
```
```    70 lemma isLub_isUb: "isLub R S x ==> isUb R S x"
```
```    71 apply (simp add: isUb_def)
```
```    72 apply (blast dest: isLubD1 isLubD1a)
```
```    73 done
```
```    74
```
```    75 lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x"
```
```    76 by (blast dest!: isLubD1 setleD)
```
```    77
```
```    78 lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
```
```    79 by (simp add: isLub_def)
```
```    80
```
```    81 lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
```
```    82 by (simp add: isLub_def)
```
```    83
```
```    84 lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"
```
```    85 by (simp add: isLub_def leastP_def)
```
```    86
```
```    87 lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x"
```
```    88 by (simp add: isUb_def setle_def)
```
```    89
```
```    90 lemma isUbD2: "isUb R S x ==> S *<= x"
```
```    91 by (simp add: isUb_def)
```
```    92
```
```    93 lemma isUbD2a: "isUb R S x ==> x: R"
```
```    94 by (simp add: isUb_def)
```
```    95
```
```    96 lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x"
```
```    97 by (simp add: isUb_def)
```
```    98
```
```    99 lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y"
```
```   100 apply (simp add: isLub_def)
```
```   101 apply (blast intro!: leastPD3)
```
```   102 done
```
```   103
```
```   104 lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S"
```
```   105 apply (simp add: ubs_def isLub_def)
```
```   106 apply (erule leastPD2)
```
```   107 done
```
```   108
```
```   109 ML
```
```   110 {*
```
```   111 val setle_def = thm "setle_def";
```
```   112 val setge_def = thm "setge_def";
```
```   113 val leastP_def = thm "leastP_def";
```
```   114 val isLub_def = thm "isLub_def";
```
```   115 val isUb_def = thm "isUb_def";
```
```   116 val ubs_def = thm "ubs_def";
```
```   117
```
```   118 val setleI = thm "setleI";
```
```   119 val setleD = thm "setleD";
```
```   120 val setgeI = thm "setgeI";
```
```   121 val setgeD = thm "setgeD";
```
```   122 val leastPD1 = thm "leastPD1";
```
```   123 val leastPD2 = thm "leastPD2";
```
```   124 val leastPD3 = thm "leastPD3";
```
```   125 val isLubD1 = thm "isLubD1";
```
```   126 val isLubD1a = thm "isLubD1a";
```
```   127 val isLub_isUb = thm "isLub_isUb";
```
```   128 val isLubD2 = thm "isLubD2";
```
```   129 val isLubD3 = thm "isLubD3";
```
```   130 val isLubI1 = thm "isLubI1";
```
```   131 val isLubI2 = thm "isLubI2";
```
```   132 val isUbD = thm "isUbD";
```
```   133 val isUbD2 = thm "isUbD2";
```
```   134 val isUbD2a = thm "isUbD2a";
```
```   135 val isUbI = thm "isUbI";
```
```   136 val isLub_le_isUb = thm "isLub_le_isUb";
```
```   137 val isLub_ubs = thm "isLub_ubs";
```
```   138 *}
```
```   139
```
```   140 end
```