author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10231  178a272bceeb 
child 10753  e43e017df8c1 
permissions  rwrr 
1465  1 
(* Title: HOL/Ord.ML 
923  2 
ID: $Id$ 
1465  3 
Author: Tobias Nipkow, Cambridge University Computer Laboratory 
923  4 
Copyright 1993 University of Cambridge 
5 

6 
The type class for ordered types 

7 
*) 

8 

5449
d853d1ac85a3
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents:
5316
diff
changeset

9 
(*Tell Blast_tac about overloading of < and <= to reduce the risk of 
d853d1ac85a3
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents:
5316
diff
changeset

10 
its applying a rule for the wrong type*) 
d853d1ac85a3
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents:
5316
diff
changeset

11 
Blast.overloaded ("op <", domain_type); 
d853d1ac85a3
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents:
5316
diff
changeset

12 
Blast.overloaded ("op <=", domain_type); 
d853d1ac85a3
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents:
5316
diff
changeset

13 

2608  14 
(** mono **) 
923  15 

5316  16 
val [prem] = Goalw [mono_def] 
923  17 
"[ !!A B. A <= B ==> f(A) <= f(B) ] ==> mono(f)"; 
18 
by (REPEAT (ares_tac [allI, impI, prem] 1)); 

19 
qed "monoI"; 

6956  20 
AddXIs [monoI]; 
923  21 

5316  22 
Goalw [mono_def] "[ mono(f); A <= B ] ==> f(A) <= f(B)"; 
23 
by (Fast_tac 1); 

923  24 
qed "monoD"; 
6956  25 
AddXDs [monoD]; 
923  26 

2608  27 

28 
section "Orders"; 

29 

5538  30 
(** Reflexivity **) 
31 

6115  32 
AddIffs [order_refl]; 
2608  33 

4600  34 
(*This form is useful with the classical reasoner*) 
5069  35 
Goal "!!x::'a::order. x = y ==> x <= y"; 
4600  36 
by (etac ssubst 1); 
37 
by (rtac order_refl 1); 

38 
qed "order_eq_refl"; 

39 

5069  40 
Goal "~ x < (x::'a::order)"; 
4089  41 
by (simp_tac (simpset() addsimps [order_less_le]) 1); 
2608  42 
qed "order_less_irrefl"; 
5449
d853d1ac85a3
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents:
5316
diff
changeset

43 
Addsimps [order_less_irrefl]; 
2608  44 

5069  45 
Goal "(x::'a::order) <= y = (x < y  x = y)"; 
4089  46 
by (simp_tac (simpset() addsimps [order_less_le]) 1); 
5449
d853d1ac85a3
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents:
5316
diff
changeset

47 
(*NOT suitable for AddIffs, since it can cause PROOF FAILED*) 
d853d1ac85a3
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents:
5316
diff
changeset

48 
by (blast_tac (claset() addSIs [order_refl]) 1); 
2608  49 
qed "order_le_less"; 
50 

8214  51 
Goal "!!x::'a::order. x < y ==> x <= y"; 
52 
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1); 

53 
qed "order_less_imp_le"; 

54 

5538  55 
(** Asymmetry **) 
56 

57 
Goal "(x::'a::order) < y ==> ~ (y<x)"; 

58 
by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1); 

59 
qed "order_less_not_sym"; 

60 

61 
(* [ n<m; ~P ==> m<n ] ==> P *) 

10231  62 
bind_thm ("order_less_asym", order_less_not_sym RS contrapos_np); 
5538  63 

6073  64 
(* Transitivity *) 
65 

66 
Goal "!!x::'a::order. [ x < y; y < z ] ==> x < z"; 

67 
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1); 

68 
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1); 

69 
qed "order_less_trans"; 

70 

6780  71 
Goal "!!x::'a::order. [ x <= y; y < z ] ==> x < z"; 
72 
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1); 

73 
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1); 

74 
qed "order_le_less_trans"; 

75 

