src/HOL/Lubs.thy
author hoelzl
Tue Mar 26 12:20:54 2013 +0100 (2013-03-26)
changeset 51520 e9b361845809
parent 46509 c4b2ec379fdd
permissions -rw-r--r--
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
     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 lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
    98   apply (frule isLub_isUb)
    99   apply (frule_tac x = y in isLub_isUb)
   100   apply (blast intro!: order_antisym dest!: isLub_le_isUb)
   101   done
   102 
   103 end