5 header {* The datatype of finite lists *}
8 imports Plain Relation_Power Presburger Recdef ATP_Linkup
9 uses "Tools/string_syntax.ML"
14 | Cons 'a "'a list" (infixr "#" 65)
16 subsection{*Basic list processing functions*}
19 filter:: "('a => bool) => 'a list => 'a list"
20 concat:: "'a list list => 'a list"
21 foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
22 foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
24 tl:: "'a list => 'a list"
25 last:: "'a list => 'a"
26 butlast :: "'a list => 'a list"
27 set :: "'a list => 'a set"
28 map :: "('a=>'b) => ('a list => 'b list)"
29 listsum :: "'a list => 'a::monoid_add"
30 list_update :: "'a list => nat => 'a => 'a list"
31 take:: "nat => 'a list => 'a list"
32 drop:: "nat => 'a list => 'a list"
33 takeWhile :: "('a => bool) => 'a list => 'a list"
34 dropWhile :: "('a => bool) => 'a list => 'a list"
35 rev :: "'a list => 'a list"
36 zip :: "'a list => 'b list => ('a * 'b) list"
37 upt :: "nat => nat => nat list" ("(1[_..</_'])")
38 remdups :: "'a list => 'a list"
39 remove1 :: "'a => 'a list => 'a list"
40 removeAll :: "'a => 'a list => 'a list"
41 "distinct":: "'a list => bool"
42 replicate :: "nat => 'a => 'a list"
43 splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
46 nonterminals lupdbinds lupdbind
49 -- {* list Enumeration *}
50 "@list" :: "args => 'a list" ("[(_)]")
52 -- {* Special syntax for filter *}
53 "@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
56 "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")
57 "" :: "lupdbind => lupdbinds" ("_")
58 "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")
59 "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900)
64 "[x<-xs . P]"== "filter (%x. P) xs"
66 "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
67 "xs[i:=x]" == "list_update xs i x"
71 "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
73 "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
77 Function @{text size} is overloaded for all datatypes. Users may
78 refer to the list version as @{text length}. *}
81 length :: "'a list => nat" where
92 "last(x#xs) = (if xs=[] then x else last xs)"
96 "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
100 "set (x#xs) = insert x (set xs)"
104 "map f (x#xs) = f(x)#map f xs"
107 append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
109 append_Nil:"[] @ ys = ys"
110 | append_Cons: "(x#xs) @ ys = x # xs @ ys"
114 "rev(x#xs) = rev(xs) @ [x]"
118 "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
121 foldl_Nil:"foldl f a [] = a"
122 foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
126 "foldr f (x#xs) a = f x (foldr f xs a)"
130 "concat(x#xs) = x @ concat(xs)"
134 "listsum (x # xs) = x + listsum xs"
137 drop_Nil:"drop n [] = []"
138 drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
139 -- {*Warning: simpset does not contain this definition, but separate
140 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
143 take_Nil:"take n [] = []"
144 take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
145 -- {*Warning: simpset does not contain this definition, but separate
146 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
148 primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where
149 nth_Cons: "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
150 -- {*Warning: simpset does not contain this definition, but separate
151 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
155 "(x#xs)[i:=v] = (case i of 0 => v # xs | Suc j => x # xs[j:=v])"
158 "takeWhile P [] = []"
159 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
162 "dropWhile P [] = []"
163 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
167 zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
168 -- {*Warning: simpset does not contain this definition, but separate
169 theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
172 upt_0: "[i..<0] = []"
173 upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
177 "distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
181 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
185 "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
188 "removeAll x [] = []"
189 "removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)"
192 replicate_0: "replicate 0 x = []"
193 replicate_Suc: "replicate (Suc n) x = x # replicate n x"
196 rotate1 :: "'a list \<Rightarrow> 'a list" where
197 "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
200 rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
201 "rotate n = rotate1 ^ n"
204 list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
205 [code del]: "list_all2 P xs ys =
206 (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
209 sublist :: "'a list => nat set => 'a list" where
210 "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
214 "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
215 -- {*Warning: simpset does not contain the second eqn but a derived one. *}
221 @{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\
222 @{lemma "length [a,b,c] = 3" by simp}\\
223 @{lemma "set [a,b,c] = {a,b,c}" by simp}\\
224 @{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\
225 @{lemma "rev [a,b,c] = [c,b,a]" by simp}\\
226 @{lemma "hd [a,b,c,d] = a" by simp}\\
227 @{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\
228 @{lemma "last [a,b,c,d] = d" by simp}\\
229 @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
230 @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
231 @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
232 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
233 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
234 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
235 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
236 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
237 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
238 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
239 @{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
240 @{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\
241 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\
242 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
243 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
244 @{lemma "distinct [2,0,1::nat]" by simp}\\
245 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
246 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
247 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
248 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
249 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
250 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
251 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
252 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\
253 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\
254 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\
255 @{lemma "listsum [1,2,3::nat] = 6" by simp}
257 \caption{Characteristic examples}
258 \label{fig:Characteristic}
260 Figure~\ref{fig:Characteristic} shows charachteristic examples
261 that should give an intuitive understanding of the above functions.
264 text{* The following simple sort functions are intended for proofs,
265 not for efficient implementations. *}
270 fun sorted :: "'a list \<Rightarrow> bool" where
271 "sorted [] \<longleftrightarrow> True" |
272 "sorted [x] \<longleftrightarrow> True" |
273 "sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
275 primrec insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
276 "insort x [] = [x]" |
277 "insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
279 primrec sort :: "'a list \<Rightarrow> 'a list" where
281 "sort (x#xs) = insort x (sort xs)"
286 subsubsection {* List comprehension *}
288 text{* Input syntax for Haskell-like list comprehension notation.
289 Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
290 the list of all pairs of distinct elements from @{text xs} and @{text ys}.
291 The syntax is as in Haskell, except that @{text"|"} becomes a dot
292 (like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
293 \verb![e| x <- xs, ...]!.
295 The qualifiers after the dot are
297 \item[generators] @{text"p \<leftarrow> xs"},
298 where @{text p} is a pattern and @{text xs} an expression of list type, or
299 \item[guards] @{text"b"}, where @{text b} is a boolean expression.
300 %\item[local bindings] @ {text"let x = e"}.
303 Just like in Haskell, list comprehension is just a shorthand. To avoid
304 misunderstandings, the translation into desugared form is not reversed
305 upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is
306 optmized to @{term"map (%x. e) xs"}.
308 It is easy to write short list comprehensions which stand for complex
309 expressions. During proofs, they may become unreadable (and
310 mangled). In such cases it can be advisable to introduce separate
311 definitions for the list comprehensions in question. *}
314 Proper theorem proving support would be nice. For example, if
315 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
316 produced something like
317 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
320 nonterminals lc_qual lc_quals
323 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __")
324 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
325 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
326 (*"_lc_let" :: "letbinds => lc_qual" ("let _")*)
327 "_lc_end" :: "lc_quals" ("]")
328 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
329 "_lc_abs" :: "'a => 'b list => 'b list"
331 (* These are easier than ML code but cannot express the optimized
332 translation of [e. p<-xs]
334 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
335 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
336 => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
337 "[e. P]" => "if P then [e] else []"
338 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
339 => "if P then (_listcompr e Q Qs) else []"
340 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
341 => "_Let b (_listcompr e Q Qs)"
345 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
347 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
349 parse_translation (advanced) {*
351 val NilC = Syntax.const @{const_name Nil};
352 val ConsC = Syntax.const @{const_name Cons};
353 val mapC = Syntax.const @{const_name map};
354 val concatC = Syntax.const @{const_name concat};
355 val IfC = Syntax.const @{const_name If};
356 fun singl x = ConsC $ x $ NilC;
358 fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
360 val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
361 val e = if opti then singl e else e;
362 val case1 = Syntax.const "_case1" $ p $ e;
363 val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
365 val cs = Syntax.const "_case2" $ case1 $ case2
366 val ft = DatatypeCase.case_tr false DatatypePackage.datatype_of_constr
370 fun abs_tr ctxt (p as Free(s,T)) e opti =
371 let val thy = ProofContext.theory_of ctxt;
372 val s' = Sign.intern_const thy s
373 in if Sign.declared_const thy s'
374 then (pat_tr ctxt p e opti, false)
375 else (lambda p e, true)
377 | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
379 fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] =
380 let val res = case qs of Const("_lc_end",_) => singl e
381 | Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs];
382 in IfC $ b $ res $ NilC end
383 | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] =
384 (case abs_tr ctxt p e true of
385 (f,true) => mapC $ f $ es
386 | (f, false) => concatC $ (mapC $ f $ es))
387 | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] =
388 let val e' = lc_tr ctxt [e,q,qs];
389 in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end
391 in [("_listcompr", lc_tr)] end
396 term "[(x,y,z). x\<leftarrow>xs]"
397 term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
398 term "[(x,y,z). x<a, x>b]"
399 term "[(x,y,z). x\<leftarrow>xs, x>b]"
400 term "[(x,y,z). x<a, x\<leftarrow>xs]"
401 term "[(x,y). Cons True x \<leftarrow> xs]"
402 term "[(x,y,z). Cons x [] \<leftarrow> xs]"
403 term "[(x,y,z). x<a, x>b, x=d]"
404 term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
405 term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
406 term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
407 term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
408 term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
409 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
410 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
411 term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
414 subsubsection {* @{const Nil} and @{const Cons} *}
416 lemma not_Cons_self [simp]:
420 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]
422 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
426 "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
427 by (rule measure_induct [of length]) iprover
430 subsubsection {* @{const length} *}
433 Needs to come before @{text "@"} because of theorem @{text
434 append_eq_append_conv}.
437 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"
440 lemma length_map [simp]: "length (map f xs) = length xs"
443 lemma length_rev [simp]: "length (rev xs) = length xs"
446 lemma length_tl [simp]: "length (tl xs) = length xs - 1"
449 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
452 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])"
455 lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0"
458 lemma length_Suc_conv:
459 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
462 lemma Suc_length_conv:
463 "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
464 apply (induct xs, simp, simp)
468 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"
471 lemma list_induct2 [consumes 1, case_names Nil Cons]:
472 "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>
473 (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys))
474 \<Longrightarrow> P xs ys"
475 proof (induct xs arbitrary: ys)
476 case Nil then show ?case by simp
478 case (Cons x xs ys) then show ?case by (cases ys) simp_all
481 lemma list_induct3 [consumes 2, case_names Nil Cons]:
482 "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow>
483 (\<And>x xs y ys z zs. length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P xs ys zs \<Longrightarrow> P (x#xs) (y#ys) (z#zs))
484 \<Longrightarrow> P xs ys zs"
485 proof (induct xs arbitrary: ys zs)
486 case Nil then show ?case by simp
488 case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)
494 \<And>x xs. P (x#xs) [];
495 \<And>y ys. P [] (y#ys);
496 \<And>x xs y ys. P xs ys \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
497 \<Longrightarrow> P xs ys"
498 by (induct xs arbitrary: ys) (case_tac x, auto)+
500 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
501 by (rule Eq_FalseI) auto
503 simproc_setup list_neq ("(xs::'a list) = ys") = {*
505 Reduces xs=ys to False if xs and ys cannot be of the same length.
506 This is the case if the atomic sublists of one are a submultiset
507 of those of the other list and there are fewer Cons's in one than the other.
512 fun len (Const(@{const_name Nil},_)) acc = acc
513 | len (Const(@{const_name Cons},_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
514 | len (Const(@{const_name append},_) $ xs $ ys) acc = len xs (len ys acc)
515 | len (Const(@{const_name rev},_) $ xs) acc = len xs acc
516 | len (Const(@{const_name map},_) $ _ $ xs) acc = len xs acc
517 | len t (ts,n) = (t::ts,n);
519 fun list_neq _ ss ct =
521 val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
522 val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
525 val Type(_,listT::_) = eqT;
526 val size = HOLogic.size_const listT;
527 val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
528 val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
529 val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
530 (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));
531 in SOME (thm RS @{thm neq_if_length_neq}) end
533 if m < n andalso submultiset (op aconv) (ls,rs) orelse
534 n < m andalso submultiset (op aconv) (rs,ls)
535 then prove_neq() else NONE
541 subsubsection {* @{text "@"} -- append *}
543 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
546 lemma append_Nil2 [simp]: "xs @ [] = xs"
549 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
552 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])"
555 lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"
558 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
561 lemma append_eq_append_conv [simp, noatp]:
562 "length xs = length ys \<or> length us = length vs
563 ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
564 apply (induct xs arbitrary: ys)
565 apply (case_tac ys, simp, force)
566 apply (case_tac ys, force, simp)
569 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
570 (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
571 apply (induct xs arbitrary: ys zs ts)
578 lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"
581 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"
584 lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)"
587 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"
588 using append_same_eq [of _ _ "[]"] by auto
590 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
591 using append_same_eq [of "[]"] by auto
593 lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
596 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
599 lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"
600 by (simp add: hd_append split: list.split)
602 lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"
603 by (simp split: list.split)
605 lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"
606 by (simp add: tl_append split: list.split)
609 lemma Cons_eq_append_conv: "x#xs = ys@zs =
610 (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"
613 lemma append_eq_Cons_conv: "(ys@zs = x#xs) =
614 (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
618 text {* Trivial rules for solving @{text "@"}-equations automatically. *}
620 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
623 lemma Cons_eq_appendI:
624 "[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"
627 lemma append_eq_appendI:
628 "[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"
633 Simplification procedure for all list equalities.
634 Currently only tries to rearrange @{text "@"} to see if
635 - both lists end in a singleton list,
636 - or both lists end in the same list.
642 fun last (cons as Const(@{const_name Cons},_) $ _ $ xs) =
643 (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)
644 | last (Const(@{const_name append},_) $ _ $ ys) = last ys
647 fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
650 fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
651 (case xs of Const(@{const_name Nil},_) => xs | _ => cons $ butlast xs)
652 | butlast ((app as Const(@{const_name append},_) $ xs) $ ys) = app $ butlast ys
653 | butlast xs = Const(@{const_name Nil},fastype_of xs);
655 val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
656 @{thm append_Nil}, @{thm append_Cons}];
658 fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
660 val lastl = last lhs and lastr = last rhs;
663 val lhs1 = butlast lhs and rhs1 = butlast rhs;
664 val Type(_,listT::_) = eqT
665 val appT = [listT,listT] ---> listT
666 val app = Const(@{const_name append},appT)
667 val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
668 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
669 val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
670 (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
671 in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
674 if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
675 else if lastl aconv lastr then rearr @{thm append_same_eq}
681 val list_eq_simproc =
682 Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
686 Addsimprocs [list_eq_simproc];
690 subsubsection {* @{text map} *}
692 lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
693 by (induct xs) simp_all
695 lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)"
696 by (rule ext, induct_tac xs) auto
698 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"
701 lemma map_compose: "map (f o g) xs = map f (map g xs)"
702 by (induct xs) (auto simp add: o_def)
704 lemma rev_map: "rev (map f xs) = map f (rev xs)"
707 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
710 lemma map_cong [fundef_cong, recdef_cong]:
711 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
712 -- {* a congruence rule for @{text map} *}
715 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
718 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
721 lemma map_eq_Cons_conv:
722 "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
725 lemma Cons_eq_map_conv:
726 "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
729 lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]
730 lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]
731 declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!]
734 "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
735 by(induct ys, auto simp add: Cons_eq_map_conv)
737 lemma map_eq_imp_length_eq:
738 assumes "map f xs = map f ys"
739 shows "length xs = length ys"
740 using assms proof (induct ys arbitrary: xs)
741 case Nil then show ?case by simp
743 case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
744 from Cons xs have "map f zs = map f ys" by simp
745 moreover with Cons have "length zs = length ys" by blast
746 with xs show ?case by simp
750 "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
752 apply(frule map_eq_imp_length_eq)
754 apply(induct rule:list_induct2)
757 apply (blast intro:sym)
760 lemma inj_on_map_eq_map:
761 "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
762 by(blast dest:map_inj_on)
765 "map f xs = map f ys ==> inj f ==> xs = ys"
766 by (induct ys arbitrary: xs) (auto dest!:injD)
768 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
769 by(blast dest:map_injective)
771 lemma inj_mapI: "inj f ==> inj (map f)"
772 by (iprover dest: map_injective injD intro: inj_onI)
774 lemma inj_mapD: "inj (map f) ==> inj f"
775 apply (unfold inj_on_def, clarify)
776 apply (erule_tac x = "[x]" in ballE)
777 apply (erule_tac x = "[y]" in ballE, simp, blast)
781 lemma inj_map[iff]: "inj (map f) = inj f"
782 by (blast dest: inj_mapD intro: inj_mapI)
784 lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
786 apply(erule map_inj_on)
787 apply(blast intro:inj_onI dest:inj_onD)
790 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
793 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
796 lemma map_fst_zip[simp]:
797 "length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs"
798 by (induct rule:list_induct2, simp_all)
800 lemma map_snd_zip[simp]:
801 "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
802 by (induct rule:list_induct2, simp_all)
805 subsubsection {* @{text rev} *}
807 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
810 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
813 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
816 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
819 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
822 lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
825 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
828 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
829 apply (induct xs arbitrary: ys, force)
830 apply (case_tac ys, simp, force)
833 lemma inj_on_rev[iff]: "inj_on rev A"
834 by(simp add:inj_on_def)
836 lemma rev_induct [case_names Nil snoc]:
837 "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
838 apply(simplesubst rev_rev_ident[symmetric])
839 apply(rule_tac list = "rev xs" in list.induct, simp_all)
842 lemma rev_exhaust [case_names Nil snoc]:
843 "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"
844 by (induct xs rule: rev_induct) auto
846 lemmas rev_cases = rev_exhaust
848 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
849 by(rule rev_cases[of xs]) auto
852 subsubsection {* @{text set} *}
854 lemma finite_set [iff]: "finite (set xs)"
857 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)"
860 lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs"
863 lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
866 lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs"
869 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
872 lemma set_empty2[iff]: "({} = set xs) = (xs = [])"
875 lemma set_rev [simp]: "set (rev xs) = set xs"
878 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
881 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
884 lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}"
885 apply (induct j, simp_all)
886 apply (erule ssubst, auto)
890 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
892 case Nil thus ?case by simp
894 case Cons thus ?case by (auto intro: Cons_eq_appendI)
897 lemma in_set_conv_decomp: "x \<in> set xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"
898 by (auto elim: split_list)
900 lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
902 case Nil thus ?case by simp
907 assume "x = a" thus ?case using Cons by fastsimp
909 assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
913 lemma in_set_conv_decomp_first:
914 "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
915 by (auto dest!: split_list_first)
917 lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
918 proof (induct xs rule:rev_induct)
919 case Nil thus ?case by simp
924 assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
926 assume "x \<noteq> a" thus ?case using snoc by fastsimp
930 lemma in_set_conv_decomp_last:
931 "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
932 by (auto dest!: split_list_last)
934 lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x"
936 case Nil thus ?case by simp
939 by(simp add:Bex_def)(metis append_Cons append.simps(1))
942 lemma split_list_propE:
943 assumes "\<exists>x \<in> set xs. P x"
944 obtains ys x zs where "xs = ys @ x # zs" and "P x"
945 using split_list_prop [OF assms] by blast
947 lemma split_list_first_prop:
948 "\<exists>x \<in> set xs. P x \<Longrightarrow>
949 \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)"
951 case Nil thus ?case by simp
958 (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
961 hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
962 thus ?thesis using `\<not> P x` Cons(1) by (metis append_Cons set_ConsD)
966 lemma split_list_first_propE:
967 assumes "\<exists>x \<in> set xs. P x"
968 obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y"
969 using split_list_first_prop [OF assms] by blast
971 lemma split_list_first_prop_iff:
972 "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
973 (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))"
974 by (rule, erule split_list_first_prop) auto
976 lemma split_list_last_prop:
977 "\<exists>x \<in> set xs. P x \<Longrightarrow>
978 \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)"
979 proof(induct xs rule:rev_induct)
980 case Nil thus ?case by simp
985 assume "P x" thus ?thesis by (metis emptyE set_empty)
988 hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
989 thus ?thesis using `\<not> P x` snoc(1) by fastsimp
993 lemma split_list_last_propE:
994 assumes "\<exists>x \<in> set xs. P x"
995 obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z"
996 using split_list_last_prop [OF assms] by blast
998 lemma split_list_last_prop_iff:
999 "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
1000 (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
1001 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)
1003 lemma finite_list: "finite A ==> EX xs. set xs = A"
1004 by (erule finite_induct)
1005 (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))
1007 lemma card_length: "card (set xs) \<le> length xs"
1008 by (induct xs) (auto simp add: card_insert_if)
1010 lemma set_minus_filter_out:
1011 "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
1014 subsubsection {* @{text filter} *}
1016 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
1019 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"
1020 by (induct xs) simp_all
1022 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
1025 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
1026 by (induct xs) (auto simp add: le_SucI)
1028 lemma sum_length_filter_compl:
1029 "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
1030 by(induct xs) simp_all
1032 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
1035 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
1038 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
1039 by (induct xs) simp_all
1041 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
1044 apply(cut_tac P=P and xs=xs in length_filter_le)
1049 "filter P (map f xs) = map f (filter (P o f) xs)"
1050 by (induct xs) simp_all
1052 lemma length_filter_map[simp]:
1053 "length (filter P (map f xs)) = length(filter (P o f) xs)"
1054 by (simp add:filter_map)
1056 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
1059 lemma length_filter_less:
1060 "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
1062 case Nil thus ?case by simp
1064 case (Cons x xs) thus ?case
1065 apply (auto split:split_if_asm)
1066 using length_filter_le[of P xs] apply arith
1070 lemma length_filter_conv_card:
1071 "length(filter p xs) = card{i. i < length xs & p(xs!i)}"
1073 case Nil thus ?case by simp
1076 let ?S = "{i. i < length xs & p(xs!i)}"
1077 have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)
1078 show ?case (is "?l = card ?S'")
1081 hence eq: "?S' = insert 0 (Suc ` ?S)"
1082 by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
1083 have "length (filter p (x # xs)) = Suc(card ?S)"
1084 using Cons `p x` by simp
1085 also have "\<dots> = Suc(card(Suc ` ?S))" using fin
1086 by (simp add: card_image inj_Suc)
1087 also have "\<dots> = card ?S'" using eq fin
1088 by (simp add:card_insert_if) (simp add:image_def)
1089 finally show ?thesis .
1092 hence eq: "?S' = Suc ` ?S"
1093 by(auto simp add: image_def split:nat.split elim:lessE)
1094 have "length (filter p (x # xs)) = card ?S"
1095 using Cons `\<not> p x` by simp
1096 also have "\<dots> = card(Suc ` ?S)" using fin
1097 by (simp add: card_image inj_Suc)
1098 also have "\<dots> = card ?S'" using eq fin
1099 by (simp add:card_insert_if)
1100 finally show ?thesis .
1104 lemma Cons_eq_filterD:
1105 "x#xs = filter P ys \<Longrightarrow>
1106 \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
1107 (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
1109 case Nil thus ?case by simp
1112 show ?case (is "\<exists>x. ?Q x")
1118 with Py Cons.prems have "?Q []" by simp
1119 then show ?thesis ..
1121 assume "x \<noteq> y"
1122 with Py Cons.prems show ?thesis by simp
1126 with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
1127 then have "?Q (y#us)" by simp
1128 then show ?thesis ..
1132 lemma filter_eq_ConsD:
1133 "filter P ys = x#xs \<Longrightarrow>
1134 \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
1135 by(rule Cons_eq_filterD) simp
1137 lemma filter_eq_Cons_iff:
1138 "(filter P ys = x#xs) =
1139 (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
1140 by(auto dest:filter_eq_ConsD)
1142 lemma Cons_eq_filter_iff:
1143 "(x#xs = filter P ys) =
1144 (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
1145 by(auto dest:Cons_eq_filterD)
1147 lemma filter_cong[fundef_cong, recdef_cong]:
1148 "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
1150 apply(erule thin_rl)
1151 by (induct ys) simp_all
1154 subsubsection {* List partitioning *}
1156 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
1157 "partition P [] = ([], [])"
1158 | "partition P (x # xs) =
1159 (let (yes, no) = partition P xs
1160 in if P x then (x # yes, no) else (yes, x # no))"
1162 lemma partition_filter1:
1163 "fst (partition P xs) = filter P xs"
1164 by (induct xs) (auto simp add: Let_def split_def)
1166 lemma partition_filter2:
1167 "snd (partition P xs) = filter (Not o P) xs"
1168 by (induct xs) (auto simp add: Let_def split_def)
1171 assumes "partition P xs = (yes, no)"
1172 shows "(\<forall>p \<in> set yes. P p) \<and> (\<forall>p \<in> set no. \<not> P p)"
1174 from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
1176 then show ?thesis by (simp_all add: partition_filter1 partition_filter2)
1179 lemma partition_set:
1180 assumes "partition P xs = (yes, no)"
1181 shows "set yes \<union> set no = set xs"
1183 from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
1185 then show ?thesis by (auto simp add: partition_filter1 partition_filter2)
1189 subsubsection {* @{text concat} *}
1191 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
1194 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
1195 by (induct xss) auto
1197 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
1198 by (induct xss) auto
1200 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
1203 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
1206 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
1209 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
1212 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
1216 subsubsection {* @{text nth} *}
1218 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
1221 lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
1224 declare nth.simps [simp del]
1227 "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
1228 apply (induct xs arbitrary: n, simp)
1229 apply (case_tac n, auto)
1232 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
1235 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
1238 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
1239 apply (induct xs arbitrary: n, simp)
1240 apply (case_tac n, auto)
1243 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
1244 by(cases xs) simp_all
1247 lemma list_eq_iff_nth_eq:
1248 "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
1249 apply(induct xs arbitrary: ys)
1253 apply(simp add:nth_Cons split:nat.split)apply blast
1256 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
1257 apply (induct xs, simp, simp)
1259 apply (metis nat_case_0 nth.simps zero_less_Suc)
1260 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
1261 apply (case_tac i, simp)
1262 apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
1265 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
1266 by(auto simp:set_conv_nth)
1268 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
1269 by (auto simp add: set_conv_nth)
1271 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"
1272 by (auto simp add: set_conv_nth)
1274 lemma all_nth_imp_all_set:
1275 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"
1276 by (auto simp add: set_conv_nth)
1278 lemma all_set_conv_all_nth:
1279 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"
1280 by (auto simp add: set_conv_nth)
1283 "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
1284 proof (induct xs arbitrary: n)
1285 case Nil thus ?case by simp
1288 hence n: "n < Suc (length xs)" by simp
1290 { assume "n < length xs"
1291 with n obtain n' where "length xs - n = Suc n'"
1292 by (cases "length xs - n", auto)
1294 then have "length xs - Suc n = n'" by simp
1296 have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
1299 show ?case by (clarsimp simp add: Cons nth_append)
1302 subsubsection {* @{text list_update} *}
1304 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
1305 by (induct xs arbitrary: i) (auto split: nat.split)
1307 lemma nth_list_update:
1308 "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
1309 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
1311 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
1312 by (simp add: nth_list_update)
1314 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
1315 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
1317 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
1318 by (induct xs arbitrary: i) (simp_all split:nat.splits)
1320 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
1321 apply (induct xs arbitrary: i)
1327 lemma list_update_same_conv:
1328 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
1329 by (induct xs arbitrary: i) (auto split: nat.split)
1331 lemma list_update_append1:
1332 "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
1333 apply (induct xs arbitrary: i, simp)
1334 apply(simp split:nat.split)
1337 lemma list_update_append:
1338 "(xs @ ys) [n:= x] =
1339 (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
1340 by (induct xs arbitrary: n) (auto split:nat.splits)
1342 lemma list_update_length [simp]:
1343 "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
1344 by (induct xs, auto)
1347 "length xs = length ys ==>
1348 (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
1349 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
1351 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
1352 by (induct xs arbitrary: i) (auto split: nat.split)
1354 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
1355 by (blast dest!: set_update_subset_insert [THEN subsetD])
1357 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
1358 by (induct xs arbitrary: n) (auto split:nat.splits)
1360 lemma list_update_overwrite:
1361 "xs [i := x, i := y] = xs [i := y]"
1362 apply (induct xs arbitrary: i)
1368 lemma list_update_swap:
1369 "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
1370 apply (induct xs arbitrary: i i')
1372 apply (case_tac i, case_tac i')
1378 lemma list_update_code [code]:
1380 "(x # xs)[0 := y] = y # xs"
1381 "(x # xs)[Suc i := y] = x # xs[i := y]"
1385 subsubsection {* @{text last} and @{text butlast} *}
1387 lemma last_snoc [simp]: "last (xs @ [x]) = x"
1390 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
1393 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
1394 by(simp add:last.simps)
1396 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
1397 by(simp add:last.simps)
1399 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
1400 by (induct xs) (auto)
1402 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
1403 by(simp add:last_append)
1405 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
1406 by(simp add:last_append)
1408 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
1409 by(rule rev_exhaust[of xs]) simp_all
1411 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
1412 by(cases xs) simp_all
1414 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
1417 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
1418 by (induct xs rule: rev_induct) auto
1420 lemma butlast_append:
1421 "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
1422 by (induct xs arbitrary: ys) auto
1424 lemma append_butlast_last_id [simp]:
1425 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
1428 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
1429 by (induct xs) (auto split: split_if_asm)
1431 lemma in_set_butlast_appendI:
1432 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
1433 by (auto dest: in_set_butlastD simp add: butlast_append)
1435 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
1436 apply (induct xs arbitrary: n)
1438 apply (auto split:nat.split)
1441 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
1442 by(induct xs)(auto simp:neq_Nil_conv)
1444 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
1445 by (induct xs, simp, case_tac xs, simp_all)
1448 subsubsection {* @{text take} and @{text drop} *}
1450 lemma take_0 [simp]: "take 0 xs = []"
1453 lemma drop_0 [simp]: "drop 0 xs = xs"
1456 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
1459 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
1462 declare take_Cons [simp del] and drop_Cons [simp del]
1464 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
1465 by(clarsimp simp add:neq_Nil_conv)
1467 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
1468 by(cases xs, simp_all)
1470 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
1471 by (induct xs arbitrary: n) simp_all
1473 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
1474 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
1476 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
1477 by (cases n, simp, cases xs, auto)
1479 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
1480 by (simp only: drop_tl)
1482 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
1483 apply (induct xs arbitrary: n, simp)
1484 apply(simp add:drop_Cons nth_Cons split:nat.splits)
1487 lemma take_Suc_conv_app_nth:
1488 "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
1489 apply (induct xs arbitrary: i, simp)
1490 apply (case_tac i, auto)
1493 lemma drop_Suc_conv_tl:
1494 "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
1495 apply (induct xs arbitrary: i, simp)
1496 apply (case_tac i, auto)
1499 lemma length_take [simp]: "length (take n xs) = min (length xs) n"
1500 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1502 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
1503 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1505 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
1506 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1508 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
1509 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1511 lemma take_append [simp]:
1512 "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
1513 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1515 lemma drop_append [simp]:
1516 "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
1517 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1519 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
1520 apply (induct m arbitrary: xs n, auto)
1521 apply (case_tac xs, auto)
1522 apply (case_tac n, auto)
1525 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
1526 apply (induct m arbitrary: xs, auto)
1527 apply (case_tac xs, auto)
1530 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
1531 apply (induct m arbitrary: xs n, auto)
1532 apply (case_tac xs, auto)
1535 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
1536 apply(induct xs arbitrary: m n)
1538 apply(simp add: take_Cons drop_Cons split:nat.split)
1541 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
1542 apply (induct n arbitrary: xs, auto)
1543 apply (case_tac xs, auto)
1546 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
1547 apply(induct xs arbitrary: n)
1549 apply(simp add:take_Cons split:nat.split)
1552 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
1553 apply(induct xs arbitrary: n)
1555 apply(simp add:drop_Cons split:nat.split)
1558 lemma take_map: "take n (map f xs) = map f (take n xs)"
1559 apply (induct n arbitrary: xs, auto)
1560 apply (case_tac xs, auto)
1563 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
1564 apply (induct n arbitrary: xs, auto)
1565 apply (case_tac xs, auto)
1568 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
1569 apply (induct xs arbitrary: i, auto)
1570 apply (case_tac i, auto)
1573 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
1574 apply (induct xs arbitrary: i, auto)
1575 apply (case_tac i, auto)
1578 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
1579 apply (induct xs arbitrary: i n, auto)
1580 apply (case_tac n, blast)
1581 apply (case_tac i, auto)
1584 lemma nth_drop [simp]:
1585 "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
1586 apply (induct n arbitrary: xs i, auto)
1587 apply (case_tac xs, auto)
1591 "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
1592 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
1594 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
1595 by (simp add: butlast_conv_take drop_take)
1597 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
1598 by (simp add: butlast_conv_take min_max.inf_absorb1)
1600 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
1601 by (simp add: butlast_conv_take drop_take)
1603 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
1604 by(simp add: hd_conv_nth)
1606 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
1607 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
1609 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
1610 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
1612 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
1613 using set_take_subset by fast
1615 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
1616 using set_drop_subset by fast
1618 lemma append_eq_conv_conj:
1619 "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
1620 apply (induct xs arbitrary: zs, simp, clarsimp)
1621 apply (case_tac zs, auto)
1625 "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
1626 apply (induct xs arbitrary: i, auto)
1627 apply (case_tac i, simp_all)
1630 lemma append_eq_append_conv_if:
1631 "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
1632 (if size xs\<^isub>1 \<le> size ys\<^isub>1
1633 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
1634 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)"
1635 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
1637 apply(case_tac ys\<^isub>1)
1642 "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
1643 apply(induct xs arbitrary: n)
1645 apply(simp add:drop_Cons split:nat.split)
1648 lemma id_take_nth_drop:
1649 "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs"
1651 assume si: "i < length xs"
1652 hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
1654 from si have "take (Suc i) xs = take i xs @ [xs!i]"
1655 apply (rule_tac take_Suc_conv_app_nth) by arith
1656 ultimately show ?thesis by auto
1659 lemma upd_conv_take_nth_drop:
1660 "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
1662 assume i: "i < length xs"
1663 have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"
1664 by(rule arg_cong[OF id_take_nth_drop[OF i]])
1665 also have "\<dots> = take i xs @ a # drop (Suc i) xs"
1666 using i by (simp add: list_update_append)
1667 finally show ?thesis .
1671 "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
1672 apply (induct i arbitrary: xs)
1673 apply (simp add: neq_Nil_conv)
1681 subsubsection {* @{text takeWhile} and @{text dropWhile} *}
1683 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
1686 lemma takeWhile_append1 [simp]:
1687 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"
1690 lemma takeWhile_append2 [simp]:
1691 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
1694 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
1697 lemma dropWhile_append1 [simp]:
1698 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
1701 lemma dropWhile_append2 [simp]:
1702 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
1705 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
1706 by (induct xs) (auto split: split_if_asm)
1708 lemma takeWhile_eq_all_conv[simp]:
1709 "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
1712 lemma dropWhile_eq_Nil_conv[simp]:
1713 "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
1716 lemma dropWhile_eq_Cons_conv:
1717 "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
1720 text{* The following two lemmmas could be generalized to an arbitrary
1723 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1724 takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
1725 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
1727 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1728 dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
1732 apply(subst dropWhile_append2)
1736 lemma takeWhile_not_last:
1737 "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
1744 lemma takeWhile_cong [fundef_cong, recdef_cong]:
1745 "[| l = k; !!x. x : set l ==> P x = Q x |]
1746 ==> takeWhile P l = takeWhile Q k"
1747 by (induct k arbitrary: l) (simp_all)
1749 lemma dropWhile_cong [fundef_cong, recdef_cong]:
1750 "[| l = k; !!x. x : set l ==> P x = Q x |]
1751 ==> dropWhile P l = dropWhile Q k"
1752 by (induct k arbitrary: l, simp_all)
1755 subsubsection {* @{text zip} *}
1757 lemma zip_Nil [simp]: "zip [] ys = []"
1760 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
1763 declare zip_Cons [simp del]
1766 "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
1767 by(auto split:list.split)
1769 lemma length_zip [simp]:
1770 "length (zip xs ys) = min (length xs) (length ys)"
1771 by (induct xs ys rule:list_induct2') auto
1775 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
1776 by (induct xs zs rule:list_induct2') auto
1780 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
1781 by (induct xs ys rule:list_induct2') auto
1783 lemma zip_append [simp]:
1784 "[| length xs = length us; length ys = length vs |] ==>
1785 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
1786 by (simp add: zip_append1)
1789 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
1790 by (induct rule:list_induct2, simp_all)
1793 "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
1794 apply(induct xs arbitrary:ys) apply simp
1800 "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
1801 apply(induct xs arbitrary:ys) apply simp
1806 lemma nth_zip [simp]:
1807 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
1808 apply (induct ys arbitrary: i xs, simp)
1810 apply (simp_all add: nth.simps split: nat.split)
1814 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
1815 by (simp add: set_conv_nth cong: rev_conj_cong)
1818 "length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
1819 by (rule sym, simp add: update_zip)
1821 lemma zip_replicate [simp]:
1822 "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
1823 apply (induct i arbitrary: j, auto)
1824 apply (case_tac j, auto)
1828 "take n (zip xs ys) = zip (take n xs) (take n ys)"
1829 apply (induct n arbitrary: xs ys)
1831 apply (case_tac xs, simp)
1832 apply (case_tac ys, simp_all)
1836 "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
1837 apply (induct n arbitrary: xs ys)
1839 apply (case_tac xs, simp)
1840 apply (case_tac ys, simp_all)
1843 lemma set_zip_leftD:
1844 "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
1845 by (induct xs ys rule:list_induct2') auto
1847 lemma set_zip_rightD:
1848 "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
1849 by (induct xs ys rule:list_induct2') auto
1852 "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
1853 by(blast dest: set_zip_leftD set_zip_rightD)
1855 lemma zip_map_fst_snd:
1856 "zip (map fst zs) (map snd zs) = zs"
1857 by (induct zs) simp_all
1860 "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
1861 by (auto simp add: zip_map_fst_snd)
1864 subsubsection {* @{text list_all2} *}
1866 lemma list_all2_lengthD [intro?]:
1867 "list_all2 P xs ys ==> length xs = length ys"
1868 by (simp add: list_all2_def)
1870 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
1871 by (simp add: list_all2_def)
1873 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
1874 by (simp add: list_all2_def)
1876 lemma list_all2_Cons [iff, code]:
1877 "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
1878 by (auto simp add: list_all2_def)
1880 lemma list_all2_Cons1:
1881 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
1884 lemma list_all2_Cons2:
1885 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
1888 lemma list_all2_rev [iff]:
1889 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
1890 by (simp add: list_all2_def zip_rev cong: conj_cong)
1892 lemma list_all2_rev1:
1893 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
1894 by (subst list_all2_rev [symmetric]) simp
1896 lemma list_all2_append1:
1897 "list_all2 P (xs @ ys) zs =
1898 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
1899 list_all2 P xs us \<and> list_all2 P ys vs)"
1900 apply (simp add: list_all2_def zip_append1)
1902 apply (rule_tac x = "take (length xs) zs" in exI)
1903 apply (rule_tac x = "drop (length xs) zs" in exI)
1904 apply (force split: nat_diff_split simp add: min_def, clarify)
1905 apply (simp add: ball_Un)
1908 lemma list_all2_append2:
1909 "list_all2 P xs (ys @ zs) =
1910 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
1911 list_all2 P us ys \<and> list_all2 P vs zs)"
1912 apply (simp add: list_all2_def zip_append2)
1914 apply (rule_tac x = "take (length ys) xs" in exI)
1915 apply (rule_tac x = "drop (length ys) xs" in exI)
1916 apply (force split: nat_diff_split simp add: min_def, clarify)
1917 apply (simp add: ball_Un)
1920 lemma list_all2_append:
1921 "length xs = length ys \<Longrightarrow>
1922 list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
1923 by (induct rule:list_induct2, simp_all)
1925 lemma list_all2_appendI [intro?, trans]:
1926 "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
1927 by (simp add: list_all2_append list_all2_lengthD)
1929 lemma list_all2_conv_all_nth:
1930 "list_all2 P xs ys =
1931 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
1932 by (force simp add: list_all2_def set_zip)
1934 lemma list_all2_trans:
1935 assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
1936 shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
1937 (is "!!bs cs. PROP ?Q as bs cs")
1939 fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
1940 show "!!cs. PROP ?Q (x # xs) bs cs"
1942 fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"
1943 show "PROP ?Q (x # xs) (y # ys) cs"
1944 by (induct cs) (auto intro: tr I1 I2)
1948 lemma list_all2_all_nthI [intro?]:
1949 "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
1950 by (simp add: list_all2_conv_all_nth)
1953 "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
1954 by (simp add: list_all2_def)
1956 lemma list_all2_nthD:
1957 "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
1958 by (simp add: list_all2_conv_all_nth)
1960 lemma list_all2_nthD2:
1961 "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
1962 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
1964 lemma list_all2_map1:
1965 "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
1966 by (simp add: list_all2_conv_all_nth)
1968 lemma list_all2_map2:
1969 "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
1970 by (auto simp add: list_all2_conv_all_nth)
1972 lemma list_all2_refl [intro?]:
1973 "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
1974 by (simp add: list_all2_conv_all_nth)
1976 lemma list_all2_update_cong:
1977 "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
1978 by (simp add: list_all2_conv_all_nth nth_list_update)
1980 lemma list_all2_update_cong2:
1981 "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
1982 by (simp add: list_all2_lengthD list_all2_update_cong)
1984 lemma list_all2_takeI [simp,intro?]:
1985 "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
1986 apply (induct xs arbitrary: n ys)
1988 apply (clarsimp simp add: list_all2_Cons1)
1993 lemma list_all2_dropI [simp,intro?]:
1994 "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
1995 apply (induct as arbitrary: n bs, simp)
1996 apply (clarsimp simp add: list_all2_Cons1)
1997 apply (case_tac n, simp, simp)
2000 lemma list_all2_mono [intro?]:
2001 "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
2002 apply (induct xs arbitrary: ys, simp)
2003 apply (case_tac ys, auto)
2007 "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
2008 by (induct xs ys rule: list_induct2') auto
2011 subsubsection {* @{text foldl} and @{text foldr} *}
2013 lemma foldl_append [simp]:
2014 "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
2015 by (induct xs arbitrary: a) auto
2017 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
2020 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
2021 by(induct xs) simp_all
2023 text{* For efficient code generation: avoid intermediate list. *}
2024 lemma foldl_map[code unfold]:
2025 "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
2026 by(induct xs arbitrary:a) simp_all
2028 lemma foldl_cong [fundef_cong, recdef_cong]:
2029 "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
2030 ==> foldl f a l = foldl g b k"
2031 by (induct k arbitrary: a b l) simp_all
2033 lemma foldr_cong [fundef_cong, recdef_cong]:
2034 "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]
2035 ==> foldr f l a = foldr g k b"
2036 by (induct k arbitrary: a b l) simp_all
2038 lemma (in semigroup_add) foldl_assoc:
2039 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
2040 by (induct zs arbitrary: y) (simp_all add:add_assoc)
2042 lemma (in monoid_add) foldl_absorb0:
2043 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
2044 by (induct zs) (simp_all add:foldl_assoc)
2047 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
2049 lemma foldl_foldr1_lemma:
2050 "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
2051 by (induct xs arbitrary: a) (auto simp:add_assoc)
2053 corollary foldl_foldr1:
2054 "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
2055 by (simp add:foldl_foldr1_lemma)
2058 text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
2060 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
2063 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
2064 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
2066 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
2067 by (induct xs, auto simp add: foldl_assoc add_commute)
2070 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
2071 difficult to use because it requires an additional transitivity step.
2074 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
2075 by (induct ns arbitrary: n) auto
2077 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
2078 by (force intro: start_le_sum simp add: in_set_conv_decomp)
2080 lemma sum_eq_0_conv [iff]:
2081 "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
2082 by (induct ns arbitrary: m) auto
2084 lemma foldr_invariant:
2085 "\<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)"
2086 by (induct xs, simp_all)
2088 lemma foldl_invariant:
2089 "\<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)"
2090 by (induct xs arbitrary: x, simp_all)
2092 text{* @{const foldl} and @{text concat} *}
2094 lemma foldl_conv_concat:
2095 "foldl (op @) xs xss = xs @ concat xss"
2096 proof (induct xss arbitrary: xs)
2097 case Nil show ?case by simp
2099 interpret monoid_add "[]" "op @" proof qed simp_all
2100 case Cons then show ?case by (simp add: foldl_absorb0)
2103 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
2104 by (simp add: foldl_conv_concat)
2107 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
2109 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
2110 by (induct xs) (simp_all add:add_assoc)
2112 lemma listsum_rev [simp]:
2113 fixes xs :: "'a\<Colon>comm_monoid_add list"
2114 shows "listsum (rev xs) = listsum xs"
2115 by (induct xs) (simp_all add:add_ac)
2117 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
2120 lemma length_concat: "length (concat xss) = listsum (map length xss)"
2121 by (induct xss) simp_all
2123 text{* For efficient code generation ---
2124 @{const listsum} is not tail recursive but @{const foldl} is. *}
2125 lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
2126 by(simp add:listsum_foldr foldl_foldr1)
2129 text{* Some syntactic sugar for summing a function over a list: *}
2132 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
2134 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
2135 syntax (HTML output)
2136 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
2138 translations -- {* Beware of argument permutation! *}
2139 "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
2140 "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
2142 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
2143 by (induct xs) (simp_all add: left_distrib)
2145 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
2146 by (induct xs) (simp_all add: left_distrib)
2148 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
2149 lemma uminus_listsum_map:
2150 fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
2151 shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
2152 by (induct xs) simp_all
2155 subsubsection {* @{text upt} *}
2157 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
2158 -- {* simp does not terminate! *}
2161 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
2162 by (subst upt_rec) simp
2164 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
2165 by(induct j)simp_all
2167 lemma upt_eq_Cons_conv:
2168 "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
2169 apply(induct j arbitrary: x xs)
2171 apply(clarsimp simp add: append_eq_Cons_conv)
2175 lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
2176 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}
2179 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
2180 by (simp add: upt_rec)
2182 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
2183 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
2186 lemma length_upt [simp]: "length [i..<j] = j - i"
2187 by (induct j) (auto simp add: Suc_diff_le)
2189 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
2191 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
2195 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
2196 by(simp add:upt_conv_Cons)
2198 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
2201 by(simp add:upt_Suc_append)
2203 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
2204 apply (induct m arbitrary: i, simp)
2205 apply (subst upt_rec)
2207 apply (subst upt_rec)
2208 apply (simp del: upt.simps)
2211 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
2216 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
2219 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
2220 apply (induct n m arbitrary: i rule: diff_induct)
2221 prefer 3 apply (subst map_Suc_upt[symmetric])
2222 apply (auto simp add: less_diff_conv nth_upt)
2225 lemma nth_take_lemma:
2226 "k <= length xs ==> k <= length ys ==>
2227 (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
2228 apply (atomize, induct k arbitrary: xs ys)
2229 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
2230 txt {* Both lists must be non-empty *}
2231 apply (case_tac xs, simp)
2232 apply (case_tac ys, clarify)
2233 apply (simp (no_asm_use))
2235 txt {* prenexing's needed, not miniscoping *}
2236 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)
2240 lemma nth_equalityI:
2241 "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
2242 apply (frule nth_take_lemma [OF le_refl eq_imp_le])
2243 apply (simp_all add: take_all)
2247 "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
2248 by (rule nth_equalityI, auto)
2250 (* needs nth_equalityI *)
2251 lemma list_all2_antisym:
2252 "\<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>
2253 \<Longrightarrow> xs = ys"
2254 apply (simp add: list_all2_conv_all_nth)
2255 apply (rule nth_equalityI, blast, simp)
2258 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
2259 -- {* The famous take-lemma. *}
2260 apply (drule_tac x = "max (length xs) (length ys)" in spec)
2261 apply (simp add: le_max_iff_disj take_all)
2266 "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
2267 by (cases n) simp_all
2270 "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
2271 by (cases n) simp_all
2273 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
2274 by (cases n) simp_all
2276 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
2277 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
2278 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
2280 declare take_Cons_number_of [simp]
2281 drop_Cons_number_of [simp]
2282 nth_Cons_number_of [simp]
2285 subsubsection {* @{text "distinct"} and @{text remdups} *}
2287 lemma distinct_append [simp]:
2288 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
2291 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
2294 lemma set_remdups [simp]: "set (remdups xs) = set xs"
2295 by (induct xs) (auto simp add: insert_absorb)
2297 lemma distinct_remdups [iff]: "distinct (remdups xs)"
2300 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
2301 by (induct xs, auto)
2303 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
2304 by (metis distinct_remdups distinct_remdups_id)
2306 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
2307 by (metis distinct_remdups finite_list set_remdups)
2309 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
2312 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
2315 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
2318 lemma length_remdups_eq[iff]:
2319 "(length (remdups xs) = length xs) = (remdups xs = xs)"
2322 apply(subgoal_tac "length (remdups xs) <= length xs")
2324 apply(rule length_remdups_leq)
2329 "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
2333 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
2336 lemma distinct_upt[simp]: "distinct[i..<j]"
2339 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
2340 apply(induct xs arbitrary: i)
2344 apply(blast dest:in_set_takeD)
2347 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
2348 apply(induct xs arbitrary: i)
2354 lemma distinct_list_update:
2355 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
2356 shows "distinct (xs[i:=a])"
2357 proof (cases "i < length xs")
2359 with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
2360 apply (drule_tac id_take_nth_drop) by simp
2361 with d True show ?thesis
2362 apply (simp add: upd_conv_take_nth_drop)
2363 apply (drule subst [OF id_take_nth_drop]) apply assumption
2364 apply simp apply (cases "a = xs!i") apply simp by blast
2366 case False with d show ?thesis by auto
2370 text {* It is best to avoid this indexed version of distinct, but
2371 sometimes it is useful. *}
2373 lemma distinct_conv_nth:
2374 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
2375 apply (induct xs, simp, simp)
2376 apply (rule iffI, clarsimp)
2378 apply (case_tac j, simp)
2379 apply (simp add: set_conv_nth)
2381 apply (clarsimp simp add: set_conv_nth, simp)
2384 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
2386 apply (clarsimp simp add: set_conv_nth)
2387 apply (erule_tac x = 0 in allE, simp)
2388 apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
2390 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
2392 apply (erule_tac x = "Suc i" in allE, simp)
2393 apply (erule_tac x = "Suc j" in allE, simp)
2396 lemma nth_eq_iff_index_eq:
2397 "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
2398 by(auto simp: distinct_conv_nth)
2400 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
2403 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
2405 case Nil thus ?case by simp
2409 proof (cases "x \<in> set xs")
2410 case False with Cons show ?thesis by simp
2412 case True with Cons.prems
2413 have "card (set xs) = Suc (length xs)"
2414 by (simp add: card_insert_if split: split_if_asm)
2415 moreover have "card (set xs) \<le> length xs" by (rule card_length)
2416 ultimately have False by simp
2421 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
2422 apply (induct n == "length ws" arbitrary:ws) apply simp
2423 apply(case_tac ws) apply simp
2424 apply (simp split:split_if_asm)
2425 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
2428 lemma length_remdups_concat:
2429 "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
2430 by(simp add: set_concat distinct_card[symmetric])
2433 subsubsection {* @{text remove1} *}
2435 lemma remove1_append:
2436 "remove1 x (xs @ ys) =
2437 (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
2440 lemma in_set_remove1[simp]:
2441 "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
2446 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
2453 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
2460 lemma length_remove1:
2461 "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
2463 apply (auto dest!:length_pos_if_in_set)
2466 lemma remove1_filter_not[simp]:
2467 "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
2470 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
2471 apply(insert set_remove1_subset)
2475 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
2476 by (induct xs) simp_all
2479 subsubsection {* @{text removeAll} *}
2481 lemma removeAll_append[simp]:
2482 "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
2485 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
2488 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
2491 (* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
2492 lemma length_removeAll:
2493 "length(removeAll x xs) = length xs - count x xs"
2496 lemma removeAll_filter_not[simp]:
2497 "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
2501 lemma distinct_remove1_removeAll:
2502 "distinct xs ==> remove1 x xs = removeAll x xs"
2503 by (induct xs) simp_all
2505 lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>
2506 map f (removeAll x xs) = removeAll (f x) (map f xs)"
2507 by (induct xs) (simp_all add:inj_on_def)
2509 lemma map_removeAll_inj: "inj f \<Longrightarrow>
2510 map f (removeAll x xs) = removeAll (f x) (map f xs)"
2511 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
2514 subsubsection {* @{text replicate} *}
2516 lemma length_replicate [simp]: "length (replicate n x) = n"
2519 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
2522 lemma replicate_app_Cons_same:
2523 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
2526 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
2527 apply (induct n, simp)
2528 apply (simp add: replicate_app_Cons_same)
2531 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
2534 text{* Courtesy of Matthias Daum: *}
2535 lemma append_replicate_commute:
2536 "replicate n x @ replicate k x = replicate k x @ replicate n x"
2537 apply (simp add: replicate_add [THEN sym])
2538 apply (simp add: add_commute)
2541 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
2544 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"
2547 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
2548 by (atomize (full), induct n) auto
2550 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
2551 apply (induct n arbitrary: i, simp)
2552 apply (simp add: nth_Cons split: nat.split)
2555 text{* Courtesy of Matthias Daum (2 lemmas): *}
2556 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
2557 apply (case_tac "k \<le> i")
2558 apply (simp add: min_def)
2559 apply (drule not_leE)
2560 apply (simp add: min_def)
2561 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
2563 apply (simp add: replicate_add [symmetric])
2566 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
2567 apply (induct k arbitrary: i)
2576 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
2579 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
2580 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
2582 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
2585 lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
2586 by (simp add: set_replicate_conv_if split: split_if_asm)
2588 lemma replicate_append_same:
2589 "replicate i x @ [x] = x # replicate i x"
2590 by (induct i) simp_all
2592 lemma map_replicate_trivial:
2593 "map (\<lambda>i. x) [0..<i] = replicate i x"
2594 by (induct i) (simp_all add: replicate_append_same)
2597 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
2600 lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"
2603 lemma replicate_eq_replicate[simp]:
2604 "(replicate m x = replicate n y) \<longleftrightarrow> (m=n & (m\<noteq>0 \<longrightarrow> x=y))"
2605 apply(induct m arbitrary: n)
2612 subsubsection{*@{text rotate1} and @{text rotate}*}
2614 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
2615 by(simp add:rotate1_def)
2617 lemma rotate0[simp]: "rotate 0 = id"
2618 by(simp add:rotate_def)
2620 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
2621 by(simp add:rotate_def)
2624 "rotate (m+n) = rotate m o rotate n"
2625 by(simp add:rotate_def funpow_add)
2627 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
2628 by(simp add:rotate_add)
2630 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
2631 by(simp add:rotate_def funpow_swap1)
2633 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
2634 by(cases xs) simp_all
2636 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
2639 apply (simp add:rotate_def)
2642 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
2643 by(simp add:rotate1_def split:list.split)
2645 lemma rotate_drop_take:
2646 "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
2649 apply(simp add:rotate_def)
2650 apply(cases "xs = []")
2652 apply(case_tac "n mod length xs = 0")
2653 apply(simp add:mod_Suc)
2654 apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
2655 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
2656 take_hd_drop linorder_not_le)
2659 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
2660 by(simp add:rotate_drop_take)
2662 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
2663 by(simp add:rotate_drop_take)
2665 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
2666 by(simp add:rotate1_def split:list.split)
2668 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
2669 by (induct n arbitrary: xs) (simp_all add:rotate_def)
2671 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
2672 by(simp add:rotate1_def split:list.split) blast
2674 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
2675 by (induct n) (simp_all add:rotate_def)
2677 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
2678 by(simp add:rotate_drop_take take_map drop_map)
2680 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
2681 by(simp add:rotate1_def split:list.split)
2683 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
2684 by (induct n) (simp_all add:rotate_def)
2686 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
2687 by(simp add:rotate1_def split:list.split)
2689 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
2690 by (induct n) (simp_all add:rotate_def)
2693 "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
2694 apply(simp add:rotate_drop_take rev_drop rev_take)
2695 apply(cases "length xs = 0")
2697 apply(cases "n mod length xs = 0")
2699 apply(simp add:rotate_drop_take rev_drop rev_take)
2702 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
2703 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
2704 apply(subgoal_tac "length xs \<noteq> 0")
2706 using mod_less_divisor[of "length xs" n] by arith
2709 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
2711 lemma sublist_empty [simp]: "sublist xs {} = []"
2712 by (auto simp add: sublist_def)
2714 lemma sublist_nil [simp]: "sublist [] A = []"
2715 by (auto simp add: sublist_def)
2717 lemma length_sublist:
2718 "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
2719 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
2721 lemma sublist_shift_lemma_Suc:
2722 "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
2723 map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
2724 apply(induct xs arbitrary: "is")
2726 apply (case_tac "is")
2731 lemma sublist_shift_lemma:
2732 "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
2733 map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
2734 by (induct xs rule: rev_induct) (simp_all add: add_commute)
2736 lemma sublist_append:
2737 "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
2738 apply (unfold sublist_def)
2739 apply (induct l' rule: rev_induct, simp)
2740 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
2741 apply (simp add: add_commute)
2745 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
2746 apply (induct l rule: rev_induct)
2747 apply (simp add: sublist_def)
2748 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
2751 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
2752 apply(induct xs arbitrary: I)
2753 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
2756 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
2757 by(auto simp add:set_sublist)
2759 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
2760 by(auto simp add:set_sublist)
2762 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
2763 by(auto simp add:set_sublist)
2765 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
2766 by (simp add: sublist_Cons)
2769 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
2770 apply(induct xs arbitrary: I)
2772 apply(auto simp add:sublist_Cons)
2776 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
2777 apply (induct l rule: rev_induct, simp)
2778 apply (simp split: nat_diff_split add: sublist_append)
2781 lemma filter_in_sublist:
2782 "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
2783 proof (induct xs arbitrary: s)
2784 case Nil thus ?case by simp
2787 moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
2788 ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
2792 subsubsection {* @{const splice} *}
2794 lemma splice_Nil2 [simp, code]:
2796 by (cases xs) simp_all
2798 lemma splice_Cons_Cons [simp, code]:
2799 "splice (x#xs) (y#ys) = x # y # splice xs ys"
2802 declare splice.simps(2) [simp del, code del]
2804 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
2805 apply(induct xs arbitrary: ys) apply simp
2811 subsubsection {* Infiniteness *}
2813 lemma finite_maxlen:
2814 "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
2815 proof (induct rule: finite.induct)
2816 case emptyI show ?case by simp
2819 then obtain n where "\<forall>s\<in>M. length s < n" by blast
2820 hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
2824 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
2826 apply(drule finite_maxlen)
2827 apply (metis UNIV_I length_replicate less_not_refl)
2831 subsection {*Sorting*}
2833 text{* Currently it is not shown that @{const sort} returns a
2834 permutation of its input because the nicest proof is via multisets,
2835 which are not yet available. Alternatively one could define a function
2836 that counts the number of occurrences of an element in a list and use
2837 that instead of multisets to state the correctness property. *}
2842 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
2843 apply(induct xs arbitrary: x) apply simp
2844 by simp (blast intro: order_trans)
2846 lemma sorted_append:
2847 "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
2848 by (induct xs) (auto simp add:sorted_Cons)
2850 lemma set_insort: "set(insort x xs) = insert x (set xs)"
2853 lemma set_sort[simp]: "set(sort xs) = set xs"
2854 by (induct xs) (simp_all add:set_insort)
2856 lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
2857 by(induct xs)(auto simp:set_insort)
2859 lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
2860 by(induct xs)(simp_all add:distinct_insort set_sort)
2862 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
2864 apply(auto simp:sorted_Cons set_insort)
2867 theorem sorted_sort[simp]: "sorted (sort xs)"
2868 by (induct xs) (auto simp:sorted_insort)
2870 lemma insort_is_Cons: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
2873 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
2874 by (induct xs, auto simp add: sorted_Cons)
2876 lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
2877 by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
2879 lemma sorted_remdups[simp]:
2880 "sorted l \<Longrightarrow> sorted (remdups l)"
2881 by (induct l) (auto simp: sorted_Cons)
2883 lemma sorted_distinct_set_unique:
2884 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
2887 from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
2888 from assms show ?thesis
2889 proof(induct rule:list_induct2[OF 1])
2890 case 1 show ?case by simp
2892 case 2 thus ?case by (simp add:sorted_Cons)
2893 (metis Diff_insert_absorb antisym insertE insert_iff)
2897 lemma finite_sorted_distinct_unique:
2898 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
2899 apply(drule finite_distinct_list)
2901 apply(rule_tac a="sort xs" in ex1I)
2902 apply (auto simp: sorted_distinct_set_unique)
2906 "sorted xs \<Longrightarrow> sorted (take n xs)"
2907 proof (induct xs arbitrary: n rule: sorted.induct)
2908 case 1 show ?case by simp
2910 case 2 show ?case by (cases n) simp_all
2913 then have "x \<le> y" by simp
2914 show ?case proof (cases n)
2915 case 0 then show ?thesis by simp
2918 with 3 have "sorted (take m (y # xs))" by simp
2919 with Suc `x \<le> y` show ?thesis by (cases m) simp_all
2924 "sorted xs \<Longrightarrow> sorted (drop n xs)"
2925 proof (induct xs arbitrary: n rule: sorted.induct)
2926 case 1 show ?case by simp
2928 case 2 show ?case by (cases n) simp_all
2930 case 3 then show ?case by (cases n) simp_all
2936 lemma sorted_upt[simp]: "sorted[i..<j]"
2937 by (induct j) (simp_all add:sorted_append)
2940 subsubsection {* @{text sorted_list_of_set} *}
2942 text{* This function maps (finite) linearly ordered sets to sorted
2943 lists. Warning: in most cases it is not a good idea to convert from
2944 sets to lists but one should convert in the other direction (via
2952 sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
2953 [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
2955 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
2956 set(sorted_list_of_set A) = A &
2957 sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
2958 apply(simp add:sorted_list_of_set_def)
2960 apply(simp_all add: finite_sorted_distinct_unique)
2963 lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
2964 unfolding sorted_list_of_set_def
2965 apply(subst the_equality[of _ "[]"])
2972 subsubsection {* @{text upto}: the generic interval-list *}
2974 class finite_intvl_succ = linorder +
2975 fixes successor :: "'a \<Rightarrow> 'a"
2976 assumes finite_intvl: "finite{a..b}"
2977 and successor_incr: "a < successor a"
2978 and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
2980 context finite_intvl_succ
2984 upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
2985 "upto i j == sorted_list_of_set {i..j}"
2987 lemma upto[simp]: "set[a..b] = {a..b} & sorted[a..b] & distinct[a..b]"
2988 by(simp add:upto_def finite_intvl)
2990 lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
2991 apply(insert successor_incr[of i])
2992 apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
2993 apply(metis ord_discrete less_le not_le)
2996 lemma sorted_list_of_set_rec: "i \<le> j \<Longrightarrow>
2997 sorted_list_of_set {i..j} = i # sorted_list_of_set {successor i..j}"
2998 apply(simp add:sorted_list_of_set_def upto_def)
2999 apply (rule the1_equality[OF finite_sorted_distinct_unique])
3000 apply (simp add:finite_intvl)
3001 apply(rule the1I2[OF finite_sorted_distinct_unique])
3002 apply (simp add:finite_intvl)
3003 apply (simp add: sorted_Cons insert_intvl Ball_def)
3004 apply (metis successor_incr leD less_imp_le order_trans)
3007 lemma sorted_list_of_set_rec2: "i \<le> j \<Longrightarrow>
3008 sorted_list_of_set {i..successor j} =
3009 sorted_list_of_set {i..j} @ [successor j]"
3010 apply(simp add:sorted_list_of_set_def upto_def)
3011 apply (rule the1_equality[OF finite_sorted_distinct_unique])
3012 apply (simp add:finite_intvl)
3013 apply(rule the1I2[OF finite_sorted_distinct_unique])
3014 apply (simp add:finite_intvl)
3015 apply (simp add: sorted_append Ball_def expand_set_eq)
3017 apply (metis eq_iff leD linear not_leE ord_discrete order_trans successor_incr)
3018 apply (metis leD linear order_trans successor_incr)
3021 lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
3022 by(simp add: upto_def sorted_list_of_set_rec)
3024 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
3025 by(simp add: upto_rec)
3027 lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..successor j] = [i..j] @ [successor j]"
3028 by(simp add: upto_def sorted_list_of_set_rec2)
3032 text{* The integers are an instance of the above class: *}
3034 instantiation int:: finite_intvl_succ
3038 successor_int_def: "successor = (%i\<Colon>int. i+1)"
3041 by intro_classes (simp_all add: successor_int_def)
3045 text{* Now @{term"[i..j::int]"} is defined for integers. *}
3047 hide (open) const successor
3049 lemma upto_rec2_int: "(i::int) \<le> j \<Longrightarrow> [i..j+1] = [i..j] @ [j+1]"
3050 by(rule upto_rec2[where 'a = int, simplified successor_int_def])
3053 subsubsection {* @{text lists}: the list-forming operator over sets *}
3056 lists :: "'a set => 'a list set"
3059 Nil [intro!]: "[]: lists A"
3060 | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
3062 inductive_cases listsE [elim!,noatp]: "x#l : lists A"
3063 inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
3065 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
3066 by (rule predicate1I, erule listsp.induct, blast+)
3068 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
3071 assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
3074 lemmas lists_IntI = listsp_infI [to_set]
3076 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
3077 proof (rule mono_inf [where f=listsp, THEN order_antisym])
3078 show "mono listsp" by (simp add: mono_def listsp_mono)
3079 show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
3082 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
3084 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
3086 lemma append_in_listsp_conv [iff]:
3087 "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
3090 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
3092 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
3093 -- {* eliminate @{text listsp} in favour of @{text set} *}
3096 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
3098 lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
3099 by (rule in_listsp_conv_set [THEN iffD1])
3101 lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
3103 lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
3104 by (rule in_listsp_conv_set [THEN iffD2])
3106 lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
3108 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
3113 subsubsection{* Inductive definition for membership *}
3115 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
3117 elem: "ListMem x (x # xs)"
3118 | insert: "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
3120 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
3122 apply (induct set: ListMem)
3125 apply (auto intro: ListMem.intros)
3130 subsubsection{*Lists as Cartesian products*}
3132 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
3133 @{term A} and tail drawn from @{term Xs}.*}
3136 set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
3137 "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
3138 declare set_Cons_def [code del]
3140 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
3141 by (auto simp add: set_Cons_def)
3143 text{*Yields the set of lists, all of the same length as the argument and
3144 with elements drawn from the corresponding element of the argument.*}
3146 consts listset :: "'a set list \<Rightarrow> 'a list set"
3149 "listset(A#As) = set_Cons A (listset As)"
3152 subsection{*Relations on Lists*}
3154 subsubsection {* Length Lexicographic Ordering *}
3156 text{*These orderings preserve well-foundedness: shorter lists
3157 precede longer lists. These ordering are not used in dictionaries.*}
3159 consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
3160 --{*The lexicographic ordering for lists of the specified length*}
3164 (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
3165 {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
3168 lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
3169 "lex r == \<Union>n. lexn r n"
3170 --{*Holds only between lists of the same length*}
3172 lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
3173 "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
3174 --{*Compares lists by their length and then lexicographically*}
3176 declare lex_def [code del]
3179 lemma wf_lexn: "wf r ==> wf (lexn r n)"
3180 apply (induct n, simp, simp)
3181 apply(rule wf_subset)
3182 prefer 2 apply (rule Int_lower1)
3183 apply(rule wf_prod_fun_image)
3184 prefer 2 apply (rule inj_onI, auto)
3188 "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
3189 by (induct n arbitrary: xs ys) auto
3191 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
3192 apply (unfold lex_def)
3194 apply (blast intro: wf_lexn, clarify)
3195 apply (rename_tac m n)
3196 apply (subgoal_tac "m \<noteq> n")
3197 prefer 2 apply blast
3198 apply (blast dest: lexn_length not_sym)
3203 {(xs,ys). length xs = n \<and> length ys = n \<and>
3204 (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
3205 apply (induct n, simp)
3206 apply (simp add: image_Collect lex_prod_def, safe, blast)
3207 apply (rule_tac x = "ab # xys" in exI, simp)
3208 apply (case_tac xys, simp_all, blast)
3213 {(xs,ys). length xs = length ys \<and>
3214 (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
3215 by (force simp add: lex_def lexn_conv)
3217 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
3218 by (unfold lenlex_def) blast
3221 "lenlex r = {(xs,ys). length xs < length ys |
3222 length xs = length ys \<and> (xs, ys) : lex r}"
3223 by (simp add: lenlex_def diag_def lex_prod_def inv_image_def)
3225 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
3226 by (simp add: lex_conv)
3228 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
3229 by (simp add:lex_conv)
3231 lemma Cons_in_lex [simp]:
3232 "((x # xs, y # ys) : lex r) =
3233 ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
3234 apply (simp add: lex_conv)
3236 prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
3237 apply (case_tac xys, simp, simp)
3242 subsubsection {* Lexicographic Ordering *}
3244 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
3245 This ordering does \emph{not} preserve well-foundedness.
3246 Author: N. Voelker, March 2005. *}
3249 lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set"
3250 "lexord r == {(x,y). \<exists> a v. y = x @ a # v \<or>
3251 (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
3252 declare lexord_def [code del]
3254 lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
3255 by (unfold lexord_def, induct_tac y, auto)
3257 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
3258 by (unfold lexord_def, induct_tac x, auto)
3260 lemma lexord_cons_cons[simp]:
3261 "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
3262 apply (unfold lexord_def, safe, simp_all)
3263 apply (case_tac u, simp, simp)
3264 apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
3265 apply (erule_tac x="b # u" in allE)
3268 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
3270 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
3271 by (induct_tac x, auto)
3273 lemma lexord_append_left_rightI:
3274 "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
3275 by (induct_tac u, auto)
3277 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
3280 lemma lexord_append_leftD:
3281 "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
3282 by (erule rev_mp, induct_tac x, auto)
3284 lemma lexord_take_index_conv:
3285 "((x,y) : lexord r) =
3286 ((length x < length y \<and> take (length x) y = x) \<or>
3287 (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
3288 apply (unfold lexord_def Let_def, clarsimp)
3289 apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
3291 apply (rule_tac x="hd (drop (length x) y)" in exI)
3292 apply (rule_tac x="tl (drop (length x) y)" in exI)
3293 apply (erule subst, simp add: min_def)
3294 apply (rule_tac x ="length u" in exI, simp)
3295 apply (rule_tac x ="take i x" in exI)
3296 apply (rule_tac x ="x ! i" in exI)
3297 apply (rule_tac x ="y ! i" in exI, safe)
3298 apply (rule_tac x="drop (Suc i) x" in exI)
3299 apply (drule sym, simp add: drop_Suc_conv_tl)
3300 apply (rule_tac x="drop (Suc i) y" in exI)
3301 by (simp add: drop_Suc_conv_tl)
3303 -- {* lexord is extension of partial ordering List.lex *}
3304 lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
3305 apply (rule_tac x = y in spec)
3306 apply (induct_tac x, clarsimp)
3307 by (clarify, case_tac x, simp, force)
3309 lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
3313 "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
3314 apply (erule rev_mp)+
3315 apply (rule_tac x = x in spec)
3316 apply (rule_tac x = z in spec)
3317 apply ( induct_tac y, simp, clarify)
3318 apply (case_tac xa, erule ssubst)
3319 apply (erule allE, erule allE) -- {* avoid simp recursion *}
3320 apply (case_tac x, simp, simp)
3321 apply (case_tac x, erule allE, erule allE, simp)
3322 apply (erule_tac x = listb in allE)
3323 apply (erule_tac x = lista in allE, simp)
3324 apply (unfold trans_def)
3327 lemma lexord_transI: "trans r \<Longrightarrow> trans (lexord r)"
3328 by (rule transI, drule lexord_trans, blast)
3330 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"
3331 apply (rule_tac x = y in spec)
3332 apply (induct_tac x, rule allI)
3333 apply (case_tac x, simp, simp)
3334 apply (rule allI, case_tac x, simp, simp)
3338 subsection {* Lexicographic combination of measure functions *}
3340 text {* These are useful for termination proofs *}
3343 "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
3345 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
3346 unfolding measures_def
3349 lemma in_measures[simp]:
3350 "(x, y) \<in> measures [] = False"
3351 "(x, y) \<in> measures (f # fs)
3352 = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"
3353 unfolding measures_def
3356 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
3359 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
3363 subsubsection{*Lifting a Relation on List Elements to the Lists*}
3366 listrel :: "('a * 'a)set => ('a list * 'a list)set"
3367 for r :: "('a * 'a)set"
3369 Nil: "([],[]) \<in> listrel r"
3370 | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
3372 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
3373 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
3374 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
3375 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
3378 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
3380 apply (erule listrel.induct)
3381 apply (blast intro: listrel.intros)+
3384 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
3386 apply (erule listrel.induct, auto)
3389 lemma listrel_refl: "refl A r \<Longrightarrow> refl (lists A) (listrel r)"
3390 apply (simp add: refl_def listrel_subset Ball_def)
3392 apply (induct_tac x)
3393 apply (auto intro: listrel.intros)
3396 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"
3397 apply (auto simp add: sym_def)
3398 apply (erule listrel.induct)
3399 apply (blast intro: listrel.intros)+
3402 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"
3403 apply (simp add: trans_def)
3406 apply (erule listrel.induct)
3407 apply (blast intro: listrel.intros)+
3410 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
3411 by (simp add: equiv_def listrel_refl listrel_sym listrel_trans)
3413 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
3414 by (blast intro: listrel.intros)
3417 "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
3418 by (auto simp add: set_Cons_def intro: listrel.intros)
3421 subsection{*Miscellany*}
3423 subsubsection {* Characters and strings *}
3426 Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
3427 | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
3430 "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
3431 Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
3432 proof (rule UNIV_eq_I)
3433 fix x show "x \<in> ?A" by (cases x) simp_all
3436 instance nibble :: finite
3437 by default (simp add: UNIV_nibble)
3439 datatype char = Char nibble nibble
3440 -- "Note: canonical order of character encoding coincides with standard term ordering"
3443 "UNIV = image (split Char) (UNIV \<times> UNIV)"
3444 proof (rule UNIV_eq_I)
3445 fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
3448 instance char :: finite
3449 by default (simp add: UNIV_char)
3451 lemma size_char [code, simp]:
3452 "size (c::char) = 0" by (cases c) simp
3454 lemma char_size [code, simp]:
3455 "char_size (c::char) = 0" by (cases c) simp
3457 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
3458 "nibble_pair_of_char (Char n m) = (n, m)"
3460 declare nibble_pair_of_char.simps [code del]
3464 val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
3465 val thms = map_product
3466 (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
3469 PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
3470 #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
3474 lemma char_case_nibble_pair [code, code inline]:
3475 "char_case f = split f o nibble_pair_of_char"
3476 by (simp add: expand_fun_eq split: char.split)
3478 lemma char_rec_nibble_pair [code, code inline]:
3479 "char_rec f = split f o nibble_pair_of_char"
3480 unfolding char_case_nibble_pair [symmetric]
3481 by (simp add: expand_fun_eq split: char.split)
3483 types string = "char list"
3486 "_Char" :: "xstr => char" ("CHR _")
3487 "_String" :: "xstr => string" ("_")
3489 setup StringSyntax.setup
3492 subsection {* Size function *}
3494 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
3495 by (rule is_measure_trivial)
3497 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
3498 by (rule is_measure_trivial)
3500 lemma list_size_estimation[termination_simp]:
3501 "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
3504 lemma list_size_estimation'[termination_simp]:
3505 "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
3508 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
3511 lemma list_size_pointwise[termination_simp]:
3512 "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
3513 by (induct xs) force+
3515 subsection {* Code generator *}
3517 subsubsection {* Setup *}
3522 fun term_of_list f T = HOLogic.mk_list T o map f;
3525 fun gen_list' aG aT i j = frequency
3529 val (xs, ts) = gen_list' aG aT (i-1) j
3530 in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
3531 (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
3532 and gen_list aG aT i = gen_list' aG aT i i;
3536 val term_of_char = HOLogic.mk_char o ord;
3540 let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
3541 in (chr j, fn () => HOLogic.mk_char j) end;
3544 consts_code "Cons" ("(_ ::/ _)")
3565 open Basic_Code_Thingol;
3567 fun implode_list (nil', cons') t =
3569 fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
3573 | dest_cons _ = NONE;
3574 val (ts, t') = Code_Thingol.unfoldr dest_cons t;
3576 of IConst (c, _) => if c = nil' then SOME ts else NONE
3580 fun decode_char nibbles' (IConst (c1, _), IConst (c2, _)) =
3582 fun idx c = find_index (curry (op =) c) nibbles';
3583 fun decode ~1 _ = NONE
3584 | decode _ ~1 = NONE
3585 | decode n m = SOME (chr (n * 16 + m));
3586 in decode (idx c1) (idx c2) end
3587 | decode_char _ _ = NONE;
3589 fun implode_string (char', nibbles') mk_char mk_string ts =
3591 fun implode_char (IConst (c, _) `$ t1 `$ t2) =
3592 if c = char' then decode_char nibbles' (t1, t2) else NONE
3593 | implode_char _ = NONE;
3594 val ts' = map implode_char ts;
3595 in if forall is_some ts'
3596 then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
3600 fun list_names naming = pairself (the o Code_Thingol.lookup_const naming)
3601 (@{const_name Nil}, @{const_name Cons});
3602 fun char_name naming = (the o Code_Thingol.lookup_const naming)
3604 fun nibble_names naming = map (the o Code_Thingol.lookup_const naming)
3605 [@{const_name Nibble0}, @{const_name Nibble1},
3606 @{const_name Nibble2}, @{const_name Nibble3},
3607 @{const_name Nibble4}, @{const_name Nibble5},
3608 @{const_name Nibble6}, @{const_name Nibble7},
3609 @{const_name Nibble8}, @{const_name Nibble9},
3610 @{const_name NibbleA}, @{const_name NibbleB},
3611 @{const_name NibbleC}, @{const_name NibbleD},
3612 @{const_name NibbleE}, @{const_name NibbleF}];
3614 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
3615 Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
3616 pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
3617 Code_Printer.str target_cons,
3618 pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
3621 fun pretty_list literals =
3623 val mk_list = Code_Printer.literal_list literals;
3624 fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
3625 case Option.map (cons t1) (implode_list (list_names naming) t2)
3626 of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
3627 | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
3630 fun pretty_list_string literals =
3632 val mk_list = Code_Printer.literal_list literals;
3633 val mk_char = Code_Printer.literal_char literals;
3634 val mk_string = Code_Printer.literal_string literals;
3635 fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
3636 case Option.map (cons t1) (implode_list (list_names naming) t2)
3637 of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
3639 | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
3640 | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
3643 fun pretty_char literals =
3645 val mk_char = Code_Printer.literal_char literals;
3646 fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
3647 case decode_char (nibble_names naming) (t1, t2)
3648 of SOME c => (Code_Printer.str o mk_char) c
3649 | NONE => Code_Printer.nerror thm "Illegal character expression";
3652 fun pretty_message literals =
3654 val mk_char = Code_Printer.literal_char literals;
3655 val mk_string = Code_Printer.literal_string literals;
3656 fun pretty _ naming thm _ _ [(t, _)] =
3657 case implode_list (list_names naming) t
3658 of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
3660 | NONE => Code_Printer.nerror thm "Illegal message expression")
3661 | NONE => Code_Printer.nerror thm "Illegal message expression";
3666 fun add_literal_list target thy =
3668 val pr = pretty_list (Code_Target.the_literals thy target);
3671 |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
3674 fun add_literal_list_string target thy =
3676 val pr = pretty_list_string (Code_Target.the_literals thy target);
3679 |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
3682 fun add_literal_char target thy =
3684 val pr = pretty_char (Code_Target.the_literals thy target);
3687 |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
3690 fun add_literal_message str target thy =
3692 val pr = pretty_message (Code_Target.the_literals thy target);
3695 |> Code_Target.add_syntax_const target str (SOME pr)
3702 fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
3705 code_instance list :: eq
3708 code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
3709 (Haskell infixl 4 "==")
3714 fun list_codegen thy defs dep thyname b t gr =
3716 val ts = HOLogic.dest_list t;
3717 val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
3719 val (ps, gr'') = fold_map
3720 (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
3721 in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
3723 fun char_codegen thy defs dep thyname b t gr =
3725 val i = HOLogic.dest_char t;
3726 val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
3728 in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
3729 end handle TERM _ => NONE;
3732 Codegen.add_codegen "list_codegen" list_codegen
3733 #> Codegen.add_codegen "char_codegen" char_codegen
3738 subsubsection {* Generation of efficient code *}
3741 member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
3743 "x mem [] \<longleftrightarrow> False"
3744 | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
3747 null:: "'a list \<Rightarrow> bool"
3750 | "null (x#xs) = False"
3753 list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
3755 "list_inter [] bs = []"
3756 | "list_inter (a#as) bs =
3757 (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
3760 list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
3762 "list_all P [] = True"
3763 | "list_all P (x#xs) = (P x \<and> list_all P xs)"
3766 list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
3768 "list_ex P [] = False"
3769 | "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
3772 filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
3774 "filtermap f [] = []"
3775 | "filtermap f (x#xs) =
3776 (case f x of None \<Rightarrow> filtermap f xs
3777 | Some y \<Rightarrow> y # filtermap f xs)"
3780 map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
3782 "map_filter f P [] = []"
3783 | "map_filter f P (x#xs) =
3784 (if P x then f x # map_filter f P xs else map_filter f P xs)"
3787 length_unique :: "'a list \<Rightarrow> nat"
3789 "length_unique [] = 0"
3790 | "length_unique (x#xs) =
3791 (if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
3794 Only use @{text mem} for generating executable code. Otherwise use
3795 @{prop "x : set xs"} instead --- it is much easier to reason about.
3796 The same is true for @{const list_all} and @{const list_ex}: write
3797 @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
3798 quantifiers are aleady known to the automatic provers. In fact, the
3799 declarations in the code subsection make sure that @{text "\<in>"},
3800 @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} are implemented
3803 Efficient emptyness check is implemented by @{const null}.
3805 The functions @{const filtermap} and @{const map_filter} are just
3806 there to generate efficient code. Do not use
3807 them for modelling and proving.
3810 lemma rev_foldl_cons [code]:
3811 "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
3813 case Nil then show ?case by simp
3818 have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
3819 = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
3820 by (induct xs arbitrary: ys) auto
3823 show ?case by (induct xs) (auto simp add: Cons aux)
3826 lemma mem_iff [code post]:
3827 "x mem xs \<longleftrightarrow> x \<in> set xs"
3830 lemmas in_set_code [code unfold] = mem_iff [symmetric]
3832 lemma empty_null [code inline]:
3833 "xs = [] \<longleftrightarrow> null xs"
3834 by (cases xs) simp_all
3836 lemmas null_empty [code post] =
3837 empty_null [symmetric]
3839 lemma list_inter_conv:
3840 "set (list_inter xs ys) = set xs \<inter> set ys"
3843 lemma list_all_iff [code post]:
3844 "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
3847 lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
3849 lemma list_all_append [simp]:
3850 "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
3853 lemma list_all_rev [simp]:
3854 "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
3855 by (simp add: list_all_iff)
3857 lemma list_all_length:
3858 "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
3859 unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
3861 lemma list_ex_iff [code post]:
3862 "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
3863 by (induct xs) simp_all
3865 lemmas list_bex_code [code unfold] =
3866 list_ex_iff [symmetric]
3868 lemma list_ex_length:
3869 "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
3870 unfolding list_ex_iff set_conv_nth by auto
3872 lemma filtermap_conv:
3873 "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
3874 by (induct xs) (simp_all split: option.split)
3876 lemma map_filter_conv [simp]:
3877 "map_filter f P xs = map f (filter P xs)"
3880 lemma length_remdups_length_unique [code inline]:
3881 "length (remdups xs) = length_unique xs"
3882 by (induct xs) simp_all
3884 hide (open) const length_unique
3887 text {* Code for bounded quantification and summation over nats. *}
3889 lemma atMost_upto [code unfold]:
3890 "{..n} = set [0..<Suc n]"
3893 lemma atLeast_upt [code unfold]:
3894 "{..<n} = set [0..<n]"
3897 lemma greaterThanLessThan_upt [code unfold]:
3898 "{n<..<m} = set [Suc n..<m]"
3901 lemma atLeastLessThan_upt [code unfold]:
3902 "{n..<m} = set [n..<m]"
3905 lemma greaterThanAtMost_upt [code unfold]:
3906 "{n<..m} = set [Suc n..<Suc m]"
3909 lemma atLeastAtMost_upt [code unfold]:
3910 "{n..m} = set [n..<Suc m]"
3913 lemma all_nat_less_eq [code unfold]:
3914 "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
3917 lemma ex_nat_less_eq [code unfold]:
3918 "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
3921 lemma all_nat_less [code unfold]:
3922 "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
3925 lemma ex_nat_less [code unfold]:
3926 "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
3929 lemma setsum_set_distinct_conv_listsum:
3930 "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
3931 by (induct xs) simp_all
3933 lemma setsum_set_upt_conv_listsum [code unfold]:
3934 "setsum f (set [m..<n]) = listsum (map f [m..<n])"
3935 by (rule setsum_set_distinct_conv_listsum) simp
3938 text {* Code for summation over ints. *}
3940 lemma greaterThanLessThan_upto [code unfold]:
3941 "{i<..<j::int} = set [i+1..j - 1]"
3944 lemma atLeastLessThan_upto [code unfold]:
3945 "{i..<j::int} = set [i..j - 1]"
3948 lemma greaterThanAtMost_upto [code unfold]:
3949 "{i<..j::int} = set [i+1..j]"
3952 lemma atLeastAtMost_upto [code unfold]:
3953 "{i..j::int} = set [i..j]"
3956 lemma setsum_set_upto_conv_listsum [code unfold]:
3957 "setsum f (set [i..j::int]) = listsum (map f [i..j])"
3958 by (rule setsum_set_distinct_conv_listsum) simp