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