author | wenzelm |
Mon, 03 Apr 2000 14:02:40 +0200 | |
changeset 8662 | f9679ddbc492 |
parent 8442 | 96023903c2df |
permissions | -rw-r--r-- |
7626 | 1 |
(* Title: HOL/BCV/Orders0.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1999 TUM |
|
5 |
*) |
|
6 |
||
7 |
(** option **) |
|
8 |
section "option"; |
|
9 |
||
10 |
Goalw [le_option] "(o1::('a::order)option) <= o1"; |
|
7961 | 11 |
by (simp_tac (simpset() addsplits [option.split]) 1); |
7626 | 12 |
qed "le_option_refl"; |
13 |
||
14 |
Goalw [le_option] "(o1::('a::order)option) <= o2 --> o2<=o3 --> o1<=o3"; |
|
7961 | 15 |
by (simp_tac (simpset() addsplits [option.split]) 1); |
16 |
by (blast_tac (claset() addIs [order_trans]) 1); |
|
7626 | 17 |
qed_spec_mp "le_option_trans"; |
18 |
||
19 |
Goalw [le_option] "(o1::('a::order)option) <= o2 --> o2<=o1 --> o1=o2"; |
|
7961 | 20 |
by (simp_tac (simpset() addsplits [option.split]) 1); |
21 |
by (blast_tac (claset() addIs [order_antisym]) 1); |
|
7626 | 22 |
qed_spec_mp "le_option_antisym"; |
23 |
||
24 |
Goalw [less_option] "(o1::('a::ord)option) < o2 = (o1<=o2 & o1 ~= o2)"; |
|
7961 | 25 |
by (rtac refl 1); |
7626 | 26 |
qed "less_le_option"; |
27 |
||
28 |
Goalw [le_option] "Some x <= opt = (? y. opt = Some y & x <= y)"; |
|
7961 | 29 |
by (simp_tac (simpset() addsplits [option.split]) 1); |
7626 | 30 |
qed_spec_mp "Some_le_conv"; |
31 |
AddIffs [Some_le_conv]; |
|
32 |
||
33 |
Goalw [le_option] "None <= opt"; |
|
7961 | 34 |
by (simp_tac (simpset() addsplits [option.split]) 1); |
7626 | 35 |
qed "None_le"; |
36 |
AddIffs [None_le]; |
|
37 |
||
38 |
||
39 |
(** list **) |
|
40 |
section "list"; |
|
41 |
||
42 |
Goalw [le_list] "[| xs <= ys; p < size xs |] ==> xs!p <= ys!p"; |
|
7961 | 43 |
by (Blast_tac 1); |
7626 | 44 |
qed "le_listD"; |
45 |
||
46 |
Goalw [le_list] "([] <= ys) = (ys = [])"; |
|
7961 | 47 |
by (Simp_tac 1); |
7626 | 48 |
qed "Nil_le_conv"; |
49 |
AddIffs [Nil_le_conv]; |
|
50 |
||
51 |
Goalw [le_list] "(xs::('a::order)list) <= xs"; |
|
7961 | 52 |
by (induct_tac "xs" 1); |
53 |
by (Auto_tac); |
|
7626 | 54 |
qed "le_list_refl"; |
55 |
||
56 |
Goalw [le_list] |
|
57 |
"!ys zs.(xs::('a::order)list) <= ys --> ys <= zs --> xs <= zs"; |
|
7961 | 58 |
by (induct_tac "xs" 1); |
59 |
by (Simp_tac 1); |
|
60 |
by (rtac allI 1); |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
61 |
by (case_tac "ys" 1); |
7961 | 62 |
by (hyp_subst_tac 1); |
63 |
by (Simp_tac 1); |
|
64 |
by (rtac allI 1); |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
65 |
by (case_tac "zs" 1); |
7961 | 66 |
by (hyp_subst_tac 1); |
67 |
by (Simp_tac 1); |
|
68 |
by (hyp_subst_tac 1); |
|
69 |
by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); |
|
70 |
by (Clarify_tac 1); |
|
71 |
by (rtac conjI 1); |
|
72 |
by (REPEAT(EVERY1[etac allE, etac conjE, etac impE, rtac refl])); |
|
73 |
by (blast_tac (claset() addIs [order_trans]) 1); |
|
74 |
by (Clarify_tac 1); |
|
75 |
by (EVERY[etac allE 1, etac allE 1, etac impE 1, etac impE 2]); |
|
76 |
by (rtac conjI 1); |
|
77 |
by (assume_tac 1); |
|
78 |
by (Blast_tac 1); |
|
79 |
by (rtac conjI 1); |
|
80 |
by (assume_tac 1); |
|
81 |
by (Blast_tac 1); |
|
82 |
by (Asm_full_simp_tac 1); |
|
7626 | 83 |
qed_spec_mp "le_list_trans"; |
84 |
||
85 |
Goalw [le_list] |
|
86 |
"!ys. (xs::('a::order)list) <= ys --> ys <= xs --> xs = ys"; |
|
7961 | 87 |
by (induct_tac "xs" 1); |
88 |
by (Simp_tac 1); |
|
89 |
by (rtac allI 1); |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
90 |
by (case_tac "ys" 1); |
7961 | 91 |
by (hyp_subst_tac 1); |
92 |
by (Simp_tac 1); |
|
93 |
by (hyp_subst_tac 1); |
|
94 |
by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); |
|
95 |
by (Clarify_tac 1); |
|
96 |
by (rtac conjI 1); |
|
97 |
by (blast_tac (claset() addIs [order_antisym]) 1); |
|
98 |
by (Asm_full_simp_tac 1); |
|
7626 | 99 |
qed_spec_mp "le_list_antisym"; |
100 |
||
101 |
Goalw [less_list] "(xs::('a::ord)list) < ys = (xs<=ys & xs ~= ys)"; |
|
7961 | 102 |
by (rtac refl 1); |
7626 | 103 |
qed "less_le_list"; |
104 |
||
105 |
(** product **) |
|
106 |
section "product"; |
|
107 |
||
108 |
Goalw [le_prod] "(p1::('a::order * 'b::order)) <= p1"; |
|
7961 | 109 |
by (Simp_tac 1); |
7626 | 110 |
qed "le_prod_refl"; |
111 |
||
112 |
Goalw [le_prod] |
|
113 |
"[| (p1::('a::order * 'b::order)) <= p2; p2<=p3 |] ==> p1<=p3"; |
|
7961 | 114 |
by (blast_tac (claset() addIs [order_trans]) 1); |
7626 | 115 |
qed "le_prod_trans"; |
116 |
||
117 |
Goalw [le_prod] |
|
118 |
"[| (p1::('a::order * 'b::order)) <= p2; p2 <= p1 |] ==> p1 = p2"; |
|
7961 | 119 |
by (blast_tac (claset() addIs [order_antisym,trans,surjective_pairing,sym]) 1); |
7626 | 120 |
qed_spec_mp "le_prod_antisym"; |
121 |
||
122 |
Goalw [less_prod] "(p1::('a::order * 'b::order)) < p2 = (p1<=p2 & p1 ~= p2)"; |
|
7961 | 123 |
by (rtac refl 1); |
7626 | 124 |
qed "less_le_prod"; |
125 |
||
126 |
Goalw [le_prod] "((a,b) <= (c,d)) = (a <= c & b <= d)"; |
|
7961 | 127 |
by (Simp_tac 1); |
7626 | 128 |
qed "le_prod_iff"; |
129 |
AddIffs [le_prod_iff]; |