author | wenzelm |
Mon, 02 May 2011 16:33:21 +0200 | |
changeset 42616 | 92715b528e78 |
parent 30738 | 0842e906300c |
child 46509 | c4b2ec379fdd |
permissions | -rw-r--r-- |
5078 | 1 |
(* Title : Lubs.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
4 |
*) |
5078 | 5 |
|
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
6 |
header{*Definitions of Upper Bounds and Least Upper Bounds*} |
5078 | 7 |
|
15131 | 8 |
theory Lubs |
30738 | 9 |
imports Main |
15131 | 10 |
begin |
5078 | 11 |
|
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
12 |
text{*Thanks to suggestions by James Margetson*} |
5078 | 13 |
|
19765 | 14 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
15 |
setle :: "['a set, 'a::ord] => bool" (infixl "*<=" 70) where |
19765 | 16 |
"S *<= x = (ALL y: S. y <= x)" |
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
17 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
18 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
19 |
setge :: "['a::ord, 'a set] => bool" (infixl "<=*" 70) where |
19765 | 20 |
"x <=* S = (ALL y: S. x <= y)" |
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
21 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
22 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
23 |
leastP :: "['a =>bool,'a::ord] => bool" where |
19765 | 24 |
"leastP P x = (P x & x <=* Collect P)" |
5078 | 25 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
26 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
27 |
isUb :: "['a set, 'a set, 'a::ord] => bool" where |
19765 | 28 |
"isUb R S x = (S *<= x & x: R)" |
14653 | 29 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
30 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
31 |
isLub :: "['a set, 'a set, 'a::ord] => bool" where |
19765 | 32 |
"isLub R S x = leastP (isUb R S) x" |
5078 | 33 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
34 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset
|
35 |
ubs :: "['a set, 'a::ord set] => 'a set" where |
19765 | 36 |
"ubs R S = Collect (isUb R S)" |
5078 | 37 |
|
14368
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 |
|
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
40 |
subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*} |
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 setleI: "ALL y: S. y <= x ==> S *<= 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 setleD: "[| S *<= x; y: S |] ==> y <= x" |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
46 |
by (simp add: setle_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 setgeI: "ALL y: S. x<= y ==> x <=* S" |
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 |
lemma setgeD: "[| x <=* S; y: S |] ==> x <= y" |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
52 |
by (simp add: setge_def) |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
53 |
|
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 |
subsection{*Rules about the Operators @{term leastP}, @{term ub} |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
56 |
and @{term lub}*} |
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 leastPD1: "leastP P x ==> P x" |
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 leastPD2: "leastP P x ==> x <=* Collect P" |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
62 |
by (simp add: leastP_def) |
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 leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y" |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
65 |
by (blast dest!: leastPD2 setgeD) |
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 isLubD1: "isLub R S x ==> S *<= x" |
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 isLubD1a: "isLub R S x ==> x: R" |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
71 |
by (simp add: isLub_def isUb_def leastP_def) |
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 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
|
74 |
apply (simp add: isUb_def) |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
75 |
apply (blast dest: isLubD1 isLubD1a) |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
76 |
done |
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 isLubD2: "[| isLub R S x; y : S |] ==> y <= x" |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
79 |
by (blast dest!: isLubD1 setleD) |
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 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
|
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 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
|
85 |
by (simp add: isLub_def) |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
86 |
|
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
87 |
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
|
88 |
by (simp add: isLub_def leastP_def) |
5078 | 89 |
|
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
90 |
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
|
91 |
by (simp add: isUb_def setle_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 isUbD2: "isUb R S x ==> S *<= x" |
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 isUbD2a: "isUb R S x ==> x: R" |
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 isUbI: "[| S *<= x; x: R |] ==> isUb R S x" |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
100 |
by (simp add: isUb_def) |
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_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
|
103 |
apply (simp add: isLub_def) |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
104 |
apply (blast intro!: leastPD3) |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
105 |
done |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
106 |
|
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
107 |
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
|
108 |
apply (simp add: ubs_def isLub_def) |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
109 |
apply (erule leastPD2) |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
110 |
done |
5078 | 111 |
|
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset
|
112 |
end |