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"; |
|
11 by (simp_tac (simpset() addsplits [option.split]) 1); |
|
12 qed "le_option_refl"; |
|
13 |
|
14 Goalw [le_option] "(o1::('a::order)option) <= o2 --> o2<=o3 --> o1<=o3"; |
|
15 by (simp_tac (simpset() addsplits [option.split]) 1); |
|
16 by (blast_tac (claset() addIs [order_trans]) 1); |
|
17 qed_spec_mp "le_option_trans"; |
|
18 |
|
19 Goalw [le_option] "(o1::('a::order)option) <= o2 --> o2<=o1 --> o1=o2"; |
|
20 by (simp_tac (simpset() addsplits [option.split]) 1); |
|
21 by (blast_tac (claset() addIs [order_antisym]) 1); |
|
22 qed_spec_mp "le_option_antisym"; |
|
23 |
|
24 Goalw [less_option] "(o1::('a::ord)option) < o2 = (o1<=o2 & o1 ~= o2)"; |
|
25 by (rtac refl 1); |
|
26 qed "less_le_option"; |
|
27 |
|
28 Goalw [le_option] "Some x <= opt = (? y. opt = Some y & x <= y)"; |
|
29 by (simp_tac (simpset() addsplits [option.split]) 1); |
|
30 qed_spec_mp "Some_le_conv"; |
|
31 AddIffs [Some_le_conv]; |
|
32 |
|
33 Goalw [le_option] "None <= opt"; |
|
34 by (simp_tac (simpset() addsplits [option.split]) 1); |
|
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"; |
|
43 by (Blast_tac 1); |
|
44 qed "le_listD"; |
|
45 |
|
46 Goalw [le_list] "([] <= ys) = (ys = [])"; |
|
47 by (Simp_tac 1); |
|
48 qed "Nil_le_conv"; |
|
49 AddIffs [Nil_le_conv]; |
|
50 |
|
51 Goalw [le_list] "(xs::('a::order)list) <= xs"; |
|
52 by (induct_tac "xs" 1); |
|
53 by (Auto_tac); |
|
54 qed "le_list_refl"; |
|
55 |
|
56 Goalw [le_list] |
|
57 "!ys zs.(xs::('a::order)list) <= ys --> ys <= zs --> xs <= zs"; |
|
58 by (induct_tac "xs" 1); |
|
59 by (Simp_tac 1); |
|
60 by (rtac allI 1); |
|
61 by (case_tac "ys" 1); |
|
62 by (hyp_subst_tac 1); |
|
63 by (Simp_tac 1); |
|
64 by (rtac allI 1); |
|
65 by (case_tac "zs" 1); |
|
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); |
|
83 qed_spec_mp "le_list_trans"; |
|
84 |
|
85 Goalw [le_list] |
|
86 "!ys. (xs::('a::order)list) <= ys --> ys <= xs --> xs = ys"; |
|
87 by (induct_tac "xs" 1); |
|
88 by (Simp_tac 1); |
|
89 by (rtac allI 1); |
|
90 by (case_tac "ys" 1); |
|
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); |
|
99 qed_spec_mp "le_list_antisym"; |
|
100 |
|
101 Goalw [less_list] "(xs::('a::ord)list) < ys = (xs<=ys & xs ~= ys)"; |
|
102 by (rtac refl 1); |
|
103 qed "less_le_list"; |
|
104 |
|
105 (** product **) |
|
106 section "product"; |
|
107 |
|
108 Goalw [le_prod] "(p1::('a::order * 'b::order)) <= p1"; |
|
109 by (Simp_tac 1); |
|
110 qed "le_prod_refl"; |
|
111 |
|
112 Goalw [le_prod] |
|
113 "[| (p1::('a::order * 'b::order)) <= p2; p2<=p3 |] ==> p1<=p3"; |
|
114 by (blast_tac (claset() addIs [order_trans]) 1); |
|
115 qed "le_prod_trans"; |
|
116 |
|
117 Goalw [le_prod] |
|
118 "[| (p1::('a::order * 'b::order)) <= p2; p2 <= p1 |] ==> p1 = p2"; |
|
119 by (blast_tac (claset() addIs [order_antisym,trans,surjective_pairing,sym]) 1); |
|
120 qed_spec_mp "le_prod_antisym"; |
|
121 |
|
122 Goalw [less_prod] "(p1::('a::order * 'b::order)) < p2 = (p1<=p2 & p1 ~= p2)"; |
|
123 by (rtac refl 1); |
|
124 qed "less_le_prod"; |
|
125 |
|
126 Goalw [le_prod] "((a,b) <= (c,d)) = (a <= c & b <= d)"; |
|
127 by (Simp_tac 1); |
|
128 qed "le_prod_iff"; |
|
129 AddIffs [le_prod_iff]; |
|