76 
Goal "!!x::'a::order. [ x < y; y <= z ] ==> x < z"; 

77 
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1); 

78 
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1); 

79 
qed "order_less_le_trans"; 

80 

5538  81 

82 
(** Useful for simplification, but too risky to include by default. **) 

83 

84 
Goal "(x::'a::order) < y ==> (~ y < x) = True"; 

85 
by (blast_tac (claset() addEs [order_less_asym]) 1); 

86 
qed "order_less_imp_not_less"; 

87 

88 
Goal "(x::'a::order) < y ==> (y < x > P) = True"; 

89 
by (blast_tac (claset() addEs [order_less_asym]) 1); 

90 
qed "order_less_imp_triv"; 

91 

92 
Goal "(x::'a::order) < y ==> (x = y) = False"; 

93 
by Auto_tac; 

94 
qed "order_less_imp_not_eq"; 

95 

96 
Goal "(x::'a::order) < y ==> (y = x) = False"; 

97 
by Auto_tac; 

98 
qed "order_less_imp_not_eq2"; 

99 

100 

2608  101 
(** min **) 
102 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

103 
val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least"; 
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

104 
by (simp_tac (simpset() addsimps prems) 1); 
2608  105 
qed "min_leastL"; 
106 

5316  107 
val prems = Goalw [min_def] 
2608  108 
"(!!x::'a::order. least <= x) ==> min x least = least"; 
2935  109 
by (cut_facts_tac prems 1); 
110 
by (Asm_simp_tac 1); 

4089  111 
by (blast_tac (claset() addIs [order_antisym]) 1); 
2608  112 
qed "min_leastR"; 
4640  113 

114 

115 
section "Linear/Total Orders"; 

116 

5069  117 
Goal "!!x::'a::linorder. x<y  x=y  y<x"; 
4640  118 
by (simp_tac (simpset() addsimps [order_less_le]) 1); 
5132  119 
by (cut_facts_tac [linorder_linear] 1); 
4640  120 
by (Blast_tac 1); 
121 
qed "linorder_less_linear"; 

122 

9969  123 
val prems = Goal "[ (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P ] ==> P"; 
124 
by (cut_facts_tac [linorder_less_linear] 1); 

125 
by (REPEAT(eresolve_tac (prems@[disjE]) 1)); 

8024  126 
qed "linorder_less_split"; 
127 

6128  128 
Goal "!!x::'a::linorder. (~ x < y) = (y <= x)"; 
129 
by (simp_tac (simpset() addsimps [order_less_le]) 1); 

130 
by (cut_facts_tac [linorder_linear] 1); 

131 
by (blast_tac (claset() addIs [order_antisym]) 1); 

132 
qed "linorder_not_less"; 

133 

134 
Goal "!!x::'a::linorder. (~ x <= y) = (y < x)"; 

135 
by (simp_tac (simpset() addsimps [order_less_le]) 1); 

136 
by (cut_facts_tac [linorder_linear] 1); 

137 
by (blast_tac (claset() addIs [order_antisym]) 1); 

138 
qed "linorder_not_le"; 

139 

140 
Goal "!!x::'a::linorder. (x ~= y) = (x<y  y<x)"; 

141 
by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1); 

142 
by Auto_tac; 

143 
qed "linorder_neq_iff"; 

144 

145 
(* eliminates ~= in premises *) 

146 
bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE); 

147 

148 
(** min & max **) 

149 

6433  150 
Goalw [min_def] "min (x::'a::order) x = x"; 
6814  151 
by (Simp_tac 1); 
6433  152 
qed "min_same"; 
153 
Addsimps [min_same]; 

154 

155 
Goalw [max_def] "max (x::'a::order) x = x"; 

6814  156 
by (Simp_tac 1); 
6433  157 
qed "max_same"; 
158 
Addsimps [max_same]; 

159 

