author | wenzelm |
Wed, 08 May 2002 12:15:30 +0200 | |
changeset 13122 | c63612ffb186 |
parent 13114 | f2b00262bdfc |
child 13124 | 6e1decd8a7a9 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/List.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1994 TU Muenchen |
|
5 |
*) |
|
6 |
||
13114 | 7 |
header {* The datatype of finite lists *} |
13122 | 8 |
|
9 |
theory List = PreList: |
|
923 | 10 |
|
13114 | 11 |
datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) |
923 | 12 |
|
13 |
consts |
|
13114 | 14 |
"@" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr 65) |
15 |
filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
16 |
concat :: "'a list list \<Rightarrow> 'a list" |
|
17 |
foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" |
|
18 |
foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" |
|
19 |
hd :: "'a list \<Rightarrow> 'a" |
|
20 |
tl :: "'a list \<Rightarrow> 'a list" |
|
21 |
last :: "'a list \<Rightarrow> 'a" |
|
22 |
butlast :: "'a list \<Rightarrow> 'a list" |
|
23 |
set :: "'a list \<Rightarrow> 'a set" |
|
24 |
list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)" |
|
25 |
list_all2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool" |
|
26 |
map :: "('a\<Rightarrow>'b) \<Rightarrow> ('a list \<Rightarrow> 'b list)" |
|
27 |
mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl 55) |
|
28 |
nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100) |
|
29 |
list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" |
|
30 |
take :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
31 |
drop :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
32 |
takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
33 |
dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
34 |
rev :: "'a list \<Rightarrow> 'a list" |
|
35 |
zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list" |
|
36 |
upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_../_'(])") |
|
37 |
remdups :: "'a list \<Rightarrow> 'a list" |
|
38 |
null :: "'a list \<Rightarrow> bool" |
|
39 |
"distinct" :: "'a list \<Rightarrow> bool" |
|
40 |
replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" |
|
923 | 41 |
|
5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
nipkow
parents:
4643
diff
changeset
|
42 |
nonterminals |
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
nipkow
parents:
4643
diff
changeset
|
43 |
lupdbinds lupdbind |
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
nipkow
parents:
4643
diff
changeset
|
44 |
|
923 | 45 |
syntax |
46 |
(* list Enumeration *) |
|
13114 | 47 |
"@list" :: "args \<Rightarrow> 'a list" ("[(_)]") |
923 | 48 |
|
2512 | 49 |
(* Special syntax for filter *) |
13114 | 50 |
"@filter" :: "[pttrn, 'a list, bool] \<Rightarrow> 'a list" ("(1[_:_./ _])") |
923 | 51 |
|
5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
nipkow
parents:
4643
diff
changeset
|
52 |
(* list update *) |
13114 | 53 |
"_lupdbind" :: "['a, 'a] \<Rightarrow> lupdbind" ("(2_ :=/ _)") |
54 |
"" :: "lupdbind \<Rightarrow> lupdbinds" ("_") |
|
55 |
"_lupdbinds" :: "[lupdbind, lupdbinds] \<Rightarrow> lupdbinds" ("_,/ _") |
|
56 |
"_LUpdate" :: "['a, lupdbinds] \<Rightarrow> 'a" ("_/[(_)]" [900,0] 900) |
|
5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
nipkow
parents:
4643
diff
changeset
|
57 |
|
13114 | 58 |
upto :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_../_])") |
5427 | 59 |
|
923 | 60 |
translations |
61 |
"[x, xs]" == "x#[xs]" |
|
62 |
"[x]" == "x#[]" |
|
3842 | 63 |
"[x:xs . P]" == "filter (%x. P) xs" |
923 | 64 |
|
5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
nipkow
parents:
4643
diff
changeset
|
65 |
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs" |
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
nipkow
parents:
4643
diff
changeset
|
66 |
"xs[i:=x]" == "list_update xs i x" |
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
nipkow
parents:
4643
diff
changeset
|
67 |
|
5427 | 68 |
"[i..j]" == "[i..(Suc j)(]" |
69 |
||
70 |
||
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
10832
diff
changeset
|
71 |
syntax (xsymbols) |
13114 | 72 |
"@filter" :: "[pttrn, 'a list, bool] \<Rightarrow> 'a list" ("(1[_\<in>_ ./ _])") |
2262 | 73 |
|
74 |
||
3342
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset
|
75 |
consts |
13114 | 76 |
lists :: "'a set \<Rightarrow> 'a list set" |
3342
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset
|
77 |
|
13114 | 78 |
inductive "lists A" |
79 |
intros |
|
80 |
Nil: "[]: lists A" |
|
81 |
Cons: "\<lbrakk> a: A; l: lists A \<rbrakk> \<Longrightarrow> a#l : lists A" |
|
3342
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset
|
82 |
|
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset
|
83 |
|
3437
bea2faf1641d
Replacing the primrec definition of "length" by a translation to the built-in
paulson
parents:
3401
diff
changeset
|
84 |
(*Function "size" is overloaded for all datatypes. Users may refer to the |
bea2faf1641d
Replacing the primrec definition of "length" by a translation to the built-in
paulson
parents:
3401
diff
changeset
|
85 |
list version as "length".*) |
13114 | 86 |
syntax length :: "'a list \<Rightarrow> nat" |
87 |
translations "length" => "size:: _ list \<Rightarrow> nat" |
|
88 |
||
89 |
(* translating size::list -> length *) |
|
90 |
typed_print_translation |
|
91 |
{* |
|
92 |
let |
|
93 |
fun size_tr' _ (Type ("fun", (Type ("list", _) :: _))) [t] = |
|
94 |
Syntax.const "length" $ t |
|
95 |
| size_tr' _ _ _ = raise Match; |
|
96 |
in [("size", size_tr')] end |
|
97 |
*} |
|
3437
bea2faf1641d
Replacing the primrec definition of "length" by a translation to the built-in
paulson
parents:
3401
diff
changeset
|
98 |
|
5183 | 99 |
primrec |
1898 | 100 |
"hd(x#xs) = x" |
5183 | 101 |
primrec |
8972 | 102 |
"tl([]) = []" |
1898 | 103 |
"tl(x#xs) = xs" |
5183 | 104 |
primrec |
8972 | 105 |
"null([]) = True" |
106 |
"null(x#xs) = False" |
|
107 |
primrec |
|
3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3842
diff
changeset
|
108 |
"last(x#xs) = (if xs=[] then x else last xs)" |
5183 | 109 |
primrec |
8972 | 110 |
"butlast [] = []" |
3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3842
diff
changeset
|
111 |
"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" |
5183 | 112 |
primrec |
8972 | 113 |
"x mem [] = False" |
5518 | 114 |
"x mem (y#ys) = (if y=x then True else x mem ys)" |
115 |
primrec |
|
3465 | 116 |
"set [] = {}" |
117 |
"set (x#xs) = insert x (set xs)" |
|
5183 | 118 |
primrec |
13114 | 119 |
list_all_Nil: "list_all P [] = True" |
120 |
list_all_Cons: "list_all P (x#xs) = (P(x) & list_all P xs)" |
|
5518 | 121 |
primrec |
8972 | 122 |
"map f [] = []" |
1898 | 123 |
"map f (x#xs) = f(x)#map f xs" |
5183 | 124 |
primrec |
13114 | 125 |
append_Nil: "[] @ys = ys" |
126 |
append_Cons: "(x#xs)@ys = x#(xs@ys)" |
|
5183 | 127 |
primrec |
8972 | 128 |
"rev([]) = []" |
1898 | 129 |
"rev(x#xs) = rev(xs) @ [x]" |
5183 | 130 |
primrec |
8972 | 131 |
"filter P [] = []" |
1898 | 132 |
"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" |
5183 | 133 |
primrec |
13114 | 134 |
foldl_Nil: "foldl f a [] = a" |
135 |
foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs" |
|
5183 | 136 |
primrec |
8972 | 137 |
"foldr f [] a = a" |
8000 | 138 |
"foldr f (x#xs) a = f x (foldr f xs a)" |
139 |
primrec |
|
8972 | 140 |
"concat([]) = []" |
2608 | 141 |
"concat(x#xs) = x @ concat(xs)" |
5183 | 142 |
primrec |
13114 | 143 |
drop_Nil: "drop n [] = []" |
144 |
drop_Cons: "drop n (x#xs) = (case n of 0 \<Rightarrow> x#xs | Suc(m) \<Rightarrow> drop m xs)" |
|
6408 | 145 |
(* Warning: simpset does not contain this definition but separate theorems |
146 |
for n=0 / n=Suc k*) |
|
5183 | 147 |
primrec |
13114 | 148 |
take_Nil: "take n [] = []" |
149 |
take_Cons: "take n (x#xs) = (case n of 0 \<Rightarrow> [] | Suc(m) \<Rightarrow> x # take m xs)" |
|
6408 | 150 |
(* Warning: simpset does not contain this definition but separate theorems |
151 |
for n=0 / n=Suc k*) |
|
152 |
primrec |
|
13114 | 153 |
nth_Cons: "(x#xs)!n = (case n of 0 \<Rightarrow> x | (Suc k) \<Rightarrow> xs!k)" |
6408 | 154 |
(* Warning: simpset does not contain this definition but separate theorems |
155 |
for n=0 / n=Suc k*) |
|
5183 | 156 |
primrec |
5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
nipkow
parents:
4643
diff
changeset
|
157 |
" [][i:=v] = []" |
13114 | 158 |
"(x#xs)[i:=v] = (case i of 0 \<Rightarrow> v # xs |
159 |
| Suc j \<Rightarrow> x # xs[j:=v])" |
|
5183 | 160 |
primrec |
8972 | 161 |
"takeWhile P [] = []" |
2608 | 162 |
"takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" |
5183 | 163 |
primrec |
8972 | 164 |
"dropWhile P [] = []" |
3584
8f9ee0f79d9a
Corected bug in def of dropWhile (also present in Haskell lib!)
nipkow
parents:
3507
diff
changeset
|
165 |
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" |
5183 | 166 |
primrec |
4132 | 167 |
"zip xs [] = []" |
13114 | 168 |
zip_Cons: |
169 |
"zip xs (y#ys) = (case xs of [] \<Rightarrow> [] | z#zs \<Rightarrow> (z,y)#zip zs ys)" |
|
6408 | 170 |
(* Warning: simpset does not contain this definition but separate theorems |
171 |
for xs=[] / xs=z#zs *) |
|
5427 | 172 |
primrec |
13114 | 173 |
upt_0: "[i..0(] = []" |
174 |
upt_Suc: "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])" |
|
5183 | 175 |
primrec |
12887 | 176 |
"distinct [] = True" |
177 |
"distinct (x#xs) = (x ~: set xs & distinct xs)" |
|
5183 | 178 |
primrec |
4605 | 179 |
"remdups [] = []" |
180 |
"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" |
|
5183 | 181 |
primrec |
13114 | 182 |
replicate_0: "replicate 0 x = []" |
183 |
replicate_Suc: "replicate (Suc n) x = x # replicate n x" |
|
8115 | 184 |
defs |
13114 | 185 |
list_all2_def: |
8115 | 186 |
"list_all2 P xs ys == length xs = length ys & (!(x,y):set(zip xs ys). P x y)" |
187 |
||
3196 | 188 |
|
6408 | 189 |
(** Lexicographic orderings on lists **) |
5281 | 190 |
|
191 |
consts |
|
13114 | 192 |
lexn :: "('a * 'a)set \<Rightarrow> nat \<Rightarrow> ('a list * 'a list)set" |
5281 | 193 |
primrec |
194 |
"lexn r 0 = {}" |
|
10832 | 195 |
"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int |
5281 | 196 |
{(xs,ys). length xs = Suc n & length ys = Suc n}" |
197 |
||
198 |
constdefs |
|
13114 | 199 |
lex :: "('a * 'a)set \<Rightarrow> ('a list * 'a list)set" |
9336 | 200 |
"lex r == UN n. lexn r n" |
5281 | 201 |
|
13114 | 202 |
lexico :: "('a * 'a)set \<Rightarrow> ('a list * 'a list)set" |
9336 | 203 |
"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))" |
204 |
||
13114 | 205 |
sublist :: "['a list, nat set] \<Rightarrow> 'a list" |
9336 | 206 |
"sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..size xs(]))" |
5281 | 207 |
|
13114 | 208 |
|
209 |
lemma not_Cons_self[simp]: "\<And>x. xs ~= x#xs" |
|
210 |
by(induct_tac "xs", auto) |
|
211 |
||
212 |
lemmas not_Cons_self2[simp] = not_Cons_self[THEN not_sym] |
|
213 |
||
13122 | 214 |
lemma neq_Nil_conv: "(xs ~= []) = (? y ys. xs = y#ys)" |
13114 | 215 |
by(induct_tac "xs", auto) |
216 |
||
217 |
(* Induction over the length of a list: *) |
|
218 |
(* "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)" *) |
|
219 |
lemmas length_induct = measure_induct[of length] |
|
220 |
||
221 |
||
222 |
(** "lists": the list-forming operator over sets **) |
|
223 |
||
224 |
lemma lists_mono: "A<=B ==> lists A <= lists B" |
|
225 |
apply(unfold lists.defs) |
|
226 |
apply(blast intro!:lfp_mono) |
|
227 |
done |
|
228 |
||
229 |
inductive_cases listsE[elim!]: "x#l : lists A" |
|
230 |
declare lists.intros[intro!] |
|
231 |
||
232 |
lemma lists_IntI[rule_format]: |
|
13122 | 233 |
"l: lists A ==> l: lists B --> l: lists (A Int B)" |
13114 | 234 |
apply(erule lists.induct) |
235 |
apply blast+ |
|
236 |
done |
|
237 |
||
238 |
lemma lists_Int_eq[simp]: "lists (A Int B) = lists A Int lists B" |
|
239 |
apply(rule mono_Int[THEN equalityI]) |
|
240 |
apply(simp add:mono_def lists_mono) |
|
241 |
apply(blast intro!: lists_IntI) |
|
242 |
done |
|
243 |
||
244 |
lemma append_in_lists_conv[iff]: |
|
245 |
"(xs@ys : lists A) = (xs : lists A & ys : lists A)" |
|
246 |
by(induct_tac "xs", auto) |
|
247 |
||
248 |
(** length **) |
|
249 |
(* needs to come before "@" because of thm append_eq_append_conv *) |
|
250 |
||
251 |
section "length" |
|
252 |
||
253 |
lemma length_append[simp]: "length(xs@ys) = length(xs)+length(ys)" |
|
254 |
by(induct_tac "xs", auto) |
|
255 |
||
256 |
lemma length_map[simp]: "length (map f xs) = length xs" |
|
257 |
by(induct_tac "xs", auto) |
|
258 |
||
259 |
lemma length_rev[simp]: "length(rev xs) = length(xs)" |
|
260 |
by(induct_tac "xs", auto) |
|
261 |
||
262 |
lemma length_tl[simp]: "length(tl xs) = (length xs) - 1" |
|
263 |
by(case_tac "xs", auto) |
|
264 |
||
265 |
lemma length_0_conv[iff]: "(length xs = 0) = (xs = [])" |
|
266 |
by(induct_tac "xs", auto) |
|
267 |
||
268 |
lemma length_greater_0_conv[iff]: "(0 < length xs) = (xs ~= [])" |
|
269 |
by(induct_tac xs, auto) |
|
270 |
||
271 |
lemma length_Suc_conv: |
|
272 |
"(length xs = Suc n) = (? y ys. xs = y#ys & length ys = n)" |
|
273 |
by(induct_tac "xs", auto) |
|
274 |
||
275 |
(** @ - append **) |
|
276 |
||
277 |
section "@ - append" |
|
278 |
||
279 |
lemma append_assoc[simp]: "(xs@ys)@zs = xs@(ys@zs)" |
|
280 |
by(induct_tac "xs", auto) |
|
3507 | 281 |
|
13114 | 282 |
lemma append_Nil2[simp]: "xs @ [] = xs" |
283 |
by(induct_tac "xs", auto) |
|
284 |
||
285 |
lemma append_is_Nil_conv[iff]: "(xs@ys = []) = (xs=[] & ys=[])" |
|
286 |
by(induct_tac "xs", auto) |
|
287 |
||
288 |
lemma Nil_is_append_conv[iff]: "([] = xs@ys) = (xs=[] & ys=[])" |
|
289 |
by(induct_tac "xs", auto) |
|
290 |
||
291 |
lemma append_self_conv[iff]: "(xs @ ys = xs) = (ys=[])" |
|
292 |
by(induct_tac "xs", auto) |
|
293 |
||
294 |
lemma self_append_conv[iff]: "(xs = xs @ ys) = (ys=[])" |
|
295 |
by(induct_tac "xs", auto) |
|
296 |
||
297 |
lemma append_eq_append_conv[rule_format,simp]: |
|
298 |
"!ys. length xs = length ys | length us = length vs |
|
299 |
--> (xs@us = ys@vs) = (xs=ys & us=vs)" |
|
300 |
apply(induct_tac "xs") |
|
301 |
apply(rule allI) |
|
302 |
apply(case_tac "ys") |
|
303 |
apply simp |
|
304 |
apply force |
|
305 |
apply(rule allI) |
|
306 |
apply(case_tac "ys") |
|
307 |
apply force |
|
308 |
apply simp |
|
309 |
done |
|
310 |
||
311 |
lemma same_append_eq[iff]: "(xs @ ys = xs @ zs) = (ys=zs)" |
|
312 |
by simp |
|
313 |
||
314 |
lemma append1_eq_conv[iff]: "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)" |
|
315 |
by simp |
|
316 |
||
317 |
lemma append_same_eq[iff]: "(ys @ xs = zs @ xs) = (ys=zs)" |
|
318 |
by simp |
|
3507 | 319 |
|
13114 | 320 |
lemma append_self_conv2[iff]: "(xs @ ys = ys) = (xs=[])" |
321 |
by(insert append_same_eq[of _ _ "[]"], auto) |
|
322 |
||
323 |
lemma self_append_conv2[iff]: "(ys = xs @ ys) = (xs=[])" |
|
324 |
by(auto simp add: append_same_eq[of "[]", simplified]) |
|
325 |
||
326 |
lemma hd_Cons_tl[rule_format,simp]: "xs ~= [] --> hd xs # tl xs = xs" |
|
327 |
by(induct_tac "xs", auto) |
|
328 |
||
329 |
lemma hd_append: "hd(xs@ys) = (if xs=[] then hd ys else hd xs)" |
|
330 |
by(induct_tac "xs", auto) |
|
331 |
||
332 |
lemma hd_append2[simp]: "xs ~= [] ==> hd(xs @ ys) = hd xs" |
|
333 |
by(simp add: hd_append split: list.split) |
|
334 |
||
335 |
lemma tl_append: "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)" |
|
336 |
by(simp split: list.split) |
|
337 |
||
338 |
lemma tl_append2[simp]: "xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys" |
|
339 |
by(simp add: tl_append split: list.split) |
|
340 |
||
341 |
(* trivial rules for solving @-equations automatically *) |
|
342 |
||
343 |
lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys" |
|
344 |
by simp |
|
345 |
||
346 |
lemma Cons_eq_appendI: "[| x#xs1 = ys; xs = xs1 @ zs |] ==> x#xs = ys@zs" |
|
347 |
by(drule sym, simp) |
|
348 |
||
349 |
lemma append_eq_appendI: "[| xs@xs1 = zs; ys = xs1 @ us |] ==> xs@ys = zs@us" |
|
350 |
by(drule sym, simp) |
|
351 |
||
352 |
||
353 |
(*** |
|
354 |
Simplification procedure for all list equalities. |
|
355 |
Currently only tries to rearrange @ to see if |
|
356 |
- both lists end in a singleton list, |
|
357 |
- or both lists end in the same list. |
|
358 |
***) |
|
359 |
ML_setup{* |
|
3507 | 360 |
local |
361 |
||
13122 | 362 |
val append_assoc = thm "append_assoc"; |
363 |
val append_Nil = thm "append_Nil"; |
|
364 |
val append_Cons = thm "append_Cons"; |
|
365 |
val append1_eq_conv = thm "append1_eq_conv"; |
|
366 |
val append_same_eq = thm "append_same_eq"; |
|
367 |
||
13114 | 368 |
val list_eq_pattern = |
369 |
Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT) |
|
370 |
||
371 |
fun last (cons as Const("List.list.Cons",_) $ _ $ xs) = |
|
372 |
(case xs of Const("List.list.Nil",_) => cons | _ => last xs) |
|
373 |
| last (Const("List.op @",_) $ _ $ ys) = last ys |
|
374 |
| last t = t |
|
375 |
||
376 |
fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true |
|
377 |
| list1 _ = false |
|
378 |
||
379 |
fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) = |
|
380 |
(case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs) |
|
381 |
| butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys |
|
382 |
| butlast xs = Const("List.list.Nil",fastype_of xs) |
|
383 |
||
384 |
val rearr_tac = |
|
385 |
simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]) |
|
386 |
||
387 |
fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) = |
|
388 |
let |
|
389 |
val lastl = last lhs and lastr = last rhs |
|
390 |
fun rearr conv = |
|
391 |
let val lhs1 = butlast lhs and rhs1 = butlast rhs |
|
392 |
val Type(_,listT::_) = eqT |
|
393 |
val appT = [listT,listT] ---> listT |
|
394 |
val app = Const("List.op @",appT) |
|
395 |
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr) |
|
396 |
val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2))) |
|
397 |
val thm = prove_goalw_cterm [] ct (K [rearr_tac 1]) |
|
398 |
handle ERROR => |
|
399 |
error("The error(s) above occurred while trying to prove " ^ |
|
400 |
string_of_cterm ct) |
|
401 |
in Some((conv RS (thm RS trans)) RS eq_reflection) end |
|
402 |
||
403 |
in if list1 lastl andalso list1 lastr |
|
404 |
then rearr append1_eq_conv |
|
405 |
else |
|
406 |
if lastl aconv lastr |
|
407 |
then rearr append_same_eq |
|
408 |
else None |
|
409 |
end |
|
410 |
in |
|
411 |
val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq |
|
412 |
end; |
|
413 |
||
414 |
Addsimprocs [list_eq_simproc]; |
|
415 |
*} |
|
416 |
||
417 |
||
418 |
(** map **) |
|
419 |
||
420 |
section "map" |
|
421 |
||
422 |
lemma map_ext: "(\<And>x. x : set xs \<longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g xs" |
|
423 |
by (induct xs, simp_all) |
|
424 |
||
425 |
lemma map_ident[simp]: "map (%x. x) = (%xs. xs)" |
|
426 |
by(rule ext, induct_tac "xs", auto) |
|
427 |
||
428 |
lemma map_append[simp]: "map f (xs@ys) = map f xs @ map f ys" |
|
429 |
by(induct_tac "xs", auto) |
|
430 |
||
431 |
lemma map_compose(*[simp]*): "map (f o g) xs = map f (map g xs)" |
|
432 |
by(unfold o_def, induct_tac "xs", auto) |
|
433 |
||
434 |
lemma rev_map: "rev(map f xs) = map f (rev xs)" |
|
435 |
by(induct_tac xs, auto) |
|
436 |
||
437 |
(* a congruence rule for map: *) |
|
438 |
lemma map_cong: |
|
439 |
"xs=ys ==> (!!x. x : set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys" |
|
440 |
by (clarify, induct ys, auto) |
|
441 |
||
442 |
lemma map_is_Nil_conv[iff]: "(map f xs = []) = (xs = [])" |
|
443 |
by(case_tac xs, auto) |
|
444 |
||
445 |
lemma Nil_is_map_conv[iff]: "([] = map f xs) = (xs = [])" |
|
446 |
by(case_tac xs, auto) |
|
447 |
||
448 |
lemma map_eq_Cons: |
|
449 |
"(map f xs = y#ys) = (? x xs'. xs = x#xs' & f x = y & map f xs' = ys)" |
|
450 |
by(case_tac xs, auto) |
|
451 |
||
452 |
lemma map_injective: |
|
453 |
"\<And>xs. map f xs = map f ys \<Longrightarrow> (!x y. f x = f y --> x=y) \<Longrightarrow> xs=ys" |
|
454 |
by(induct "ys", simp, fastsimp simp add:map_eq_Cons) |
|
455 |
||
456 |
lemma inj_mapI: "inj f ==> inj (map f)" |
|
457 |
by(blast dest:map_injective injD intro:injI) |
|
458 |
||
459 |
lemma inj_mapD: "inj (map f) ==> inj f" |
|
460 |
apply(unfold inj_on_def) |
|
461 |
apply clarify |
|
462 |
apply(erule_tac x = "[x]" in ballE) |
|
463 |
apply(erule_tac x = "[y]" in ballE) |
|
464 |
apply simp |
|
465 |
apply blast |
|
466 |
apply blast |
|
467 |
done |
|
468 |
||
469 |
lemma inj_map: "inj (map f) = inj f" |
|
470 |
by(blast dest:inj_mapD intro:inj_mapI) |
|
471 |
||
472 |
(** rev **) |
|
473 |
||
474 |
section "rev" |
|
475 |
||
476 |
lemma rev_append[simp]: "rev(xs@ys) = rev(ys) @ rev(xs)" |
|
477 |
by(induct_tac xs, auto) |
|
478 |
||
479 |
lemma rev_rev_ident[simp]: "rev(rev xs) = xs" |
|
480 |
by(induct_tac xs, auto) |
|
481 |
||
482 |
lemma rev_is_Nil_conv[iff]: "(rev xs = []) = (xs = [])" |
|
483 |
by(induct_tac xs, auto) |
|
484 |
||
485 |
lemma Nil_is_rev_conv[iff]: "([] = rev xs) = (xs = [])" |
|
486 |
by(induct_tac xs, auto) |
|
487 |
||
488 |
lemma rev_is_rev_conv[iff]: "!!ys. (rev xs = rev ys) = (xs = ys)" |
|
489 |
apply(induct "xs" ) |
|
490 |
apply force |
|
491 |
apply(case_tac ys) |
|
492 |
apply simp |
|
493 |
apply force |
|
494 |
done |
|
495 |
||
496 |
lemma rev_induct: "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs" |
|
497 |
apply(subst rev_rev_ident[symmetric]) |
|
498 |
apply(rule_tac list = "rev xs" in list.induct, simp_all) |
|
499 |
done |
|
500 |
||
501 |
(* Instead of (rev_induct_tac xs) use (induct_tac xs rule: rev_induct) *) |
|
502 |
||
503 |
lemma rev_exhaust: "(xs = [] \<Longrightarrow> P) \<Longrightarrow> (!!ys y. xs = ys@[y] \<Longrightarrow> P) \<Longrightarrow> P" |
|
504 |
by(induct xs rule: rev_induct, auto) |
|
505 |
||
506 |
||
507 |
(** set **) |
|
508 |
||
509 |
section "set" |
|
510 |
||
511 |
lemma finite_set[iff]: "finite (set xs)" |
|
512 |
by(induct_tac xs, auto) |
|
513 |
||
514 |
lemma set_append[simp]: "set (xs@ys) = (set xs Un set ys)" |
|
515 |
by(induct_tac xs, auto) |
|
516 |
||
517 |
lemma set_subset_Cons: "set xs \<subseteq> set (x#xs)" |
|
518 |
by auto |
|
519 |
||
520 |
lemma set_empty[iff]: "(set xs = {}) = (xs = [])" |
|
521 |
by(induct_tac xs, auto) |
|
522 |
||
523 |
lemma set_rev[simp]: "set(rev xs) = set(xs)" |
|
524 |
by(induct_tac xs, auto) |
|
525 |
||
526 |
lemma set_map[simp]: "set(map f xs) = f`(set xs)" |
|
527 |
by(induct_tac xs, auto) |
|
528 |
||
529 |
lemma set_filter[simp]: "set(filter P xs) = {x. x : set xs & P x}" |
|
530 |
by(induct_tac xs, auto) |
|
531 |
||
532 |
lemma set_upt[simp]: "set[i..j(] = {k. i <= k & k < j}" |
|
533 |
apply(induct_tac j) |
|
534 |
apply simp_all |
|
535 |
apply(erule ssubst) |
|
536 |
apply auto |
|
537 |
apply arith |
|
538 |
done |
|
539 |
||
540 |
lemma in_set_conv_decomp: "(x : set xs) = (? ys zs. xs = ys@x#zs)" |
|
541 |
apply(induct_tac "xs") |
|
542 |
apply simp |
|
543 |
apply simp |
|
544 |
apply(rule iffI) |
|
545 |
apply(blast intro: eq_Nil_appendI Cons_eq_appendI) |
|
546 |
apply(erule exE)+ |
|
547 |
apply(case_tac "ys") |
|
548 |
apply auto |
|
549 |
done |
|
550 |
||
551 |
||
552 |
(* eliminate `lists' in favour of `set' *) |
|
553 |
||
554 |
lemma in_lists_conv_set: "(xs : lists A) = (!x : set xs. x : A)" |
|
555 |
by(induct_tac xs, auto) |
|
556 |
||
557 |
lemmas in_listsD[dest!] = in_lists_conv_set[THEN iffD1] |
|
558 |
lemmas in_listsI[intro!] = in_lists_conv_set[THEN iffD2] |
|
559 |
||
560 |
||
561 |
(** mem **) |
|
562 |
||
563 |
section "mem" |
|
564 |
||
565 |
lemma set_mem_eq: "(x mem xs) = (x : set xs)" |
|
566 |
by(induct_tac xs, auto) |
|
567 |
||
568 |
||
569 |
(** list_all **) |
|
570 |
||
571 |
section "list_all" |
|
572 |
||
573 |
lemma list_all_conv: "list_all P xs = (!x:set xs. P x)" |
|
574 |
by(induct_tac xs, auto) |
|
575 |
||
576 |
lemma list_all_append[simp]: |
|
577 |
"list_all P (xs@ys) = (list_all P xs & list_all P ys)" |
|
578 |
by(induct_tac xs, auto) |
|
579 |
||
580 |
||
581 |
(** filter **) |
|
582 |
||
583 |
section "filter" |
|
584 |
||
585 |
lemma filter_append[simp]: "filter P (xs@ys) = filter P xs @ filter P ys" |
|
586 |
by(induct_tac xs, auto) |
|
587 |
||
588 |
lemma filter_filter[simp]: "filter P (filter Q xs) = filter (%x. Q x & P x) xs" |
|
589 |
by(induct_tac xs, auto) |
|
590 |
||
591 |
lemma filter_True[simp]: "!x : set xs. P x \<Longrightarrow> filter P xs = xs" |
|
592 |
by(induct xs, auto) |
|
593 |
||
594 |
lemma filter_False[simp]: "!x : set xs. ~P x \<Longrightarrow> filter P xs = []" |
|
595 |
by(induct xs, auto) |
|
596 |
||
597 |
lemma length_filter[simp]: "length (filter P xs) <= length xs" |
|
598 |
by(induct xs, auto simp add: le_SucI) |
|
599 |
||
600 |
lemma filter_is_subset[simp]: "set (filter P xs) <= set xs" |
|
601 |
by auto |
|
602 |
||
603 |
||
604 |
section "concat" |
|
605 |
||
606 |
lemma concat_append[simp]: "concat(xs@ys) = concat(xs)@concat(ys)" |
|
607 |
by(induct xs, auto) |
|
608 |
||
609 |
lemma concat_eq_Nil_conv[iff]: "(concat xss = []) = (!xs:set xss. xs=[])" |
|
610 |
by(induct xss, auto) |
|
611 |
||
612 |
lemma Nil_eq_concat_conv[iff]: "([] = concat xss) = (!xs:set xss. xs=[])" |
|
613 |
by(induct xss, auto) |
|
614 |
||
615 |
lemma set_concat[simp]: "set(concat xs) = Union(set ` set xs)" |
|
616 |
by(induct xs, auto) |
|
617 |
||
618 |
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" |
|
619 |
by(induct xs, auto) |
|
620 |
||
621 |
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" |
|
622 |
by(induct xs, auto) |
|
623 |
||
624 |
lemma rev_concat: "rev(concat xs) = concat (map rev (rev xs))" |
|
625 |
by(induct xs, auto) |
|
626 |
||
627 |
(** nth **) |
|
628 |
||
629 |
section "nth" |
|
630 |
||
631 |
lemma nth_Cons_0[simp]: "(x#xs)!0 = x" |
|
632 |
by auto |
|
633 |
||
634 |
lemma nth_Cons_Suc[simp]: "(x#xs)!(Suc n) = xs!n" |
|
635 |
by auto |
|
636 |
||
637 |
declare nth.simps[simp del] |
|
638 |
||
639 |
lemma nth_append: |
|
640 |
"!!n. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))" |
|
641 |
apply(induct "xs") |
|
642 |
apply simp |
|
643 |
apply(case_tac "n" ) |
|
644 |
apply auto |
|
645 |
done |
|
646 |
||
647 |
lemma nth_map[simp]: "!!n. n < length xs \<Longrightarrow> (map f xs)!n = f(xs!n)" |
|
648 |
apply(induct "xs" ) |
|
649 |
apply simp |
|
650 |
apply(case_tac "n") |
|
651 |
apply auto |
|
652 |
done |
|
653 |
||
654 |
lemma set_conv_nth: "set xs = {xs!i |i. i < length xs}" |
|
655 |
apply(induct_tac "xs") |
|
656 |
apply simp |
|
657 |
apply simp |
|
658 |
apply safe |
|
659 |
apply(rule_tac x = 0 in exI) |
|
660 |
apply simp |
|
661 |
apply(rule_tac x = "Suc i" in exI) |
|
662 |
apply simp |
|
663 |
apply(case_tac "i") |
|
664 |
apply simp |
|
665 |
apply(rename_tac "j") |
|
666 |
apply(rule_tac x = "j" in exI) |
|
667 |
apply simp |
|
668 |
done |
|
669 |
||
670 |
lemma list_ball_nth: "\<lbrakk> n < length xs; !x : set xs. P x \<rbrakk> \<Longrightarrow> P(xs!n)" |
|
671 |
by(simp add:set_conv_nth, blast) |
|
672 |
||
673 |
lemma nth_mem[simp]: "n < length xs ==> xs!n : set xs" |
|
674 |
by(simp add:set_conv_nth, blast) |
|
675 |
||
676 |
lemma all_nth_imp_all_set: |
|
677 |
"\<lbrakk> !i < length xs. P(xs!i); x : set xs \<rbrakk> \<Longrightarrow> P x" |
|
678 |
by(simp add:set_conv_nth, blast) |
|
679 |
||
680 |
lemma all_set_conv_all_nth: |
|
681 |
"(!x : set xs. P x) = (!i. i<length xs --> P (xs ! i))" |
|
682 |
by(simp add:set_conv_nth, blast) |
|
683 |
||
684 |
||
685 |
(** list update **) |
|
686 |
||
687 |
section "list update" |
|
688 |
||
689 |
lemma length_list_update[simp]: "!!i. length(xs[i:=x]) = length xs" |
|
690 |
by(induct xs, simp, simp split:nat.split) |
|
691 |
||
692 |
lemma nth_list_update: |
|
693 |
"!!i j. i < length xs \<Longrightarrow> (xs[i:=x])!j = (if i=j then x else xs!j)" |
|
694 |
by(induct xs, simp, auto simp add:nth_Cons split:nat.split) |
|
695 |
||
696 |
lemma nth_list_update_eq[simp]: "i < length xs ==> (xs[i:=x])!i = x" |
|
697 |
by(simp add:nth_list_update) |
|
698 |
||
699 |
lemma nth_list_update_neq[simp]: "!!i j. i ~= j \<Longrightarrow> xs[i:=x]!j = xs!j" |
|
700 |
by(induct xs, simp, auto simp add:nth_Cons split:nat.split) |
|
701 |
||
702 |
lemma list_update_overwrite[simp]: |
|
703 |
"!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]" |
|
704 |
by(induct xs, simp, simp split:nat.split) |
|
705 |
||
706 |
lemma list_update_same_conv: |
|
707 |
"!!i. i < length xs \<Longrightarrow> (xs[i := x] = xs) = (xs!i = x)" |
|
708 |
by(induct xs, simp, simp split:nat.split, blast) |
|
709 |
||
710 |
lemma update_zip: |
|
711 |
"!!i xy xs. length xs = length ys \<Longrightarrow> |
|
712 |
(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])" |
|
713 |
by(induct ys, auto, case_tac xs, auto split:nat.split) |
|
714 |
||
715 |
lemma set_update_subset_insert: "!!i. set(xs[i:=x]) <= insert x (set xs)" |
|
716 |
by(induct xs, simp, simp split:nat.split, fast) |
|
717 |
||
718 |
lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A" |
|
719 |
by(fast dest!:set_update_subset_insert[THEN subsetD]) |
|
720 |
||
721 |
||
722 |
(** last & butlast **) |
|
723 |
||
724 |
section "last / butlast" |
|
725 |
||
726 |
lemma last_snoc[simp]: "last(xs@[x]) = x" |
|
727 |
by(induct xs, auto) |
|
728 |
||
729 |
lemma butlast_snoc[simp]:"butlast(xs@[x]) = xs" |
|
730 |
by(induct xs, auto) |
|
731 |
||
732 |
lemma length_butlast[simp]: "length(butlast xs) = length xs - 1" |
|
733 |
by(induct xs rule:rev_induct, auto) |
|
734 |
||
735 |
lemma butlast_append: |
|
736 |
"!!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)" |
|
737 |
by(induct xs, auto) |
|
738 |
||
739 |
lemma append_butlast_last_id[simp]: |
|
740 |
"xs ~= [] --> butlast xs @ [last xs] = xs" |
|
741 |
by(induct xs, auto) |
|
742 |
||
743 |
lemma in_set_butlastD: "x:set(butlast xs) ==> x:set xs" |
|
744 |
by(induct xs, auto split:split_if_asm) |
|
745 |
||
746 |
lemma in_set_butlast_appendI: |
|
747 |
"x:set(butlast xs) | x:set(butlast ys) ==> x:set(butlast(xs@ys))" |
|
748 |
by(auto dest:in_set_butlastD simp add:butlast_append) |
|
749 |
||
750 |
(** take & drop **) |
|
751 |
section "take & drop" |
|
752 |
||
753 |
lemma take_0[simp]: "take 0 xs = []" |
|
754 |
by(induct xs, auto) |
|
755 |
||
756 |
lemma drop_0[simp]: "drop 0 xs = xs" |
|
757 |
by(induct xs, auto) |
|
758 |
||
759 |
lemma take_Suc_Cons[simp]: "take (Suc n) (x#xs) = x # take n xs" |
|
760 |
by simp |
|
761 |
||
762 |
lemma drop_Suc_Cons[simp]: "drop (Suc n) (x#xs) = drop n xs" |
|
763 |
by simp |
|
764 |
||
765 |
declare take_Cons[simp del] drop_Cons[simp del] |
|
766 |
||
767 |
lemma length_take[simp]: "!!xs. length(take n xs) = min (length xs) n" |
|
768 |
by(induct n, auto, case_tac xs, auto) |
|
769 |
||
770 |
lemma length_drop[simp]: "!!xs. length(drop n xs) = (length xs - n)" |
|
771 |
by(induct n, auto, case_tac xs, auto) |
|
772 |
||
773 |
lemma take_all[simp]: "!!xs. length xs <= n ==> take n xs = xs" |
|
774 |
by(induct n, auto, case_tac xs, auto) |
|
775 |
||
776 |
lemma drop_all[simp]: "!!xs. length xs <= n ==> drop n xs = []" |
|
777 |
by(induct n, auto, case_tac xs, auto) |
|
778 |
||
779 |
lemma take_append[simp]: |
|
780 |
"!!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)" |
|
781 |
by(induct n, auto, case_tac xs, auto) |
|
782 |
||
783 |
lemma drop_append[simp]: |
|
784 |
"!!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys" |
|
785 |
by(induct n, auto, case_tac xs, auto) |
|
786 |
||
787 |
lemma take_take[simp]: "!!xs n. take n (take m xs) = take (min n m) xs" |
|
788 |
apply(induct m) |
|
789 |
apply auto |
|
790 |
apply(case_tac xs) |
|
791 |
apply auto |
|
792 |
apply(case_tac na) |
|
793 |
apply auto |
|
794 |
done |
|
795 |
||
796 |
lemma drop_drop[simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs" |
|
797 |
apply(induct m) |
|
798 |
apply auto |
|
799 |
apply(case_tac xs) |
|
800 |
apply auto |
|
801 |
done |
|
802 |
||
803 |
lemma take_drop: "!!xs n. take n (drop m xs) = drop m (take (n + m) xs)" |
|
804 |
apply(induct m) |
|
805 |
apply auto |
|
806 |
apply(case_tac xs) |
|
807 |
apply auto |
|
808 |
done |
|
809 |
||
810 |
lemma append_take_drop_id[simp]: "!!xs. take n xs @ drop n xs = xs" |
|
811 |
apply(induct n) |
|
812 |
apply auto |
|
813 |
apply(case_tac xs) |
|
814 |
apply auto |
|
815 |
done |
|
816 |
||
817 |
lemma take_map: "!!xs. take n (map f xs) = map f (take n xs)" |
|
818 |
apply(induct n) |
|
819 |
apply auto |
|
820 |
apply(case_tac xs) |
|
821 |
apply auto |
|
822 |
done |
|
823 |
||
824 |
lemma drop_map: "!!xs. drop n (map f xs) = map f (drop n xs)" |
|
825 |
apply(induct n) |
|
826 |
apply auto |
|
827 |
apply(case_tac xs) |
|
828 |
apply auto |
|
829 |
done |
|
830 |
||
831 |
lemma rev_take: "!!i. rev (take i xs) = drop (length xs - i) (rev xs)" |
|
832 |
apply(induct xs) |
|
833 |
apply auto |
|
834 |
apply(case_tac i) |
|
835 |
apply auto |
|
836 |
done |
|
837 |
||
838 |
lemma rev_drop: "!!i. rev (drop i xs) = take (length xs - i) (rev xs)" |
|
839 |
apply(induct xs) |
|
840 |
apply auto |
|
841 |
apply(case_tac i) |
|
842 |
apply auto |
|
843 |
done |
|
844 |
||
845 |
lemma nth_take[simp]: "!!n i. i < n ==> (take n xs)!i = xs!i" |
|
846 |
apply(induct xs) |
|
847 |
apply auto |
|
848 |
apply(case_tac n) |
|
849 |
apply(blast ) |
|
850 |
apply(case_tac i) |
|
851 |
apply auto |
|
852 |
done |
|
853 |
||
854 |
lemma nth_drop[simp]: "!!xs i. n + i <= length xs ==> (drop n xs)!i = xs!(n+i)" |
|
855 |
apply(induct n) |
|
856 |
apply auto |
|
857 |
apply(case_tac xs) |
|
858 |
apply auto |
|
859 |
done |
|
3507 | 860 |
|
13114 | 861 |
lemma append_eq_conv_conj: |
862 |
"!!zs. (xs@ys = zs) = (xs = take (length xs) zs & ys = drop (length xs) zs)" |
|
863 |
apply(induct xs) |
|
864 |
apply simp |
|
865 |
apply clarsimp |
|
866 |
apply(case_tac zs) |
|
867 |
apply auto |
|
868 |
done |
|
869 |
||
870 |
(** takeWhile & dropWhile **) |
|
871 |
||
872 |
section "takeWhile & dropWhile" |
|
873 |
||
874 |
lemma takeWhile_dropWhile_id[simp]: "takeWhile P xs @ dropWhile P xs = xs" |
|
875 |
by(induct xs, auto) |
|
876 |
||
877 |
lemma takeWhile_append1[simp]: |
|
878 |
"\<lbrakk> x:set xs; ~P(x) \<rbrakk> \<Longrightarrow> takeWhile P (xs @ ys) = takeWhile P xs" |
|
879 |
by(induct xs, auto) |
|
880 |
||
881 |
lemma takeWhile_append2[simp]: |
|
882 |
"(!!x. x : set xs \<Longrightarrow> P(x)) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys" |
|
883 |
by(induct xs, auto) |
|
884 |
||
885 |
lemma takeWhile_tail: "~P(x) ==> takeWhile P (xs @ (x#l)) = takeWhile P xs" |
|
886 |
by(induct xs, auto) |
|
887 |
||
888 |
lemma dropWhile_append1[simp]: |
|
889 |
"\<lbrakk> x : set xs; ~P(x) \<rbrakk> \<Longrightarrow> dropWhile P (xs @ ys) = (dropWhile P xs)@ys" |
|
890 |
by(induct xs, auto) |
|
891 |
||
892 |
lemma dropWhile_append2[simp]: |
|
893 |
"(!!x. x:set xs \<Longrightarrow> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys" |
|
894 |
by(induct xs, auto) |
|
895 |
||
896 |
lemma set_take_whileD: "x:set(takeWhile P xs) ==> x:set xs & P x" |
|
897 |
by(induct xs, auto split:split_if_asm) |
|
898 |
||
899 |
||
900 |
(** zip **) |
|
901 |
section "zip" |
|
902 |
||
903 |
lemma zip_Nil[simp]: "zip [] ys = []" |
|
904 |
by(induct ys, auto) |
|
905 |
||
906 |
lemma zip_Cons_Cons[simp]: "zip (x#xs) (y#ys) = (x,y)#zip xs ys" |
|
907 |
by simp |
|
908 |
||
909 |
declare zip_Cons[simp del] |
|
910 |
||
911 |
lemma length_zip[simp]: |
|
912 |
"!!xs. length (zip xs ys) = min (length xs) (length ys)" |
|
913 |
apply(induct ys) |
|
914 |
apply simp |
|
915 |
apply(case_tac xs) |
|
916 |
apply auto |
|
917 |
done |
|
918 |
||
919 |
lemma zip_append1: |
|
920 |
"!!xs. zip (xs@ys) zs = |
|
921 |
zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)" |
|
922 |
apply(induct zs) |
|
923 |
apply simp |
|
924 |
apply(case_tac xs) |
|
925 |
apply simp_all |
|
926 |
done |
|
927 |
||
928 |
lemma zip_append2: |
|
929 |
"!!ys. zip xs (ys@zs) = |
|
930 |
zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs" |
|
931 |
apply(induct xs) |
|
932 |
apply simp |
|
933 |
apply(case_tac ys) |
|
934 |
apply simp_all |
|
935 |
done |
|
936 |
||
937 |
lemma zip_append[simp]: |
|
938 |
"[| length xs = length us; length ys = length vs |] ==> \ |
|
939 |
\ zip (xs@ys) (us@vs) = zip xs us @ zip ys vs" |
|
940 |
by(simp add: zip_append1) |
|
941 |
||
942 |
lemma zip_rev: |
|
943 |
"!!xs. length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)" |
|
944 |
apply(induct ys) |
|
945 |
apply simp |
|
946 |
apply(case_tac xs) |
|
947 |
apply simp_all |
|
948 |
done |
|
949 |
||
950 |
lemma nth_zip[simp]: |
|
951 |
"!!i xs. \<lbrakk> i < length xs; i < length ys \<rbrakk> \<Longrightarrow> (zip xs ys)!i = (xs!i, ys!i)" |
|
952 |
apply(induct ys) |
|
953 |
apply simp |
|
954 |
apply(case_tac xs) |
|
955 |
apply (simp_all add: nth.simps split:nat.split) |
|
956 |
done |
|
957 |
||
958 |
lemma set_zip: |
|
959 |
"set(zip xs ys) = {(xs!i,ys!i) |i. i < min (length xs) (length ys)}" |
|
960 |
by(simp add: set_conv_nth cong: rev_conj_cong) |
|
961 |
||
962 |
lemma zip_update: |
|
963 |
"length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]" |
|
964 |
by(rule sym, simp add: update_zip) |
|
965 |
||
966 |
lemma zip_replicate[simp]: |
|
967 |
"!!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)" |
|
968 |
apply(induct i) |
|
969 |
apply auto |
|
970 |
apply(case_tac j) |
|
971 |
apply auto |
|
972 |
done |
|
973 |
||
974 |
(** list_all2 **) |
|
975 |
section "list_all2" |
|
976 |
||
977 |
lemma list_all2_lengthD: "list_all2 P xs ys ==> length xs = length ys" |
|
978 |
by(simp add:list_all2_def) |
|
979 |
||
980 |
lemma list_all2_Nil[iff]: "list_all2 P [] ys = (ys=[])" |
|
981 |
by(simp add:list_all2_def) |
|
982 |
||
983 |
lemma list_all2_Nil2[iff]: "list_all2 P xs [] = (xs=[])" |
|
984 |
by(simp add:list_all2_def) |
|
985 |
||
986 |
lemma list_all2_Cons[iff]: |
|
987 |
"list_all2 P (x#xs) (y#ys) = (P x y & list_all2 P xs ys)" |
|
988 |
by(auto simp add:list_all2_def) |
|
989 |
||
990 |
lemma list_all2_Cons1: |
|
991 |
"list_all2 P (x#xs) ys = (? z zs. ys = z#zs & P x z & list_all2 P xs zs)" |
|
992 |
by(case_tac ys, auto) |
|
993 |
||
994 |
lemma list_all2_Cons2: |
|
995 |
"list_all2 P xs (y#ys) = (? z zs. xs = z#zs & P z y & list_all2 P zs ys)" |
|
996 |
by(case_tac xs, auto) |
|
997 |
||
998 |
lemma list_all2_rev[iff]: |
|
999 |
"list_all2 P (rev xs) (rev ys) = list_all2 P xs ys" |
|
1000 |
by(simp add:list_all2_def zip_rev cong:conj_cong) |
|
1001 |
||
1002 |
lemma list_all2_append1: |
|
1003 |
"list_all2 P (xs@ys) zs = |
|
1004 |
(EX us vs. zs = us@vs & length us = length xs & length vs = length ys & |
|
1005 |
list_all2 P xs us & list_all2 P ys vs)" |
|
1006 |
apply(simp add:list_all2_def zip_append1) |
|
1007 |
apply(rule iffI) |
|
1008 |
apply(rule_tac x = "take (length xs) zs" in exI) |
|
1009 |
apply(rule_tac x = "drop (length xs) zs" in exI) |
|
1010 |
apply(force split: nat_diff_split simp add:min_def) |
|
1011 |
apply clarify |
|
1012 |
apply(simp add: ball_Un) |
|
1013 |
done |
|
1014 |
||
1015 |
lemma list_all2_append2: |
|
1016 |
"list_all2 P xs (ys@zs) = |
|
1017 |
(EX us vs. xs = us@vs & length us = length ys & length vs = length zs & |
|
1018 |
list_all2 P us ys & list_all2 P vs zs)" |
|
1019 |
apply(simp add:list_all2_def zip_append2) |
|
1020 |
apply(rule iffI) |
|
1021 |
apply(rule_tac x = "take (length ys) xs" in exI) |
|
1022 |
apply(rule_tac x = "drop (length ys) xs" in exI) |
|
1023 |
apply(force split: nat_diff_split simp add:min_def) |
|
1024 |
apply clarify |
|
1025 |
apply(simp add: ball_Un) |
|
1026 |
done |
|
1027 |
||
1028 |
lemma list_all2_conv_all_nth: |
|
1029 |
"list_all2 P xs ys = |
|
1030 |
(length xs = length ys & (!i<length xs. P (xs!i) (ys!i)))" |
|
1031 |
by(force simp add:list_all2_def set_zip) |
|
1032 |
||
1033 |
lemma list_all2_trans[rule_format]: |
|
1034 |
"ALL a b c. P1 a b --> P2 b c --> P3 a c ==> |
|
1035 |
ALL bs cs. list_all2 P1 as bs --> list_all2 P2 bs cs --> list_all2 P3 as cs" |
|
1036 |
apply(induct_tac as) |
|
1037 |
apply simp |
|
1038 |
apply(rule allI) |
|
1039 |
apply(induct_tac bs) |
|
1040 |
apply simp |
|
1041 |
apply(rule allI) |
|
1042 |
apply(induct_tac cs) |
|
1043 |
apply auto |
|
1044 |
done |
|
1045 |
||
1046 |
||
1047 |
section "foldl" |
|
1048 |
||
1049 |
lemma foldl_append[simp]: |
|
1050 |
"!!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys" |
|
1051 |
by(induct xs, auto) |
|
1052 |
||
1053 |
(* Note: `n <= foldl op+ n ns' looks simpler, but is more difficult to use |
|
1054 |
because it requires an additional transitivity step |
|
1055 |
*) |
|
1056 |
lemma start_le_sum: "!!n::nat. m <= n ==> m <= foldl op+ n ns" |
|
1057 |
by(induct ns, auto) |
|
1058 |
||
1059 |
lemma elem_le_sum: "!!n::nat. n : set ns ==> n <= foldl op+ 0 ns" |
|
1060 |
by(force intro: start_le_sum simp add:in_set_conv_decomp) |
|
1061 |
||
1062 |
lemma sum_eq_0_conv[iff]: |
|
1063 |
"!!m::nat. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))" |
|
1064 |
by(induct ns, auto) |
|
1065 |
||
1066 |
(** upto **) |
|
1067 |
||
1068 |
(* Does not terminate! *) |
|
1069 |
lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])" |
|
1070 |
by(induct j, auto) |
|
1071 |
||
1072 |
lemma upt_conv_Nil[simp]: "j<=i ==> [i..j(] = []" |
|
1073 |
by(subst upt_rec, simp) |
|
1074 |
||
1075 |
(*Only needed if upt_Suc is deleted from the simpset*) |
|
1076 |
lemma upt_Suc_append: "i<=j ==> [i..(Suc j)(] = [i..j(]@[j]" |
|
1077 |
by simp |
|
1078 |
||
1079 |
lemma upt_conv_Cons: "i<j ==> [i..j(] = i#[Suc i..j(]" |
|
1080 |
apply(rule trans) |
|
1081 |
apply(subst upt_rec) |
|
1082 |
prefer 2 apply(rule refl) |
|
1083 |
apply simp |
|
1084 |
done |
|
1085 |
||
1086 |
(*LOOPS as a simprule, since j<=j*) |
|
1087 |
lemma upt_add_eq_append: "i<=j ==> [i..j+k(] = [i..j(]@[j..j+k(]" |
|
1088 |
by(induct_tac "k", auto) |
|
1089 |
||
1090 |
lemma length_upt[simp]: "length [i..j(] = j-i" |
|
1091 |
by(induct_tac j, simp, simp add: Suc_diff_le) |
|
1092 |
||
1093 |
lemma nth_upt[simp]: "i+k < j ==> [i..j(] ! k = i+k" |
|
1094 |
apply(induct j) |
|
1095 |
apply(auto simp add: less_Suc_eq nth_append split:nat_diff_split) |
|
1096 |
done |
|
1097 |
||
1098 |
lemma take_upt[simp]: "!!i. i+m <= n ==> take m [i..n(] = [i..i+m(]" |
|
1099 |
apply(induct m) |
|
1100 |
apply simp |
|
1101 |
apply(subst upt_rec) |
|
1102 |
apply(rule sym) |
|
1103 |
apply(subst upt_rec) |
|
1104 |
apply(simp del: upt.simps) |
|
1105 |
done |
|
3507 | 1106 |
|
13114 | 1107 |
lemma map_Suc_upt: "map Suc [m..n(] = [Suc m..n]" |
1108 |
by(induct n, auto) |
|
1109 |
||
1110 |
lemma nth_map_upt: "!!i. i < n-m ==> (map f [m..n(]) ! i = f(m+i)" |
|
1111 |
thm diff_induct |
|
1112 |
apply(induct n m rule: diff_induct) |
|
1113 |
prefer 3 apply(subst map_Suc_upt[symmetric]) |
|
1114 |
apply(auto simp add: less_diff_conv nth_upt) |
|
1115 |
done |
|
1116 |
||
1117 |
lemma nth_take_lemma[rule_format]: |
|
1118 |
"ALL xs ys. k <= length xs --> k <= length ys |
|
1119 |
--> (ALL i. i < k --> xs!i = ys!i) |
|
1120 |
--> take k xs = take k ys" |
|
1121 |
apply(induct_tac k) |
|
1122 |
apply(simp_all add: less_Suc_eq_0_disj all_conj_distrib) |
|
1123 |
apply clarify |
|
1124 |
(*Both lists must be non-empty*) |
|
1125 |
apply(case_tac xs) |
|
1126 |
apply simp |
|
1127 |
apply(case_tac ys) |
|
1128 |
apply clarify |
|
1129 |
apply(simp (no_asm_use)) |
|
1130 |
apply clarify |
|
1131 |
(*prenexing's needed, not miniscoping*) |
|
1132 |
apply(simp (no_asm_use) add: all_simps[symmetric] del: all_simps) |
|
1133 |
apply blast |
|
1134 |
(*prenexing's needed, not miniscoping*) |
|
1135 |
done |
|
1136 |
||
1137 |
lemma nth_equalityI: |
|
1138 |
"[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys" |
|
1139 |
apply(frule nth_take_lemma[OF le_refl eq_imp_le]) |
|
1140 |
apply(simp_all add: take_all) |
|
1141 |
done |
|
1142 |
||
1143 |
(*The famous take-lemma*) |
|
1144 |
lemma take_equalityI: "(ALL i. take i xs = take i ys) ==> xs = ys" |
|
1145 |
apply(drule_tac x = "max (length xs) (length ys)" in spec) |
|
1146 |
apply(simp add: le_max_iff_disj take_all) |
|
1147 |
done |
|
1148 |
||
1149 |
||
1150 |
(** distinct & remdups **) |
|
1151 |
section "distinct & remdups" |
|
1152 |
||
1153 |
lemma distinct_append[simp]: |
|
1154 |
"distinct(xs@ys) = (distinct xs & distinct ys & set xs Int set ys = {})" |
|
1155 |
by(induct xs, auto) |
|
1156 |
||
1157 |
lemma set_remdups[simp]: "set(remdups xs) = set xs" |
|
1158 |
by(induct xs, simp, simp add:insert_absorb) |
|
1159 |
||
1160 |
lemma distinct_remdups[iff]: "distinct(remdups xs)" |
|
1161 |
by(induct xs, auto) |
|
1162 |
||
1163 |
lemma distinct_filter[simp]: "distinct xs ==> distinct (filter P xs)" |
|
1164 |
by(induct xs, auto) |
|
1165 |
||
1166 |
(** replicate **) |
|
1167 |
section "replicate" |
|
1168 |
||
1169 |
lemma length_replicate[simp]: "length(replicate n x) = n" |
|
1170 |
by(induct n, auto) |
|
1171 |
||
1172 |
lemma map_replicate[simp]: "map f (replicate n x) = replicate n (f x)" |
|
1173 |
by(induct n, auto) |
|
1174 |
||
1175 |
lemma replicate_app_Cons_same: |
|
1176 |
"(replicate n x) @ (x#xs) = x # replicate n x @ xs" |
|
1177 |
by(induct n, auto) |
|
1178 |
||
1179 |
lemma rev_replicate[simp]: "rev(replicate n x) = replicate n x" |
|
1180 |
apply(induct n) |
|
1181 |
apply simp |
|
1182 |
apply(simp add: replicate_app_Cons_same) |
|
1183 |
done |
|
1184 |
||
1185 |
lemma replicate_add: "replicate (n+m) x = replicate n x @ replicate m x" |
|
1186 |
by(induct n, auto) |
|
1187 |
||
1188 |
lemma hd_replicate[simp]: "n ~= 0 ==> hd(replicate n x) = x" |
|
1189 |
by(induct n, auto) |
|
1190 |
||
1191 |
lemma tl_replicate[simp]: "n ~= 0 ==> tl(replicate n x) = replicate (n - 1) x" |
|
1192 |
by(induct n, auto) |
|
1193 |
||
1194 |
lemma last_replicate[rule_format,simp]: |
|
1195 |
"n ~= 0 --> last(replicate n x) = x" |
|
1196 |
by(induct_tac n, auto) |
|
1197 |
||
1198 |
lemma nth_replicate[simp]: "!!i. i<n ==> (replicate n x)!i = x" |
|
1199 |
apply(induct n) |
|
1200 |
apply simp |
|
1201 |
apply(simp add: nth_Cons split:nat.split) |
|
1202 |
done |
|
1203 |
||
1204 |
lemma set_replicate_Suc: "set(replicate (Suc n) x) = {x}" |
|
1205 |
by(induct n, auto) |
|
1206 |
||
1207 |
lemma set_replicate[simp]: "n ~= 0 ==> set(replicate n x) = {x}" |
|
1208 |
by(fast dest!: not0_implies_Suc intro!: set_replicate_Suc) |
|
1209 |
||
1210 |
lemma set_replicate_conv_if: "set(replicate n x) = (if n=0 then {} else {x})" |
|
1211 |
by auto |
|
1212 |
||
1213 |
lemma in_set_replicateD: "x : set(replicate n y) ==> x=y" |
|
1214 |
by(simp add: set_replicate_conv_if split:split_if_asm) |
|
1215 |
||
1216 |
||
1217 |
(*** Lexcicographic orderings on lists ***) |
|
1218 |
section"Lexcicographic orderings on lists" |
|
3507 | 1219 |
|
13114 | 1220 |
lemma wf_lexn: "wf r ==> wf(lexn r n)" |
1221 |
apply(induct_tac n) |
|
1222 |
apply simp |
|
1223 |
apply simp |
|
1224 |
apply(rule wf_subset) |
|
1225 |
prefer 2 apply(rule Int_lower1) |
|
1226 |
apply(rule wf_prod_fun_image) |
|
1227 |
prefer 2 apply(rule injI) |
|
1228 |
apply auto |
|
1229 |
done |
|
1230 |
||
1231 |
lemma lexn_length: |
|
1232 |
"!!xs ys. (xs,ys) : lexn r n ==> length xs = n & length ys = n" |
|
1233 |
by(induct n, auto) |
|
1234 |
||
1235 |
lemma wf_lex[intro!]: "wf r ==> wf(lex r)" |
|
1236 |
apply(unfold lex_def) |
|
1237 |
apply(rule wf_UN) |
|
1238 |
apply(blast intro: wf_lexn) |
|
1239 |
apply clarify |
|
1240 |
apply(rename_tac m n) |
|
1241 |
apply(subgoal_tac "m ~= n") |
|
1242 |
prefer 2 apply blast |
|
1243 |
apply(blast dest: lexn_length not_sym) |
|
1244 |
done |
|
1245 |
||
1246 |
||
1247 |
lemma lexn_conv: |
|
1248 |
"lexn r n = |
|
1249 |
{(xs,ys). length xs = n & length ys = n & |
|
1250 |
(? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}" |
|
1251 |
apply(induct_tac n) |
|
1252 |
apply simp |
|
1253 |
apply blast |
|
1254 |
apply(simp add: image_Collect lex_prod_def) |
|
1255 |
apply auto |
|
1256 |
apply blast |
|
1257 |
apply(rename_tac a xys x xs' y ys') |
|
1258 |
apply(rule_tac x = "a#xys" in exI) |
|
1259 |
apply simp |
|
1260 |
apply(case_tac xys) |
|
1261 |
apply simp_all |
|
1262 |
apply blast |
|
1263 |
done |
|
1264 |
||
1265 |
lemma lex_conv: |
|
1266 |
"lex r = |
|
1267 |
{(xs,ys). length xs = length ys & |
|
1268 |
(? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}" |
|
1269 |
by(force simp add: lex_def lexn_conv) |
|
1270 |
||
1271 |
lemma wf_lexico[intro!]: "wf r ==> wf(lexico r)" |
|
1272 |
by(unfold lexico_def, blast) |
|
1273 |
||
1274 |
lemma lexico_conv: |
|
1275 |
"lexico r = {(xs,ys). length xs < length ys | |
|
1276 |
length xs = length ys & (xs,ys) : lex r}" |
|
1277 |
by(simp add: lexico_def diag_def lex_prod_def measure_def inv_image_def) |
|
1278 |
||
1279 |
lemma Nil_notin_lex[iff]: "([],ys) ~: lex r" |
|
1280 |
by(simp add:lex_conv) |
|
1281 |
||
1282 |
lemma Nil2_notin_lex[iff]: "(xs,[]) ~: lex r" |
|
1283 |
by(simp add:lex_conv) |
|
1284 |
||
1285 |
lemma Cons_in_lex[iff]: |
|
1286 |
"((x#xs,y#ys) : lex r) = |
|
1287 |
((x,y) : r & length xs = length ys | x=y & (xs,ys) : lex r)" |
|
1288 |
apply(simp add:lex_conv) |
|
1289 |
apply(rule iffI) |
|
1290 |
prefer 2 apply(blast intro: Cons_eq_appendI) |
|
1291 |
apply clarify |
|
1292 |
apply(case_tac xys) |
|
1293 |
apply simp |
|
1294 |
apply simp |
|
1295 |
apply blast |
|
1296 |
done |
|
1297 |
||
1298 |
||
1299 |
(*** sublist (a generalization of nth to sets) ***) |
|
1300 |
||
1301 |
lemma sublist_empty[simp]: "sublist xs {} = []" |
|
1302 |
by(auto simp add:sublist_def) |
|
1303 |
||
1304 |
lemma sublist_nil[simp]: "sublist [] A = []" |
|
1305 |
by(auto simp add:sublist_def) |
|
1306 |
||
1307 |
lemma sublist_shift_lemma: |
|
1308 |
"map fst [p:zip xs [i..i + length xs(] . snd p : A] = |
|
1309 |
map fst [p:zip xs [0..length xs(] . snd p + i : A]" |
|
1310 |
apply(induct_tac xs rule: rev_induct) |
|
1311 |
apply simp |
|
1312 |
apply(simp add:add_commute) |
|
1313 |
done |
|
1314 |
||
1315 |
lemma sublist_append: |
|
1316 |
"sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}" |
|
1317 |
apply(unfold sublist_def) |
|
1318 |
apply(induct_tac l' rule: rev_induct) |
|
1319 |
apply simp |
|
1320 |
apply(simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma) |
|
1321 |
apply(simp add:add_commute) |
|
1322 |
done |
|
1323 |
||
1324 |
lemma sublist_Cons: |
|
1325 |
"sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}" |
|
1326 |
apply(induct_tac l rule: rev_induct) |
|
1327 |
apply(simp add:sublist_def) |
|
1328 |
apply(simp del: append_Cons add: append_Cons[symmetric] sublist_append) |
|
1329 |
done |
|
1330 |
||
1331 |
lemma sublist_singleton[simp]: "sublist [x] A = (if 0 : A then [x] else [])" |
|
1332 |
by(simp add:sublist_Cons) |
|
1333 |
||
1334 |
lemma sublist_upt_eq_take[simp]: "sublist l {..n(} = take n l" |
|
1335 |
apply(induct_tac l rule: rev_induct) |
|
1336 |
apply simp |
|
1337 |
apply(simp split:nat_diff_split add:sublist_append) |
|
1338 |
done |
|
1339 |
||
1340 |
||
1341 |
lemma take_Cons': "take n (x#xs) = (if n=0 then [] else x # take (n - 1) xs)" |
|
1342 |
by(case_tac n, simp_all) |
|
1343 |
||
1344 |
lemma drop_Cons': "drop n (x#xs) = (if n=0 then x#xs else drop (n - 1) xs)" |
|
1345 |
by(case_tac n, simp_all) |
|
1346 |
||
1347 |
lemma nth_Cons': "(x#xs)!n = (if n=0 then x else xs!(n - 1))" |
|
1348 |
by(case_tac n, simp_all) |
|
1349 |
||
1350 |
lemmas [simp] = take_Cons'[of "number_of v",standard] |
|
1351 |
drop_Cons'[of "number_of v",standard] |
|
1352 |
nth_Cons'[of "number_of v",standard] |
|
3507 | 1353 |
|
13122 | 1354 |
end |