src/HOL/Lubs.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 30738 0842e906300c
child 46509 c4b2ec379fdd
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title       : Lubs.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4 *)
     5 
     6 header{*Definitions of Upper Bounds and Least Upper Bounds*}
     7 
     8 theory Lubs
     9 imports Main
    10 begin
    11 
    12 text{*Thanks to suggestions by James Margetson*}
    13 
    14 definition
    15   setle :: "['a set, 'a::ord] => bool"  (infixl "*<=" 70) where
    16   "S *<= x = (ALL y: S. y <= x)"
    17 
    18 definition
    19   setge :: "['a::ord, 'a set] => bool"  (infixl "<=*" 70) where
    20   "x <=* S = (ALL y: S. x <= y)"
    21 
    22 definition
    23   leastP      :: "['a =>bool,'a::ord] => bool" where
    24   "leastP P x = (P x & x <=* Collect P)"
    25 
    26 definition
    27   isUb        :: "['a set, 'a set, 'a::ord] => bool" where
    28   "isUb R S x = (S *<= x & x: R)"
    29 
    30 definition
    31   isLub       :: "['a set, 'a set, 'a::ord] => bool" where
    32   "isLub R S x = leastP (isUb R S) x"
    33 
    34 definition
    35   ubs         :: "['a set, 'a::ord set] => 'a set" where
    36   "ubs R S = Collect (isUb R S)"
    37 
    38 
    39 
    40 subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}
    41 
    42 lemma setleI: "ALL y: S. y <= x ==> S *<= x"
    43 by (simp add: setle_def)
    44 
    45 lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
    46 by (simp add: setle_def)
    47 
    48 lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
    49 by (simp add: setge_def)
    50 
    51 lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
    52 by (simp add: setge_def)
    53 
    54 
    55 subsection{*Rules about the Operators @{term leastP}, @{term ub}
    56     and @{term lub}*}
    57 
    58 lemma leastPD1: "leastP P x ==> P x"
    59 by (simp add: leastP_def)
    60 
    61 lemma leastPD2: "leastP P x ==> x <=* Collect P"
    62 by (simp add: leastP_def)
    63 
    64 lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
    65 by (blast dest!: leastPD2 setgeD)
    66 
    67 lemma isLubD1: "isLub R S x ==> S *<= x"
    68 by (simp add: isLub_def isUb_def leastP_def)
    69 
    70 lemma isLubD1a: "isLub R S x ==> x: R"
    71 by (simp add: isLub_def isUb_def leastP_def)
    72 
    73 lemma isLub_isUb: "isLub R S x ==> isUb R S x"
    74 apply (simp add: isUb_def)
    75 apply (blast dest: isLubD1 isLubD1a)
    76 done
    77 
    78 lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x"
    79 by (blast dest!: isLubD1 setleD)
    80 
    81 lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
    82 by (simp add: isLub_def)
    83 
    84 lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
    85 by (simp add: isLub_def)
    86 
    87 lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"
    88 by (simp add: isLub_def leastP_def)
    89 
    90 lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x"
    91 by (simp add: isUb_def setle_def)
    92 
    93 lemma isUbD2: "isUb R S x ==> S *<= x"
    94 by (simp add: isUb_def)
    95 
    96 lemma isUbD2a: "isUb R S x ==> x: R"
    97 by (simp add: isUb_def)
    98 
    99 lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x"
   100 by (simp add: isUb_def)
   101 
   102 lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y"
   103 apply (simp add: isLub_def)
   104 apply (blast intro!: leastPD3)
   105 done
   106 
   107 lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S"
   108 apply (simp add: ubs_def isLub_def)
   109 apply (erule leastPD2)
   110 done
   111 
   112 end