src/HOL/Lubs.thy
author huffman
Mon Jan 12 12:09:54 2009 -0800 (2009-01-12)
changeset 29460 ad87e5d1488b
parent 28952 15a4b2cf8c34
child 29654 24e73987bfe2
permissions -rw-r--r--
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
     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 Plain
    11 begin
    12 
    13 text{*Thanks to suggestions by James Margetson*}
    14 
    15 definition
    16   setle :: "['a set, 'a::ord] => bool"  (infixl "*<=" 70) where
    17   "S *<= x = (ALL y: S. y <= x)"
    18 
    19 definition
    20   setge :: "['a::ord, 'a set] => bool"  (infixl "<=*" 70) where
    21   "x <=* S = (ALL y: S. x <= y)"
    22 
    23 definition
    24   leastP      :: "['a =>bool,'a::ord] => bool" where
    25   "leastP P x = (P x & x <=* Collect P)"
    26 
    27 definition
    28   isUb        :: "['a set, 'a set, 'a::ord] => bool" where
    29   "isUb R S x = (S *<= x & x: R)"
    30 
    31 definition
    32   isLub       :: "['a set, 'a set, 'a::ord] => bool" where
    33   "isLub R S x = leastP (isUb R S) x"
    34 
    35 definition
    36   ubs         :: "['a set, 'a::ord set] => 'a set" where
    37   "ubs R S = Collect (isUb R S)"
    38 
    39 
    40 
    41 subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}
    42 
    43 lemma setleI: "ALL y: S. y <= x ==> S *<= x"
    44 by (simp add: setle_def)
    45 
    46 lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
    47 by (simp add: setle_def)
    48 
    49 lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
    50 by (simp add: setge_def)
    51 
    52 lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
    53 by (simp add: setge_def)
    54 
    55 
    56 subsection{*Rules about the Operators @{term leastP}, @{term ub}
    57     and @{term lub}*}
    58 
    59 lemma leastPD1: "leastP P x ==> P x"
    60 by (simp add: leastP_def)
    61 
    62 lemma leastPD2: "leastP P x ==> x <=* Collect P"
    63 by (simp add: leastP_def)
    64 
    65 lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
    66 by (blast dest!: leastPD2 setgeD)
    67 
    68 lemma isLubD1: "isLub R S x ==> S *<= x"
    69 by (simp add: isLub_def isUb_def leastP_def)
    70 
    71 lemma isLubD1a: "isLub R S x ==> x: R"
    72 by (simp add: isLub_def isUb_def leastP_def)
    73 
    74 lemma isLub_isUb: "isLub R S x ==> isUb R S x"
    75 apply (simp add: isUb_def)
    76 apply (blast dest: isLubD1 isLubD1a)
    77 done
    78 
    79 lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x"
    80 by (blast dest!: isLubD1 setleD)
    81 
    82 lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
    83 by (simp add: isLub_def)
    84 
    85 lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
    86 by (simp add: isLub_def)
    87 
    88 lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"
    89 by (simp add: isLub_def leastP_def)
    90 
    91 lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x"
    92 by (simp add: isUb_def setle_def)
    93 
    94 lemma isUbD2: "isUb R S x ==> S *<= x"
    95 by (simp add: isUb_def)
    96 
    97 lemma isUbD2a: "isUb R S x ==> x: R"
    98 by (simp add: isUb_def)
    99 
   100 lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x"
   101 by (simp add: isUb_def)
   102 
   103 lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y"
   104 apply (simp add: isLub_def)
   105 apply (blast intro!: leastPD3)
   106 done
   107 
   108 lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S"
   109 apply (simp add: ubs_def isLub_def)
   110 apply (erule leastPD2)
   111 done
   112 
   113 end