author  wenzelm 
Fri, 17 Nov 2006 02:20:03 +0100  
changeset 21404  eb85850d3eb7 
parent 19765  dfe940911617 
child 27368  9f90ac19e32b 
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 
15140  10 
imports Main 
15131  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 

19765  15 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

16 
setle :: "['a set, 'a::ord] => bool" (infixl "*<=" 70) where 
19765  17 
"S *<= x = (ALL y: S. y <= x)" 
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

18 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

19 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

20 
setge :: "['a::ord, 'a set] => bool" (infixl "<=*" 70) where 
19765  21 
"x <=* S = (ALL y: S. x <= y)" 
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

22 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

23 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

24 
leastP :: "['a =>bool,'a::ord] => bool" where 
19765  25 
"leastP P x = (P x & x <=* Collect P)" 
5078  26 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

27 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

28 
isUb :: "['a set, 'a set, 'a::ord] => bool" where 
19765  29 
"isUb R S x = (S *<= x & x: R)" 
14653  30 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

31 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

32 
isLub :: "['a set, 'a set, 'a::ord] => bool" where 
19765  33 
"isLub R S x = leastP (isUb R S) x" 
5078  34 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

35 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

36 
ubs :: "['a set, 'a::ord set] => 'a set" where 
19765  37 
"ubs R S = Collect (isUb R S)" 
5078  38 

14368
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 

2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

41 
subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*} 
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 setleI: "ALL y: S. y <= x ==> S *<= x" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

44 
by (simp add: setle_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 setleD: "[ S *<= x; y: S ] ==> y <= x" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

47 
by (simp add: setle_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 
lemma setgeI: "ALL y: S. x<= y ==> x <=* S" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

50 
by (simp add: setge_def) 
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 
lemma setgeD: "[ x <=* S; y: S ] ==> x <= y" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

53 
by (simp add: setge_def) 
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 

2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

56 
subsection{*Rules about the Operators @{term leastP}, @{term ub} 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

57 
and @{term lub}*} 
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 leastPD1: "leastP P x ==> P x" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

60 
by (simp add: leastP_def) 
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 leastPD2: "leastP P x ==> x <=* Collect P" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

63 
by (simp add: 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 leastPD3: "[ leastP P x; y: Collect P ] ==> x <= y" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

66 
by (blast dest!: leastPD2 setgeD) 
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 isLubD1: "isLub R S x ==> S *<= x" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

69 
by (simp add: isLub_def isUb_def leastP_def) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

70 

2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

71 
lemma isLubD1a: "isLub R S x ==> x: R" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

72 
by (simp add: isLub_def isUb_def leastP_def) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

73 

2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

74 
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

75 
apply (simp add: isUb_def) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

76 
apply (blast dest: isLubD1 isLubD1a) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

77 
done 
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 isLubD2: "[ isLub R S x; y : S ] ==> y <= x" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

80 
by (blast dest!: isLubD1 setleD) 
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 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

83 
by (simp add: isLub_def) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

84 

2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

85 
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

86 
by (simp add: isLub_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 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

89 
by (simp add: isLub_def leastP_def) 
5078  90 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

91 
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

92 
by (simp add: isUb_def setle_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 isUbD2: "isUb R S x ==> 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 isUbD2a: "isUb R S x ==> x: R" 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

98 
by (simp add: isUb_def) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

99 

2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

100 
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

101 
by (simp add: isUb_def) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

102 

2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

103 
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

104 
apply (simp add: isLub_def) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

105 
apply (blast intro!: leastPD3) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

106 
done 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

107 

2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

108 
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

109 
apply (simp add: ubs_def isLub_def) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

110 
apply (erule leastPD2) 
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

111 
done 
5078  112 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

113 
end 