src/HOL/Real/Lubs.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 14653 0848ab6fe5fc
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
     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 import 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