1 (* Title: HOL/Ord.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 The type class for ordered types |
|
7 *) |
|
8 |
|
9 (*Tell Blast_tac about overloading of < and <= to reduce the risk of |
|
10 its applying a rule for the wrong type*) |
|
11 Blast.overloaded ("op <", domain_type); |
|
12 Blast.overloaded ("op <=", domain_type); |
|
13 |
|
14 (** mono **) |
|
15 |
|
16 val [prem] = Goalw [mono_def] |
|
17 "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
|
18 by (REPEAT (ares_tac [allI, impI, prem] 1)); |
|
19 qed "monoI"; |
|
20 AddXIs [monoI]; |
|
21 |
|
22 Goalw [mono_def] "[| mono(f); A <= B |] ==> f(A) <= f(B)"; |
|
23 by (Fast_tac 1); |
|
24 qed "monoD"; |
|
25 AddXDs [monoD]; |
|
26 |
|
27 |
|
28 section "Orders"; |
|
29 |
|
30 (** Reflexivity **) |
|
31 |
|
32 AddIffs [order_refl]; |
|
33 |
|
34 (*This form is useful with the classical reasoner*) |
|
35 Goal "!!x::'a::order. x = y ==> x <= y"; |
|
36 by (etac ssubst 1); |
|
37 by (rtac order_refl 1); |
|
38 qed "order_eq_refl"; |
|
39 |
|
40 Goal "~ x < (x::'a::order)"; |
|
41 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
|
42 qed "order_less_irrefl"; |
|
43 Addsimps [order_less_irrefl]; |
|
44 |
|
45 Goal "(x::'a::order) <= y = (x < y | x = y)"; |
|
46 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
|
47 (*NOT suitable for AddIffs, since it can cause PROOF FAILED*) |
|
48 by (blast_tac (claset() addSIs [order_refl]) 1); |
|
49 qed "order_le_less"; |
|
50 |
|
51 bind_thm ("order_le_imp_less_or_eq", order_le_less RS iffD1); |
|
52 |
|
53 Goal "!!x::'a::order. x < y ==> x <= y"; |
|
54 by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1); |
|
55 qed "order_less_imp_le"; |
|
56 |
|
57 (** Asymmetry **) |
|
58 |
|
59 Goal "(x::'a::order) < y ==> ~ (y<x)"; |
|
60 by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1); |
|
61 qed "order_less_not_sym"; |
|
62 |
|
63 (* [| n<m; ~P ==> m<n |] ==> P *) |
|
64 bind_thm ("order_less_asym", order_less_not_sym RS contrapos_np); |
|
65 |
|
66 (* Transitivity *) |
|
67 |
|
68 Goal "!!x::'a::order. [| x < y; y < z |] ==> x < z"; |
|
69 by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1); |
|
70 by (blast_tac (claset() addIs [order_trans,order_antisym]) 1); |
|
71 qed "order_less_trans"; |
|
72 |
|
73 Goal "!!x::'a::order. [| x <= y; y < z |] ==> x < z"; |
|
74 by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1); |
|
75 by (blast_tac (claset() addIs [order_trans,order_antisym]) 1); |
|
76 qed "order_le_less_trans"; |
|
77 |
|
78 Goal "!!x::'a::order. [| x < y; y <= z |] ==> x < z"; |
|
79 by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1); |
|
80 by (blast_tac (claset() addIs [order_trans,order_antisym]) 1); |
|
81 qed "order_less_le_trans"; |
|
82 |
|
83 |
|
84 (** Useful for simplification, but too risky to include by default. **) |
|
85 |
|
86 Goal "(x::'a::order) < y ==> (~ y < x) = True"; |
|
87 by (blast_tac (claset() addEs [order_less_asym]) 1); |
|
88 qed "order_less_imp_not_less"; |
|
89 |
|
90 Goal "(x::'a::order) < y ==> (y < x --> P) = True"; |
|
91 by (blast_tac (claset() addEs [order_less_asym]) 1); |
|
92 qed "order_less_imp_triv"; |
|
93 |
|
94 Goal "(x::'a::order) < y ==> (x = y) = False"; |
|
95 by Auto_tac; |
|
96 qed "order_less_imp_not_eq"; |
|
97 |
|
98 Goal "(x::'a::order) < y ==> (y = x) = False"; |
|
99 by Auto_tac; |
|
100 qed "order_less_imp_not_eq2"; |
|
101 |
|
102 |
|
103 (** min **) |
|
104 |
|
105 val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least"; |
|
106 by (simp_tac (simpset() addsimps prems) 1); |
|
107 qed "min_leastL"; |
|
108 |
|
109 val prems = Goalw [min_def] |
|
110 "(!!x::'a::order. least <= x) ==> min x least = least"; |
|
111 by (cut_facts_tac prems 1); |
|
112 by (Asm_simp_tac 1); |
|
113 by (blast_tac (claset() addIs [order_antisym]) 1); |
|
114 qed "min_leastR"; |
|
115 |
|
116 |
|
117 section "Linear/Total Orders"; |
|
118 |
|
119 Goal "!!x::'a::linorder. x<y | x=y | y<x"; |
|
120 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
|
121 by (cut_facts_tac [linorder_linear] 1); |
|
122 by (Blast_tac 1); |
|
123 qed "linorder_less_linear"; |
|
124 |
|
125 val prems = Goal "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P"; |
|
126 by (cut_facts_tac [linorder_less_linear] 1); |
|
127 by (REPEAT(eresolve_tac (prems@[disjE]) 1)); |
|
128 qed "linorder_less_split"; |
|
129 |
|
130 Goal "!!x::'a::linorder. (~ x < y) = (y <= x)"; |
|
131 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
|
132 by (cut_facts_tac [linorder_linear] 1); |
|
133 by (blast_tac (claset() addIs [order_antisym]) 1); |
|
134 qed "linorder_not_less"; |
|
135 |
|
136 Goal "!!x::'a::linorder. (~ x <= y) = (y < x)"; |
|
137 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
|
138 by (cut_facts_tac [linorder_linear] 1); |
|
139 by (blast_tac (claset() addIs [order_antisym]) 1); |
|
140 qed "linorder_not_le"; |
|
141 |
|
142 Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)"; |
|
143 by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1); |
|
144 by Auto_tac; |
|
145 qed "linorder_neq_iff"; |
|
146 |
|
147 (* eliminates ~= in premises *) |
|
148 bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE); |
|
149 |
|
150 (** min & max **) |
|
151 |
|
152 Goalw [min_def] "min (x::'a::order) x = x"; |
|
153 by (Simp_tac 1); |
|
154 qed "min_same"; |
|
155 Addsimps [min_same]; |
|
156 |
|
157 Goalw [max_def] "max (x::'a::order) x = x"; |
|
158 by (Simp_tac 1); |
|
159 qed "max_same"; |
|
160 Addsimps [max_same]; |
|
161 |
|
162 Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"; |
|
163 by (Simp_tac 1); |
|
164 by (cut_facts_tac [linorder_linear] 1); |
|
165 by (blast_tac (claset() addIs [order_trans]) 1); |
|
166 qed "le_max_iff_disj"; |
|
167 |
|
168 Goal "(x::'a::linorder) <= max x y"; |
|
169 by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1); |
|
170 qed "le_maxI1"; |
|
171 |
|
172 Goal "(y::'a::linorder) <= max x y"; |
|
173 by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1); |
|
174 qed "le_maxI2"; |
|
175 (*CANNOT use with AddSIs because blast_tac will give PROOF FAILED.*) |
|
176 |
|
177 Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"; |
|
178 by (simp_tac (simpset() addsimps [order_le_less]) 1); |
|
179 by (cut_facts_tac [linorder_less_linear] 1); |
|
180 by (blast_tac (claset() addIs [order_less_trans]) 1); |
|
181 qed "less_max_iff_disj"; |
|
182 |
|
183 Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"; |
|
184 by (Simp_tac 1); |
|
185 by (cut_facts_tac [linorder_linear] 1); |
|
186 by (blast_tac (claset() addIs [order_trans]) 1); |
|
187 qed "max_le_iff_conj"; |
|
188 Addsimps [max_le_iff_conj]; |
|
189 |
|
190 Goalw [max_def] "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"; |
|
191 by (simp_tac (simpset() addsimps [order_le_less]) 1); |
|
192 by (cut_facts_tac [linorder_less_linear] 1); |
|
193 by (blast_tac (claset() addIs [order_less_trans]) 1); |
|
194 qed "max_less_iff_conj"; |
|
195 Addsimps [max_less_iff_conj]; |
|
196 |
|
197 Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"; |
|
198 by (Simp_tac 1); |
|
199 by (cut_facts_tac [linorder_linear] 1); |
|
200 by (blast_tac (claset() addIs [order_trans]) 1); |
|
201 qed "le_min_iff_conj"; |
|
202 Addsimps [le_min_iff_conj]; |
|
203 (* AddIffs screws up a blast_tac in MiniML *) |
|
204 |
|
205 Goalw [min_def] "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"; |
|
206 by (simp_tac (simpset() addsimps [order_le_less]) 1); |
|
207 by (cut_facts_tac [linorder_less_linear] 1); |
|
208 by (blast_tac (claset() addIs [order_less_trans]) 1); |
|
209 qed "min_less_iff_conj"; |
|
210 Addsimps [min_less_iff_conj]; |
|
211 |
|
212 Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"; |
|
213 by (Simp_tac 1); |
|
214 by (cut_facts_tac [linorder_linear] 1); |
|
215 by (blast_tac (claset() addIs [order_trans]) 1); |
|
216 qed "min_le_iff_disj"; |
|
217 |
|
218 Goalw [min_def] "!!z::'a::linorder. (min x y < z) = (x < z | y < z)"; |
|
219 by (simp_tac (simpset() addsimps [order_le_less]) 1); |
|
220 by (cut_facts_tac [linorder_less_linear] 1); |
|
221 by (blast_tac (claset() addIs [order_less_trans]) 1); |
|
222 qed "min_less_iff_disj"; |
|
223 |
|
224 Goalw [min_def] |
|
225 "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"; |
|
226 by (Simp_tac 1); |
|
227 qed "split_min"; |
|
228 |
|
229 Goalw [max_def] |
|
230 "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))"; |
|
231 by (Simp_tac 1); |
|
232 qed "split_max"; |
|