author | wenzelm |
Sat, 21 Nov 1998 12:17:18 +0100 | |
changeset 5944 | dcc446da8e19 |
parent 5673 | 5dc45f449198 |
child 6073 | fba734ba6894 |
permissions | -rw-r--r-- |
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 |
||
5449
d853d1ac85a3
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents:
5316
diff
changeset
|
30 |
Addsimps [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 |
||
58 |
||
59 |
(** Useful for simplification, but too risky to include by default. **) |
|
60 |
||
61 |
Goal "(x::'a::order) < y ==> (~ y < x) = True"; |
|
62 |
by (blast_tac (claset() addEs [order_less_asym]) 1); |
|
63 |
qed "order_less_imp_not_less"; |
|
64 |
||
65 |
Goal "(x::'a::order) < y ==> (y < x --> P) = True"; |
|
66 |
by (blast_tac (claset() addEs [order_less_asym]) 1); |
|
67 |
qed "order_less_imp_triv"; |
|
68 |
||
69 |
Goal "(x::'a::order) < y ==> (x = y) = False"; |
|
70 |
by Auto_tac; |
|
71 |
qed "order_less_imp_not_eq"; |
|
72 |
||
73 |
Goal "(x::'a::order) < y ==> (y = x) = False"; |
|
74 |
by Auto_tac; |
|
75 |
qed "order_less_imp_not_eq2"; |
|
76 |
||
77 |
||
2608 | 78 |
(** min **) |
79 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
80 |
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
|
81 |
by (simp_tac (simpset() addsimps prems) 1); |
2608 | 82 |
qed "min_leastL"; |
83 |
||
5316 | 84 |
val prems = Goalw [min_def] |
2608 | 85 |
"(!!x::'a::order. least <= x) ==> min x least = least"; |
2935 | 86 |
by (cut_facts_tac prems 1); |
87 |
by (Asm_simp_tac 1); |
|
4089 | 88 |
by (blast_tac (claset() addIs [order_antisym]) 1); |
2608 | 89 |
qed "min_leastR"; |
4640 | 90 |
|
91 |
||
92 |
section "Linear/Total Orders"; |
|
93 |
||
5069 | 94 |
Goal "!!x::'a::linorder. x<y | x=y | y<x"; |
4640 | 95 |
by (simp_tac (simpset() addsimps [order_less_le]) 1); |
5132 | 96 |
by (cut_facts_tac [linorder_linear] 1); |
4640 | 97 |
by (Blast_tac 1); |
98 |
qed "linorder_less_linear"; |
|
99 |
||
5069 | 100 |
Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"; |
4686 | 101 |
by (Simp_tac 1); |
5132 | 102 |
by (cut_facts_tac [linorder_linear] 1); |
4640 | 103 |
by (blast_tac (claset() addIs [order_trans]) 1); |
104 |
qed "le_max_iff_disj"; |
|
105 |
||
5069 | 106 |
Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"; |
4686 | 107 |
by (Simp_tac 1); |
5132 | 108 |
by (cut_facts_tac [linorder_linear] 1); |
4640 | 109 |
by (blast_tac (claset() addIs [order_trans]) 1); |
110 |
qed "max_le_iff_conj"; |
|
5673 | 111 |
Addsimps [max_le_iff_conj]; |
4640 | 112 |
|
5069 | 113 |
Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"; |
4686 | 114 |
by (Simp_tac 1); |
5132 | 115 |
by (cut_facts_tac [linorder_linear] 1); |
4640 | 116 |
by (blast_tac (claset() addIs [order_trans]) 1); |
117 |
qed "le_min_iff_conj"; |
|
5673 | 118 |
Addsimps [le_min_iff_conj]; |
119 |
(* AddIffs screws up a blast_tac in MiniML *) |
|
4640 | 120 |
|
5069 | 121 |
Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"; |
4686 | 122 |
by (Simp_tac 1); |
5132 | 123 |
by (cut_facts_tac [linorder_linear] 1); |
4640 | 124 |
by (blast_tac (claset() addIs [order_trans]) 1); |
125 |
qed "min_le_iff_disj"; |
|
126 |
||
5625 | 127 |
Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)"; |
128 |
by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1); |
|
129 |
by Auto_tac; |
|
130 |
qed "linorder_neq_iff"; |
|
4640 | 131 |
|
5625 | 132 |
(*** eliminates ~= in premises ***) |
133 |
bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE); |