src/HOL/Lubs.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 46509 c4b2ec379fdd child 51520 e9b361845809 permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
```     1 (*  Title:      HOL/Lubs.thy
```
```     2     Author:     Jacques D. Fleuriot, University of Cambridge
```
```     3 *)
```
```     4
```
```     5 header {* Definitions of Upper Bounds and Least Upper Bounds *}
```
```     6
```
```     7 theory Lubs
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 text {* Thanks to suggestions by James Margetson *}
```
```    12
```
```    13 definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl "*<=" 70)
```
```    14   where "S *<= x = (ALL y: S. y \<le> x)"
```
```    15
```
```    16 definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "<=*" 70)
```
```    17   where "x <=* S = (ALL y: S. x \<le> y)"
```
```    18
```
```    19 definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
```
```    20   where "leastP P x = (P x \<and> x <=* Collect P)"
```
```    21
```
```    22 definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
```
```    23   where "isUb R S x = (S *<= x \<and> x: R)"
```
```    24
```
```    25 definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
```
```    26   where "isLub R S x = leastP (isUb R S) x"
```
```    27
```
```    28 definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
```
```    29   where "ubs R S = Collect (isUb R S)"
```
```    30
```
```    31
```
```    32 subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
```
```    33
```
```    34 lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
```
```    35   by (simp add: setle_def)
```
```    36
```
```    37 lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
```
```    38   by (simp add: setle_def)
```
```    39
```
```    40 lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
```
```    41   by (simp add: setge_def)
```
```    42
```
```    43 lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
```
```    44   by (simp add: setge_def)
```
```    45
```
```    46
```
```    47 subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
```
```    48
```
```    49 lemma leastPD1: "leastP P x \<Longrightarrow> P x"
```
```    50   by (simp add: leastP_def)
```
```    51
```
```    52 lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
```
```    53   by (simp add: leastP_def)
```
```    54
```
```    55 lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
```
```    56   by (blast dest!: leastPD2 setgeD)
```
```    57
```
```    58 lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
```
```    59   by (simp add: isLub_def isUb_def leastP_def)
```
```    60
```
```    61 lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
```
```    62   by (simp add: isLub_def isUb_def leastP_def)
```
```    63
```
```    64 lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
```
```    65   unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
```
```    66
```
```    67 lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
```
```    68   by (blast dest!: isLubD1 setleD)
```
```    69
```
```    70 lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
```
```    71   by (simp add: isLub_def)
```
```    72
```
```    73 lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
```
```    74   by (simp add: isLub_def)
```
```    75
```
```    76 lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
```
```    77   by (simp add: isLub_def leastP_def)
```
```    78
```
```    79 lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
```
```    80   by (simp add: isUb_def setle_def)
```
```    81
```
```    82 lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
```
```    83   by (simp add: isUb_def)
```
```    84
```
```    85 lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
```
```    86   by (simp add: isUb_def)
```
```    87
```
```    88 lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
```
```    89   by (simp add: isUb_def)
```
```    90
```
```    91 lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
```
```    92   unfolding isLub_def by (blast intro!: leastPD3)
```
```    93
```
```    94 lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
```
```    95   unfolding ubs_def isLub_def by (rule leastPD2)
```
```    96
```
```    97 end
```