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