5 header {* The datatype of finite lists *}
8 imports Plain Relation_Power Presburger Recdef ATP_Linkup
9 uses "Tools/string_syntax.ML"
14 | Cons 'a "'a list" (infixr "#" 65)
16 subsection{*Basic list processing functions*}
19 filter:: "('a => bool) => 'a list => 'a list"
20 concat:: "'a list list => 'a list"
21 foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
22 foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
24 tl:: "'a list => 'a list"
25 last:: "'a list => 'a"
26 butlast :: "'a list => 'a list"
27 set :: "'a list => 'a set"
28 map :: "('a=>'b) => ('a list => 'b list)"
29 listsum :: "'a list => 'a::monoid_add"
30 list_update :: "'a list => nat => 'a => 'a list"
31 take:: "nat => 'a list => 'a list"
32 drop:: "nat => 'a list => 'a list"
33 takeWhile :: "('a => bool) => 'a list => 'a list"
34 dropWhile :: "('a => bool) => 'a list => 'a list"
35 rev :: "'a list => 'a list"
36 zip :: "'a list => 'b list => ('a * 'b) list"
37 upt :: "nat => nat => nat list" ("(1[_..</_'])")
38 remdups :: "'a list => 'a list"
39 remove1 :: "'a => 'a list => 'a list"
40 removeAll :: "'a => 'a list => 'a list"
41 "distinct":: "'a list => bool"
42 replicate :: "nat => 'a => 'a list"
43 splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
46 nonterminals lupdbinds lupdbind
49 -- {* list Enumeration *}
50 "@list" :: "args => 'a list" ("[(_)]")
52 -- {* Special syntax for filter *}
53 "@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
56 "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")
57 "" :: "lupdbind => lupdbinds" ("_")
58 "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")
59 "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900)
64 "[x<-xs . P]"== "filter (%x. P) xs"
66 "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
67 "xs[i:=x]" == "list_update xs i x"
71 "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
73 "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
77 Function @{text size} is overloaded for all datatypes. Users may
78 refer to the list version as @{text length}. *}
81 length :: "'a list => nat" where
92 "last(x#xs) = (if xs=[] then x else last xs)"
96 "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
100 "set (x#xs) = insert x (set xs)"
104 "map f (x#xs) = f(x)#map f xs"
107 append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
109 append_Nil:"[] @ ys = ys"
110 | append_Cons: "(x#xs) @ ys = x # xs @ ys"
114 "rev(x#xs) = rev(xs) @ [x]"
118 "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
121 foldl_Nil:"foldl f a [] = a"
122 foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
126 "foldr f (x#xs) a = f x (foldr f xs a)"
130 "concat(x#xs) = x @ concat(xs)"
134 "listsum (x # xs) = x + listsum xs"
137 drop_Nil:"drop n [] = []"
138 drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
139 -- {*Warning: simpset does not contain this definition, but separate
140 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
143 take_Nil:"take n [] = []"
144 take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
145 -- {*Warning: simpset does not contain this definition, but separate
146 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
148 primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where
149 nth_Cons: "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
150 -- {*Warning: simpset does not contain this definition, but separate
151 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
155 "(x#xs)[i:=v] = (case i of 0 => v # xs | Suc j => x # xs[j:=v])"
158 "takeWhile P [] = []"
159 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
162 "dropWhile P [] = []"
163 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
167 zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
168 -- {*Warning: simpset does not contain this definition, but separate
169 theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
172 upt_0: "[i..<0] = []"
173 upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
177 "distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
181 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
185 "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
188 "removeAll x [] = []"
189 "removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)"
192 replicate_0: "replicate 0 x = []"
193 replicate_Suc: "replicate (Suc n) x = x # replicate n x"
196 rotate1 :: "'a list \<Rightarrow> 'a list" where
197 "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
200 rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
201 "rotate n = rotate1 ^ n"
204 list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
205 [code del]: "list_all2 P xs ys =
206 (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
209 sublist :: "'a list => nat set => 'a list" where
210 "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
214 "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
215 -- {*Warning: simpset does not contain the second eqn but a derived one. *}
221 @{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\
222 @{lemma "length [a,b,c] = 3" by simp}\\
223 @{lemma "set [a,b,c] = {a,b,c}" by simp}\\
224 @{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\
225 @{lemma "rev [a,b,c] = [c,b,a]" by simp}\\
226 @{lemma "hd [a,b,c,d] = a" by simp}\\
227 @{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\
228 @{lemma "last [a,b,c,d] = d" by simp}\\
229 @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
230 @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
231 @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
232 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
233 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
234 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
235 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
236 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
237 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
238 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
239 @{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
240 @{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\
241 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\
242 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
243 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
244 @{lemma "distinct [2,0,1::nat]" by simp}\\
245 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
246 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
247 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
248 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
249 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
250 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
251 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
252 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\
253 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\
254 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\
255 @{lemma "listsum [1,2,3::nat] = 6" by simp}
257 \caption{Characteristic examples}
258 \label{fig:Characteristic}
260 Figure~\ref{fig:Characteristic} shows charachteristic examples
261 that should give an intuitive understanding of the above functions.
264 text{* The following simple sort functions are intended for proofs,
265 not for efficient implementations. *}
270 fun sorted :: "'a list \<Rightarrow> bool" where
271 "sorted [] \<longleftrightarrow> True" |
272 "sorted [x] \<longleftrightarrow> True" |
273 "sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
275 primrec insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
276 "insort x [] = [x]" |
277 "insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
279 primrec sort :: "'a list \<Rightarrow> 'a list" where
281 "sort (x#xs) = insort x (sort xs)"
286 subsubsection {* List comprehension *}
288 text{* Input syntax for Haskell-like list comprehension notation.
289 Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
290 the list of all pairs of distinct elements from @{text xs} and @{text ys}.
291 The syntax is as in Haskell, except that @{text"|"} becomes a dot
292 (like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
293 \verb![e| x <- xs, ...]!.
295 The qualifiers after the dot are
297 \item[generators] @{text"p \<leftarrow> xs"},
298 where @{text p} is a pattern and @{text xs} an expression of list type, or
299 \item[guards] @{text"b"}, where @{text b} is a boolean expression.
300 %\item[local bindings] @ {text"let x = e"}.
303 Just like in Haskell, list comprehension is just a shorthand. To avoid
304 misunderstandings, the translation into desugared form is not reversed
305 upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is
306 optmized to @{term"map (%x. e) xs"}.
308 It is easy to write short list comprehensions which stand for complex
309 expressions. During proofs, they may become unreadable (and
310 mangled). In such cases it can be advisable to introduce separate
311 definitions for the list comprehensions in question. *}
314 Proper theorem proving support would be nice. For example, if
315 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
316 produced something like
317 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
320 nonterminals lc_qual lc_quals
323 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __")
324 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
325 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
326 (*"_lc_let" :: "letbinds => lc_qual" ("let _")*)
327 "_lc_end" :: "lc_quals" ("]")
328 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
329 "_lc_abs" :: "'a => 'b list => 'b list"
331 (* These are easier than ML code but cannot express the optimized
332 translation of [e. p<-xs]
334 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
335 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
336 => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
337 "[e. P]" => "if P then [e] else []"
338 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
339 => "if P then (_listcompr e Q Qs) else []"
340 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
341 => "_Let b (_listcompr e Q Qs)"
345 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
347 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
349 parse_translation (advanced) {*
351 val NilC = Syntax.const @{const_name Nil};
352 val ConsC = Syntax.const @{const_name Cons};
353 val mapC = Syntax.const @{const_name map};
354 val concatC = Syntax.const @{const_name concat};
355 val IfC = Syntax.const @{const_name If};
356 fun singl x = ConsC $ x $ NilC;
358 fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
360 val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
361 val e = if opti then singl e else e;
362 val case1 = Syntax.const "_case1" $ p $ e;
363 val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
365 val cs = Syntax.const "_case2" $ case1 $ case2
366 val ft = DatatypeCase.case_tr false DatatypePackage.datatype_of_constr
370 fun abs_tr ctxt (p as Free(s,T)) e opti =
371 let val thy = ProofContext.theory_of ctxt;
372 val s' = Sign.intern_const thy s
373 in if Sign.declared_const thy s'
374 then (pat_tr ctxt p e opti, false)
375 else (lambda p e, true)
377 | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
379 fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] =
380 let val res = case qs of Const("_lc_end",_) => singl e
381 | Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs];
382 in IfC $ b $ res $ NilC end
383 | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] =
384 (case abs_tr ctxt p e true of
385 (f,true) => mapC $ f $ es
386 | (f, false) => concatC $ (mapC $ f $ es))
387 | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] =
388 let val e' = lc_tr ctxt [e,q,qs];
389 in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end
391 in [("_listcompr", lc_tr)] end
396 term "[(x,y,z). x\<leftarrow>xs]"
397 term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
398 term "[(x,y,z). x<a, x>b]"
399 term "[(x,y,z). x\<leftarrow>xs, x>b]"
400 term "[(x,y,z). x<a, x\<leftarrow>xs]"
401 term "[(x,y). Cons True x \<leftarrow> xs]"
402 term "[(x,y,z). Cons x [] \<leftarrow> xs]"
403 term "[(x,y,z). x<a, x>b, x=d]"
404 term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
405 term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
406 term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
407 term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
408 term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
409 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
410 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
411 term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
414 subsubsection {* @{const Nil} and @{const Cons} *}
416 lemma not_Cons_self [simp]:
420 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]
422 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
426 "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
427 by (rule measure_induct [of length]) iprover
430 subsubsection {* @{const length} *}
433 Needs to come before @{text "@"} because of theorem @{text
434 append_eq_append_conv}.
437 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"
440 lemma length_map [simp]: "length (map f xs) = length xs"
443 lemma length_rev [simp]: "length (rev xs) = length xs"
446 lemma length_tl [simp]: "length (tl xs) = length xs - 1"
449 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
452 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])"
455 lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0"
458 lemma length_Suc_conv:
459 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
462 lemma Suc_length_conv:
463 "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
464 apply (induct xs, simp, simp)
468 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"
471 lemma list_induct2 [consumes 1, case_names Nil Cons]:
472 "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>
473 (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys))
474 \<Longrightarrow> P xs ys"
475 proof (induct xs arbitrary: ys)
476 case Nil then show ?case by simp
478 case (Cons x xs ys) then show ?case by (cases ys) simp_all
481 lemma list_induct3 [consumes 2, case_names Nil Cons]:
482 "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow>
483 (\<And>x xs y ys z zs. length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P xs ys zs \<Longrightarrow> P (x#xs) (y#ys) (z#zs))
484 \<Longrightarrow> P xs ys zs"
485 proof (induct xs arbitrary: ys zs)
486 case Nil then show ?case by simp
488 case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)
494 \<And>x xs. P (x#xs) [];
495 \<And>y ys. P [] (y#ys);
496 \<And>x xs y ys. P xs ys \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
497 \<Longrightarrow> P xs ys"
498 by (induct xs arbitrary: ys) (case_tac x, auto)+
500 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
501 by (rule Eq_FalseI) auto
503 simproc_setup list_neq ("(xs::'a list) = ys") = {*
505 Reduces xs=ys to False if xs and ys cannot be of the same length.
506 This is the case if the atomic sublists of one are a submultiset
507 of those of the other list and there are fewer Cons's in one than the other.
512 fun len (Const("List.list.Nil",_)) acc = acc
513 | len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
514 | len (Const("List.append",_) $ xs $ ys) acc = len xs (len ys acc)
515 | len (Const("List.rev",_) $ xs) acc = len xs acc
516 | len (Const("List.map",_) $ _ $ xs) acc = len xs acc
517 | len t (ts,n) = (t::ts,n);
519 fun list_neq _ ss ct =
521 val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
522 val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
525 val Type(_,listT::_) = eqT;
526 val size = HOLogic.size_const listT;
527 val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
528 val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
529 val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
530 (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));
531 in SOME (thm RS @{thm neq_if_length_neq}) end
533 if m < n andalso submultiset (op aconv) (ls,rs) orelse
534 n < m andalso submultiset (op aconv) (rs,ls)
535 then prove_neq() else NONE
541 subsubsection {* @{text "@"} -- append *}
543 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
546 lemma append_Nil2 [simp]: "xs @ [] = xs"
549 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
552 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])"
555 lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"
558 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
561 lemma append_eq_append_conv [simp, noatp]:
562 "length xs = length ys \<or> length us = length vs
563 ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
564 apply (induct xs arbitrary: ys)
565 apply (case_tac ys, simp, force)
566 apply (case_tac ys, force, simp)
569 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
570 (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
571 apply (induct xs arbitrary: ys zs ts)
578 lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"
581 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"
584 lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)"
587 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"
588 using append_same_eq [of _ _ "[]"] by auto
590 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
591 using append_same_eq [of "[]"] by auto
593 lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
596 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
599 lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"
600 by (simp add: hd_append split: list.split)
602 lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"
603 by (simp split: list.split)
605 lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"
606 by (simp add: tl_append split: list.split)
609 lemma Cons_eq_append_conv: "x#xs = ys@zs =
610 (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"
613 lemma append_eq_Cons_conv: "(ys@zs = x#xs) =
614 (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
618 text {* Trivial rules for solving @{text "@"}-equations automatically. *}
620 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
623 lemma Cons_eq_appendI:
624 "[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"
627 lemma append_eq_appendI:
628 "[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"
633 Simplification procedure for all list equalities.
634 Currently only tries to rearrange @{text "@"} to see if
635 - both lists end in a singleton list,
636 - or both lists end in the same list.
642 fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
643 (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
644 | last (Const("List.append",_) $ _ $ ys) = last ys
647 fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
650 fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
651 (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
652 | butlast ((app as Const("List.append",_) $ xs) $ ys) = app $ butlast ys
653 | butlast xs = Const("List.list.Nil",fastype_of xs);
655 val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
656 @{thm append_Nil}, @{thm append_Cons}];
658 fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
660 val lastl = last lhs and lastr = last rhs;
663 val lhs1 = butlast lhs and rhs1 = butlast rhs;
664 val Type(_,listT::_) = eqT
665 val appT = [listT,listT] ---> listT
666 val app = Const("List.append",appT)
667 val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
668 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
669 val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
670 (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
671 in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
674 if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
675 else if lastl aconv lastr then rearr @{thm append_same_eq}
681 val list_eq_simproc =
682 Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
686 Addsimprocs [list_eq_simproc];
690 subsubsection {* @{text map} *}
692 lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
693 by (induct xs) simp_all
695 lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)"
696 by (rule ext, induct_tac xs) auto
698 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"
701 lemma map_compose: "map (f o g) xs = map f (map g xs)"
702 by (induct xs) (auto simp add: o_def)
704 lemma rev_map: "rev (map f xs) = map f (rev xs)"
707 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
710 lemma map_cong [fundef_cong, recdef_cong]:
711 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
712 -- {* a congruence rule for @{text map} *}
715 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
718 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
721 lemma map_eq_Cons_conv:
722 "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
725 lemma Cons_eq_map_conv:
726 "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
729 lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]
730 lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]
731 declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!]
734 "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
735 by(induct ys, auto simp add: Cons_eq_map_conv)
737 lemma map_eq_imp_length_eq:
738 assumes "map f xs = map f ys"
739 shows "length xs = length ys"
740 using assms proof (induct ys arbitrary: xs)
741 case Nil then show ?case by simp
743 case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
744 from Cons xs have "map f zs = map f ys" by simp
745 moreover with Cons have "length zs = length ys" by blast
746 with xs show ?case by simp
750 "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
752 apply(frule map_eq_imp_length_eq)
754 apply(induct rule:list_induct2)
757 apply (blast intro:sym)
760 lemma inj_on_map_eq_map:
761 "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
762 by(blast dest:map_inj_on)
765 "map f xs = map f ys ==> inj f ==> xs = ys"
766 by (induct ys arbitrary: xs) (auto dest!:injD)
768 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
769 by(blast dest:map_injective)
771 lemma inj_mapI: "inj f ==> inj (map f)"
772 by (iprover dest: map_injective injD intro: inj_onI)
774 lemma inj_mapD: "inj (map f) ==> inj f"
775 apply (unfold inj_on_def, clarify)
776 apply (erule_tac x = "[x]" in ballE)
777 apply (erule_tac x = "[y]" in ballE, simp, blast)
781 lemma inj_map[iff]: "inj (map f) = inj f"
782 by (blast dest: inj_mapD intro: inj_mapI)
784 lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
786 apply(erule map_inj_on)
787 apply(blast intro:inj_onI dest:inj_onD)
790 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
793 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
796 lemma map_fst_zip[simp]:
797 "length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs"
798 by (induct rule:list_induct2, simp_all)
800 lemma map_snd_zip[simp]:
801 "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
802 by (induct rule:list_induct2, simp_all)
805 subsubsection {* @{text rev} *}
807 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
810 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
813 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
816 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
819 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
822 lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
825 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
828 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
829 apply (induct xs arbitrary: ys, force)
830 apply (case_tac ys, simp, force)
833 lemma inj_on_rev[iff]: "inj_on rev A"
834 by(simp add:inj_on_def)
836 lemma rev_induct [case_names Nil snoc]:
837 "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
838 apply(simplesubst rev_rev_ident[symmetric])
839 apply(rule_tac list = "rev xs" in list.induct, simp_all)
842 lemma rev_exhaust [case_names Nil snoc]:
843 "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"
844 by (induct xs rule: rev_induct) auto
846 lemmas rev_cases = rev_exhaust
848 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
849 by(rule rev_cases[of xs]) auto
852 subsubsection {* @{text set} *}
854 lemma finite_set [iff]: "finite (set xs)"
857 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)"
860 lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs"
863 lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
866 lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs"
869 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
872 lemma set_empty2[iff]: "({} = set xs) = (xs = [])"
875 lemma set_rev [simp]: "set (rev xs) = set xs"
878 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
881 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
884 lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}"
885 apply (induct j, simp_all)
886 apply (erule ssubst, auto)
890 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
892 case Nil thus ?case by simp
894 case Cons thus ?case by (auto intro: Cons_eq_appendI)
897 lemma in_set_conv_decomp: "x \<in> set xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"
898 by (auto elim: split_list)
900 lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
902 case Nil thus ?case by simp
907 assume "x = a" thus ?case using Cons by fastsimp
909 assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
913 lemma in_set_conv_decomp_first:
914 "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
915 by (auto dest!: split_list_first)
917 lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
918 proof (induct xs rule:rev_induct)
919 case Nil thus ?case by simp
924 assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
926 assume "x \<noteq> a" thus ?case using snoc by fastsimp
930 lemma in_set_conv_decomp_last:
931 "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
932 by (auto dest!: split_list_last)
934 lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x"
936 case Nil thus ?case by simp
939 by(simp add:Bex_def)(metis append_Cons append.simps(1))
942 lemma split_list_propE:
943 assumes "\<exists>x \<in> set xs. P x"
944 obtains ys x zs where "xs = ys @ x # zs" and "P x"
945 using split_list_prop [OF assms] by blast
947 lemma split_list_first_prop:
948 "\<exists>x \<in> set xs. P x \<Longrightarrow>
949 \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)"
951 case Nil thus ?case by simp
958 (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
961 hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
962 thus ?thesis using `\<not> P x` Cons(1) by (metis append_Cons set_ConsD)
966 lemma split_list_first_propE:
967 assumes "\<exists>x \<in> set xs. P x"
968 obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y"
969 using split_list_first_prop [OF assms] by blast
971 lemma split_list_first_prop_iff:
972 "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
973 (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))"
974 by (rule, erule split_list_first_prop) auto
976 lemma split_list_last_prop:
977 "\<exists>x \<in> set xs. P x \<Longrightarrow>
978 \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)"
979 proof(induct xs rule:rev_induct)
980 case Nil thus ?case by simp
985 assume "P x" thus ?thesis by (metis emptyE set_empty)
988 hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
989 thus ?thesis using `\<not> P x` snoc(1) by fastsimp
993 lemma split_list_last_propE:
994 assumes "\<exists>x \<in> set xs. P x"
995 obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z"
996 using split_list_last_prop [OF assms] by blast
998 lemma split_list_last_prop_iff:
999 "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
1000 (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
1001 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)
1003 lemma finite_list: "finite A ==> EX xs. set xs = A"
1004 by (erule finite_induct)
1005 (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))
1007 lemma card_length: "card (set xs) \<le> length xs"
1008 by (induct xs) (auto simp add: card_insert_if)
1010 lemma set_minus_filter_out:
1011 "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
1014 subsubsection {* @{text filter} *}
1016 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
1019 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"
1020 by (induct xs) simp_all
1022 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
1025 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
1026 by (induct xs) (auto simp add: le_SucI)
1028 lemma sum_length_filter_compl:
1029 "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
1030 by(induct xs) simp_all
1032 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
1035 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
1038 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
1039 by (induct xs) simp_all
1041 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
1044 apply(cut_tac P=P and xs=xs in length_filter_le)
1049 "filter P (map f xs) = map f (filter (P o f) xs)"
1050 by (induct xs) simp_all
1052 lemma length_filter_map[simp]:
1053 "length (filter P (map f xs)) = length(filter (P o f) xs)"
1054 by (simp add:filter_map)
1056 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
1059 lemma length_filter_less:
1060 "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
1062 case Nil thus ?case by simp
1064 case (Cons x xs) thus ?case
1065 apply (auto split:split_if_asm)
1066 using length_filter_le[of P xs] apply arith
1070 lemma length_filter_conv_card:
1071 "length(filter p xs) = card{i. i < length xs & p(xs!i)}"
1073 case Nil thus ?case by simp
1076 let ?S = "{i. i < length xs & p(xs!i)}"
1077 have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)
1078 show ?case (is "?l = card ?S'")
1081 hence eq: "?S' = insert 0 (Suc ` ?S)"
1082 by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
1083 have "length (filter p (x # xs)) = Suc(card ?S)"
1084 using Cons `p x` by simp
1085 also have "\<dots> = Suc(card(Suc ` ?S))" using fin
1086 by (simp add: card_image inj_Suc)
1087 also have "\<dots> = card ?S'" using eq fin
1088 by (simp add:card_insert_if) (simp add:image_def)
1089 finally show ?thesis .
1092 hence eq: "?S' = Suc ` ?S"
1093 by(auto simp add: image_def split:nat.split elim:lessE)
1094 have "length (filter p (x # xs)) = card ?S"
1095 using Cons `\<not> p x` by simp
1096 also have "\<dots> = card(Suc ` ?S)" using fin
1097 by (simp add: card_image inj_Suc)
1098 also have "\<dots> = card ?S'" using eq fin
1099 by (simp add:card_insert_if)
1100 finally show ?thesis .
1104 lemma Cons_eq_filterD:
1105 "x#xs = filter P ys \<Longrightarrow>
1106 \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
1107 (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
1109 case Nil thus ?case by simp
1112 show ?case (is "\<exists>x. ?Q x")
1118 with Py Cons.prems have "?Q []" by simp
1119 then show ?thesis ..
1121 assume "x \<noteq> y"
1122 with Py Cons.prems show ?thesis by simp
1126 with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
1127 then have "?Q (y#us)" by simp
1128 then show ?thesis ..
1132 lemma filter_eq_ConsD:
1133 "filter P ys = x#xs \<Longrightarrow>
1134 \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
1135 by(rule Cons_eq_filterD) simp
1137 lemma filter_eq_Cons_iff:
1138 "(filter P ys = x#xs) =
1139 (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
1140 by(auto dest:filter_eq_ConsD)
1142 lemma Cons_eq_filter_iff:
1143 "(x#xs = filter P ys) =
1144 (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
1145 by(auto dest:Cons_eq_filterD)
1147 lemma filter_cong[fundef_cong, recdef_cong]:
1148 "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
1150 apply(erule thin_rl)
1151 by (induct ys) simp_all
1154 subsubsection {* List partitioning *}
1156 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
1157 "partition P [] = ([], [])"
1158 | "partition P (x # xs) =
1159 (let (yes, no) = partition P xs
1160 in if P x then (x # yes, no) else (yes, x # no))"
1162 lemma partition_filter1:
1163 "fst (partition P xs) = filter P xs"
1164 by (induct xs) (auto simp add: Let_def split_def)
1166 lemma partition_filter2:
1167 "snd (partition P xs) = filter (Not o P) xs"
1168 by (induct xs) (auto simp add: Let_def split_def)
1171 assumes "partition P xs = (yes, no)"
1172 shows "(\<forall>p \<in> set yes. P p) \<and> (\<forall>p \<in> set no. \<not> P p)"
1174 from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
1176 then show ?thesis by (simp_all add: partition_filter1 partition_filter2)
1179 lemma partition_set:
1180 assumes "partition P xs = (yes, no)"
1181 shows "set yes \<union> set no = set xs"
1183 from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
1185 then show ?thesis by (auto simp add: partition_filter1 partition_filter2)
1189 subsubsection {* @{text concat} *}
1191 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
1194 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
1195 by (induct xss) auto
1197 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
1198 by (induct xss) auto
1200 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
1203 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
1206 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
1209 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
1212 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
1216 subsubsection {* @{text nth} *}
1218 lemma nth_Cons_0 [simp]: "(x # xs)!0 = x"
1221 lemma nth_Cons_Suc [simp]: "(x # xs)!(Suc n) = xs!n"
1224 declare nth.simps [simp del]
1227 "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
1228 apply (induct xs arbitrary: n, simp)
1229 apply (case_tac n, auto)
1232 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
1235 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
1238 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
1239 apply (induct xs arbitrary: n, simp)
1240 apply (case_tac n, auto)
1243 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
1244 by(cases xs) simp_all
1247 lemma list_eq_iff_nth_eq:
1248 "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
1249 apply(induct xs arbitrary: ys)
1253 apply(simp add:nth_Cons split:nat.split)apply blast
1256 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
1257 apply (induct xs, simp, simp)
1259 apply (metis nat_case_0 nth.simps zero_less_Suc)
1260 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
1261 apply (case_tac i, simp)
1262 apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
1265 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
1266 by(auto simp:set_conv_nth)
1268 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
1269 by (auto simp add: set_conv_nth)
1271 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"
1272 by (auto simp add: set_conv_nth)
1274 lemma all_nth_imp_all_set:
1275 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"
1276 by (auto simp add: set_conv_nth)
1278 lemma all_set_conv_all_nth:
1279 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"
1280 by (auto simp add: set_conv_nth)
1283 "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
1284 proof (induct xs arbitrary: n)
1285 case Nil thus ?case by simp
1288 hence n: "n < Suc (length xs)" by simp
1290 { assume "n < length xs"
1291 with n obtain n' where "length xs - n = Suc n'"
1292 by (cases "length xs - n", auto)
1294 then have "length xs - Suc n = n'" by simp
1296 have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
1299 show ?case by (clarsimp simp add: Cons nth_append)
1302 subsubsection {* @{text list_update} *}
1304 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
1305 by (induct xs arbitrary: i) (auto split: nat.split)
1307 lemma nth_list_update:
1308 "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
1309 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
1311 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
1312 by (simp add: nth_list_update)
1314 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
1315 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
1317 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
1318 by (induct xs arbitrary: i) (simp_all split:nat.splits)
1320 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
1321 apply (induct xs arbitrary: i)
1327 lemma list_update_same_conv:
1328 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
1329 by (induct xs arbitrary: i) (auto split: nat.split)
1331 lemma list_update_append1:
1332 "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
1333 apply (induct xs arbitrary: i, simp)
1334 apply(simp split:nat.split)
1337 lemma list_update_append:
1338 "(xs @ ys) [n:= x] =
1339 (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
1340 by (induct xs arbitrary: n) (auto split:nat.splits)
1342 lemma list_update_length [simp]:
1343 "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
1344 by (induct xs, auto)
1347 "length xs = length ys ==>
1348 (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
1349 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
1351 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
1352 by (induct xs arbitrary: i) (auto split: nat.split)
1354 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
1355 by (blast dest!: set_update_subset_insert [THEN subsetD])
1357 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
1358 by (induct xs arbitrary: n) (auto split:nat.splits)
1360 lemma list_update_overwrite:
1361 "xs [i := x, i := y] = xs [i := y]"
1362 apply (induct xs arbitrary: i)
1368 lemma list_update_swap:
1369 "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
1370 apply (induct xs arbitrary: i i')
1372 apply (case_tac i, case_tac i')
1379 subsubsection {* @{text last} and @{text butlast} *}
1381 lemma last_snoc [simp]: "last (xs @ [x]) = x"
1384 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
1387 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
1388 by(simp add:last.simps)
1390 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
1391 by(simp add:last.simps)
1393 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
1394 by (induct xs) (auto)
1396 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
1397 by(simp add:last_append)
1399 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
1400 by(simp add:last_append)
1402 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
1403 by(rule rev_exhaust[of xs]) simp_all
1405 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
1406 by(cases xs) simp_all
1408 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
1411 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
1412 by (induct xs rule: rev_induct) auto
1414 lemma butlast_append:
1415 "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
1416 by (induct xs arbitrary: ys) auto
1418 lemma append_butlast_last_id [simp]:
1419 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
1422 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
1423 by (induct xs) (auto split: split_if_asm)
1425 lemma in_set_butlast_appendI:
1426 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
1427 by (auto dest: in_set_butlastD simp add: butlast_append)
1429 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
1430 apply (induct xs arbitrary: n)
1432 apply (auto split:nat.split)
1435 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
1436 by(induct xs)(auto simp:neq_Nil_conv)
1438 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
1439 by (induct xs, simp, case_tac xs, simp_all)
1442 subsubsection {* @{text take} and @{text drop} *}
1444 lemma take_0 [simp]: "take 0 xs = []"
1447 lemma drop_0 [simp]: "drop 0 xs = xs"
1450 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
1453 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
1456 declare take_Cons [simp del] and drop_Cons [simp del]
1458 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
1459 by(clarsimp simp add:neq_Nil_conv)
1461 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
1462 by(cases xs, simp_all)
1464 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
1465 by (induct xs arbitrary: n) simp_all
1467 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
1468 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
1470 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
1471 by (cases n, simp, cases xs, auto)
1473 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
1474 by (simp only: drop_tl)
1476 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
1477 apply (induct xs arbitrary: n, simp)
1478 apply(simp add:drop_Cons nth_Cons split:nat.splits)
1481 lemma take_Suc_conv_app_nth:
1482 "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
1483 apply (induct xs arbitrary: i, simp)
1484 apply (case_tac i, auto)
1487 lemma drop_Suc_conv_tl:
1488 "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
1489 apply (induct xs arbitrary: i, simp)
1490 apply (case_tac i, auto)
1493 lemma length_take [simp]: "length (take n xs) = min (length xs) n"
1494 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1496 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
1497 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1499 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
1500 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1502 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
1503 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1505 lemma take_append [simp]:
1506 "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
1507 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1509 lemma drop_append [simp]:
1510 "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
1511 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1513 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
1514 apply (induct m arbitrary: xs n, auto)
1515 apply (case_tac xs, auto)
1516 apply (case_tac n, auto)
1519 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
1520 apply (induct m arbitrary: xs, auto)
1521 apply (case_tac xs, auto)
1524 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
1525 apply (induct m arbitrary: xs n, auto)
1526 apply (case_tac xs, auto)
1529 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
1530 apply(induct xs arbitrary: m n)
1532 apply(simp add: take_Cons drop_Cons split:nat.split)
1535 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
1536 apply (induct n arbitrary: xs, auto)
1537 apply (case_tac xs, auto)
1540 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
1541 apply(induct xs arbitrary: n)
1543 apply(simp add:take_Cons split:nat.split)
1546 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
1547 apply(induct xs arbitrary: n)
1549 apply(simp add:drop_Cons split:nat.split)
1552 lemma take_map: "take n (map f xs) = map f (take n xs)"
1553 apply (induct n arbitrary: xs, auto)
1554 apply (case_tac xs, auto)
1557 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
1558 apply (induct n arbitrary: xs, auto)
1559 apply (case_tac xs, auto)
1562 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
1563 apply (induct xs arbitrary: i, auto)
1564 apply (case_tac i, auto)
1567 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
1568 apply (induct xs arbitrary: i, auto)
1569 apply (case_tac i, auto)
1572 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
1573 apply (induct xs arbitrary: i n, auto)
1574 apply (case_tac n, blast)
1575 apply (case_tac i, auto)
1578 lemma nth_drop [simp]:
1579 "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
1580 apply (induct n arbitrary: xs i, auto)
1581 apply (case_tac xs, auto)
1585 "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
1586 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
1588 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
1589 by (simp add: butlast_conv_take drop_take)
1591 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
1592 by (simp add: butlast_conv_take min_max.inf_absorb1)
1594 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
1595 by (simp add: butlast_conv_take drop_take)
1597 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
1598 by(simp add: hd_conv_nth)
1600 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
1601 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
1603 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
1604 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
1606 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
1607 using set_take_subset by fast
1609 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
1610 using set_drop_subset by fast
1612 lemma append_eq_conv_conj:
1613 "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
1614 apply (induct xs arbitrary: zs, simp, clarsimp)
1615 apply (case_tac zs, auto)
1619 "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
1620 apply (induct xs arbitrary: i, auto)
1621 apply (case_tac i, simp_all)
1624 lemma append_eq_append_conv_if:
1625 "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
1626 (if size xs\<^isub>1 \<le> size ys\<^isub>1
1627 then xs\<^isub>1 = take (size xs\<^isub>1) ys\<^isub>1 \<and> xs\<^isub>2 = drop (size xs\<^isub>1) ys\<^isub>1 @ ys\<^isub>2
1628 else take (size ys\<^isub>1) xs\<^isub>1 = ys\<^isub>1 \<and> drop (size ys\<^isub>1) xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>2)"
1629 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
1631 apply(case_tac ys\<^isub>1)
1636 "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
1637 apply(induct xs arbitrary: n)
1639 apply(simp add:drop_Cons split:nat.split)
1642 lemma id_take_nth_drop:
1643 "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs"
1645 assume si: "i < length xs"
1646 hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
1648 from si have "take (Suc i) xs = take i xs @ [xs!i]"
1649 apply (rule_tac take_Suc_conv_app_nth) by arith
1650 ultimately show ?thesis by auto
1653 lemma upd_conv_take_nth_drop:
1654 "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
1656 assume i: "i < length xs"
1657 have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"
1658 by(rule arg_cong[OF id_take_nth_drop[OF i]])
1659 also have "\<dots> = take i xs @ a # drop (Suc i) xs"
1660 using i by (simp add: list_update_append)
1661 finally show ?thesis .
1665 "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
1666 apply (induct i arbitrary: xs)
1667 apply (simp add: neq_Nil_conv)
1675 subsubsection {* @{text takeWhile} and @{text dropWhile} *}
1677 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
1680 lemma takeWhile_append1 [simp]:
1681 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"
1684 lemma takeWhile_append2 [simp]:
1685 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
1688 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
1691 lemma dropWhile_append1 [simp]:
1692 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
1695 lemma dropWhile_append2 [simp]:
1696 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
1699 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
1700 by (induct xs) (auto split: split_if_asm)
1702 lemma takeWhile_eq_all_conv[simp]:
1703 "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
1706 lemma dropWhile_eq_Nil_conv[simp]:
1707 "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
1710 lemma dropWhile_eq_Cons_conv:
1711 "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
1714 text{* The following two lemmmas could be generalized to an arbitrary
1717 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1718 takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
1719 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
1721 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1722 dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
1726 apply(subst dropWhile_append2)
1730 lemma takeWhile_not_last:
1731 "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
1738 lemma takeWhile_cong [fundef_cong, recdef_cong]:
1739 "[| l = k; !!x. x : set l ==> P x = Q x |]
1740 ==> takeWhile P l = takeWhile Q k"
1741 by (induct k arbitrary: l) (simp_all)
1743 lemma dropWhile_cong [fundef_cong, recdef_cong]:
1744 "[| l = k; !!x. x : set l ==> P x = Q x |]
1745 ==> dropWhile P l = dropWhile Q k"
1746 by (induct k arbitrary: l, simp_all)
1749 subsubsection {* @{text zip} *}
1751 lemma zip_Nil [simp]: "zip [] ys = []"
1754 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
1757 declare zip_Cons [simp del]
1760 "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
1761 by(auto split:list.split)
1763 lemma length_zip [simp]:
1764 "length (zip xs ys) = min (length xs) (length ys)"
1765 by (induct xs ys rule:list_induct2') auto
1769 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
1770 by (induct xs zs rule:list_induct2') auto
1774 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
1775 by (induct xs ys rule:list_induct2') auto
1777 lemma zip_append [simp]:
1778 "[| length xs = length us; length ys = length vs |] ==>
1779 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
1780 by (simp add: zip_append1)
1783 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
1784 by (induct rule:list_induct2, simp_all)
1787 "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
1788 apply(induct xs arbitrary:ys) apply simp
1794 "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
1795 apply(induct xs arbitrary:ys) apply simp
1800 lemma nth_zip [simp]:
1801 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
1802 apply (induct ys arbitrary: i xs, simp)
1804 apply (simp_all add: nth.simps split: nat.split)
1808 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
1809 by (simp add: set_conv_nth cong: rev_conj_cong)
1812 "length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
1813 by (rule sym, simp add: update_zip)
1815 lemma zip_replicate [simp]:
1816 "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
1817 apply (induct i arbitrary: j, auto)
1818 apply (case_tac j, auto)
1822 "take n (zip xs ys) = zip (take n xs) (take n ys)"
1823 apply (induct n arbitrary: xs ys)
1825 apply (case_tac xs, simp)
1826 apply (case_tac ys, simp_all)
1830 "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
1831 apply (induct n arbitrary: xs ys)
1833 apply (case_tac xs, simp)
1834 apply (case_tac ys, simp_all)
1837 lemma set_zip_leftD:
1838 "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
1839 by (induct xs ys rule:list_induct2') auto
1841 lemma set_zip_rightD:
1842 "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
1843 by (induct xs ys rule:list_induct2') auto
1846 "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
1847 by(blast dest: set_zip_leftD set_zip_rightD)
1849 subsubsection {* @{text list_all2} *}
1851 lemma list_all2_lengthD [intro?]:
1852 "list_all2 P xs ys ==> length xs = length ys"
1853 by (simp add: list_all2_def)
1855 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
1856 by (simp add: list_all2_def)
1858 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
1859 by (simp add: list_all2_def)
1861 lemma list_all2_Cons [iff, code]:
1862 "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
1863 by (auto simp add: list_all2_def)
1865 lemma list_all2_Cons1:
1866 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
1869 lemma list_all2_Cons2:
1870 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
1873 lemma list_all2_rev [iff]:
1874 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
1875 by (simp add: list_all2_def zip_rev cong: conj_cong)
1877 lemma list_all2_rev1:
1878 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
1879 by (subst list_all2_rev [symmetric]) simp
1881 lemma list_all2_append1:
1882 "list_all2 P (xs @ ys) zs =
1883 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
1884 list_all2 P xs us \<and> list_all2 P ys vs)"
1885 apply (simp add: list_all2_def zip_append1)
1887 apply (rule_tac x = "take (length xs) zs" in exI)
1888 apply (rule_tac x = "drop (length xs) zs" in exI)
1889 apply (force split: nat_diff_split simp add: min_def, clarify)
1890 apply (simp add: ball_Un)
1893 lemma list_all2_append2:
1894 "list_all2 P xs (ys @ zs) =
1895 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
1896 list_all2 P us ys \<and> list_all2 P vs zs)"
1897 apply (simp add: list_all2_def zip_append2)
1899 apply (rule_tac x = "take (length ys) xs" in exI)
1900 apply (rule_tac x = "drop (length ys) xs" in exI)
1901 apply (force split: nat_diff_split simp add: min_def, clarify)
1902 apply (simp add: ball_Un)
1905 lemma list_all2_append:
1906 "length xs = length ys \<Longrightarrow>
1907 list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
1908 by (induct rule:list_induct2, simp_all)
1910 lemma list_all2_appendI [intro?, trans]:
1911 "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
1912 by (simp add: list_all2_append list_all2_lengthD)
1914 lemma list_all2_conv_all_nth:
1915 "list_all2 P xs ys =
1916 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
1917 by (force simp add: list_all2_def set_zip)
1919 lemma list_all2_trans:
1920 assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
1921 shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
1922 (is "!!bs cs. PROP ?Q as bs cs")
1924 fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
1925 show "!!cs. PROP ?Q (x # xs) bs cs"
1927 fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"
1928 show "PROP ?Q (x # xs) (y # ys) cs"
1929 by (induct cs) (auto intro: tr I1 I2)
1933 lemma list_all2_all_nthI [intro?]:
1934 "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
1935 by (simp add: list_all2_conv_all_nth)
1938 "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
1939 by (simp add: list_all2_def)
1941 lemma list_all2_nthD:
1942 "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
1943 by (simp add: list_all2_conv_all_nth)
1945 lemma list_all2_nthD2:
1946 "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
1947 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
1949 lemma list_all2_map1:
1950 "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
1951 by (simp add: list_all2_conv_all_nth)
1953 lemma list_all2_map2:
1954 "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
1955 by (auto simp add: list_all2_conv_all_nth)
1957 lemma list_all2_refl [intro?]:
1958 "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
1959 by (simp add: list_all2_conv_all_nth)
1961 lemma list_all2_update_cong:
1962 "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
1963 by (simp add: list_all2_conv_all_nth nth_list_update)
1965 lemma list_all2_update_cong2:
1966 "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
1967 by (simp add: list_all2_lengthD list_all2_update_cong)
1969 lemma list_all2_takeI [simp,intro?]:
1970 "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
1971 apply (induct xs arbitrary: n ys)
1973 apply (clarsimp simp add: list_all2_Cons1)
1978 lemma list_all2_dropI [simp,intro?]:
1979 "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
1980 apply (induct as arbitrary: n bs, simp)
1981 apply (clarsimp simp add: list_all2_Cons1)
1982 apply (case_tac n, simp, simp)
1985 lemma list_all2_mono [intro?]:
1986 "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
1987 apply (induct xs arbitrary: ys, simp)
1988 apply (case_tac ys, auto)
1992 "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
1993 by (induct xs ys rule: list_induct2') auto
1996 subsubsection {* @{text foldl} and @{text foldr} *}
1998 lemma foldl_append [simp]:
1999 "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
2000 by (induct xs arbitrary: a) auto
2002 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
2005 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
2006 by(induct xs) simp_all
2008 text{* For efficient code generation: avoid intermediate list. *}
2009 lemma foldl_map[code unfold]:
2010 "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
2011 by(induct xs arbitrary:a) simp_all
2013 lemma foldl_cong [fundef_cong, recdef_cong]:
2014 "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
2015 ==> foldl f a l = foldl g b k"
2016 by (induct k arbitrary: a b l) simp_all
2018 lemma foldr_cong [fundef_cong, recdef_cong]:
2019 "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]
2020 ==> foldr f l a = foldr g k b"
2021 by (induct k arbitrary: a b l) simp_all
2023 lemma (in semigroup_add) foldl_assoc:
2024 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
2025 by (induct zs arbitrary: y) (simp_all add:add_assoc)
2027 lemma (in monoid_add) foldl_absorb0:
2028 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
2029 by (induct zs) (simp_all add:foldl_assoc)
2032 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
2034 lemma foldl_foldr1_lemma:
2035 "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
2036 by (induct xs arbitrary: a) (auto simp:add_assoc)
2038 corollary foldl_foldr1:
2039 "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
2040 by (simp add:foldl_foldr1_lemma)
2043 text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
2045 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
2048 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
2049 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
2051 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
2052 by (induct xs, auto simp add: foldl_assoc add_commute)
2055 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
2056 difficult to use because it requires an additional transitivity step.
2059 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
2060 by (induct ns arbitrary: n) auto
2062 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
2063 by (force intro: start_le_sum simp add: in_set_conv_decomp)
2065 lemma sum_eq_0_conv [iff]:
2066 "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
2067 by (induct ns arbitrary: m) auto
2069 lemma foldr_invariant:
2070 "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f x y) \<rbrakk> \<Longrightarrow> Q (foldr f xs x)"
2071 by (induct xs, simp_all)
2073 lemma foldl_invariant:
2074 "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f y x) \<rbrakk> \<Longrightarrow> Q (foldl f x xs)"
2075 by (induct xs arbitrary: x, simp_all)
2077 text{* @{const foldl} and @{text concat} *}
2079 lemma foldl_conv_concat:
2080 "foldl (op @) xs xss = xs @ concat xss"
2081 proof (induct xss arbitrary: xs)
2082 case Nil show ?case by simp
2084 interpret monoid_add "[]" "op @" proof qed simp_all
2085 case Cons then show ?case by (simp add: foldl_absorb0)
2088 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
2089 by (simp add: foldl_conv_concat)
2092 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
2094 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
2095 by (induct xs) (simp_all add:add_assoc)
2097 lemma listsum_rev [simp]:
2098 fixes xs :: "'a\<Colon>comm_monoid_add list"
2099 shows "listsum (rev xs) = listsum xs"
2100 by (induct xs) (simp_all add:add_ac)
2102 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
2105 lemma length_concat: "length (concat xss) = listsum (map length xss)"
2106 by (induct xss) simp_all
2108 text{* For efficient code generation ---
2109 @{const listsum} is not tail recursive but @{const foldl} is. *}
2110 lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
2111 by(simp add:listsum_foldr foldl_foldr1)
2114 text{* Some syntactic sugar for summing a function over a list: *}
2117 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
2119 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
2120 syntax (HTML output)
2121 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
2123 translations -- {* Beware of argument permutation! *}
2124 "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
2125 "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
2127 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
2128 by (induct xs) (simp_all add: left_distrib)
2130 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
2131 by (induct xs) (simp_all add: left_distrib)
2133 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
2134 lemma uminus_listsum_map:
2135 fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
2136 shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
2137 by (induct xs) simp_all
2140 subsubsection {* @{text upt} *}
2142 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
2143 -- {* simp does not terminate! *}
2146 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
2147 by (subst upt_rec) simp
2149 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
2150 by(induct j)simp_all
2152 lemma upt_eq_Cons_conv:
2153 "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
2154 apply(induct j arbitrary: x xs)
2156 apply(clarsimp simp add: append_eq_Cons_conv)
2160 lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
2161 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}
2164 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
2165 by (simp add: upt_rec)
2167 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
2168 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
2171 lemma length_upt [simp]: "length [i..<j] = j - i"
2172 by (induct j) (auto simp add: Suc_diff_le)
2174 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
2176 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
2180 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
2181 by(simp add:upt_conv_Cons)
2183 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
2186 by(simp add:upt_Suc_append)
2188 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
2189 apply (induct m arbitrary: i, simp)
2190 apply (subst upt_rec)
2192 apply (subst upt_rec)
2193 apply (simp del: upt.simps)
2196 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
2201 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
2204 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
2205 apply (induct n m arbitrary: i rule: diff_induct)
2206 prefer 3 apply (subst map_Suc_upt[symmetric])
2207 apply (auto simp add: less_diff_conv nth_upt)
2210 lemma nth_take_lemma:
2211 "k <= length xs ==> k <= length ys ==>
2212 (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
2213 apply (atomize, induct k arbitrary: xs ys)
2214 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
2215 txt {* Both lists must be non-empty *}
2216 apply (case_tac xs, simp)
2217 apply (case_tac ys, clarify)
2218 apply (simp (no_asm_use))
2220 txt {* prenexing's needed, not miniscoping *}
2221 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)
2225 lemma nth_equalityI:
2226 "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
2227 apply (frule nth_take_lemma [OF le_refl eq_imp_le])
2228 apply (simp_all add: take_all)
2232 "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
2233 by (rule nth_equalityI, auto)
2235 (* needs nth_equalityI *)
2236 lemma list_all2_antisym:
2237 "\<lbrakk> (\<And>x y. \<lbrakk>P x y; Q y x\<rbrakk> \<Longrightarrow> x = y); list_all2 P xs ys; list_all2 Q ys xs \<rbrakk>
2238 \<Longrightarrow> xs = ys"
2239 apply (simp add: list_all2_conv_all_nth)
2240 apply (rule nth_equalityI, blast, simp)
2243 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
2244 -- {* The famous take-lemma. *}
2245 apply (drule_tac x = "max (length xs) (length ys)" in spec)
2246 apply (simp add: le_max_iff_disj take_all)
2251 "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
2252 by (cases n) simp_all
2255 "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
2256 by (cases n) simp_all
2258 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
2259 by (cases n) simp_all
2261 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
2262 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
2263 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
2265 declare take_Cons_number_of [simp]
2266 drop_Cons_number_of [simp]
2267 nth_Cons_number_of [simp]
2270 subsubsection {* @{text "distinct"} and @{text remdups} *}
2272 lemma distinct_append [simp]:
2273 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
2276 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
2279 lemma set_remdups [simp]: "set (remdups xs) = set xs"
2280 by (induct xs) (auto simp add: insert_absorb)
2282 lemma distinct_remdups [iff]: "distinct (remdups xs)"
2285 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
2286 by (induct xs, auto)
2288 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
2289 by (metis distinct_remdups distinct_remdups_id)
2291 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
2292 by (metis distinct_remdups finite_list set_remdups)
2294 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
2297 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
2300 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
2303 lemma length_remdups_eq[iff]:
2304 "(length (remdups xs) = length xs) = (remdups xs = xs)"
2307 apply(subgoal_tac "length (remdups xs) <= length xs")
2309 apply(rule length_remdups_leq)
2314 "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
2318 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
2321 lemma distinct_upt[simp]: "distinct[i..<j]"
2324 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
2325 apply(induct xs arbitrary: i)
2329 apply(blast dest:in_set_takeD)
2332 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
2333 apply(induct xs arbitrary: i)
2339 lemma distinct_list_update:
2340 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
2341 shows "distinct (xs[i:=a])"
2342 proof (cases "i < length xs")
2344 with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
2345 apply (drule_tac id_take_nth_drop) by simp
2346 with d True show ?thesis
2347 apply (simp add: upd_conv_take_nth_drop)
2348 apply (drule subst [OF id_take_nth_drop]) apply assumption
2349 apply simp apply (cases "a = xs!i") apply simp by blast
2351 case False with d show ?thesis by auto
2355 text {* It is best to avoid this indexed version of distinct, but
2356 sometimes it is useful. *}
2358 lemma distinct_conv_nth:
2359 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
2360 apply (induct xs, simp, simp)
2361 apply (rule iffI, clarsimp)
2363 apply (case_tac j, simp)
2364 apply (simp add: set_conv_nth)
2366 apply (clarsimp simp add: set_conv_nth, simp)
2369 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
2371 apply (clarsimp simp add: set_conv_nth)
2372 apply (erule_tac x = 0 in allE, simp)
2373 apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
2375 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
2377 apply (erule_tac x = "Suc i" in allE, simp)
2378 apply (erule_tac x = "Suc j" in allE, simp)
2381 lemma nth_eq_iff_index_eq:
2382 "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
2383 by(auto simp: distinct_conv_nth)
2385 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
2388 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
2390 case Nil thus ?case by simp
2394 proof (cases "x \<in> set xs")
2395 case False with Cons show ?thesis by simp
2397 case True with Cons.prems
2398 have "card (set xs) = Suc (length xs)"
2399 by (simp add: card_insert_if split: split_if_asm)
2400 moreover have "card (set xs) \<le> length xs" by (rule card_length)
2401 ultimately have False by simp
2406 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
2407 apply (induct n == "length ws" arbitrary:ws) apply simp
2408 apply(case_tac ws) apply simp
2409 apply (simp split:split_if_asm)
2410 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
2413 lemma length_remdups_concat:
2414 "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
2415 by(simp add: set_concat distinct_card[symmetric])
2418 subsubsection {* @{text remove1} *}
2420 lemma remove1_append:
2421 "remove1 x (xs @ ys) =
2422 (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
2425 lemma in_set_remove1[simp]:
2426 "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
2431 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
2438 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
2445 lemma length_remove1:
2446 "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
2448 apply (auto dest!:length_pos_if_in_set)
2451 lemma remove1_filter_not[simp]:
2452 "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
2455 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
2456 apply(insert set_remove1_subset)
2460 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
2461 by (induct xs) simp_all
2464 subsubsection {* @{text removeAll} *}
2466 lemma removeAll_append[simp]:
2467 "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
2470 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
2473 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
2476 (* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
2477 lemma length_removeAll:
2478 "length(removeAll x xs) = length xs - count x xs"
2481 lemma removeAll_filter_not[simp]:
2482 "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
2486 lemma distinct_remove1_removeAll:
2487 "distinct xs ==> remove1 x xs = removeAll x xs"
2488 by (induct xs) simp_all
2490 lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>
2491 map f (removeAll x xs) = removeAll (f x) (map f xs)"
2492 by (induct xs) (simp_all add:inj_on_def)
2494 lemma map_removeAll_inj: "inj f \<Longrightarrow>
2495 map f (removeAll x xs) = removeAll (f x) (map f xs)"
2496 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
2499 subsubsection {* @{text replicate} *}
2501 lemma length_replicate [simp]: "length (replicate n x) = n"
2504 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
2507 lemma replicate_app_Cons_same:
2508 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
2511 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
2512 apply (induct n, simp)
2513 apply (simp add: replicate_app_Cons_same)
2516 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
2519 text{* Courtesy of Matthias Daum: *}
2520 lemma append_replicate_commute:
2521 "replicate n x @ replicate k x = replicate k x @ replicate n x"
2522 apply (simp add: replicate_add [THEN sym])
2523 apply (simp add: add_commute)
2526 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
2529 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"
2532 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
2533 by (atomize (full), induct n) auto
2535 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
2536 apply (induct n arbitrary: i, simp)
2537 apply (simp add: nth_Cons split: nat.split)
2540 text{* Courtesy of Matthias Daum (2 lemmas): *}
2541 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
2542 apply (case_tac "k \<le> i")
2543 apply (simp add: min_def)
2544 apply (drule not_leE)
2545 apply (simp add: min_def)
2546 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
2548 apply (simp add: replicate_add [symmetric])
2551 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
2552 apply (induct k arbitrary: i)
2561 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
2564 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
2565 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
2567 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
2570 lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
2571 by (simp add: set_replicate_conv_if split: split_if_asm)
2573 lemma replicate_append_same:
2574 "replicate i x @ [x] = x # replicate i x"
2575 by (induct i) simp_all
2577 lemma map_replicate_trivial:
2578 "map (\<lambda>i. x) [0..<i] = replicate i x"
2579 by (induct i) (simp_all add: replicate_append_same)
2582 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
2585 lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"
2588 lemma replicate_eq_replicate[simp]:
2589 "(replicate m x = replicate n y) \<longleftrightarrow> (m=n & (m\<noteq>0 \<longrightarrow> x=y))"
2590 apply(induct m arbitrary: n)
2597 subsubsection{*@{text rotate1} and @{text rotate}*}
2599 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
2600 by(simp add:rotate1_def)
2602 lemma rotate0[simp]: "rotate 0 = id"
2603 by(simp add:rotate_def)
2605 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
2606 by(simp add:rotate_def)
2609 "rotate (m+n) = rotate m o rotate n"
2610 by(simp add:rotate_def funpow_add)
2612 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
2613 by(simp add:rotate_add)
2615 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
2616 by(simp add:rotate_def funpow_swap1)
2618 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
2619 by(cases xs) simp_all
2621 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
2624 apply (simp add:rotate_def)
2627 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
2628 by(simp add:rotate1_def split:list.split)
2630 lemma rotate_drop_take:
2631 "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
2634 apply(simp add:rotate_def)
2635 apply(cases "xs = []")
2637 apply(case_tac "n mod length xs = 0")
2638 apply(simp add:mod_Suc)
2639 apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
2640 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
2641 take_hd_drop linorder_not_le)
2644 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
2645 by(simp add:rotate_drop_take)
2647 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
2648 by(simp add:rotate_drop_take)
2650 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
2651 by(simp add:rotate1_def split:list.split)
2653 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
2654 by (induct n arbitrary: xs) (simp_all add:rotate_def)
2656 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
2657 by(simp add:rotate1_def split:list.split) blast
2659 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
2660 by (induct n) (simp_all add:rotate_def)
2662 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
2663 by(simp add:rotate_drop_take take_map drop_map)
2665 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
2666 by(simp add:rotate1_def split:list.split)
2668 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
2669 by (induct n) (simp_all add:rotate_def)
2671 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
2672 by(simp add:rotate1_def split:list.split)
2674 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
2675 by (induct n) (simp_all add:rotate_def)
2678 "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
2679 apply(simp add:rotate_drop_take rev_drop rev_take)
2680 apply(cases "length xs = 0")
2682 apply(cases "n mod length xs = 0")
2684 apply(simp add:rotate_drop_take rev_drop rev_take)
2687 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
2688 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
2689 apply(subgoal_tac "length xs \<noteq> 0")
2691 using mod_less_divisor[of "length xs" n] by arith
2694 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
2696 lemma sublist_empty [simp]: "sublist xs {} = []"
2697 by (auto simp add: sublist_def)
2699 lemma sublist_nil [simp]: "sublist [] A = []"
2700 by (auto simp add: sublist_def)
2702 lemma length_sublist:
2703 "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
2704 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
2706 lemma sublist_shift_lemma_Suc:
2707 "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
2708 map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
2709 apply(induct xs arbitrary: "is")
2711 apply (case_tac "is")
2716 lemma sublist_shift_lemma:
2717 "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
2718 map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
2719 by (induct xs rule: rev_induct) (simp_all add: add_commute)
2721 lemma sublist_append:
2722 "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
2723 apply (unfold sublist_def)
2724 apply (induct l' rule: rev_induct, simp)
2725 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
2726 apply (simp add: add_commute)
2730 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
2731 apply (induct l rule: rev_induct)
2732 apply (simp add: sublist_def)
2733 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
2736 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
2737 apply(induct xs arbitrary: I)
2738 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
2741 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
2742 by(auto simp add:set_sublist)
2744 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
2745 by(auto simp add:set_sublist)
2747 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
2748 by(auto simp add:set_sublist)
2750 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
2751 by (simp add: sublist_Cons)
2754 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
2755 apply(induct xs arbitrary: I)
2757 apply(auto simp add:sublist_Cons)
2761 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
2762 apply (induct l rule: rev_induct, simp)
2763 apply (simp split: nat_diff_split add: sublist_append)
2766 lemma filter_in_sublist:
2767 "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
2768 proof (induct xs arbitrary: s)
2769 case Nil thus ?case by simp
2772 moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
2773 ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
2777 subsubsection {* @{const splice} *}
2779 lemma splice_Nil2 [simp, code]:
2781 by (cases xs) simp_all
2783 lemma splice_Cons_Cons [simp, code]:
2784 "splice (x#xs) (y#ys) = x # y # splice xs ys"
2787 declare splice.simps(2) [simp del, code del]
2789 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
2790 apply(induct xs arbitrary: ys) apply simp
2796 subsubsection {* Infiniteness *}
2798 lemma finite_maxlen:
2799 "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
2800 proof (induct rule: finite.induct)
2801 case emptyI show ?case by simp
2804 then obtain n where "\<forall>s\<in>M. length s < n" by blast
2805 hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
2809 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
2811 apply(drule finite_maxlen)
2812 apply (metis UNIV_I length_replicate less_not_refl)
2816 subsection {*Sorting*}
2818 text{* Currently it is not shown that @{const sort} returns a
2819 permutation of its input because the nicest proof is via multisets,
2820 which are not yet available. Alternatively one could define a function
2821 that counts the number of occurrences of an element in a list and use
2822 that instead of multisets to state the correctness property. *}
2827 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
2828 apply(induct xs arbitrary: x) apply simp
2829 by simp (blast intro: order_trans)
2831 lemma sorted_append:
2832 "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
2833 by (induct xs) (auto simp add:sorted_Cons)
2835 lemma set_insort: "set(insort x xs) = insert x (set xs)"
2838 lemma set_sort[simp]: "set(sort xs) = set xs"
2839 by (induct xs) (simp_all add:set_insort)
2841 lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
2842 by(induct xs)(auto simp:set_insort)
2844 lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
2845 by(induct xs)(simp_all add:distinct_insort set_sort)
2847 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
2849 apply(auto simp:sorted_Cons set_insort)
2852 theorem sorted_sort[simp]: "sorted (sort xs)"
2853 by (induct xs) (auto simp:sorted_insort)
2855 lemma insort_is_Cons: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
2858 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
2859 by (induct xs, auto simp add: sorted_Cons)
2861 lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
2862 by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
2864 lemma sorted_remdups[simp]:
2865 "sorted l \<Longrightarrow> sorted (remdups l)"
2866 by (induct l) (auto simp: sorted_Cons)
2868 lemma sorted_distinct_set_unique:
2869 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
2872 from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
2873 from assms show ?thesis
2874 proof(induct rule:list_induct2[OF 1])
2875 case 1 show ?case by simp
2877 case 2 thus ?case by (simp add:sorted_Cons)
2878 (metis Diff_insert_absorb antisym insertE insert_iff)
2882 lemma finite_sorted_distinct_unique:
2883 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
2884 apply(drule finite_distinct_list)
2886 apply(rule_tac a="sort xs" in ex1I)
2887 apply (auto simp: sorted_distinct_set_unique)
2891 "sorted xs \<Longrightarrow> sorted (take n xs)"
2892 proof (induct xs arbitrary: n rule: sorted.induct)
2893 case 1 show ?case by simp
2895 case 2 show ?case by (cases n) simp_all
2898 then have "x \<le> y" by simp
2899 show ?case proof (cases n)
2900 case 0 then show ?thesis by simp
2903 with 3 have "sorted (take m (y # xs))" by simp
2904 with Suc `x \<le> y` show ?thesis by (cases m) simp_all
2909 "sorted xs \<Longrightarrow> sorted (drop n xs)"
2910 proof (induct xs arbitrary: n rule: sorted.induct)
2911 case 1 show ?case by simp
2913 case 2 show ?case by (cases n) simp_all
2915 case 3 then show ?case by (cases n) simp_all
2921 lemma sorted_upt[simp]: "sorted[i..<j]"
2922 by (induct j) (simp_all add:sorted_append)
2925 subsubsection {* @{text sorted_list_of_set} *}
2927 text{* This function maps (finite) linearly ordered sets to sorted
2928 lists. Warning: in most cases it is not a good idea to convert from
2929 sets to lists but one should convert in the other direction (via
2937 sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
2938 [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
2940 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
2941 set(sorted_list_of_set A) = A &
2942 sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
2943 apply(simp add:sorted_list_of_set_def)
2945 apply(simp_all add: finite_sorted_distinct_unique)
2948 lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
2949 unfolding sorted_list_of_set_def
2950 apply(subst the_equality[of _ "[]"])
2957 subsubsection {* @{text upto}: the generic interval-list *}
2959 class finite_intvl_succ = linorder +
2960 fixes successor :: "'a \<Rightarrow> 'a"
2961 assumes finite_intvl: "finite{a..b}"
2962 and successor_incr: "a < successor a"
2963 and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
2965 context finite_intvl_succ
2969 upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
2970 "upto i j == sorted_list_of_set {i..j}"
2972 lemma upto[simp]: "set[a..b] = {a..b} & sorted[a..b] & distinct[a..b]"
2973 by(simp add:upto_def finite_intvl)
2975 lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
2976 apply(insert successor_incr[of i])
2977 apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
2978 apply(metis ord_discrete less_le not_le)
2981 lemma sorted_list_of_set_rec: "i \<le> j \<Longrightarrow>
2982 sorted_list_of_set {i..j} = i # sorted_list_of_set {successor i..j}"
2983 apply(simp add:sorted_list_of_set_def upto_def)
2984 apply (rule the1_equality[OF finite_sorted_distinct_unique])
2985 apply (simp add:finite_intvl)
2986 apply(rule the1I2[OF finite_sorted_distinct_unique])
2987 apply (simp add:finite_intvl)
2988 apply (simp add: sorted_Cons insert_intvl Ball_def)
2989 apply (metis successor_incr leD less_imp_le order_trans)
2992 lemma sorted_list_of_set_rec2: "i \<le> j \<Longrightarrow>
2993 sorted_list_of_set {i..successor j} =
2994 sorted_list_of_set {i..j} @ [successor j]"
2995 apply(simp add:sorted_list_of_set_def upto_def)
2996 apply (rule the1_equality[OF finite_sorted_distinct_unique])
2997 apply (simp add:finite_intvl)
2998 apply(rule the1I2[OF finite_sorted_distinct_unique])
2999 apply (simp add:finite_intvl)
3000 apply (simp add: sorted_append Ball_def expand_set_eq)
3002 apply (metis eq_iff leD linear not_leE ord_discrete order_trans successor_incr)
3003 apply (metis leD linear order_trans successor_incr)
3006 lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
3007 by(simp add: upto_def sorted_list_of_set_rec)
3009 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
3010 by(simp add: upto_rec)
3012 lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..successor j] = [i..j] @ [successor j]"
3013 by(simp add: upto_def sorted_list_of_set_rec2)
3017 text{* The integers are an instance of the above class: *}
3019 instantiation int:: finite_intvl_succ
3023 successor_int_def: "successor = (%i\<Colon>int. i+1)"
3026 by intro_classes (simp_all add: successor_int_def)
3030 text{* Now @{term"[i..j::int]"} is defined for integers. *}
3032 hide (open) const successor
3034 lemma upto_rec2_int: "(i::int) \<le> j \<Longrightarrow> [i..j+1] = [i..j] @ [j+1]"
3035 by(rule upto_rec2[where 'a = int, simplified successor_int_def])
3038 subsubsection {* @{text lists}: the list-forming operator over sets *}
3041 lists :: "'a set => 'a list set"
3044 Nil [intro!]: "[]: lists A"
3045 | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
3047 inductive_cases listsE [elim!,noatp]: "x#l : lists A"
3048 inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
3050 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
3051 by (rule predicate1I, erule listsp.induct, blast+)
3053 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
3056 assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
3059 lemmas lists_IntI = listsp_infI [to_set]
3061 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
3062 proof (rule mono_inf [where f=listsp, THEN order_antisym])
3063 show "mono listsp" by (simp add: mono_def listsp_mono)
3064 show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
3067 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
3069 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
3071 lemma append_in_listsp_conv [iff]:
3072 "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
3075 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
3077 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
3078 -- {* eliminate @{text listsp} in favour of @{text set} *}
3081 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
3083 lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
3084 by (rule in_listsp_conv_set [THEN iffD1])
3086 lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
3088 lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
3089 by (rule in_listsp_conv_set [THEN iffD2])
3091 lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
3093 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
3098 subsubsection{* Inductive definition for membership *}
3100 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
3102 elem: "ListMem x (x # xs)"
3103 | insert: "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
3105 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
3107 apply (induct set: ListMem)
3110 apply (auto intro: ListMem.intros)
3115 subsubsection{*Lists as Cartesian products*}
3117 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
3118 @{term A} and tail drawn from @{term Xs}.*}
3121 set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
3122 "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
3123 declare set_Cons_def [code del]
3125 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
3126 by (auto simp add: set_Cons_def)
3128 text{*Yields the set of lists, all of the same length as the argument and
3129 with elements drawn from the corresponding element of the argument.*}
3131 consts listset :: "'a set list \<Rightarrow> 'a list set"
3134 "listset(A#As) = set_Cons A (listset As)"
3137 subsection{*Relations on Lists*}
3139 subsubsection {* Length Lexicographic Ordering *}
3141 text{*These orderings preserve well-foundedness: shorter lists
3142 precede longer lists. These ordering are not used in dictionaries.*}
3144 consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
3145 --{*The lexicographic ordering for lists of the specified length*}
3149 (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
3150 {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
3153 lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
3154 "lex r == \<Union>n. lexn r n"
3155 --{*Holds only between lists of the same length*}
3157 lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
3158 "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
3159 --{*Compares lists by their length and then lexicographically*}
3161 declare lex_def [code del]
3164 lemma wf_lexn: "wf r ==> wf (lexn r n)"
3165 apply (induct n, simp, simp)
3166 apply(rule wf_subset)
3167 prefer 2 apply (rule Int_lower1)
3168 apply(rule wf_prod_fun_image)
3169 prefer 2 apply (rule inj_onI, auto)
3173 "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
3174 by (induct n arbitrary: xs ys) auto
3176 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
3177 apply (unfold lex_def)
3179 apply (blast intro: wf_lexn, clarify)
3180 apply (rename_tac m n)
3181 apply (subgoal_tac "m \<noteq> n")
3182 prefer 2 apply blast
3183 apply (blast dest: lexn_length not_sym)
3188 {(xs,ys). length xs = n \<and> length ys = n \<and>
3189 (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
3190 apply (induct n, simp)
3191 apply (simp add: image_Collect lex_prod_def, safe, blast)
3192 apply (rule_tac x = "ab # xys" in exI, simp)
3193 apply (case_tac xys, simp_all, blast)
3198 {(xs,ys). length xs = length ys \<and>
3199 (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
3200 by (force simp add: lex_def lexn_conv)
3202 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
3203 by (unfold lenlex_def) blast
3206 "lenlex r = {(xs,ys). length xs < length ys |
3207 length xs = length ys \<and> (xs, ys) : lex r}"
3208 by (simp add: lenlex_def diag_def lex_prod_def inv_image_def)
3210 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
3211 by (simp add: lex_conv)
3213 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
3214 by (simp add:lex_conv)
3216 lemma Cons_in_lex [simp]:
3217 "((x # xs, y # ys) : lex r) =
3218 ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
3219 apply (simp add: lex_conv)
3221 prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
3222 apply (case_tac xys, simp, simp)
3227 subsubsection {* Lexicographic Ordering *}
3229 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
3230 This ordering does \emph{not} preserve well-foundedness.
3231 Author: N. Voelker, March 2005. *}
3234 lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set"
3235 "lexord r == {(x,y). \<exists> a v. y = x @ a # v \<or>
3236 (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
3237 declare lexord_def [code del]
3239 lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
3240 by (unfold lexord_def, induct_tac y, auto)
3242 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
3243 by (unfold lexord_def, induct_tac x, auto)
3245 lemma lexord_cons_cons[simp]:
3246 "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
3247 apply (unfold lexord_def, safe, simp_all)
3248 apply (case_tac u, simp, simp)
3249 apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
3250 apply (erule_tac x="b # u" in allE)
3253 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
3255 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
3256 by (induct_tac x, auto)
3258 lemma lexord_append_left_rightI:
3259 "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
3260 by (induct_tac u, auto)
3262 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
3265 lemma lexord_append_leftD:
3266 "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
3267 by (erule rev_mp, induct_tac x, auto)
3269 lemma lexord_take_index_conv:
3270 "((x,y) : lexord r) =
3271 ((length x < length y \<and> take (length x) y = x) \<or>
3272 (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
3273 apply (unfold lexord_def Let_def, clarsimp)
3274 apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
3276 apply (rule_tac x="hd (drop (length x) y)" in exI)
3277 apply (rule_tac x="tl (drop (length x) y)" in exI)
3278 apply (erule subst, simp add: min_def)
3279 apply (rule_tac x ="length u" in exI, simp)
3280 apply (rule_tac x ="take i x" in exI)
3281 apply (rule_tac x ="x ! i" in exI)
3282 apply (rule_tac x ="y ! i" in exI, safe)
3283 apply (rule_tac x="drop (Suc i) x" in exI)
3284 apply (drule sym, simp add: drop_Suc_conv_tl)
3285 apply (rule_tac x="drop (Suc i) y" in exI)
3286 by (simp add: drop_Suc_conv_tl)
3288 -- {* lexord is extension of partial ordering List.lex *}
3289 lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
3290 apply (rule_tac x = y in spec)
3291 apply (induct_tac x, clarsimp)
3292 by (clarify, case_tac x, simp, force)
3294 lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
3298 "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
3299 apply (erule rev_mp)+
3300 apply (rule_tac x = x in spec)
3301 apply (rule_tac x = z in spec)
3302 apply ( induct_tac y, simp, clarify)
3303 apply (case_tac xa, erule ssubst)
3304 apply (erule allE, erule allE) -- {* avoid simp recursion *}
3305 apply (case_tac x, simp, simp)
3306 apply (case_tac x, erule allE, erule allE, simp)
3307 apply (erule_tac x = listb in allE)
3308 apply (erule_tac x = lista in allE, simp)
3309 apply (unfold trans_def)
3312 lemma lexord_transI: "trans r \<Longrightarrow> trans (lexord r)"
3313 by (rule transI, drule lexord_trans, blast)
3315 lemma lexord_linear: "(! a b. (a,b)\<in> r | a = b | (b,a) \<in> r) \<Longrightarrow> (x,y) : lexord r | x = y | (y,x) : lexord r"
3316 apply (rule_tac x = y in spec)
3317 apply (induct_tac x, rule allI)
3318 apply (case_tac x, simp, simp)
3319 apply (rule allI, case_tac x, simp, simp)
3323 subsection {* Lexicographic combination of measure functions *}
3325 text {* These are useful for termination proofs *}
3328 "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
3330 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
3331 unfolding measures_def
3334 lemma in_measures[simp]:
3335 "(x, y) \<in> measures [] = False"
3336 "(x, y) \<in> measures (f # fs)
3337 = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"
3338 unfolding measures_def
3341 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
3344 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
3348 subsubsection{*Lifting a Relation on List Elements to the Lists*}
3351 listrel :: "('a * 'a)set => ('a list * 'a list)set"
3352 for r :: "('a * 'a)set"
3354 Nil: "([],[]) \<in> listrel r"
3355 | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
3357 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
3358 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
3359 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
3360 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
3363 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
3365 apply (erule listrel.induct)
3366 apply (blast intro: listrel.intros)+
3369 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
3371 apply (erule listrel.induct, auto)
3374 lemma listrel_refl: "refl A r \<Longrightarrow> refl (lists A) (listrel r)"
3375 apply (simp add: refl_def listrel_subset Ball_def)
3377 apply (induct_tac x)
3378 apply (auto intro: listrel.intros)
3381 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"
3382 apply (auto simp add: sym_def)
3383 apply (erule listrel.induct)
3384 apply (blast intro: listrel.intros)+
3387 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"
3388 apply (simp add: trans_def)
3391 apply (erule listrel.induct)
3392 apply (blast intro: listrel.intros)+
3395 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
3396 by (simp add: equiv_def listrel_refl listrel_sym listrel_trans)
3398 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
3399 by (blast intro: listrel.intros)
3402 "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
3403 by (auto simp add: set_Cons_def intro: listrel.intros)
3406 subsection{*Miscellany*}
3408 subsubsection {* Characters and strings *}
3411 Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
3412 | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
3415 "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
3416 Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
3417 proof (rule UNIV_eq_I)
3418 fix x show "x \<in> ?A" by (cases x) simp_all
3421 instance nibble :: finite
3422 by default (simp add: UNIV_nibble)
3424 datatype char = Char nibble nibble
3425 -- "Note: canonical order of character encoding coincides with standard term ordering"
3428 "UNIV = image (split Char) (UNIV \<times> UNIV)"
3429 proof (rule UNIV_eq_I)
3430 fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
3433 instance char :: finite
3434 by default (simp add: UNIV_char)
3436 lemma size_char [code, simp]:
3437 "size (c::char) = 0" by (cases c) simp
3439 lemma char_size [code, simp]:
3440 "char_size (c::char) = 0" by (cases c) simp
3442 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
3443 "nibble_pair_of_char (Char n m) = (n, m)"
3445 declare nibble_pair_of_char.simps [code del]
3449 val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
3450 val thms = map_product
3451 (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
3454 PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
3455 #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
3459 lemma char_case_nibble_pair [code, code inline]:
3460 "char_case f = split f o nibble_pair_of_char"
3461 by (simp add: expand_fun_eq split: char.split)
3463 lemma char_rec_nibble_pair [code, code inline]:
3464 "char_rec f = split f o nibble_pair_of_char"
3465 unfolding char_case_nibble_pair [symmetric]
3466 by (simp add: expand_fun_eq split: char.split)
3468 types string = "char list"
3471 "_Char" :: "xstr => char" ("CHR _")
3472 "_String" :: "xstr => string" ("_")
3474 setup StringSyntax.setup
3477 subsection {* Size function *}
3479 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
3480 by (rule is_measure_trivial)
3482 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
3483 by (rule is_measure_trivial)
3485 lemma list_size_estimation[termination_simp]:
3486 "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
3489 lemma list_size_estimation'[termination_simp]:
3490 "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
3493 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
3496 lemma list_size_pointwise[termination_simp]:
3497 "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
3498 by (induct xs) force+
3500 subsection {* Code generator *}
3502 subsubsection {* Setup *}
3507 fun term_of_list f T = HOLogic.mk_list T o map f;
3510 fun gen_list' aG aT i j = frequency
3514 val (xs, ts) = gen_list' aG aT (i-1) j
3515 in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
3516 (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
3517 and gen_list aG aT i = gen_list' aG aT i i;
3521 val term_of_char = HOLogic.mk_char o ord;
3525 let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
3526 in (chr j, fn () => HOLogic.mk_char j) end;
3529 consts_code "Cons" ("(_ ::/ _)")
3550 open Basic_Code_Thingol;
3552 fun implode_list (nil', cons') t =
3554 fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
3558 | dest_cons _ = NONE;
3559 val (ts, t') = Code_Thingol.unfoldr dest_cons t;
3561 of IConst (c, _) => if c = nil' then SOME ts else NONE
3565 fun decode_char nibbles' (IConst (c1, _), IConst (c2, _)) =
3567 fun idx c = find_index (curry (op =) c) nibbles';
3568 fun decode ~1 _ = NONE
3569 | decode _ ~1 = NONE
3570 | decode n m = SOME (chr (n * 16 + m));
3571 in decode (idx c1) (idx c2) end
3572 | decode_char _ _ = NONE;
3574 fun implode_string (char', nibbles') mk_char mk_string ts =
3576 fun implode_char (IConst (c, _) `$ t1 `$ t2) =
3577 if c = char' then decode_char nibbles' (t1, t2) else NONE
3578 | implode_char _ = NONE;
3579 val ts' = map implode_char ts;
3580 in if forall is_some ts'
3581 then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
3585 fun list_names naming = pairself (the o Code_Thingol.lookup_const naming)
3586 (@{const_name Nil}, @{const_name Cons});
3587 fun char_name naming = (the o Code_Thingol.lookup_const naming)
3589 fun nibble_names naming = map (the o Code_Thingol.lookup_const naming)
3590 [@{const_name Nibble0}, @{const_name Nibble1},
3591 @{const_name Nibble2}, @{const_name Nibble3},
3592 @{const_name Nibble4}, @{const_name Nibble5},
3593 @{const_name Nibble6}, @{const_name Nibble7},
3594 @{const_name Nibble8}, @{const_name Nibble9},
3595 @{const_name NibbleA}, @{const_name NibbleB},
3596 @{const_name NibbleC}, @{const_name NibbleD},
3597 @{const_name NibbleE}, @{const_name NibbleF}];
3599 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
3600 Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
3601 pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
3602 Code_Printer.str target_cons,
3603 pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
3606 fun pretty_list literals =
3608 val mk_list = Code_Printer.literal_list literals;
3609 fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
3610 case Option.map (cons t1) (implode_list (list_names naming) t2)
3611 of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
3612 | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
3615 fun pretty_list_string literals =
3617 val mk_list = Code_Printer.literal_list literals;
3618 val mk_char = Code_Printer.literal_char literals;
3619 val mk_string = Code_Printer.literal_string literals;
3620 fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
3621 case Option.map (cons t1) (implode_list (list_names naming) t2)
3622 of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
3624 | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
3625 | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
3628 fun pretty_char literals =
3630 val mk_char = Code_Printer.literal_char literals;
3631 fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
3632 case decode_char (nibble_names naming) (t1, t2)
3633 of SOME c => (Code_Printer.str o mk_char) c
3634 | NONE => Code_Printer.nerror thm "Illegal character expression";
3637 fun pretty_message literals =
3639 val mk_char = Code_Printer.literal_char literals;
3640 val mk_string = Code_Printer.literal_string literals;
3641 fun pretty _ naming thm _ _ [(t, _)] =
3642 case implode_list (list_names naming) t
3643 of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
3645 | NONE => Code_Printer.nerror thm "Illegal message expression")
3646 | NONE => Code_Printer.nerror thm "Illegal message expression";
3651 fun add_literal_list target thy =
3653 val pr = pretty_list (Code_Target.the_literals thy target);
3656 |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
3659 fun add_literal_list_string target thy =
3661 val pr = pretty_list_string (Code_Target.the_literals thy target);
3664 |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
3667 fun add_literal_char target thy =
3669 val pr = pretty_char (Code_Target.the_literals thy target);
3672 |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
3675 fun add_literal_message str target thy =
3677 val pr = pretty_message (Code_Target.the_literals thy target);
3680 |> Code_Target.add_syntax_const target str (SOME pr)
3687 fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
3690 code_instance list :: eq
3693 code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
3694 (Haskell infixl 4 "==")
3699 fun list_codegen thy defs dep thyname b t gr =
3701 val ts = HOLogic.dest_list t;
3702 val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
3704 val (ps, gr'') = fold_map
3705 (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
3706 in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
3708 fun char_codegen thy defs dep thyname b t gr =
3710 val i = HOLogic.dest_char t;
3711 val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
3713 in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
3714 end handle TERM _ => NONE;
3717 Codegen.add_codegen "list_codegen" list_codegen
3718 #> Codegen.add_codegen "char_codegen" char_codegen
3723 subsubsection {* Generation of efficient code *}
3726 member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
3728 "x mem [] \<longleftrightarrow> False"
3729 | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
3732 null:: "'a list \<Rightarrow> bool"
3735 | "null (x#xs) = False"
3738 list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
3740 "list_inter [] bs = []"
3741 | "list_inter (a#as) bs =
3742 (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
3745 list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
3747 "list_all P [] = True"
3748 | "list_all P (x#xs) = (P x \<and> list_all P xs)"
3751 list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
3753 "list_ex P [] = False"
3754 | "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
3757 filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
3759 "filtermap f [] = []"
3760 | "filtermap f (x#xs) =
3761 (case f x of None \<Rightarrow> filtermap f xs
3762 | Some y \<Rightarrow> y # filtermap f xs)"
3765 map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
3767 "map_filter f P [] = []"
3768 | "map_filter f P (x#xs) =
3769 (if P x then f x # map_filter f P xs else map_filter f P xs)"
3772 length_unique :: "'a list \<Rightarrow> nat"
3774 "length_unique [] = 0"
3775 | "length_unique (x#xs) =
3776 (if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
3779 Only use @{text mem} for generating executable code. Otherwise use
3780 @{prop "x : set xs"} instead --- it is much easier to reason about.
3781 The same is true for @{const list_all} and @{const list_ex}: write
3782 @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
3783 quantifiers are aleady known to the automatic provers. In fact, the
3784 declarations in the code subsection make sure that @{text "\<in>"},
3785 @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} are implemented
3788 Efficient emptyness check is implemented by @{const null}.
3790 The functions @{const filtermap} and @{const map_filter} are just
3791 there to generate efficient code. Do not use
3792 them for modelling and proving.
3795 lemma rev_foldl_cons [code]:
3796 "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
3798 case Nil then show ?case by simp
3803 have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
3804 = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
3805 by (induct xs arbitrary: ys) auto
3808 show ?case by (induct xs) (auto simp add: Cons aux)
3811 lemma mem_iff [code post]:
3812 "x mem xs \<longleftrightarrow> x \<in> set xs"
3815 lemmas in_set_code [code unfold] = mem_iff [symmetric]
3817 lemma empty_null [code inline]:
3818 "xs = [] \<longleftrightarrow> null xs"
3819 by (cases xs) simp_all
3821 lemmas null_empty [code post] =
3822 empty_null [symmetric]
3824 lemma list_inter_conv:
3825 "set (list_inter xs ys) = set xs \<inter> set ys"
3828 lemma list_all_iff [code post]:
3829 "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
3832 lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
3834 lemma list_all_append [simp]:
3835 "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
3838 lemma list_all_rev [simp]:
3839 "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
3840 by (simp add: list_all_iff)
3842 lemma list_all_length:
3843 "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
3844 unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
3846 lemma list_ex_iff [code post]:
3847 "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
3848 by (induct xs) simp_all
3850 lemmas list_bex_code [code unfold] =
3851 list_ex_iff [symmetric]
3853 lemma list_ex_length:
3854 "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
3855 unfolding list_ex_iff set_conv_nth by auto
3857 lemma filtermap_conv:
3858 "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
3859 by (induct xs) (simp_all split: option.split)
3861 lemma map_filter_conv [simp]:
3862 "map_filter f P xs = map f (filter P xs)"
3865 lemma length_remdups_length_unique [code inline]:
3866 "length (remdups xs) = length_unique xs"
3867 by (induct xs) simp_all
3869 hide (open) const length_unique
3872 text {* Code for bounded quantification and summation over nats. *}
3874 lemma atMost_upto [code unfold]:
3875 "{..n} = set [0..<Suc n]"
3878 lemma atLeast_upt [code unfold]:
3879 "{..<n} = set [0..<n]"
3882 lemma greaterThanLessThan_upt [code unfold]:
3883 "{n<..<m} = set [Suc n..<m]"
3886 lemma atLeastLessThan_upt [code unfold]:
3887 "{n..<m} = set [n..<m]"
3890 lemma greaterThanAtMost_upt [code unfold]:
3891 "{n<..m} = set [Suc n..<Suc m]"
3894 lemma atLeastAtMost_upt [code unfold]:
3895 "{n..m} = set [n..<Suc m]"
3898 lemma all_nat_less_eq [code unfold]:
3899 "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
3902 lemma ex_nat_less_eq [code unfold]:
3903 "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
3906 lemma all_nat_less [code unfold]:
3907 "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
3910 lemma ex_nat_less [code unfold]:
3911 "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
3914 lemma setsum_set_distinct_conv_listsum:
3915 "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
3916 by (induct xs) simp_all
3918 lemma setsum_set_upt_conv_listsum [code unfold]:
3919 "setsum f (set [m..<n]) = listsum (map f [m..<n])"
3920 by (rule setsum_set_distinct_conv_listsum) simp
3923 text {* Code for summation over ints. *}
3925 lemma greaterThanLessThan_upto [code unfold]:
3926 "{i<..<j::int} = set [i+1..j - 1]"
3929 lemma atLeastLessThan_upto [code unfold]:
3930 "{i..<j::int} = set [i..j - 1]"
3933 lemma greaterThanAtMost_upto [code unfold]:
3934 "{i<..j::int} = set [i+1..j]"
3937 lemma atLeastAtMost_upto [code unfold]:
3938 "{i..j::int} = set [i..j]"
3941 lemma setsum_set_upto_conv_listsum [code unfold]:
3942 "setsum f (set [i..j::int]) = listsum (map f [i..j])"
3943 by (rule setsum_set_distinct_conv_listsum) simp