author | berghofe |
Fri, 24 Jul 1998 13:19:38 +0200 | |
changeset 5184 | 9b8547a9496a |
parent 5143 | b94cd208f073 |
child 5316 | 7a8975451a89 |
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 |
||
2608 | 9 |
(** mono **) |
923 | 10 |
|
11 |
val [prem] = goalw Ord.thy [mono_def] |
|
12 |
"[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
|
13 |
by (REPEAT (ares_tac [allI, impI, prem] 1)); |
|
14 |
qed "monoI"; |
|
15 |
||
16 |
val [major,minor] = goalw Ord.thy [mono_def] |
|
17 |
"[| mono(f); A <= B |] ==> f(A) <= f(B)"; |
|
18 |
by (rtac (major RS spec RS spec RS mp) 1); |
|
19 |
by (rtac minor 1); |
|
20 |
qed "monoD"; |
|
21 |
||
2608 | 22 |
|
23 |
section "Orders"; |
|
24 |
||
25 |
AddIffs [order_refl]; |
|
26 |
||
4600 | 27 |
(*This form is useful with the classical reasoner*) |
5069 | 28 |
Goal "!!x::'a::order. x = y ==> x <= y"; |
4600 | 29 |
by (etac ssubst 1); |
30 |
by (rtac order_refl 1); |
|
31 |
qed "order_eq_refl"; |
|
32 |
||
5069 | 33 |
Goal "~ x < (x::'a::order)"; |
4089 | 34 |
by (simp_tac (simpset() addsimps [order_less_le]) 1); |
2608 | 35 |
qed "order_less_irrefl"; |
36 |
AddIffs [order_less_irrefl]; |
|
37 |
||
5069 | 38 |
Goal "(x::'a::order) <= y = (x < y | x = y)"; |
4089 | 39 |
by (simp_tac (simpset() addsimps [order_less_le]) 1); |
2935 | 40 |
by (Blast_tac 1); |
2608 | 41 |
qed "order_le_less"; |
42 |
||
43 |
(** min **) |
|
44 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
45 |
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
|
46 |
by (simp_tac (simpset() addsimps prems) 1); |
2608 | 47 |
qed "min_leastL"; |
48 |
||
49 |
val prems = goalw thy [min_def] |
|
50 |
"(!!x::'a::order. least <= x) ==> min x least = least"; |
|
2935 | 51 |
by (cut_facts_tac prems 1); |
52 |
by (Asm_simp_tac 1); |
|
4089 | 53 |
by (blast_tac (claset() addIs [order_antisym]) 1); |
2608 | 54 |
qed "min_leastR"; |
4640 | 55 |
|
56 |
||
57 |
section "Linear/Total Orders"; |
|
58 |
||
5069 | 59 |
Goal "!!x::'a::linorder. x<y | x=y | y<x"; |
4640 | 60 |
by (simp_tac (simpset() addsimps [order_less_le]) 1); |
5132 | 61 |
by (cut_facts_tac [linorder_linear] 1); |
4640 | 62 |
by (Blast_tac 1); |
63 |
qed "linorder_less_linear"; |
|
64 |
||
5069 | 65 |
Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"; |
4686 | 66 |
by (Simp_tac 1); |
5132 | 67 |
by (cut_facts_tac [linorder_linear] 1); |
4640 | 68 |
by (blast_tac (claset() addIs [order_trans]) 1); |
69 |
qed "le_max_iff_disj"; |
|
70 |
||
5069 | 71 |
Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"; |
4686 | 72 |
by (Simp_tac 1); |
5132 | 73 |
by (cut_facts_tac [linorder_linear] 1); |
4640 | 74 |
by (blast_tac (claset() addIs [order_trans]) 1); |
75 |
qed "max_le_iff_conj"; |
|
76 |
||
5069 | 77 |
Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"; |
4686 | 78 |
by (Simp_tac 1); |
5132 | 79 |
by (cut_facts_tac [linorder_linear] 1); |
4640 | 80 |
by (blast_tac (claset() addIs [order_trans]) 1); |
81 |
qed "le_min_iff_conj"; |
|
82 |
||
5069 | 83 |
Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"; |
4686 | 84 |
by (Simp_tac 1); |
5132 | 85 |
by (cut_facts_tac [linorder_linear] 1); |
4640 | 86 |
by (blast_tac (claset() addIs [order_trans]) 1); |
87 |
qed "min_le_iff_disj"; |
|
88 |
||
89 |