5069  160 
Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x  z <= y)"; 
4686  161 
by (Simp_tac 1); 
5132  162 
by (cut_facts_tac [linorder_linear] 1); 
4640  163 
by (blast_tac (claset() addIs [order_trans]) 1); 
164 
qed "le_max_iff_disj"; 

165 

8529  166 
Goal "(x::'a::linorder) <= max x y"; 
167 
by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1); 

168 
qed "le_maxI1"; 

169 

170 
Goal "(y::'a::linorder) <= max x y"; 

171 
by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1); 

172 
qed "le_maxI2"; 

7617
e783adccf39e
removed ordersorted theorems from the default claset
paulson
parents:
7494
diff
changeset

173 
(*CANNOT use with AddSIs because blast_tac will give PROOF FAILED.*) 
7494
45905028bb1d
added theorems le_maxI1 and le_maxI2, also in claset
oheimb
parents:
6956
diff
changeset

174 

6073  175 
Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x  z < y)"; 
176 
by (simp_tac (simpset() addsimps [order_le_less]) 1); 

177 
by (cut_facts_tac [linorder_less_linear] 1); 

178 
by (blast_tac (claset() addIs [order_less_trans]) 1); 

179 
qed "less_max_iff_disj"; 

180 

5069  181 
Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"; 
4686  182 
by (Simp_tac 1); 
5132  183 
by (cut_facts_tac [linorder_linear] 1); 
4640  184 
by (blast_tac (claset() addIs [order_trans]) 1); 
185 
qed "max_le_iff_conj"; 

5673  186 
Addsimps [max_le_iff_conj]; 
4640  187 

6433  188 
Goalw [max_def] "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"; 
189 
by (simp_tac (simpset() addsimps [order_le_less]) 1); 

190 
by (cut_facts_tac [linorder_less_linear] 1); 

191 
by (blast_tac (claset() addIs [order_less_trans]) 1); 

192 
qed "max_less_iff_conj"; 

193 
Addsimps [max_less_iff_conj]; 

194 

5069  195 
Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"; 
4686  196 
by (Simp_tac 1); 
5132  197 
by (cut_facts_tac [linorder_linear] 1); 
4640  198 
by (blast_tac (claset() addIs [order_trans]) 1); 
199 
qed "le_min_iff_conj"; 

5673  200 
Addsimps [le_min_iff_conj]; 
201 
(* AddIffs screws up a blast_tac in MiniML *) 

4640  202 

6433  203 
Goalw [min_def] "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"; 
204 
by (simp_tac (simpset() addsimps [order_le_less]) 1); 

205 
by (cut_facts_tac [linorder_less_linear] 1); 

206 
by (blast_tac (claset() addIs [order_less_trans]) 1); 

207 
qed "min_less_iff_conj"; 

208 
Addsimps [min_less_iff_conj]; 

209 

5069  210 
Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z  y <= z)"; 
4686  211 
by (Simp_tac 1); 
5132  212 
by (cut_facts_tac [linorder_linear] 1); 
4640  213 
by (blast_tac (claset() addIs [order_trans]) 1); 
214 
qed "min_le_iff_disj"; 

6157  215 

9242  216 
Goalw [min_def] "!!z::'a::linorder. (min x y < z) = (x < z  y < z)"; 
217 
by (simp_tac (simpset() addsimps [order_le_less]) 1); 

218 
by (cut_facts_tac [linorder_less_linear] 1); 

219 
by (blast_tac (claset() addIs [order_less_trans]) 1); 

220 
qed "min_less_iff_disj"; 

221 

6157  222 
Goalw [min_def] 
223 
"P(min (i::'a::linorder) j) = ((i <= j > P(i)) & (~ i <= j > P(j)))"; 

6301  224 
by (Simp_tac 1); 
6157  225 
qed "split_min"; 
226 

227 
Goalw [max_def] 

228 
"P(max (i::'a::linorder) j) = ((i <= j > P(j)) & (~ i <= j > P(i)))"; 

6301  229 
by (Simp_tac 1); 
6157  230 
qed "split_max"; 