New interface for test data generators.
6 header {* The datatype of finite lists *}
10 uses "Tools/string_syntax.ML"
15 | Cons 'a "'a list" (infixr "#" 65)
17 subsection{*Basic list processing functions*}
20 filter:: "('a => bool) => 'a list => 'a list"
21 concat:: "'a list list => 'a list"
22 foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
23 foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
25 tl:: "'a list => 'a list"
26 last:: "'a list => 'a"
27 butlast :: "'a list => 'a list"
28 set :: "'a list => 'a set"
29 map :: "('a=>'b) => ('a list => 'b list)"
30 listsum :: "'a list => 'a::monoid_add"
31 nth :: "'a list => nat => 'a" (infixl "!" 100)
32 list_update :: "'a list => nat => 'a => 'a list"
33 take:: "nat => 'a list => 'a list"
34 drop:: "nat => 'a list => 'a list"
35 takeWhile :: "('a => bool) => 'a list => 'a list"
36 dropWhile :: "('a => bool) => 'a list => 'a list"
37 rev :: "'a list => 'a list"
38 zip :: "'a list => 'b list => ('a * 'b) list"
39 upt :: "nat => nat => nat list" ("(1[_..</_'])")
40 remdups :: "'a list => 'a list"
41 remove1 :: "'a => 'a list => 'a list"
42 "distinct":: "'a list => bool"
43 replicate :: "nat => 'a => 'a list"
44 splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
47 nonterminals lupdbinds lupdbind
50 -- {* list Enumeration *}
51 "@list" :: "args => 'a list" ("[(_)]")
53 -- {* Special syntax for filter *}
54 "@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
57 "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")
58 "" :: "lupdbind => lupdbinds" ("_")
59 "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")
60 "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900)
65 "[x<-xs . P]"== "filter (%x. P) xs"
67 "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
68 "xs[i:=x]" == "list_update xs i x"
72 "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
74 "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
78 Function @{text size} is overloaded for all datatypes. Users may
79 refer to the list version as @{text length}. *}
82 length :: "'a list => nat" where
93 "last(x#xs) = (if xs=[] then x else last xs)"
97 "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
101 "set (x#xs) = insert x (set xs)"
105 "map f (x#xs) = f(x)#map f xs"
108 append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
110 append_Nil:"[] @ ys = ys"
111 | append_Cons: "(x#xs) @ ys = x # xs @ ys"
115 "rev(x#xs) = rev(xs) @ [x]"
119 "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
122 foldl_Nil:"foldl f a [] = a"
123 foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
127 "foldr f (x#xs) a = f x (foldr f xs a)"
131 "concat(x#xs) = x @ concat(xs)"
135 "listsum (x # xs) = x + listsum xs"
138 drop_Nil:"drop n [] = []"
139 drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
140 -- {*Warning: simpset does not contain this definition, but separate
141 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
144 take_Nil:"take n [] = []"
145 take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
146 -- {*Warning: simpset does not contain this definition, but separate
147 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
150 nth_Cons:"(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
151 -- {*Warning: simpset does not contain this definition, but separate
152 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
156 "(x#xs)[i:=v] = (case i of 0 => v # xs | Suc j => x # xs[j:=v])"
159 "takeWhile P [] = []"
160 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
163 "dropWhile P [] = []"
164 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
168 zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
169 -- {*Warning: simpset does not contain this definition, but separate
170 theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
173 upt_0: "[i..<0] = []"
174 upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
178 "distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
182 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
186 "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
189 replicate_0: "replicate 0 x = []"
190 replicate_Suc: "replicate (Suc n) x = x # replicate n x"
193 rotate1 :: "'a list \<Rightarrow> 'a list" where
194 "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
197 rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
198 "rotate n = rotate1 ^ n"
201 list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
203 (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
206 sublist :: "'a list => nat set => 'a list" where
207 "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
211 "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
212 -- {*Warning: simpset does not contain the second eqn but a derived one. *}
214 text{* The following simple sort functions are intended for proofs,
215 not for efficient implementations. *}
220 fun sorted :: "'a list \<Rightarrow> bool" where
221 "sorted [] \<longleftrightarrow> True" |
222 "sorted [x] \<longleftrightarrow> True" |
223 "sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
225 primrec insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
226 "insort x [] = [x]" |
227 "insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
229 primrec sort :: "'a list \<Rightarrow> 'a list" where
231 "sort (x#xs) = insort x (sort xs)"
236 subsubsection {* List comprehension *}
238 text{* Input syntax for Haskell-like list comprehension notation.
239 Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
240 the list of all pairs of distinct elements from @{text xs} and @{text ys}.
241 The syntax is as in Haskell, except that @{text"|"} becomes a dot
242 (like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
243 \verb![e| x <- xs, ...]!.
245 The qualifiers after the dot are
247 \item[generators] @{text"p \<leftarrow> xs"},
248 where @{text p} is a pattern and @{text xs} an expression of list type, or
249 \item[guards] @{text"b"}, where @{text b} is a boolean expression.
250 %\item[local bindings] @ {text"let x = e"}.
253 Just like in Haskell, list comprehension is just a shorthand. To avoid
254 misunderstandings, the translation into desugared form is not reversed
255 upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is
256 optmized to @{term"map (%x. e) xs"}.
258 It is easy to write short list comprehensions which stand for complex
259 expressions. During proofs, they may become unreadable (and
260 mangled). In such cases it can be advisable to introduce separate
261 definitions for the list comprehensions in question. *}
264 Proper theorem proving support would be nice. For example, if
265 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
266 produced something like
267 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
270 nonterminals lc_qual lc_quals
273 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __")
274 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
275 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
276 (*"_lc_let" :: "letbinds => lc_qual" ("let _")*)
277 "_lc_end" :: "lc_quals" ("]")
278 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
279 "_lc_abs" :: "'a => 'b list => 'b list"
281 (* These are easier than ML code but cannot express the optimized
282 translation of [e. p<-xs]
284 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
285 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
286 => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
287 "[e. P]" => "if P then [e] else []"
288 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
289 => "if P then (_listcompr e Q Qs) else []"
290 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
291 => "_Let b (_listcompr e Q Qs)"
295 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
297 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
299 parse_translation (advanced) {*
301 val NilC = Syntax.const @{const_name Nil};
302 val ConsC = Syntax.const @{const_name Cons};
303 val mapC = Syntax.const @{const_name map};
304 val concatC = Syntax.const @{const_name concat};
305 val IfC = Syntax.const @{const_name If};
306 fun singl x = ConsC $ x $ NilC;
308 fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
310 val x = Free (Name.variant (add_term_free_names (p$e, [])) "x", dummyT);
311 val e = if opti then singl e else e;
312 val case1 = Syntax.const "_case1" $ p $ e;
313 val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
315 val cs = Syntax.const "_case2" $ case1 $ case2
316 val ft = DatatypeCase.case_tr false DatatypePackage.datatype_of_constr
320 fun abs_tr ctxt (p as Free(s,T)) e opti =
321 let val thy = ProofContext.theory_of ctxt;
322 val s' = Sign.intern_const thy s
323 in if Sign.declared_const thy s'
324 then (pat_tr ctxt p e opti, false)
325 else (lambda p e, true)
327 | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
329 fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] =
330 let val res = case qs of Const("_lc_end",_) => singl e
331 | Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs];
332 in IfC $ b $ res $ NilC end
333 | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] =
334 (case abs_tr ctxt p e true of
335 (f,true) => mapC $ f $ es
336 | (f, false) => concatC $ (mapC $ f $ es))
337 | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] =
338 let val e' = lc_tr ctxt [e,q,qs];
339 in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end
341 in [("_listcompr", lc_tr)] end
346 term "[(x,y,z). x\<leftarrow>xs]"
347 term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
348 term "[(x,y,z). x<a, x>b]"
349 term "[(x,y,z). x\<leftarrow>xs, x>b]"
350 term "[(x,y,z). x<a, x\<leftarrow>xs]"
351 term "[(x,y). Cons True x \<leftarrow> xs]"
352 term "[(x,y,z). Cons x [] \<leftarrow> xs]"
353 term "[(x,y,z). x<a, x>b, x=d]"
354 term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
355 term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
356 term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
357 term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
358 term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
359 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
360 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
361 term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
364 subsubsection {* @{const Nil} and @{const Cons} *}
366 lemma not_Cons_self [simp]:
370 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]
372 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
376 "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
377 by (rule measure_induct [of length]) iprover
380 subsubsection {* @{const length} *}
383 Needs to come before @{text "@"} because of theorem @{text
384 append_eq_append_conv}.
387 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"
390 lemma length_map [simp]: "length (map f xs) = length xs"
393 lemma length_rev [simp]: "length (rev xs) = length xs"
396 lemma length_tl [simp]: "length (tl xs) = length xs - 1"
399 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
402 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])"
405 lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0"
408 lemma length_Suc_conv:
409 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
412 lemma Suc_length_conv:
413 "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
414 apply (induct xs, simp, simp)
418 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"
421 lemma list_induct2 [consumes 1]:
422 "\<lbrakk> length xs = length ys;
424 \<And>x xs y ys. \<lbrakk> length xs = length ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
425 \<Longrightarrow> P xs ys"
426 apply(induct xs arbitrary: ys)
435 \<And>x xs. P (x#xs) [];
436 \<And>y ys. P [] (y#ys);
437 \<And>x xs y ys. P xs ys \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
438 \<Longrightarrow> P xs ys"
439 by (induct xs arbitrary: ys) (case_tac x, auto)+
441 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
442 by (rule Eq_FalseI) auto
444 simproc_setup list_neq ("(xs::'a list) = ys") = {*
446 Reduces xs=ys to False if xs and ys cannot be of the same length.
447 This is the case if the atomic sublists of one are a submultiset
448 of those of the other list and there are fewer Cons's in one than the other.
453 fun len (Const("List.list.Nil",_)) acc = acc
454 | len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
455 | len (Const("List.append",_) $ xs $ ys) acc = len xs (len ys acc)
456 | len (Const("List.rev",_) $ xs) acc = len xs acc
457 | len (Const("List.map",_) $ _ $ xs) acc = len xs acc
458 | len t (ts,n) = (t::ts,n);
460 fun list_neq _ ss ct =
462 val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
463 val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
466 val Type(_,listT::_) = eqT;
467 val size = HOLogic.size_const listT;
468 val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
469 val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
470 val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
471 (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));
472 in SOME (thm RS @{thm neq_if_length_neq}) end
474 if m < n andalso submultiset (op aconv) (ls,rs) orelse
475 n < m andalso submultiset (op aconv) (rs,ls)
476 then prove_neq() else NONE
482 subsubsection {* @{text "@"} -- append *}
484 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
487 lemma append_Nil2 [simp]: "xs @ [] = xs"
490 interpretation semigroup_append: semigroup_add ["op @"]
491 by unfold_locales simp
492 interpretation monoid_append: monoid_add ["[]" "op @"]
493 by unfold_locales (simp+)
495 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
498 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])"
501 lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"
504 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
507 lemma append_eq_append_conv [simp, noatp]:
508 "length xs = length ys \<or> length us = length vs
509 ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
510 apply (induct xs arbitrary: ys)
511 apply (case_tac ys, simp, force)
512 apply (case_tac ys, force, simp)
515 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
516 (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
517 apply (induct xs arbitrary: ys zs ts)
524 lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"
527 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"
530 lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)"
533 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"
534 using append_same_eq [of _ _ "[]"] by auto
536 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
537 using append_same_eq [of "[]"] by auto
539 lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
542 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
545 lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"
546 by (simp add: hd_append split: list.split)
548 lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"
549 by (simp split: list.split)
551 lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"
552 by (simp add: tl_append split: list.split)
555 lemma Cons_eq_append_conv: "x#xs = ys@zs =
556 (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"
559 lemma append_eq_Cons_conv: "(ys@zs = x#xs) =
560 (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
564 text {* Trivial rules for solving @{text "@"}-equations automatically. *}
566 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
569 lemma Cons_eq_appendI:
570 "[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"
573 lemma append_eq_appendI:
574 "[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"
579 Simplification procedure for all list equalities.
580 Currently only tries to rearrange @{text "@"} to see if
581 - both lists end in a singleton list,
582 - or both lists end in the same list.
588 fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
589 (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
590 | last (Const("List.append",_) $ _ $ ys) = last ys
593 fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
596 fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
597 (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
598 | butlast ((app as Const("List.append",_) $ xs) $ ys) = app $ butlast ys
599 | butlast xs = Const("List.list.Nil",fastype_of xs);
601 val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
602 @{thm append_Nil}, @{thm append_Cons}];
604 fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
606 val lastl = last lhs and lastr = last rhs;
609 val lhs1 = butlast lhs and rhs1 = butlast rhs;
610 val Type(_,listT::_) = eqT
611 val appT = [listT,listT] ---> listT
612 val app = Const("List.append",appT)
613 val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
614 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
615 val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
616 (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
617 in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
620 if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
621 else if lastl aconv lastr then rearr @{thm append_same_eq}
627 val list_eq_simproc =
628 Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
632 Addsimprocs [list_eq_simproc];
636 subsubsection {* @{text map} *}
638 lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
639 by (induct xs) simp_all
641 lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)"
642 by (rule ext, induct_tac xs) auto
644 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"
647 lemma map_compose: "map (f o g) xs = map f (map g xs)"
648 by (induct xs) (auto simp add: o_def)
650 lemma rev_map: "rev (map f xs) = map f (rev xs)"
653 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
656 lemma map_cong [fundef_cong, recdef_cong]:
657 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
658 -- {* a congruence rule for @{text map} *}
661 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
664 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
667 lemma map_eq_Cons_conv:
668 "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
671 lemma Cons_eq_map_conv:
672 "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
675 lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]
676 lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]
677 declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!]
680 "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
681 by(induct ys, auto simp add: Cons_eq_map_conv)
683 lemma map_eq_imp_length_eq:
684 "map f xs = map f ys ==> length xs = length ys"
685 apply (induct ys arbitrary: xs)
687 apply (metis Suc_length_conv length_map)
691 "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
693 apply(frule map_eq_imp_length_eq)
695 apply(induct rule:list_induct2)
698 apply (blast intro:sym)
701 lemma inj_on_map_eq_map:
702 "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
703 by(blast dest:map_inj_on)
706 "map f xs = map f ys ==> inj f ==> xs = ys"
707 by (induct ys arbitrary: xs) (auto dest!:injD)
709 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
710 by(blast dest:map_injective)
712 lemma inj_mapI: "inj f ==> inj (map f)"
713 by (iprover dest: map_injective injD intro: inj_onI)
715 lemma inj_mapD: "inj (map f) ==> inj f"
716 apply (unfold inj_on_def, clarify)
717 apply (erule_tac x = "[x]" in ballE)
718 apply (erule_tac x = "[y]" in ballE, simp, blast)
722 lemma inj_map[iff]: "inj (map f) = inj f"
723 by (blast dest: inj_mapD intro: inj_mapI)
725 lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
727 apply(erule map_inj_on)
728 apply(blast intro:inj_onI dest:inj_onD)
731 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
734 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
737 lemma map_fst_zip[simp]:
738 "length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs"
739 by (induct rule:list_induct2, simp_all)
741 lemma map_snd_zip[simp]:
742 "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
743 by (induct rule:list_induct2, simp_all)
746 subsubsection {* @{text rev} *}
748 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
751 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
754 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
757 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
760 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
763 lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
766 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
769 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
770 apply (induct xs arbitrary: ys, force)
771 apply (case_tac ys, simp, force)
774 lemma inj_on_rev[iff]: "inj_on rev A"
775 by(simp add:inj_on_def)
777 lemma rev_induct [case_names Nil snoc]:
778 "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
779 apply(simplesubst rev_rev_ident[symmetric])
780 apply(rule_tac list = "rev xs" in list.induct, simp_all)
783 lemma rev_exhaust [case_names Nil snoc]:
784 "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"
785 by (induct xs rule: rev_induct) auto
787 lemmas rev_cases = rev_exhaust
789 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
790 by(rule rev_cases[of xs]) auto
793 subsubsection {* @{text set} *}
795 lemma finite_set [iff]: "finite (set xs)"
798 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)"
801 lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs"
804 lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
807 lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs"
810 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
813 lemma set_empty2[iff]: "({} = set xs) = (xs = [])"
816 lemma set_rev [simp]: "set (rev xs) = set xs"
819 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
822 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
825 lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}"
826 apply (induct j, simp_all)
827 apply (erule ssubst, auto)
830 lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)"
832 case Nil show ?case by simp
837 assume "x \<in> set (a # xs)"
838 with Cons show "\<exists>ys zs. a # xs = ys @ x # zs"
839 by (auto intro: Cons_eq_appendI)
841 assume "\<exists>ys zs. a # xs = ys @ x # zs"
842 then obtain ys zs where eq: "a # xs = ys @ x # zs" by blast
843 show "x \<in> set (a # xs)"
844 by (cases ys) (auto simp add: eq)
848 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
849 by (rule in_set_conv_decomp [THEN iffD1])
851 lemma in_set_conv_decomp_first:
852 "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
854 case Nil show ?case by simp
859 assume "x = a" thus ?case using Cons by fastsimp
861 assume "x \<noteq> a"
864 assume "x \<in> set (a # xs)"
865 with Cons and `x \<noteq> a` show "\<exists>ys zs. a # xs = ys @ x # zs \<and> x \<notin> set ys"
866 by (fastsimp intro!: Cons_eq_appendI)
868 assume "\<exists>ys zs. a # xs = ys @ x # zs \<and> x \<notin> set ys"
869 then obtain ys zs where eq: "a # xs = ys @ x # zs" by blast
870 show "x \<in> set (a # xs)" by (cases ys) (auto simp add: eq)
875 lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
876 by (rule in_set_conv_decomp_first [THEN iffD1])
879 lemma finite_list: "finite A ==> EX l. set l = A"
880 apply (erule finite_induct, auto)
881 apply (rule_tac x="x#l" in exI, auto)
884 lemma card_length: "card (set xs) \<le> length xs"
885 by (induct xs) (auto simp add: card_insert_if)
888 subsubsection {* @{text filter} *}
890 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
893 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"
894 by (induct xs) simp_all
896 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
899 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
900 by (induct xs) (auto simp add: le_SucI)
902 lemma sum_length_filter_compl:
903 "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
904 by(induct xs) simp_all
906 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
909 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
912 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
913 by (induct xs) simp_all
915 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
918 apply(cut_tac P=P and xs=xs in length_filter_le)
923 "filter P (map f xs) = map f (filter (P o f) xs)"
924 by (induct xs) simp_all
926 lemma length_filter_map[simp]:
927 "length (filter P (map f xs)) = length(filter (P o f) xs)"
928 by (simp add:filter_map)
930 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
933 lemma length_filter_less:
934 "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
936 case Nil thus ?case by simp
938 case (Cons x xs) thus ?case
939 apply (auto split:split_if_asm)
940 using length_filter_le[of P xs] apply arith
944 lemma length_filter_conv_card:
945 "length(filter p xs) = card{i. i < length xs & p(xs!i)}"
947 case Nil thus ?case by simp
950 let ?S = "{i. i < length xs & p(xs!i)}"
951 have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)
952 show ?case (is "?l = card ?S'")
955 hence eq: "?S' = insert 0 (Suc ` ?S)"
956 by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
957 have "length (filter p (x # xs)) = Suc(card ?S)"
958 using Cons `p x` by simp
959 also have "\<dots> = Suc(card(Suc ` ?S))" using fin
960 by (simp add: card_image inj_Suc)
961 also have "\<dots> = card ?S'" using eq fin
962 by (simp add:card_insert_if) (simp add:image_def)
963 finally show ?thesis .
966 hence eq: "?S' = Suc ` ?S"
967 by(auto simp add: image_def split:nat.split elim:lessE)
968 have "length (filter p (x # xs)) = card ?S"
969 using Cons `\<not> p x` by simp
970 also have "\<dots> = card(Suc ` ?S)" using fin
971 by (simp add: card_image inj_Suc)
972 also have "\<dots> = card ?S'" using eq fin
973 by (simp add:card_insert_if)
974 finally show ?thesis .
978 lemma Cons_eq_filterD:
979 "x#xs = filter P ys \<Longrightarrow>
980 \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
981 (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
983 case Nil thus ?case by simp
986 show ?case (is "\<exists>x. ?Q x")
992 with Py Cons.prems have "?Q []" by simp
995 assume "x \<noteq> y"
996 with Py Cons.prems show ?thesis by simp
1000 with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
1001 then have "?Q (y#us)" by simp
1002 then show ?thesis ..
1006 lemma filter_eq_ConsD:
1007 "filter P ys = x#xs \<Longrightarrow>
1008 \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
1009 by(rule Cons_eq_filterD) simp
1011 lemma filter_eq_Cons_iff:
1012 "(filter P ys = x#xs) =
1013 (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
1014 by(auto dest:filter_eq_ConsD)
1016 lemma Cons_eq_filter_iff:
1017 "(x#xs = filter P ys) =
1018 (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
1019 by(auto dest:Cons_eq_filterD)
1021 lemma filter_cong[fundef_cong, recdef_cong]:
1022 "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
1024 apply(erule thin_rl)
1025 by (induct ys) simp_all
1028 subsubsection {* @{text concat} *}
1030 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
1033 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
1034 by (induct xss) auto
1036 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
1037 by (induct xss) auto
1039 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
1042 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
1045 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
1048 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
1051 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
1055 subsubsection {* @{text nth} *}
1057 lemma nth_Cons_0 [simp]: "(x # xs)!0 = x"
1060 lemma nth_Cons_Suc [simp]: "(x # xs)!(Suc n) = xs!n"
1063 declare nth.simps [simp del]
1066 "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
1067 apply (induct xs arbitrary: n, simp)
1068 apply (case_tac n, auto)
1071 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
1074 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
1077 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
1078 apply (induct xs arbitrary: n, simp)
1079 apply (case_tac n, auto)
1082 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
1083 by(cases xs) simp_all
1086 lemma list_eq_iff_nth_eq:
1087 "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
1088 apply(induct xs arbitrary: ys)
1092 apply(simp add:nth_Cons split:nat.split)apply blast
1095 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
1096 apply (induct xs, simp, simp)
1098 apply (metis nat_case_0 nth.simps zero_less_Suc)
1099 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
1100 apply (case_tac i, simp)
1101 apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
1104 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
1105 by(auto simp:set_conv_nth)
1107 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
1108 by (auto simp add: set_conv_nth)
1110 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"
1111 by (auto simp add: set_conv_nth)
1113 lemma all_nth_imp_all_set:
1114 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"
1115 by (auto simp add: set_conv_nth)
1117 lemma all_set_conv_all_nth:
1118 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"
1119 by (auto simp add: set_conv_nth)
1122 "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
1123 proof (induct xs arbitrary: n)
1124 case Nil thus ?case by simp
1127 hence n: "n < Suc (length xs)" by simp
1129 { assume "n < length xs"
1130 with n obtain n' where "length xs - n = Suc n'"
1131 by (cases "length xs - n", auto)
1133 then have "length xs - Suc n = n'" by simp
1135 have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
1138 show ?case by (clarsimp simp add: Cons nth_append)
1141 subsubsection {* @{text list_update} *}
1143 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
1144 by (induct xs arbitrary: i) (auto split: nat.split)
1146 lemma nth_list_update:
1147 "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
1148 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
1150 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
1151 by (simp add: nth_list_update)
1153 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
1154 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
1156 lemma list_update_overwrite [simp]:
1157 "i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
1158 by (induct xs arbitrary: i) (auto split: nat.split)
1160 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
1161 by (induct xs arbitrary: i) (simp_all split:nat.splits)
1163 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
1164 apply (induct xs arbitrary: i)
1170 lemma list_update_same_conv:
1171 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
1172 by (induct xs arbitrary: i) (auto split: nat.split)
1174 lemma list_update_append1:
1175 "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
1176 apply (induct xs arbitrary: i, simp)
1177 apply(simp split:nat.split)
1180 lemma list_update_append:
1181 "(xs @ ys) [n:= x] =
1182 (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
1183 by (induct xs arbitrary: n) (auto split:nat.splits)
1185 lemma list_update_length [simp]:
1186 "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
1187 by (induct xs, auto)
1190 "length xs = length ys ==>
1191 (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
1192 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
1194 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
1195 by (induct xs arbitrary: i) (auto split: nat.split)
1197 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
1198 by (blast dest!: set_update_subset_insert [THEN subsetD])
1200 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
1201 by (induct xs arbitrary: n) (auto split:nat.splits)
1203 lemma list_update_overwrite:
1204 "xs [i := x, i := y] = xs [i := y]"
1205 apply (induct xs arbitrary: i)
1211 lemma list_update_swap:
1212 "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
1213 apply (induct xs arbitrary: i i')
1215 apply (case_tac i, case_tac i')
1222 subsubsection {* @{text last} and @{text butlast} *}
1224 lemma last_snoc [simp]: "last (xs @ [x]) = x"
1227 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
1230 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
1231 by(simp add:last.simps)
1233 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
1234 by(simp add:last.simps)
1236 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
1237 by (induct xs) (auto)
1239 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
1240 by(simp add:last_append)
1242 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
1243 by(simp add:last_append)
1245 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
1246 by(rule rev_exhaust[of xs]) simp_all
1248 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
1249 by(cases xs) simp_all
1251 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
1254 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
1255 by (induct xs rule: rev_induct) auto
1257 lemma butlast_append:
1258 "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
1259 by (induct xs arbitrary: ys) auto
1261 lemma append_butlast_last_id [simp]:
1262 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
1265 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
1266 by (induct xs) (auto split: split_if_asm)
1268 lemma in_set_butlast_appendI:
1269 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
1270 by (auto dest: in_set_butlastD simp add: butlast_append)
1272 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
1273 apply (induct xs arbitrary: n)
1275 apply (auto split:nat.split)
1278 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
1279 by(induct xs)(auto simp:neq_Nil_conv)
1282 subsubsection {* @{text take} and @{text drop} *}
1284 lemma take_0 [simp]: "take 0 xs = []"
1287 lemma drop_0 [simp]: "drop 0 xs = xs"
1290 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
1293 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
1296 declare take_Cons [simp del] and drop_Cons [simp del]
1298 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
1299 by(clarsimp simp add:neq_Nil_conv)
1301 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
1302 by(cases xs, simp_all)
1304 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
1305 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
1307 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
1308 apply (induct xs arbitrary: n, simp)
1309 apply(simp add:drop_Cons nth_Cons split:nat.splits)
1312 lemma take_Suc_conv_app_nth:
1313 "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
1314 apply (induct xs arbitrary: i, simp)
1315 apply (case_tac i, auto)
1318 lemma drop_Suc_conv_tl:
1319 "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
1320 apply (induct xs arbitrary: i, simp)
1321 apply (case_tac i, auto)
1324 lemma length_take [simp]: "length (take n xs) = min (length xs) n"
1325 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1327 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
1328 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1330 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
1331 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1333 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
1334 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1336 lemma take_append [simp]:
1337 "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
1338 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1340 lemma drop_append [simp]:
1341 "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
1342 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1344 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
1345 apply (induct m arbitrary: xs n, auto)
1346 apply (case_tac xs, auto)
1347 apply (case_tac n, auto)
1350 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
1351 apply (induct m arbitrary: xs, auto)
1352 apply (case_tac xs, auto)
1355 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
1356 apply (induct m arbitrary: xs n, auto)
1357 apply (case_tac xs, auto)
1360 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
1361 apply(induct xs arbitrary: m n)
1363 apply(simp add: take_Cons drop_Cons split:nat.split)
1366 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
1367 apply (induct n arbitrary: xs, auto)
1368 apply (case_tac xs, auto)
1371 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
1372 apply(induct xs arbitrary: n)
1374 apply(simp add:take_Cons split:nat.split)
1377 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
1378 apply(induct xs arbitrary: n)
1380 apply(simp add:drop_Cons split:nat.split)
1383 lemma take_map: "take n (map f xs) = map f (take n xs)"
1384 apply (induct n arbitrary: xs, auto)
1385 apply (case_tac xs, auto)
1388 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
1389 apply (induct n arbitrary: xs, auto)
1390 apply (case_tac xs, auto)
1393 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
1394 apply (induct xs arbitrary: i, auto)
1395 apply (case_tac i, auto)
1398 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
1399 apply (induct xs arbitrary: i, auto)
1400 apply (case_tac i, auto)
1403 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
1404 apply (induct xs arbitrary: i n, auto)
1405 apply (case_tac n, blast)
1406 apply (case_tac i, auto)
1409 lemma nth_drop [simp]:
1410 "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
1411 apply (induct n arbitrary: xs i, auto)
1412 apply (case_tac xs, auto)
1415 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
1416 by(simp add: hd_conv_nth)
1418 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
1419 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
1421 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
1422 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
1424 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
1425 using set_take_subset by fast
1427 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
1428 using set_drop_subset by fast
1430 lemma append_eq_conv_conj:
1431 "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
1432 apply (induct xs arbitrary: zs, simp, clarsimp)
1433 apply (case_tac zs, auto)
1437 "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
1438 apply (induct xs arbitrary: i, auto)
1439 apply (case_tac i, simp_all)
1442 lemma append_eq_append_conv_if:
1443 "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
1444 (if size xs\<^isub>1 \<le> size ys\<^isub>1
1445 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
1446 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)"
1447 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
1449 apply(case_tac ys\<^isub>1)
1454 "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
1455 apply(induct xs arbitrary: n)
1457 apply(simp add:drop_Cons split:nat.split)
1460 lemma id_take_nth_drop:
1461 "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs"
1463 assume si: "i < length xs"
1464 hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
1466 from si have "take (Suc i) xs = take i xs @ [xs!i]"
1467 apply (rule_tac take_Suc_conv_app_nth) by arith
1468 ultimately show ?thesis by auto
1471 lemma upd_conv_take_nth_drop:
1472 "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
1474 assume i: "i < length xs"
1475 have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"
1476 by(rule arg_cong[OF id_take_nth_drop[OF i]])
1477 also have "\<dots> = take i xs @ a # drop (Suc i) xs"
1478 using i by (simp add: list_update_append)
1479 finally show ?thesis .
1483 "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
1484 apply (induct i arbitrary: xs)
1485 apply (simp add: neq_Nil_conv)
1493 subsubsection {* @{text takeWhile} and @{text dropWhile} *}
1495 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
1498 lemma takeWhile_append1 [simp]:
1499 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"
1502 lemma takeWhile_append2 [simp]:
1503 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
1506 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
1509 lemma dropWhile_append1 [simp]:
1510 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
1513 lemma dropWhile_append2 [simp]:
1514 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
1517 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
1518 by (induct xs) (auto split: split_if_asm)
1520 lemma takeWhile_eq_all_conv[simp]:
1521 "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
1524 lemma dropWhile_eq_Nil_conv[simp]:
1525 "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
1528 lemma dropWhile_eq_Cons_conv:
1529 "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
1532 text{* The following two lemmmas could be generalized to an arbitrary
1535 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1536 takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
1537 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
1539 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1540 dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
1544 apply(subst dropWhile_append2)
1548 lemma takeWhile_not_last:
1549 "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
1556 lemma takeWhile_cong [fundef_cong, recdef_cong]:
1557 "[| l = k; !!x. x : set l ==> P x = Q x |]
1558 ==> takeWhile P l = takeWhile Q k"
1559 by (induct k arbitrary: l) (simp_all)
1561 lemma dropWhile_cong [fundef_cong, recdef_cong]:
1562 "[| l = k; !!x. x : set l ==> P x = Q x |]
1563 ==> dropWhile P l = dropWhile Q k"
1564 by (induct k arbitrary: l, simp_all)
1567 subsubsection {* @{text zip} *}
1569 lemma zip_Nil [simp]: "zip [] ys = []"
1572 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
1575 declare zip_Cons [simp del]
1578 "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
1579 by(auto split:list.split)
1581 lemma length_zip [simp]:
1582 "length (zip xs ys) = min (length xs) (length ys)"
1583 by (induct xs ys rule:list_induct2') auto
1587 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
1588 by (induct xs zs rule:list_induct2') auto
1592 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
1593 by (induct xs ys rule:list_induct2') auto
1595 lemma zip_append [simp]:
1596 "[| length xs = length us; length ys = length vs |] ==>
1597 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
1598 by (simp add: zip_append1)
1601 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
1602 by (induct rule:list_induct2, simp_all)
1605 "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
1606 apply(induct xs arbitrary:ys) apply simp
1612 "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
1613 apply(induct xs arbitrary:ys) apply simp
1618 lemma nth_zip [simp]:
1619 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
1620 apply (induct ys arbitrary: i xs, simp)
1622 apply (simp_all add: nth.simps split: nat.split)
1626 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
1627 by (simp add: set_conv_nth cong: rev_conj_cong)
1630 "length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
1631 by (rule sym, simp add: update_zip)
1633 lemma zip_replicate [simp]:
1634 "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
1635 apply (induct i arbitrary: j, auto)
1636 apply (case_tac j, auto)
1640 "take n (zip xs ys) = zip (take n xs) (take n ys)"
1641 apply (induct n arbitrary: xs ys)
1643 apply (case_tac xs, simp)
1644 apply (case_tac ys, simp_all)
1648 "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
1649 apply (induct n arbitrary: xs ys)
1651 apply (case_tac xs, simp)
1652 apply (case_tac ys, simp_all)
1655 lemma set_zip_leftD:
1656 "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
1657 by (induct xs ys rule:list_induct2') auto
1659 lemma set_zip_rightD:
1660 "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
1661 by (induct xs ys rule:list_induct2') auto
1664 "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
1665 by(blast dest: set_zip_leftD set_zip_rightD)
1667 subsubsection {* @{text list_all2} *}
1669 lemma list_all2_lengthD [intro?]:
1670 "list_all2 P xs ys ==> length xs = length ys"
1671 by (simp add: list_all2_def)
1673 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
1674 by (simp add: list_all2_def)
1676 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
1677 by (simp add: list_all2_def)
1679 lemma list_all2_Cons [iff, code]:
1680 "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
1681 by (auto simp add: list_all2_def)
1683 lemma list_all2_Cons1:
1684 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
1687 lemma list_all2_Cons2:
1688 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
1691 lemma list_all2_rev [iff]:
1692 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
1693 by (simp add: list_all2_def zip_rev cong: conj_cong)
1695 lemma list_all2_rev1:
1696 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
1697 by (subst list_all2_rev [symmetric]) simp
1699 lemma list_all2_append1:
1700 "list_all2 P (xs @ ys) zs =
1701 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
1702 list_all2 P xs us \<and> list_all2 P ys vs)"
1703 apply (simp add: list_all2_def zip_append1)
1705 apply (rule_tac x = "take (length xs) zs" in exI)
1706 apply (rule_tac x = "drop (length xs) zs" in exI)
1707 apply (force split: nat_diff_split simp add: min_def, clarify)
1708 apply (simp add: ball_Un)
1711 lemma list_all2_append2:
1712 "list_all2 P xs (ys @ zs) =
1713 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
1714 list_all2 P us ys \<and> list_all2 P vs zs)"
1715 apply (simp add: list_all2_def zip_append2)
1717 apply (rule_tac x = "take (length ys) xs" in exI)
1718 apply (rule_tac x = "drop (length ys) xs" in exI)
1719 apply (force split: nat_diff_split simp add: min_def, clarify)
1720 apply (simp add: ball_Un)
1723 lemma list_all2_append:
1724 "length xs = length ys \<Longrightarrow>
1725 list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
1726 by (induct rule:list_induct2, simp_all)
1728 lemma list_all2_appendI [intro?, trans]:
1729 "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
1730 by (simp add: list_all2_append list_all2_lengthD)
1732 lemma list_all2_conv_all_nth:
1733 "list_all2 P xs ys =
1734 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
1735 by (force simp add: list_all2_def set_zip)
1737 lemma list_all2_trans:
1738 assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
1739 shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
1740 (is "!!bs cs. PROP ?Q as bs cs")
1742 fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
1743 show "!!cs. PROP ?Q (x # xs) bs cs"
1745 fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"
1746 show "PROP ?Q (x # xs) (y # ys) cs"
1747 by (induct cs) (auto intro: tr I1 I2)
1751 lemma list_all2_all_nthI [intro?]:
1752 "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
1753 by (simp add: list_all2_conv_all_nth)
1756 "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
1757 by (simp add: list_all2_def)
1759 lemma list_all2_nthD:
1760 "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
1761 by (simp add: list_all2_conv_all_nth)
1763 lemma list_all2_nthD2:
1764 "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
1765 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
1767 lemma list_all2_map1:
1768 "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
1769 by (simp add: list_all2_conv_all_nth)
1771 lemma list_all2_map2:
1772 "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
1773 by (auto simp add: list_all2_conv_all_nth)
1775 lemma list_all2_refl [intro?]:
1776 "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
1777 by (simp add: list_all2_conv_all_nth)
1779 lemma list_all2_update_cong:
1780 "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
1781 by (simp add: list_all2_conv_all_nth nth_list_update)
1783 lemma list_all2_update_cong2:
1784 "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
1785 by (simp add: list_all2_lengthD list_all2_update_cong)
1787 lemma list_all2_takeI [simp,intro?]:
1788 "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
1789 apply (induct xs arbitrary: n ys)
1791 apply (clarsimp simp add: list_all2_Cons1)
1796 lemma list_all2_dropI [simp,intro?]:
1797 "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
1798 apply (induct as arbitrary: n bs, simp)
1799 apply (clarsimp simp add: list_all2_Cons1)
1800 apply (case_tac n, simp, simp)
1803 lemma list_all2_mono [intro?]:
1804 "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
1805 apply (induct xs arbitrary: ys, simp)
1806 apply (case_tac ys, auto)
1810 "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
1811 by (induct xs ys rule: list_induct2') auto
1814 subsubsection {* @{text foldl} and @{text foldr} *}
1816 lemma foldl_append [simp]:
1817 "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
1818 by (induct xs arbitrary: a) auto
1820 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
1823 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
1824 by(induct xs) simp_all
1826 text{* For efficient code generation: avoid intermediate list. *}
1827 lemma foldl_map[code unfold]:
1828 "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
1829 by(induct xs arbitrary:a) simp_all
1831 lemma foldl_cong [fundef_cong, recdef_cong]:
1832 "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
1833 ==> foldl f a l = foldl g b k"
1834 by (induct k arbitrary: a b l) simp_all
1836 lemma foldr_cong [fundef_cong, recdef_cong]:
1837 "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]
1838 ==> foldr f l a = foldr g k b"
1839 by (induct k arbitrary: a b l) simp_all
1841 lemma (in semigroup_add) foldl_assoc:
1842 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
1843 by (induct zs arbitrary: y) (simp_all add:add_assoc)
1845 lemma (in monoid_add) foldl_absorb0:
1846 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
1847 by (induct zs) (simp_all add:foldl_assoc)
1850 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
1852 lemma foldl_foldr1_lemma:
1853 "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
1854 by (induct xs arbitrary: a) (auto simp:add_assoc)
1856 corollary foldl_foldr1:
1857 "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
1858 by (simp add:foldl_foldr1_lemma)
1861 text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
1863 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
1866 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
1867 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
1869 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
1870 by (induct xs, auto simp add: foldl_assoc add_commute)
1873 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
1874 difficult to use because it requires an additional transitivity step.
1877 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
1878 by (induct ns arbitrary: n) auto
1880 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
1881 by (force intro: start_le_sum simp add: in_set_conv_decomp)
1883 lemma sum_eq_0_conv [iff]:
1884 "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
1885 by (induct ns arbitrary: m) auto
1887 lemma foldr_invariant:
1888 "\<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)"
1889 by (induct xs, simp_all)
1891 lemma foldl_invariant:
1892 "\<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)"
1893 by (induct xs arbitrary: x, simp_all)
1895 text{* @{const foldl} and @{text concat} *}
1897 lemma concat_conv_foldl: "concat xss = foldl op@ [] xss"
1898 by (induct xss) (simp_all add:monoid_append.foldl_absorb0)
1900 lemma foldl_conv_concat:
1901 "foldl (op @) xs xxs = xs @ (concat xxs)"
1902 by(simp add:concat_conv_foldl monoid_append.foldl_absorb0)
1904 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
1906 lemma listsum_append[simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
1907 by (induct xs) (simp_all add:add_assoc)
1909 lemma listsum_rev[simp]:
1910 fixes xs :: "'a::comm_monoid_add list"
1911 shows "listsum (rev xs) = listsum xs"
1912 by (induct xs) (simp_all add:add_ac)
1914 lemma listsum_foldr:
1915 "listsum xs = foldr (op +) xs 0"
1918 text{* For efficient code generation ---
1919 @{const listsum} is not tail recursive but @{const foldl} is. *}
1920 lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
1921 by(simp add:listsum_foldr foldl_foldr1)
1924 text{* Some syntactic sugar for summing a function over a list: *}
1927 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
1929 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
1930 syntax (HTML output)
1931 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
1933 translations -- {* Beware of argument permutation! *}
1934 "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
1935 "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
1937 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
1938 by (induct xs) simp_all
1940 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
1941 lemma uminus_listsum_map:
1942 "- listsum (map f xs) = (listsum (map (uminus o f) xs) :: 'a::ab_group_add)"
1943 by(induct xs) simp_all
1946 subsubsection {* @{text upt} *}
1948 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
1949 -- {* simp does not terminate! *}
1952 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
1953 by (subst upt_rec) simp
1955 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
1956 by(induct j)simp_all
1958 lemma upt_eq_Cons_conv:
1959 "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
1960 apply(induct j arbitrary: x xs)
1962 apply(clarsimp simp add: append_eq_Cons_conv)
1966 lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
1967 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}
1970 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
1973 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
1974 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
1977 lemma length_upt [simp]: "length [i..<j] = j - i"
1978 by (induct j) (auto simp add: Suc_diff_le)
1980 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
1982 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
1986 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
1987 by(simp add:upt_conv_Cons)
1989 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
1992 by(simp add:upt_Suc_append)
1994 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
1995 apply (induct m arbitrary: i, simp)
1996 apply (subst upt_rec)
1998 apply (subst upt_rec)
1999 apply (simp del: upt.simps)
2002 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
2007 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
2010 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
2011 apply (induct n m arbitrary: i rule: diff_induct)
2012 prefer 3 apply (subst map_Suc_upt[symmetric])
2013 apply (auto simp add: less_diff_conv nth_upt)
2016 lemma nth_take_lemma:
2017 "k <= length xs ==> k <= length ys ==>
2018 (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
2019 apply (atomize, induct k arbitrary: xs ys)
2020 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
2021 txt {* Both lists must be non-empty *}
2022 apply (case_tac xs, simp)
2023 apply (case_tac ys, clarify)
2024 apply (simp (no_asm_use))
2026 txt {* prenexing's needed, not miniscoping *}
2027 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)
2031 lemma nth_equalityI:
2032 "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
2033 apply (frule nth_take_lemma [OF le_refl eq_imp_le])
2034 apply (simp_all add: take_all)
2038 "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
2039 by (rule nth_equalityI, auto)
2041 (* needs nth_equalityI *)
2042 lemma list_all2_antisym:
2043 "\<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>
2044 \<Longrightarrow> xs = ys"
2045 apply (simp add: list_all2_conv_all_nth)
2046 apply (rule nth_equalityI, blast, simp)
2049 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
2050 -- {* The famous take-lemma. *}
2051 apply (drule_tac x = "max (length xs) (length ys)" in spec)
2052 apply (simp add: le_max_iff_disj take_all)
2057 "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
2058 by (cases n) simp_all
2061 "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
2062 by (cases n) simp_all
2064 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
2065 by (cases n) simp_all
2067 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
2068 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
2069 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
2071 declare take_Cons_number_of [simp]
2072 drop_Cons_number_of [simp]
2073 nth_Cons_number_of [simp]
2076 subsubsection {* @{text "distinct"} and @{text remdups} *}
2078 lemma distinct_append [simp]:
2079 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
2082 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
2085 lemma set_remdups [simp]: "set (remdups xs) = set xs"
2086 by (induct xs) (auto simp add: insert_absorb)
2088 lemma distinct_remdups [iff]: "distinct (remdups xs)"
2091 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
2092 by (induct xs, auto)
2094 lemma remdups_id_iff_distinct[simp]: "(remdups xs = xs) = distinct xs"
2095 by(metis distinct_remdups distinct_remdups_id)
2097 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
2098 by (metis distinct_remdups finite_list set_remdups)
2100 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
2103 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
2106 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
2109 lemma length_remdups_eq[iff]:
2110 "(length (remdups xs) = length xs) = (remdups xs = xs)"
2113 apply(subgoal_tac "length (remdups xs) <= length xs")
2115 apply(rule length_remdups_leq)
2120 "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
2124 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
2127 lemma distinct_upt[simp]: "distinct[i..<j]"
2130 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
2131 apply(induct xs arbitrary: i)
2135 apply(blast dest:in_set_takeD)
2138 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
2139 apply(induct xs arbitrary: i)
2145 lemma distinct_list_update:
2146 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
2147 shows "distinct (xs[i:=a])"
2148 proof (cases "i < length xs")
2150 with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
2151 apply (drule_tac id_take_nth_drop) by simp
2152 with d True show ?thesis
2153 apply (simp add: upd_conv_take_nth_drop)
2154 apply (drule subst [OF id_take_nth_drop]) apply assumption
2155 apply simp apply (cases "a = xs!i") apply simp by blast
2157 case False with d show ?thesis by auto
2161 text {* It is best to avoid this indexed version of distinct, but
2162 sometimes it is useful. *}
2164 lemma distinct_conv_nth:
2165 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
2166 apply (induct xs, simp, simp)
2167 apply (rule iffI, clarsimp)
2169 apply (case_tac j, simp)
2170 apply (simp add: set_conv_nth)
2172 apply (clarsimp simp add: set_conv_nth, simp)
2175 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
2177 apply (clarsimp simp add: set_conv_nth)
2178 apply (erule_tac x = 0 in allE, simp)
2179 apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
2181 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
2183 apply (erule_tac x = "Suc i" in allE, simp)
2184 apply (erule_tac x = "Suc j" in allE, simp)
2187 lemma nth_eq_iff_index_eq:
2188 "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
2189 by(auto simp: distinct_conv_nth)
2191 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
2194 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
2196 case Nil thus ?case by simp
2200 proof (cases "x \<in> set xs")
2201 case False with Cons show ?thesis by simp
2203 case True with Cons.prems
2204 have "card (set xs) = Suc (length xs)"
2205 by (simp add: card_insert_if split: split_if_asm)
2206 moreover have "card (set xs) \<le> length xs" by (rule card_length)
2207 ultimately have False by simp
2212 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
2213 apply (induct n == "length ws" arbitrary:ws) apply simp
2214 apply(case_tac ws) apply simp
2215 apply (simp split:split_if_asm)
2216 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
2219 lemma length_remdups_concat:
2220 "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
2221 by(simp add: set_concat distinct_card[symmetric])
2224 subsubsection {* @{text remove1} *}
2226 lemma remove1_append:
2227 "remove1 x (xs @ ys) =
2228 (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
2231 lemma in_set_remove1[simp]:
2232 "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
2237 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
2244 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
2251 lemma length_remove1:
2252 "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
2254 apply (auto dest!:length_pos_if_in_set)
2257 lemma remove1_filter_not[simp]:
2258 "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
2261 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
2262 apply(insert set_remove1_subset)
2266 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
2267 by (induct xs) simp_all
2270 subsubsection {* @{text replicate} *}
2272 lemma length_replicate [simp]: "length (replicate n x) = n"
2275 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
2278 lemma replicate_app_Cons_same:
2279 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
2282 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
2283 apply (induct n, simp)
2284 apply (simp add: replicate_app_Cons_same)
2287 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
2290 text{* Courtesy of Matthias Daum: *}
2291 lemma append_replicate_commute:
2292 "replicate n x @ replicate k x = replicate k x @ replicate n x"
2293 apply (simp add: replicate_add [THEN sym])
2294 apply (simp add: add_commute)
2297 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
2300 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"
2303 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
2304 by (atomize (full), induct n) auto
2306 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
2307 apply (induct n arbitrary: i, simp)
2308 apply (simp add: nth_Cons split: nat.split)
2311 text{* Courtesy of Matthias Daum (2 lemmas): *}
2312 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
2313 apply (case_tac "k \<le> i")
2314 apply (simp add: min_def)
2315 apply (drule not_leE)
2316 apply (simp add: min_def)
2317 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
2319 apply (simp add: replicate_add [symmetric])
2322 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
2323 apply (induct k arbitrary: i)
2332 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
2335 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
2336 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
2338 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
2341 lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
2342 by (simp add: set_replicate_conv_if split: split_if_asm)
2344 lemma replicate_append_same:
2345 "replicate i x @ [x] = x # replicate i x"
2346 by (induct i) simp_all
2348 lemma map_replicate_trivial:
2349 "map (\<lambda>i. x) [0..<i] = replicate i x"
2350 by (induct i) (simp_all add: replicate_append_same)
2353 subsubsection{*@{text rotate1} and @{text rotate}*}
2355 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
2356 by(simp add:rotate1_def)
2358 lemma rotate0[simp]: "rotate 0 = id"
2359 by(simp add:rotate_def)
2361 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
2362 by(simp add:rotate_def)
2365 "rotate (m+n) = rotate m o rotate n"
2366 by(simp add:rotate_def funpow_add)
2368 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
2369 by(simp add:rotate_add)
2371 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
2372 by(simp add:rotate_def funpow_swap1)
2374 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
2375 by(cases xs) simp_all
2377 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
2380 apply (simp add:rotate_def)
2383 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
2384 by(simp add:rotate1_def split:list.split)
2386 lemma rotate_drop_take:
2387 "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
2390 apply(simp add:rotate_def)
2391 apply(cases "xs = []")
2393 apply(case_tac "n mod length xs = 0")
2394 apply(simp add:mod_Suc)
2395 apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
2396 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
2397 take_hd_drop linorder_not_le)
2400 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
2401 by(simp add:rotate_drop_take)
2403 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
2404 by(simp add:rotate_drop_take)
2406 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
2407 by(simp add:rotate1_def split:list.split)
2409 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
2410 by (induct n arbitrary: xs) (simp_all add:rotate_def)
2412 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
2413 by(simp add:rotate1_def split:list.split) blast
2415 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
2416 by (induct n) (simp_all add:rotate_def)
2418 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
2419 by(simp add:rotate_drop_take take_map drop_map)
2421 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
2422 by(simp add:rotate1_def split:list.split)
2424 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
2425 by (induct n) (simp_all add:rotate_def)
2427 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
2428 by(simp add:rotate1_def split:list.split)
2430 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
2431 by (induct n) (simp_all add:rotate_def)
2434 "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
2435 apply(simp add:rotate_drop_take rev_drop rev_take)
2436 apply(cases "length xs = 0")
2438 apply(cases "n mod length xs = 0")
2440 apply(simp add:rotate_drop_take rev_drop rev_take)
2443 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
2444 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
2445 apply(subgoal_tac "length xs \<noteq> 0")
2447 using mod_less_divisor[of "length xs" n] by arith
2450 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
2452 lemma sublist_empty [simp]: "sublist xs {} = []"
2453 by (auto simp add: sublist_def)
2455 lemma sublist_nil [simp]: "sublist [] A = []"
2456 by (auto simp add: sublist_def)
2458 lemma length_sublist:
2459 "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
2460 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
2462 lemma sublist_shift_lemma_Suc:
2463 "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
2464 map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
2465 apply(induct xs arbitrary: "is")
2467 apply (case_tac "is")
2472 lemma sublist_shift_lemma:
2473 "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
2474 map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
2475 by (induct xs rule: rev_induct) (simp_all add: add_commute)
2477 lemma sublist_append:
2478 "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
2479 apply (unfold sublist_def)
2480 apply (induct l' rule: rev_induct, simp)
2481 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
2482 apply (simp add: add_commute)
2486 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
2487 apply (induct l rule: rev_induct)
2488 apply (simp add: sublist_def)
2489 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
2492 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
2493 apply(induct xs arbitrary: I)
2494 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
2497 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
2498 by(auto simp add:set_sublist)
2500 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
2501 by(auto simp add:set_sublist)
2503 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
2504 by(auto simp add:set_sublist)
2506 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
2507 by (simp add: sublist_Cons)
2510 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
2511 apply(induct xs arbitrary: I)
2513 apply(auto simp add:sublist_Cons)
2517 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
2518 apply (induct l rule: rev_induct, simp)
2519 apply (simp split: nat_diff_split add: sublist_append)
2522 lemma filter_in_sublist:
2523 "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
2524 proof (induct xs arbitrary: s)
2525 case Nil thus ?case by simp
2528 moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
2529 ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
2533 subsubsection {* @{const splice} *}
2535 lemma splice_Nil2 [simp, code]:
2537 by (cases xs) simp_all
2539 lemma splice_Cons_Cons [simp, code]:
2540 "splice (x#xs) (y#ys) = x # y # splice xs ys"
2543 declare splice.simps(2) [simp del, code del]
2545 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
2546 apply(induct xs arbitrary: ys) apply simp
2552 subsection {*Sorting*}
2554 text{* Currently it is not shown that @{const sort} returns a
2555 permutation of its input because the nicest proof is via multisets,
2556 which are not yet available. Alternatively one could define a function
2557 that counts the number of occurrences of an element in a list and use
2558 that instead of multisets to state the correctness property. *}
2563 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
2564 apply(induct xs arbitrary: x) apply simp
2565 by simp (blast intro: order_trans)
2567 lemma sorted_append:
2568 "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
2569 by (induct xs) (auto simp add:sorted_Cons)
2571 lemma set_insort: "set(insort x xs) = insert x (set xs)"
2574 lemma set_sort[simp]: "set(sort xs) = set xs"
2575 by (induct xs) (simp_all add:set_insort)
2577 lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
2578 by(induct xs)(auto simp:set_insort)
2580 lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
2581 by(induct xs)(simp_all add:distinct_insort set_sort)
2583 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
2585 apply(auto simp:sorted_Cons set_insort)
2588 theorem sorted_sort[simp]: "sorted (sort xs)"
2589 by (induct xs) (auto simp:sorted_insort)
2591 lemma sorted_distinct_set_unique:
2592 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
2595 from assms have 1: "length xs = length ys" by (metis distinct_card)
2596 from assms show ?thesis
2597 proof(induct rule:list_induct2[OF 1])
2598 case 1 show ?case by simp
2600 case 2 thus ?case by (simp add:sorted_Cons)
2601 (metis Diff_insert_absorb antisym insertE insert_iff)
2605 lemma finite_sorted_distinct_unique:
2606 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
2607 apply(drule finite_distinct_list)
2609 apply(rule_tac a="sort xs" in ex1I)
2610 apply (auto simp: sorted_distinct_set_unique)
2615 lemma sorted_upt[simp]: "sorted[i..<j]"
2616 by (induct j) (simp_all add:sorted_append)
2619 subsubsection {* @{text sorted_list_of_set} *}
2621 text{* This function maps (finite) linearly ordered sets to sorted
2622 lists. Warning: in most cases it is not a good idea to convert from
2623 sets to lists but one should convert in the other direction (via
2631 sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
2632 "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
2634 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
2635 set(sorted_list_of_set A) = A &
2636 sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
2637 apply(simp add:sorted_list_of_set_def)
2639 apply(simp_all add: finite_sorted_distinct_unique)
2642 lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
2643 unfolding sorted_list_of_set_def
2644 apply(subst the_equality[of _ "[]"])
2651 subsubsection {* @{text upto}: the generic interval-list *}
2653 class finite_intvl_succ = linorder +
2654 fixes successor :: "'a \<Rightarrow> 'a"
2655 assumes finite_intvl: "finite{a..b}"
2656 and successor_incr: "a < successor a"
2657 and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
2659 context finite_intvl_succ
2663 upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
2664 "upto i j == sorted_list_of_set {i..j}"
2666 lemma upto[simp]: "set[a..b] = {a..b} & sorted[a..b] & distinct[a..b]"
2667 by(simp add:upto_def finite_intvl)
2669 lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
2670 apply(insert successor_incr[of i])
2671 apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
2672 apply (metis ord_discrete less_le not_le)
2675 lemma sorted_list_of_set_rec: "i \<le> j \<Longrightarrow>
2676 sorted_list_of_set {i..j} = i # sorted_list_of_set {successor i..j}"
2677 apply(simp add:sorted_list_of_set_def upto_def)
2678 apply (rule the1_equality[OF finite_sorted_distinct_unique])
2679 apply (simp add:finite_intvl)
2680 apply(rule the1I2[OF finite_sorted_distinct_unique])
2681 apply (simp add:finite_intvl)
2682 apply (simp add: sorted_Cons insert_intvl Ball_def)
2683 apply (metis successor_incr leD less_imp_le order_trans)
2686 lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
2687 by(simp add: upto_def sorted_list_of_set_rec)
2691 text{* The integers are an instance of the above class: *}
2693 instantiation int:: finite_intvl_succ
2697 successor_int_def: "successor = (%i\<Colon>int. i+1)"
2700 by intro_classes (simp_all add: successor_int_def)
2704 text{* Now @{term"[i..j::int]"} is defined for integers. *}
2706 hide (open) const successor
2709 subsubsection {* @{text lists}: the list-forming operator over sets *}
2712 lists :: "'a set => 'a list set"
2715 Nil [intro!]: "[]: lists A"
2716 | Cons [intro!,noatp]: "[| a: A;l: lists A|] ==> a#l : lists A"
2718 inductive_cases listsE [elim!,noatp]: "x#l : lists A"
2719 inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
2721 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
2722 by (clarify, erule listsp.induct, blast+)
2724 lemmas lists_mono = listsp_mono [to_set]
2727 assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
2730 lemmas lists_IntI = listsp_infI [to_set]
2732 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
2733 proof (rule mono_inf [where f=listsp, THEN order_antisym])
2734 show "mono listsp" by (simp add: mono_def listsp_mono)
2735 show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro: listsp_infI)
2738 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
2740 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set]
2742 lemma append_in_listsp_conv [iff]:
2743 "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
2746 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
2748 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
2749 -- {* eliminate @{text listsp} in favour of @{text set} *}
2752 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
2754 lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
2755 by (rule in_listsp_conv_set [THEN iffD1])
2757 lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
2759 lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
2760 by (rule in_listsp_conv_set [THEN iffD2])
2762 lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
2764 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
2769 subsubsection{* Inductive definition for membership *}
2771 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
2773 elem: "ListMem x (x # xs)"
2774 | insert: "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
2776 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
2778 apply (induct set: ListMem)
2781 apply (auto intro: ListMem.intros)
2786 subsubsection{*Lists as Cartesian products*}
2788 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
2789 @{term A} and tail drawn from @{term Xs}.*}
2792 set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
2793 "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
2795 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
2796 by (auto simp add: set_Cons_def)
2798 text{*Yields the set of lists, all of the same length as the argument and
2799 with elements drawn from the corresponding element of the argument.*}
2801 consts listset :: "'a set list \<Rightarrow> 'a list set"
2804 "listset(A#As) = set_Cons A (listset As)"
2807 subsection{*Relations on Lists*}
2809 subsubsection {* Length Lexicographic Ordering *}
2811 text{*These orderings preserve well-foundedness: shorter lists
2812 precede longer lists. These ordering are not used in dictionaries.*}
2814 consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
2815 --{*The lexicographic ordering for lists of the specified length*}
2819 (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
2820 {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
2823 lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
2824 "lex r == \<Union>n. lexn r n"
2825 --{*Holds only between lists of the same length*}
2827 lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
2828 "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
2829 --{*Compares lists by their length and then lexicographically*}
2832 lemma wf_lexn: "wf r ==> wf (lexn r n)"
2833 apply (induct n, simp, simp)
2834 apply(rule wf_subset)
2835 prefer 2 apply (rule Int_lower1)
2836 apply(rule wf_prod_fun_image)
2837 prefer 2 apply (rule inj_onI, auto)
2841 "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
2842 by (induct n arbitrary: xs ys) auto
2844 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
2845 apply (unfold lex_def)
2847 apply (blast intro: wf_lexn, clarify)
2848 apply (rename_tac m n)
2849 apply (subgoal_tac "m \<noteq> n")
2850 prefer 2 apply blast
2851 apply (blast dest: lexn_length not_sym)
2856 {(xs,ys). length xs = n \<and> length ys = n \<and>
2857 (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
2858 apply (induct n, simp)
2859 apply (simp add: image_Collect lex_prod_def, safe, blast)
2860 apply (rule_tac x = "ab # xys" in exI, simp)
2861 apply (case_tac xys, simp_all, blast)
2866 {(xs,ys). length xs = length ys \<and>
2867 (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
2868 by (force simp add: lex_def lexn_conv)
2870 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
2871 by (unfold lenlex_def) blast
2874 "lenlex r = {(xs,ys). length xs < length ys |
2875 length xs = length ys \<and> (xs, ys) : lex r}"
2876 by (simp add: lenlex_def diag_def lex_prod_def inv_image_def)
2878 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
2879 by (simp add: lex_conv)
2881 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
2882 by (simp add:lex_conv)
2884 lemma Cons_in_lex [simp]:
2885 "((x # xs, y # ys) : lex r) =
2886 ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
2887 apply (simp add: lex_conv)
2889 prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
2890 apply (case_tac xys, simp, simp)
2895 subsubsection {* Lexicographic Ordering *}
2897 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
2898 This ordering does \emph{not} preserve well-foundedness.
2899 Author: N. Voelker, March 2005. *}
2902 lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set"
2903 "lexord r == {(x,y). \<exists> a v. y = x @ a # v \<or>
2904 (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
2906 lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
2907 by (unfold lexord_def, induct_tac y, auto)
2909 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
2910 by (unfold lexord_def, induct_tac x, auto)
2912 lemma lexord_cons_cons[simp]:
2913 "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
2914 apply (unfold lexord_def, safe, simp_all)
2915 apply (case_tac u, simp, simp)
2916 apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
2917 apply (erule_tac x="b # u" in allE)
2920 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
2922 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
2923 by (induct_tac x, auto)
2925 lemma lexord_append_left_rightI:
2926 "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
2927 by (induct_tac u, auto)
2929 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
2932 lemma lexord_append_leftD:
2933 "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
2934 by (erule rev_mp, induct_tac x, auto)
2936 lemma lexord_take_index_conv:
2937 "((x,y) : lexord r) =
2938 ((length x < length y \<and> take (length x) y = x) \<or>
2939 (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
2940 apply (unfold lexord_def Let_def, clarsimp)
2941 apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
2943 apply (rule_tac x="hd (drop (length x) y)" in exI)
2944 apply (rule_tac x="tl (drop (length x) y)" in exI)
2945 apply (erule subst, simp add: min_def)
2946 apply (rule_tac x ="length u" in exI, simp)
2947 apply (rule_tac x ="take i x" in exI)
2948 apply (rule_tac x ="x ! i" in exI)
2949 apply (rule_tac x ="y ! i" in exI, safe)
2950 apply (rule_tac x="drop (Suc i) x" in exI)
2951 apply (drule sym, simp add: drop_Suc_conv_tl)
2952 apply (rule_tac x="drop (Suc i) y" in exI)
2953 by (simp add: drop_Suc_conv_tl)
2955 -- {* lexord is extension of partial ordering List.lex *}
2956 lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
2957 apply (rule_tac x = y in spec)
2958 apply (induct_tac x, clarsimp)
2959 by (clarify, case_tac x, simp, force)
2961 lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
2965 "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
2966 apply (erule rev_mp)+
2967 apply (rule_tac x = x in spec)
2968 apply (rule_tac x = z in spec)
2969 apply ( induct_tac y, simp, clarify)
2970 apply (case_tac xa, erule ssubst)
2971 apply (erule allE, erule allE) -- {* avoid simp recursion *}
2972 apply (case_tac x, simp, simp)
2973 apply (case_tac x, erule allE, erule allE, simp)
2974 apply (erule_tac x = listb in allE)
2975 apply (erule_tac x = lista in allE, simp)
2976 apply (unfold trans_def)
2979 lemma lexord_transI: "trans r \<Longrightarrow> trans (lexord r)"
2980 by (rule transI, drule lexord_trans, blast)
2982 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"
2983 apply (rule_tac x = y in spec)
2984 apply (induct_tac x, rule allI)
2985 apply (case_tac x, simp, simp)
2986 apply (rule allI, case_tac x, simp, simp)
2990 subsection {* Lexicographic combination of measure functions *}
2992 text {* These are useful for termination proofs *}
2995 "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
2997 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
2998 unfolding measures_def
3001 lemma in_measures[simp]:
3002 "(x, y) \<in> measures [] = False"
3003 "(x, y) \<in> measures (f # fs)
3004 = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"
3005 unfolding measures_def
3008 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
3011 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
3015 subsubsection{*Lifting a Relation on List Elements to the Lists*}
3018 listrel :: "('a * 'a)set => ('a list * 'a list)set"
3019 for r :: "('a * 'a)set"
3021 Nil: "([],[]) \<in> listrel r"
3022 | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
3024 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
3025 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
3026 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
3027 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
3030 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
3032 apply (erule listrel.induct)
3033 apply (blast intro: listrel.intros)+
3036 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
3038 apply (erule listrel.induct, auto)
3041 lemma listrel_refl: "refl A r \<Longrightarrow> refl (lists A) (listrel r)"
3042 apply (simp add: refl_def listrel_subset Ball_def)
3044 apply (induct_tac x)
3045 apply (auto intro: listrel.intros)
3048 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"
3049 apply (auto simp add: sym_def)
3050 apply (erule listrel.induct)
3051 apply (blast intro: listrel.intros)+
3054 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"
3055 apply (simp add: trans_def)
3058 apply (erule listrel.induct)
3059 apply (blast intro: listrel.intros)+
3062 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
3063 by (simp add: equiv_def listrel_refl listrel_sym listrel_trans)
3065 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
3066 by (blast intro: listrel.intros)
3069 "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
3070 by (auto simp add: set_Cons_def intro: listrel.intros)
3073 subsection{*Miscellany*}
3075 subsubsection {* Characters and strings *}
3078 Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
3079 | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
3081 datatype char = Char nibble nibble
3082 -- "Note: canonical order of character encoding coincides with standard term ordering"
3084 types string = "char list"
3087 "_Char" :: "xstr => char" ("CHR _")
3088 "_String" :: "xstr => string" ("_")
3090 setup StringSyntax.setup
3093 subsection {* Code generator *}
3095 subsubsection {* Setup *}
3100 fun term_of_list f T = HOLogic.mk_list T o map f;
3103 fun gen_list' aG aT i j = frequency
3107 val (xs, ts) = gen_list' aG aT (i-1) j
3108 in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
3109 (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
3110 and gen_list aG aT i = gen_list' aG aT i i;
3114 val term_of_char = HOLogic.mk_char o ord;
3118 let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
3119 in (chr j, fn () => HOLogic.mk_char j) end;
3122 consts_code "Cons" ("(_ ::/ _)")
3141 fold (fn target => CodeTarget.add_pretty_list target
3142 @{const_name Nil} @{const_name Cons}
3143 ) ["SML", "OCaml", "Haskell"]
3146 code_instance list :: eq
3149 code_const "op = \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
3150 (Haskell infixl 4 "==")
3155 fun list_codegen thy defs gr dep thyname b t =
3157 val ts = HOLogic.dest_list t;
3158 val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
3160 val (gr'', ps) = foldl_map
3161 (Codegen.invoke_codegen thy defs dep thyname false) (gr', ts)
3162 in SOME (gr'', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
3164 fun char_codegen thy defs gr dep thyname b t =
3166 val i = HOLogic.dest_char t;
3167 val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
3169 in SOME (gr', Pretty.str (ML_Syntax.print_string (chr i)))
3170 end handle TERM _ => NONE;
3173 Codegen.add_codegen "list_codegen" list_codegen
3174 #> Codegen.add_codegen "char_codegen" char_codegen
3179 subsubsection {* Generation of efficient code *}
3182 null:: "'a list \<Rightarrow> bool"
3183 list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
3184 list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
3185 list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
3186 filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
3187 map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
3190 member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
3192 "x mem [] \<longleftrightarrow> False"
3193 | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
3197 "null (x#xs) = False"
3200 "list_inter [] bs = []"
3201 "list_inter (a#as) bs =
3202 (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
3205 "list_all P [] = True"
3206 "list_all P (x#xs) = (P x \<and> list_all P xs)"
3209 "list_ex P [] = False"
3210 "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
3213 "filtermap f [] = []"
3214 "filtermap f (x#xs) =
3215 (case f x of None \<Rightarrow> filtermap f xs
3216 | Some y \<Rightarrow> y # filtermap f xs)"
3219 "map_filter f P [] = []"
3220 "map_filter f P (x#xs) =
3221 (if P x then f x # map_filter f P xs else map_filter f P xs)"
3225 Only use @{text mem} for generating executable code. Otherwise use
3226 @{prop "x : set xs"} instead --- it is much easier to reason about.
3227 The same is true for @{const list_all} and @{const list_ex}: write
3228 @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
3229 quantifiers are aleady known to the automatic provers. In fact, the
3230 declarations in the code subsection make sure that @{text "\<in>"},
3231 @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} are implemented
3234 Efficient emptyness check is implemented by @{const null}.
3236 The functions @{const filtermap} and @{const map_filter} are just
3237 there to generate efficient code. Do not use
3238 them for modelling and proving.
3241 lemma rev_foldl_cons [code]:
3242 "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
3244 case Nil then show ?case by simp
3249 have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
3250 = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
3251 by (induct xs arbitrary: ys) auto
3254 show ?case by (induct xs) (auto simp add: Cons aux)
3257 lemma mem_iff [code post]:
3258 "x mem xs \<longleftrightarrow> x \<in> set xs"
3261 lemmas in_set_code [code unfold] = mem_iff [symmetric]
3263 lemma empty_null [code inline]:
3264 "xs = [] \<longleftrightarrow> null xs"
3265 by (cases xs) simp_all
3267 lemmas null_empty [code post] =
3268 empty_null [symmetric]
3270 lemma list_inter_conv:
3271 "set (list_inter xs ys) = set xs \<inter> set ys"
3274 lemma list_all_iff [code post]:
3275 "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
3278 lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
3280 lemma list_all_append [simp]:
3281 "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
3284 lemma list_all_rev [simp]:
3285 "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
3286 by (simp add: list_all_iff)
3288 lemma list_all_length:
3289 "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
3290 unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
3292 lemma list_ex_iff [code post]:
3293 "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
3294 by (induct xs) simp_all
3296 lemmas list_bex_code [code unfold] =
3297 list_ex_iff [symmetric]
3299 lemma list_ex_length:
3300 "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
3301 unfolding list_ex_iff set_conv_nth by auto
3303 lemma filtermap_conv:
3304 "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
3305 by (induct xs) (simp_all split: option.split)
3307 lemma map_filter_conv [simp]:
3308 "map_filter f P xs = map f (filter P xs)"
3312 text {* Code for bounded quantification and summation over nats. *}
3314 lemma atMost_upto [code unfold]:
3315 "{..n} = set [0..<Suc n]"
3318 lemma atLeast_upt [code unfold]:
3319 "{..<n} = set [0..<n]"
3322 lemma greaterThanLessThan_upt [code unfold]:
3323 "{n<..<m} = set [Suc n..<m]"
3326 lemma atLeastLessThan_upt [code unfold]:
3327 "{n..<m} = set [n..<m]"
3330 lemma greaterThanAtMost_upto [code unfold]:
3331 "{n<..m} = set [Suc n..<Suc m]"
3334 lemma atLeastAtMost_upto [code unfold]:
3335 "{n..m} = set [n..<Suc m]"
3338 lemma all_nat_less_eq [code unfold]:
3339 "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
3342 lemma ex_nat_less_eq [code unfold]:
3343 "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
3346 lemma all_nat_less [code unfold]:
3347 "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
3350 lemma ex_nat_less [code unfold]:
3351 "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
3354 lemma setsum_set_upt_conv_listsum[code unfold]:
3355 "setsum f (set[k..<n]) = listsum (map f [k..<n])"
3356 apply(subst atLeastLessThan_upt[symmetric])
3357 by (induct n) simp_all
3359 subsubsection {* List partitioning *}
3362 partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list"
3364 "partition P [] = ([], [])"
3365 "partition P (x # xs) =
3366 (let (yes, no) = partition P xs
3367 in if P x then (x # yes, no) else (yes, x # no))"
3370 "partition P xs = (yes, no) \<Longrightarrow> (\<forall>p\<in> set yes. P p) \<and> (\<forall>p\<in> set no. \<not> P p)"
3371 proof (induct xs arbitrary: yes no rule: partition.induct)
3372 case Nil then show ?case by simp
3375 let ?p = "partition P as"
3376 let ?p' = "partition P (a # as)"
3377 note prem = `?p' = (yes, no)`
3381 with prem have yes: "yes = a # fst ?p" and no: "no = snd ?p"
3382 by (simp_all add: Let_def split_def)
3383 have "(\<forall>p\<in> set (fst ?p). P p) \<and> (\<forall>p\<in> set no. \<not> P p)"
3384 by (rule Cons.hyps) (simp add: yes no)
3385 with True yes show ?thesis by simp
3388 with prem have yes: "yes = fst ?p" and no: "no = a # snd ?p"
3389 by (simp_all add: Let_def split_def)
3390 have "(\<forall>p\<in> set yes. P p) \<and> (\<forall>p\<in> set (snd ?p). \<not> P p)"
3391 by (rule Cons.hyps) (simp add: yes no)
3392 with False no show ?thesis by simp
3396 lemma partition_filter1:
3397 "fst (partition P xs) = filter P xs"
3398 by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
3400 lemma partition_filter2:
3401 "snd (partition P xs) = filter (Not o P) xs"
3402 by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
3404 lemma partition_set:
3405 assumes "partition P xs = (yes, no)"
3406 shows "set yes \<union> set no = set xs"
3408 have "set xs = {x. x \<in> set xs \<and> P x} \<union> {x. x \<in> set xs \<and> \<not> P x}" by blast
3409 also have "\<dots> = set (List.filter P xs) Un (set (List.filter (Not o P) xs))" by simp
3410 also have "\<dots> = set (fst (partition P xs)) \<union> set (snd (partition P xs))"
3411 using partition_filter1 [of P xs] partition_filter2 [of P xs] by simp
3412 finally show "set yes Un set no = set xs" using assms by simp