author  nipkow 
Mon, 16 Aug 2004 14:22:27 +0200  
changeset 15131  c69542757a4d 
parent 14653  0848ab6fe5fc 
child 15140  322485b816ac 
permissions  rwrr 
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 

15131  9 
theory Lubs 
10 
import Main 

11 
begin 

5078  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  14 

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  24 
"leastP P x == (P x & x <=* Collect P)" 
25 

14653  26 
isUb :: "['a set, 'a set, 'a::ord] => bool" 
27 
"isUb R S x == S *<= x & x: R" 

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  30 
"isLub R S x == leastP (isUb R S) x" 
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  33 
"ubs R S == Collect (isUb R S)" 
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  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  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  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 