7626
|
1 |
(* Title: HOL/BCV/Orders.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1999 TUM
|
|
5 |
*)
|
|
6 |
|
|
7 |
Delrules[le_maxI1, le_maxI2];
|
|
8 |
|
|
9 |
(** option **)
|
|
10 |
section "option";
|
|
11 |
|
|
12 |
Goalw [option_def] "None : option A";
|
7961
|
13 |
by (Simp_tac 1);
|
7626
|
14 |
qed "None_in_option";
|
|
15 |
AddIffs [None_in_option];
|
|
16 |
|
|
17 |
Goalw [option_def] "(Some x : option A) = (x:A)";
|
7961
|
18 |
by (Auto_tac);
|
7626
|
19 |
qed "Some_in_option";
|
|
20 |
AddIffs [Some_in_option];
|
|
21 |
|
|
22 |
Goalw [less_option,le_option]
|
|
23 |
"Some x < opt = (? y. opt = Some y & x < (y::'a::order))";
|
7961
|
24 |
by (simp_tac (simpset() addsimps [order_less_le] addsplits [option.split]) 1);
|
7626
|
25 |
qed_spec_mp "Some_less_conv";
|
|
26 |
AddIffs [Some_less_conv];
|
|
27 |
|
|
28 |
Goalw [less_option,le_option] "None < x = (? a. x = Some a)";
|
7961
|
29 |
by (asm_simp_tac (simpset() addsplits [option.split]) 1);
|
7626
|
30 |
qed_spec_mp "None_less_iff";
|
|
31 |
AddIffs [None_less_iff];
|
|
32 |
|
|
33 |
|
|
34 |
Goalw [acc_def] "acc A ==> acc(option A)";
|
7961
|
35 |
by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
|
|
36 |
by (Clarify_tac 1);
|
|
37 |
by (case_tac "? a. Some a : Q" 1);
|
|
38 |
by (eres_inst_tac [("x","{a . Some a : Q}")] allE 1);
|
|
39 |
by (Blast_tac 1);
|
8423
|
40 |
by (cases_tac "x" 1);
|
7961
|
41 |
by (Fast_tac 1);
|
|
42 |
by (Blast_tac 1);
|
7626
|
43 |
qed "acc_option";
|
|
44 |
Addsimps [acc_option];
|
|
45 |
AddSIs [acc_option];
|
|
46 |
|
|
47 |
|
|
48 |
(** list **)
|
|
49 |
section "list";
|
|
50 |
|
|
51 |
Goalw [le_list] "~ [] <= x#xs";
|
7961
|
52 |
by (Simp_tac 1);
|
7626
|
53 |
qed "Nil_notle_Cons";
|
|
54 |
|
|
55 |
Goalw [le_list] "~ x#xs <= []";
|
7961
|
56 |
by (Simp_tac 1);
|
7626
|
57 |
qed "Cons_notle_Nil";
|
|
58 |
|
|
59 |
AddIffs [Nil_notle_Cons,Cons_notle_Nil];
|
|
60 |
|
|
61 |
Goalw [le_list] "x#xs <= y#ys = (x <= y & xs <= ys)";
|
7961
|
62 |
by (rtac iffI 1);
|
|
63 |
by (Asm_full_simp_tac 1);
|
|
64 |
by (Clarify_tac 1);
|
|
65 |
by (rtac conjI 1);
|
|
66 |
by (eres_inst_tac [("x","0")] allE 1);
|
|
67 |
by (Asm_full_simp_tac 1);
|
|
68 |
by (Clarify_tac 1);
|
|
69 |
by (eres_inst_tac [("x","Suc i")] allE 1);
|
|
70 |
by (Asm_full_simp_tac 1);
|
|
71 |
by (Asm_full_simp_tac 1);
|
|
72 |
by (Clarify_tac 1);
|
8423
|
73 |
by (cases_tac "i" 1);
|
7961
|
74 |
by (ALLGOALS Asm_simp_tac);
|
7626
|
75 |
qed "Cons_le_Cons";
|
|
76 |
AddIffs [Cons_le_Cons];
|
|
77 |
|
|
78 |
Goal "(x#xs <= ys) = (? z zs. ys = z#zs & x <= z & xs <= zs)";
|
8423
|
79 |
by (cases_tac "ys" 1);
|
7961
|
80 |
by (ALLGOALS Asm_simp_tac);
|
7626
|
81 |
qed "Cons_le_iff";
|
|
82 |
|
|
83 |
Goal "(xs <= y#ys) = (? z zs. xs = z#zs & z <= y & zs <= ys)";
|
8423
|
84 |
by (cases_tac "xs" 1);
|
7961
|
85 |
by (ALLGOALS Asm_simp_tac);
|
7626
|
86 |
qed "le_Cons_iff";
|
|
87 |
|
|
88 |
Goalw [less_list]
|
|
89 |
"x#xs < y#ys = (x < (y::'a::order) & xs <= ys | x = y & xs < ys)";
|
7961
|
90 |
by (simp_tac (simpset() addsimps [order_less_le]) 1);
|
|
91 |
by (Blast_tac 1);
|
7626
|
92 |
qed "Cons_less_Cons";
|
|
93 |
AddIffs [Cons_less_Cons];
|
|
94 |
|
|
95 |
Goalw [le_list]
|
|
96 |
"[| i<size xs; xs <= ys; x <= y |] ==> xs[i:=x] <= ys[i:=y]";
|
7961
|
97 |
by (asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
|
7626
|
98 |
qed "list_update_le_cong";
|
|
99 |
|
|
100 |
Goal "!i < length xs. (xs[i := x] <= xs) = ((x::'a::order) <= xs!i)";
|
7961
|
101 |
by (induct_tac "xs" 1);
|
|
102 |
by (Simp_tac 1);
|
|
103 |
by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
|
7626
|
104 |
qed_spec_mp "list_update_le_conv";
|
|
105 |
|
|
106 |
Goalw [listsn_def] "xs : listsn n A ==> length xs = n";
|
7961
|
107 |
by (Blast_tac 1);
|
7626
|
108 |
qed "listsnE_length";
|
|
109 |
Addsimps [listsnE_length];
|
|
110 |
|
|
111 |
Goalw [listsn_def] "xs : listsn n A ==> set xs <= A";
|
7961
|
112 |
by (Blast_tac 1);
|
7626
|
113 |
qed "listsnE_set";
|
|
114 |
Addsimps [listsnE_set];
|
|
115 |
|
|
116 |
Goalw [listsn_def] "listsn 0 A = {[]}";
|
7961
|
117 |
by (Auto_tac);
|
7626
|
118 |
qed "listsn_0";
|
|
119 |
Addsimps [listsn_0];
|
|
120 |
|
|
121 |
Goalw [listsn_def]
|
|
122 |
"(xs : listsn (Suc n) A) = (? y:A. ? ys:listsn n A. xs = y#ys)";
|
8423
|
123 |
by (cases_tac "xs" 1);
|
7961
|
124 |
by (Auto_tac);
|
7626
|
125 |
qed "in_listsn_Suc_iff";
|
|
126 |
|
|
127 |
|
|
128 |
Goal "? a. a:A ==> ? xs. xs : listsn n A";
|
7961
|
129 |
by (induct_tac "n" 1);
|
|
130 |
by (Simp_tac 1);
|
|
131 |
by (asm_simp_tac (simpset() addsimps [in_listsn_Suc_iff]) 1);
|
|
132 |
by (Blast_tac 1);
|
7626
|
133 |
qed "listsn_not_empty";
|
|
134 |
|
|
135 |
|
|
136 |
Goal "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A";
|
7961
|
137 |
by (induct_tac "xs" 1);
|
|
138 |
by (Simp_tac 1);
|
|
139 |
by (asm_full_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
|
7626
|
140 |
qed_spec_mp "nth_in";
|
|
141 |
Addsimps [nth_in];
|
|
142 |
|
|
143 |
Goal "[| xs : listsn n A; i < n |] ==> (xs!i) : A";
|
7961
|
144 |
by (blast_tac (HOL_cs addIs [nth_in,listsnE_length,listsnE_set]) 1);
|
7626
|
145 |
qed "listsnE_nth_in";
|
|
146 |
|
|
147 |
Goalw [listsn_def]
|
|
148 |
"[| xs : listsn n A; x:A; i < n |] ==> xs[i := x] : listsn n A";
|
7961
|
149 |
by (Asm_full_simp_tac 1);
|
8288
|
150 |
by (blast_tac (claset() addDs [set_update_subset_insert RS subsetD]) 1);
|
7626
|
151 |
qed "list_update_in_listsn";
|
|
152 |
Addsimps [list_update_in_listsn];
|
|
153 |
AddSIs [list_update_in_listsn];
|
|
154 |
|
|
155 |
|
|
156 |
Goalw [acc_def] "acc(A) ==> acc(listsn n A)";
|
7961
|
157 |
by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
|
|
158 |
by (induct_tac "n" 1);
|
|
159 |
by (simp_tac (simpset() addcongs [conj_cong]) 1);
|
|
160 |
by (simp_tac (simpset() addsimps [in_listsn_Suc_iff]) 1);
|
|
161 |
by (Clarify_tac 1);
|
|
162 |
by (rename_tac "M m" 1);
|
|
163 |
by (case_tac "? x xs. x:A & xs:listsn n A & x#xs : M" 1);
|
|
164 |
by (etac thin_rl 2);
|
|
165 |
by (etac thin_rl 2);
|
|
166 |
by (Blast_tac 2);
|
|
167 |
by (eres_inst_tac [("x","{a. a:A & (? xs. xs:listsn n A & a#xs:M)}")] allE 1);
|
|
168 |
by (etac impE 1);
|
|
169 |
by (Blast_tac 1);
|
|
170 |
by (thin_tac "? x xs. ?P x xs" 1);
|
|
171 |
by (Clarify_tac 1);
|
|
172 |
by (rename_tac "maxA xs" 1);
|
|
173 |
by (eres_inst_tac [("x","{xs. xs:listsn n A & maxA#xs : M}")] allE 1);
|
|
174 |
by (Blast_tac 1);
|
7626
|
175 |
qed "acc_listsn";
|
|
176 |
Addsimps [acc_listsn];
|
|
177 |
AddSIs [acc_listsn];
|