author  paulson 
Thu, 10 Jun 1999 10:50:19 +0200  
changeset 6814  d96d4977f94e 
parent 6780  769cea1985e4 
child 6956  18c0457efd3d 
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"; 

20 

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

923  23 
qed "monoD"; 
24 

2608  25 

26 
section "Orders"; 

27 

5538  28 
(** Reflexivity **) 
29 

6115  30 
AddIffs [order_refl]; 
2608  31 

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

36 
qed "order_eq_refl"; 

37 

5069  38 
Goal "~ x < (x::'a::order)"; 
4089  39 
by (simp_tac (simpset() addsimps [order_less_le]) 1); 
2608  40 
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

41 
Addsimps [order_less_irrefl]; 
2608  42 

5069  43 
Goal "(x::'a::order) <= y = (x < y  x = y)"; 
4089  44 
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

45 
(*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

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

5538  49 
(** Asymmetry **) 
50 

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

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

53 
qed "order_less_not_sym"; 

54 

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

56 
bind_thm ("order_less_asym", order_less_not_sym RS swap); 

57 

6073  58 
(* Transitivity *) 
59 

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

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

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

63 
qed "order_less_trans"; 

64 

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

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

68 
qed "order_le_less_trans"; 

69 

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

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

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

73 
qed "order_less_le_trans"; 

74 

5538  75 

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

77 

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

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

80 
qed "order_less_imp_not_less"; 

81 

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

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

84 
qed "order_less_imp_triv"; 

85 

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

87 
by Auto_tac; 

88 
qed "order_less_imp_not_eq"; 

89 

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

91 
by Auto_tac; 

92 
qed "order_less_imp_not_eq2"; 

93 

94 

2608  95 
(** min **) 
96 

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

97 
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

98 
by (simp_tac (simpset() addsimps prems) 1); 
2608  99 
qed "min_leastL"; 
100 

5316  101 
val prems = Goalw [min_def] 
2608  102 
"(!!x::'a::order. least <= x) ==> min x least = least"; 
2935  103 
by (cut_facts_tac prems 1); 
104 
by (Asm_simp_tac 1); 

4089  105 
by (blast_tac (claset() addIs [order_antisym]) 1); 
2608  106 
qed "min_leastR"; 
4640  107 

108 

109 
section "Linear/Total Orders"; 

110 

5069  111 
Goal "!!x::'a::linorder. x<y  x=y  y<x"; 
4640  112 
by (simp_tac (simpset() addsimps [order_less_le]) 1); 
5132  113 
by (cut_facts_tac [linorder_linear] 1); 
4640  114 
by (Blast_tac 1); 
115 
qed "linorder_less_linear"; 

116 

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

119 
by (cut_facts_tac [linorder_linear] 1); 

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

121 
qed "linorder_not_less"; 

122 

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

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

125 
by (cut_facts_tac [linorder_linear] 1); 

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

127 
qed "linorder_not_le"; 

128 

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

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

131 
by Auto_tac; 

132 
qed "linorder_neq_iff"; 

133 

134 
(* eliminates ~= in premises *) 

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

136 

137 
(** min & max **) 

138 

6433  139 
Goalw [min_def] "min (x::'a::order) x = x"; 
6814  140 
by (Simp_tac 1); 
6433  141 
qed "min_same"; 
142 
Addsimps [min_same]; 

143 

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

6814  145 
by (Simp_tac 1); 
6433  146 
qed "max_same"; 
147 
Addsimps [max_same]; 

148 

5069  149 
Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x  z <= y)"; 
4686  150 
by (Simp_tac 1); 
5132  151 
by (cut_facts_tac [linorder_linear] 1); 
4640  152 
by (blast_tac (claset() addIs [order_trans]) 1); 
153 
qed "le_max_iff_disj"; 

154 

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

157 
by (cut_facts_tac [linorder_less_linear] 1); 

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

159 
qed "less_max_iff_disj"; 

160 

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

5673  166 
Addsimps [max_le_iff_conj]; 
4640  167 

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

170 
by (cut_facts_tac [linorder_less_linear] 1); 

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

172 
qed "max_less_iff_conj"; 

173 
Addsimps [max_less_iff_conj]; 

174 

5069  175 
Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"; 
4686  176 
by (Simp_tac 1); 
5132  177 
by (cut_facts_tac [linorder_linear] 1); 
4640  178 
by (blast_tac (claset() addIs [order_trans]) 1); 
179 
qed "le_min_iff_conj"; 

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

4640  182 

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

185 
by (cut_facts_tac [linorder_less_linear] 1); 

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

187 
qed "min_less_iff_conj"; 

188 
Addsimps [min_less_iff_conj]; 

189 

5069  190 
Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z  y <= z)"; 
4686  191 
by (Simp_tac 1); 
5132  192 
by (cut_facts_tac [linorder_linear] 1); 
4640  193 
by (blast_tac (claset() addIs [order_trans]) 1); 
194 
qed "min_le_iff_disj"; 

6157  195 

196 
Goalw [min_def] 

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

6301  198 
by (Simp_tac 1); 
6157  199 
qed "split_min"; 
200 

201 
Goalw [max_def] 

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

6301  203 
by (Simp_tac 1); 
6157  204 
qed "split_max"; 