src/HOL/Real/Lubs.thy
author nipkow
Mon, 16 Aug 2004 14:22:27 +0200
changeset 15131 c69542757a4d
parent 14653 0848ab6fe5fc
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     1
(*  Title       : Lubs.thy
7219
4e3f386c2e37 inserted Id: lines
paulson
parents: 5078
diff changeset
     2
    ID          : $Id$
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     3
    Author      : Jacques D. Fleuriot
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     4
    Copyright   : 1998  University of Cambridge
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
     5
*)
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     6
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
     7
header{*Definitions of Upper Bounds and Least Upper Bounds*}
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     8
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14653
diff changeset
     9
theory Lubs
c69542757a4d New theory header syntax.
nipkow
parents: 14653
diff changeset
    10
import Main
c69542757a4d New theory header syntax.
nipkow
parents: 14653
diff changeset
    11
begin
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    12
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    13
text{*Thanks to suggestions by James Margetson*}
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    14
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    15
constdefs
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    16
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    17
  setle :: "['a set, 'a::ord] => bool"     (infixl "*<=" 70)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    18
    "S *<= x    == (ALL y: S. y <= x)"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    19
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    20
  setge :: "['a::ord, 'a set] => bool"     (infixl "<=*" 70)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    21
    "x <=* S    == (ALL y: S. x <= y)"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    22
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    23
  leastP      :: "['a =>bool,'a::ord] => bool"
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    24
    "leastP P x == (P x & x <=* Collect P)"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    25
14653
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 14368
diff changeset
    26
  isUb        :: "['a set, 'a set, 'a::ord] => bool"
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 14368
diff changeset
    27
    "isUb R S x   == S *<= x & x: R"
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 14368
diff changeset
    28
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    29
  isLub       :: "['a set, 'a set, 'a::ord] => bool"
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    30
    "isLub R S x  == leastP (isUb R S) x"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    31
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    32
  ubs         :: "['a set, 'a::ord set] => 'a set"
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    33
    "ubs R S      == Collect (isUb R S)"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    34
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    35
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    36
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    37
subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    38
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    39
lemma setleI: "ALL y: S. y <= x ==> S *<= x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    40
by (simp add: setle_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    41
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    42
lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    43
by (simp add: setle_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    44
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    45
lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    46
by (simp add: setge_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    47
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    48
lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    49
by (simp add: setge_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    50
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    51
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    52
subsection{*Rules about the Operators @{term leastP}, @{term ub}
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    53
    and @{term lub}*}
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    54
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    55
lemma leastPD1: "leastP P x ==> P x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    56
by (simp add: leastP_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    57
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    58
lemma leastPD2: "leastP P x ==> x <=* Collect P"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    59
by (simp add: leastP_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    60
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    61
lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    62
by (blast dest!: leastPD2 setgeD)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    63
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    64
lemma isLubD1: "isLub R S x ==> S *<= x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    65
by (simp add: isLub_def isUb_def leastP_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    66
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    67
lemma isLubD1a: "isLub R S x ==> x: R"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    68
by (simp add: isLub_def isUb_def leastP_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    69
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    70
lemma isLub_isUb: "isLub R S x ==> isUb R S x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    71
apply (simp add: isUb_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    72
apply (blast dest: isLubD1 isLubD1a)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    73
done
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    74
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    75
lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    76
by (blast dest!: isLubD1 setleD)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    77
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    78
lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    79
by (simp add: isLub_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    80
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    81
lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    82
by (simp add: isLub_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    83
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    84
lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    85
by (simp add: isLub_def leastP_def)
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    86
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    87
lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    88
by (simp add: isUb_def setle_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    89
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    90
lemma isUbD2: "isUb R S x ==> S *<= x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    91
by (simp add: isUb_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    92
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    93
lemma isUbD2a: "isUb R S x ==> x: R"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    94
by (simp add: isUb_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    95
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    96
lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    97
by (simp add: isUb_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    98
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
    99
lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   100
apply (simp add: isLub_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   101
apply (blast intro!: leastPD3)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   102
done
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   103
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   104
lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S"
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   105
apply (simp add: ubs_def isLub_def)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   106
apply (erule leastPD2)
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   107
done
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   108
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   109
ML
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   110
{*
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   111
val setle_def = thm "setle_def";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   112
val setge_def = thm "setge_def";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   113
val leastP_def = thm "leastP_def";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   114
val isLub_def = thm "isLub_def";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   115
val isUb_def = thm "isUb_def";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   116
val ubs_def = thm "ubs_def";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   117
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   118
val setleI = thm "setleI";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   119
val setleD = thm "setleD";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   120
val setgeI = thm "setgeI";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   121
val setgeD = thm "setgeD";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   122
val leastPD1 = thm "leastPD1";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   123
val leastPD2 = thm "leastPD2";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   124
val leastPD3 = thm "leastPD3";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   125
val isLubD1 = thm "isLubD1";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   126
val isLubD1a = thm "isLubD1a";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   127
val isLub_isUb = thm "isLub_isUb";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   128
val isLubD2 = thm "isLubD2";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   129
val isLubD3 = thm "isLubD3";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   130
val isLubI1 = thm "isLubI1";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   131
val isLubI2 = thm "isLubI2";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   132
val isUbD = thm "isUbD";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   133
val isUbD2 = thm "isUbD2";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   134
val isUbD2a = thm "isUbD2a";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   135
val isUbI = thm "isUbI";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   136
val isLub_le_isUb = thm "isLub_le_isUb";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   137
val isLub_ubs = thm "isLub_ubs";
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   138
*}
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   139
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 9279
diff changeset
   140
end