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";
|
|
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 |
br 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 |
br allI 1;
|
|
61 |
by(exhaust_tac "ys" 1);
|
|
62 |
by(hyp_subst_tac 1);
|
|
63 |
by(Simp_tac 1);
|
|
64 |
br allI 1;
|
|
65 |
by(exhaust_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 |
br 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 |
br conjI 1;
|
|
77 |
ba 1;
|
|
78 |
by(Blast_tac 1);
|
|
79 |
br conjI 1;
|
|
80 |
ba 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 |
br allI 1;
|
|
90 |
by(exhaust_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 |
br 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 |
br 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 |
br 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];
|