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