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