author  nipkow 
Wed, 27 Jan 1999 17:11:39 +0100  
changeset 6157  29942d3a1818 
parent 6128  2acc5d36610c 
child 6301  08245f5a436d 
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 

5538  65 

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

67 

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

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

70 
qed "order_less_imp_not_less"; 

71 

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

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

74 
qed "order_less_imp_triv"; 

75 

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

77 
by Auto_tac; 

78 
qed "order_less_imp_not_eq"; 

79 

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

81 
by Auto_tac; 

82 
qed "order_less_imp_not_eq2"; 

83 

84 

2608  85 
(** min **) 
86 

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

87 
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

88 
by (simp_tac (simpset() addsimps prems) 1); 
2608  89 
qed "min_leastL"; 
90 

5316  91 
val prems = Goalw [min_def] 
2608  92 
"(!!x::'a::order. least <= x) ==> min x least = least"; 
2935  93 
by (cut_facts_tac prems 1); 
94 
by (Asm_simp_tac 1); 

4089  95 
by (blast_tac (claset() addIs [order_antisym]) 1); 
2608  96 
qed "min_leastR"; 
4640  97 

98 

99 
section "Linear/Total Orders"; 

100 

5069  101 
Goal "!!x::'a::linorder. x<y  x=y  y<x"; 
4640  102 
by (simp_tac (simpset() addsimps [order_less_le]) 1); 
5132  103 
by (cut_facts_tac [linorder_linear] 1); 
4640  104 
by (Blast_tac 1); 
105 
qed "linorder_less_linear"; 

106 

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

109 
by (cut_facts_tac [linorder_linear] 1); 

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

111 
qed "linorder_not_less"; 

112 

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

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

115 
by (cut_facts_tac [linorder_linear] 1); 

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

117 
qed "linorder_not_le"; 

118 

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

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

121 
by Auto_tac; 

122 
qed "linorder_neq_iff"; 

123 

124 
(* eliminates ~= in premises *) 

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

126 

127 
(** min & max **) 

128 

5069  129 
Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x  z <= y)"; 
4686  130 
by (Simp_tac 1); 
5132  131 
by (cut_facts_tac [linorder_linear] 1); 
4640  132 
by (blast_tac (claset() addIs [order_trans]) 1); 
133 
qed "le_max_iff_disj"; 

134 

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

137 
by (cut_facts_tac [linorder_less_linear] 1); 

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

139 
qed "less_max_iff_disj"; 

140 

5069  141 
Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"; 
4686  142 
by (Simp_tac 1); 
5132  143 
by (cut_facts_tac [linorder_linear] 1); 
4640  144 
by (blast_tac (claset() addIs [order_trans]) 1); 
145 
qed "max_le_iff_conj"; 

5673  146 
Addsimps [max_le_iff_conj]; 
4640  147 

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

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

4640  155 

5069  156 
Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z  y <= z)"; 
4686  157 
by (Simp_tac 1); 
5132  158 
by (cut_facts_tac [linorder_linear] 1); 
4640  159 
by (blast_tac (claset() addIs [order_trans]) 1); 
160 
qed "min_le_iff_disj"; 

6157  161 

162 
Goalw [min_def] 

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

164 
by(Simp_tac 1); 

165 
qed "split_min"; 

166 

167 
Goalw [max_def] 

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

169 
by(Simp_tac 1); 

170 
qed "split_max"; 