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
```