6 header {* The datatype of finite lists *}
9 imports Plain Relation_Power Presburger Recdef ATP_Linkup
10 uses "Tools/string_syntax.ML"
15 | Cons 'a "'a list" (infixr "#" 65)
17 subsection{*Basic list processing functions*}
20 filter:: "('a => bool) => 'a list => 'a list"
21 concat:: "'a list list => 'a list"
22 foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
23 foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
25 tl:: "'a list => 'a list"
26 last:: "'a list => 'a"
27 butlast :: "'a list => 'a list"
28 set :: "'a list => 'a set"
29 map :: "('a=>'b) => ('a list => 'b list)"
30 listsum :: "'a list => 'a::monoid_add"
31 nth :: "'a list => nat => 'a" (infixl "!" 100)
32 list_update :: "'a list => nat => 'a => 'a list"
33 take:: "nat => 'a list => 'a list"
34 drop:: "nat => 'a list => 'a list"
35 takeWhile :: "('a => bool) => 'a list => 'a list"
36 dropWhile :: "('a => bool) => 'a list => 'a list"
37 rev :: "'a list => 'a list"
38 zip :: "'a list => 'b list => ('a * 'b) list"
39 upt :: "nat => nat => nat list" ("(1[_..</_'])")
40 remdups :: "'a list => 'a list"
41 remove1 :: "'a => 'a list => 'a list"
42 removeAll :: "'a => 'a list => 'a list"
43 "distinct":: "'a list => bool"
44 replicate :: "nat => 'a => 'a list"
45 splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
48 nonterminals lupdbinds lupdbind
51 -- {* list Enumeration *}
52 "@list" :: "args => 'a list" ("[(_)]")
54 -- {* Special syntax for filter *}
55 "@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
58 "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")
59 "" :: "lupdbind => lupdbinds" ("_")
60 "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")
61 "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900)
66 "[x<-xs . P]"== "filter (%x. P) xs"
68 "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
69 "xs[i:=x]" == "list_update xs i x"
73 "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
75 "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
79 Function @{text size} is overloaded for all datatypes. Users may
80 refer to the list version as @{text length}. *}
83 length :: "'a list => nat" where
94 "last(x#xs) = (if xs=[] then x else last xs)"
98 "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
102 "set (x#xs) = insert x (set xs)"
106 "map f (x#xs) = f(x)#map f xs"
109 append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
111 append_Nil:"[] @ ys = ys"
112 | append_Cons: "(x#xs) @ ys = x # xs @ ys"
116 "rev(x#xs) = rev(xs) @ [x]"
120 "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
123 foldl_Nil:"foldl f a [] = a"
124 foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
128 "foldr f (x#xs) a = f x (foldr f xs a)"
132 "concat(x#xs) = x @ concat(xs)"
136 "listsum (x # xs) = x + listsum xs"
139 drop_Nil:"drop n [] = []"
140 drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
141 -- {*Warning: simpset does not contain this definition, but separate
142 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
145 take_Nil:"take n [] = []"
146 take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
147 -- {*Warning: simpset does not contain this definition, but separate
148 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
151 nth_Cons:"(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
152 -- {*Warning: simpset does not contain this definition, but separate
153 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
157 "(x#xs)[i:=v] = (case i of 0 => v # xs | Suc j => x # xs[j:=v])"
160 "takeWhile P [] = []"
161 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
164 "dropWhile P [] = []"
165 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
169 zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
170 -- {*Warning: simpset does not contain this definition, but separate
171 theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
174 upt_0: "[i..<0] = []"
175 upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
179 "distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
183 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
187 "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
190 "removeAll x [] = []"
191 "removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)"
194 replicate_0: "replicate 0 x = []"
195 replicate_Suc: "replicate (Suc n) x = x # replicate n x"
198 rotate1 :: "'a list \<Rightarrow> 'a list" where
199 "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
202 rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
203 "rotate n = rotate1 ^ n"
206 list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
207 [code func del]: "list_all2 P xs ys =
208 (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
211 sublist :: "'a list => nat set => 'a list" where
212 "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
216 "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
217 -- {*Warning: simpset does not contain the second eqn but a derived one. *}
223 @{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\
224 @{lemma "length [a,b,c] = 3" by simp}\\
225 @{lemma "set [a,b,c] = {a,b,c}" by simp}\\
226 @{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\
227 @{lemma "rev [a,b,c] = [c,b,a]" by simp}\\
228 @{lemma "hd [a,b,c,d] = a" by simp}\\
229 @{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\
230 @{lemma "last [a,b,c,d] = d" by simp}\\
231 @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
232 @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
233 @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
234 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
235 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
236 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
237 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
238 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
239 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
240 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
241 @{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
242 @{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\
243 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\
244 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
245 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
246 @{lemma "distinct [2,0,1::nat]" by simp}\\
247 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
248 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
249 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
250 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
251 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
252 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
253 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
254 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\
255 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\
256 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\
257 @{lemma "listsum [1,2,3::nat] = 6" by simp}
259 \caption{Characteristic examples}
260 \label{fig:Characteristic}
262 Figure~\ref{fig:Characteristic} shows charachteristic examples
263 that should give an intuitive understanding of the above functions.
266 text{* The following simple sort functions are intended for proofs,
267 not for efficient implementations. *}
272 fun sorted :: "'a list \<Rightarrow> bool" where
273 "sorted [] \<longleftrightarrow> True" |
274 "sorted [x] \<longleftrightarrow> True" |
275 "sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
277 primrec insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
278 "insort x [] = [x]" |
279 "insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
281 primrec sort :: "'a list \<Rightarrow> 'a list" where
283 "sort (x#xs) = insort x (sort xs)"
288 subsubsection {* List comprehension *}
290 text{* Input syntax for Haskell-like list comprehension notation.
291 Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
292 the list of all pairs of distinct elements from @{text xs} and @{text ys}.
293 The syntax is as in Haskell, except that @{text"|"} becomes a dot
294 (like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
295 \verb![e| x <- xs, ...]!.
297 The qualifiers after the dot are
299 \item[generators] @{text"p \<leftarrow> xs"},
300 where @{text p} is a pattern and @{text xs} an expression of list type, or
301 \item[guards] @{text"b"}, where @{text b} is a boolean expression.
302 %\item[local bindings] @ {text"let x = e"}.
305 Just like in Haskell, list comprehension is just a shorthand. To avoid
306 misunderstandings, the translation into desugared form is not reversed
307 upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is
308 optmized to @{term"map (%x. e) xs"}.
310 It is easy to write short list comprehensions which stand for complex
311 expressions. During proofs, they may become unreadable (and
312 mangled). In such cases it can be advisable to introduce separate
313 definitions for the list comprehensions in question. *}
316 Proper theorem proving support would be nice. For example, if
317 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
318 produced something like
319 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
322 nonterminals lc_qual lc_quals
325 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __")
326 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
327 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
328 (*"_lc_let" :: "letbinds => lc_qual" ("let _")*)
329 "_lc_end" :: "lc_quals" ("]")
330 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
331 "_lc_abs" :: "'a => 'b list => 'b list"
333 (* These are easier than ML code but cannot express the optimized
334 translation of [e. p<-xs]
336 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
337 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
338 => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
339 "[e. P]" => "if P then [e] else []"
340 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
341 => "if P then (_listcompr e Q Qs) else []"
342 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
343 => "_Let b (_listcompr e Q Qs)"
347 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
349 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
351 parse_translation (advanced) {*
353 val NilC = Syntax.const @{const_name Nil};
354 val ConsC = Syntax.const @{const_name Cons};
355 val mapC = Syntax.const @{const_name map};
356 val concatC = Syntax.const @{const_name concat};
357 val IfC = Syntax.const @{const_name If};
358 fun singl x = ConsC $ x $ NilC;
360 fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
362 val x = Free (Name.variant (add_term_free_names (p$e, [])) "x", dummyT);
363 val e = if opti then singl e else e;
364 val case1 = Syntax.const "_case1" $ p $ e;
365 val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
367 val cs = Syntax.const "_case2" $ case1 $ case2
368 val ft = DatatypeCase.case_tr false DatatypePackage.datatype_of_constr
372 fun abs_tr ctxt (p as Free(s,T)) e opti =
373 let val thy = ProofContext.theory_of ctxt;
374 val s' = Sign.intern_const thy s
375 in if Sign.declared_const thy s'
376 then (pat_tr ctxt p e opti, false)
377 else (lambda p e, true)
379 | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
381 fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] =
382 let val res = case qs of Const("_lc_end",_) => singl e
383 | Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs];
384 in IfC $ b $ res $ NilC end
385 | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] =
386 (case abs_tr ctxt p e true of
387 (f,true) => mapC $ f $ es
388 | (f, false) => concatC $ (mapC $ f $ es))
389 | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] =
390 let val e' = lc_tr ctxt [e,q,qs];
391 in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end
393 in [("_listcompr", lc_tr)] end
398 term "[(x,y,z). x\<leftarrow>xs]"
399 term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
400 term "[(x,y,z). x<a, x>b]"
401 term "[(x,y,z). x\<leftarrow>xs, x>b]"
402 term "[(x,y,z). x<a, x\<leftarrow>xs]"
403 term "[(x,y). Cons True x \<leftarrow> xs]"
404 term "[(x,y,z). Cons x [] \<leftarrow> xs]"
405 term "[(x,y,z). x<a, x>b, x=d]"
406 term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
407 term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
408 term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
409 term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
410 term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
411 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
412 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
413 term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
416 subsubsection {* @{const Nil} and @{const Cons} *}
418 lemma not_Cons_self [simp]:
422 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]
424 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
428 "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
429 by (rule measure_induct [of length]) iprover
432 subsubsection {* @{const length} *}
435 Needs to come before @{text "@"} because of theorem @{text
436 append_eq_append_conv}.
439 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"
442 lemma length_map [simp]: "length (map f xs) = length xs"
445 lemma length_rev [simp]: "length (rev xs) = length xs"
448 lemma length_tl [simp]: "length (tl xs) = length xs - 1"
451 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
454 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])"
457 lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0"
460 lemma length_Suc_conv:
461 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
464 lemma Suc_length_conv:
465 "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
466 apply (induct xs, simp, simp)
470 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"
473 lemma list_induct2 [consumes 1, case_names Nil Cons]:
474 "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>
475 (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys))
476 \<Longrightarrow> P xs ys"
477 proof (induct xs arbitrary: ys)
478 case Nil then show ?case by simp
480 case (Cons x xs ys) then show ?case by (cases ys) simp_all
483 lemma list_induct3 [consumes 2, case_names Nil Cons]:
484 "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow>
485 (\<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))
486 \<Longrightarrow> P xs ys zs"
487 proof (induct xs arbitrary: ys zs)
488 case Nil then show ?case by simp
490 case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)
496 \<And>x xs. P (x#xs) [];
497 \<And>y ys. P [] (y#ys);
498 \<And>x xs y ys. P xs ys \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
499 \<Longrightarrow> P xs ys"
500 by (induct xs arbitrary: ys) (case_tac x, auto)+
502 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
503 by (rule Eq_FalseI) auto
505 simproc_setup list_neq ("(xs::'a list) = ys") = {*
507 Reduces xs=ys to False if xs and ys cannot be of the same length.
508 This is the case if the atomic sublists of one are a submultiset
509 of those of the other list and there are fewer Cons's in one than the other.
514 fun len (Const("List.list.Nil",_)) acc = acc
515 | len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
516 | len (Const("List.append",_) $ xs $ ys) acc = len xs (len ys acc)
517 | len (Const("List.rev",_) $ xs) acc = len xs acc
518 | len (Const("List.map",_) $ _ $ xs) acc = len xs acc
519 | len t (ts,n) = (t::ts,n);
521 fun list_neq _ ss ct =
523 val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
524 val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
527 val Type(_,listT::_) = eqT;
528 val size = HOLogic.size_const listT;
529 val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
530 val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
531 val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
532 (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));
533 in SOME (thm RS @{thm neq_if_length_neq}) end
535 if m < n andalso submultiset (op aconv) (ls,rs) orelse
536 n < m andalso submultiset (op aconv) (rs,ls)
537 then prove_neq() else NONE
543 subsubsection {* @{text "@"} -- append *}
545 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
548 lemma append_Nil2 [simp]: "xs @ [] = xs"
551 interpretation semigroup_append: semigroup_add ["op @"]
552 by unfold_locales simp
553 interpretation monoid_append: monoid_add ["[]" "op @"]
554 by unfold_locales (simp+)
556 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
559 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])"
562 lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"
565 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
568 lemma append_eq_append_conv [simp, noatp]:
569 "length xs = length ys \<or> length us = length vs
570 ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
571 apply (induct xs arbitrary: ys)
572 apply (case_tac ys, simp, force)
573 apply (case_tac ys, force, simp)
576 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
577 (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
578 apply (induct xs arbitrary: ys zs ts)
585 lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"
588 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"
591 lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)"
594 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"
595 using append_same_eq [of _ _ "[]"] by auto
597 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
598 using append_same_eq [of "[]"] by auto
600 lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
603 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
606 lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"
607 by (simp add: hd_append split: list.split)
609 lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"
610 by (simp split: list.split)
612 lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"
613 by (simp add: tl_append split: list.split)
616 lemma Cons_eq_append_conv: "x#xs = ys@zs =
617 (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"
620 lemma append_eq_Cons_conv: "(ys@zs = x#xs) =
621 (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
625 text {* Trivial rules for solving @{text "@"}-equations automatically. *}
627 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
630 lemma Cons_eq_appendI:
631 "[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"
634 lemma append_eq_appendI:
635 "[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"
640 Simplification procedure for all list equalities.
641 Currently only tries to rearrange @{text "@"} to see if
642 - both lists end in a singleton list,
643 - or both lists end in the same list.
649 fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
650 (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
651 | last (Const("List.append",_) $ _ $ ys) = last ys
654 fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
657 fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
658 (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
659 | butlast ((app as Const("List.append",_) $ xs) $ ys) = app $ butlast ys
660 | butlast xs = Const("List.list.Nil",fastype_of xs);
662 val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
663 @{thm append_Nil}, @{thm append_Cons}];
665 fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
667 val lastl = last lhs and lastr = last rhs;
670 val lhs1 = butlast lhs and rhs1 = butlast rhs;
671 val Type(_,listT::_) = eqT
672 val appT = [listT,listT] ---> listT
673 val app = Const("List.append",appT)
674 val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
675 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
676 val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
677 (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
678 in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
681 if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
682 else if lastl aconv lastr then rearr @{thm append_same_eq}
688 val list_eq_simproc =
689 Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
693 Addsimprocs [list_eq_simproc];
697 subsubsection {* @{text map} *}
699 lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
700 by (induct xs) simp_all
702 lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)"
703 by (rule ext, induct_tac xs) auto
705 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"
708 lemma map_compose: "map (f o g) xs = map f (map g xs)"
709 by (induct xs) (auto simp add: o_def)
711 lemma rev_map: "rev (map f xs) = map f (rev xs)"
714 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
717 lemma map_cong [fundef_cong, recdef_cong]:
718 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
719 -- {* a congruence rule for @{text map} *}
722 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
725 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
728 lemma map_eq_Cons_conv:
729 "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
732 lemma Cons_eq_map_conv:
733 "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
736 lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]
737 lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]
738 declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!]
741 "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
742 by(induct ys, auto simp add: Cons_eq_map_conv)
744 lemma map_eq_imp_length_eq:
745 assumes "map f xs = map f ys"
746 shows "length xs = length ys"
747 using assms proof (induct ys arbitrary: xs)
748 case Nil then show ?case by simp
750 case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
751 from Cons xs have "map f zs = map f ys" by simp
752 moreover with Cons have "length zs = length ys" by blast
753 with xs show ?case by simp
757 "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
759 apply(frule map_eq_imp_length_eq)
761 apply(induct rule:list_induct2)
764 apply (blast intro:sym)
767 lemma inj_on_map_eq_map:
768 "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
769 by(blast dest:map_inj_on)
772 "map f xs = map f ys ==> inj f ==> xs = ys"
773 by (induct ys arbitrary: xs) (auto dest!:injD)
775 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
776 by(blast dest:map_injective)
778 lemma inj_mapI: "inj f ==> inj (map f)"
779 by (iprover dest: map_injective injD intro: inj_onI)
781 lemma inj_mapD: "inj (map f) ==> inj f"
782 apply (unfold inj_on_def, clarify)
783 apply (erule_tac x = "[x]" in ballE)
784 apply (erule_tac x = "[y]" in ballE, simp, blast)
788 lemma inj_map[iff]: "inj (map f) = inj f"
789 by (blast dest: inj_mapD intro: inj_mapI)
791 lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
793 apply(erule map_inj_on)
794 apply(blast intro:inj_onI dest:inj_onD)
797 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
800 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
803 lemma map_fst_zip[simp]:
804 "length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs"
805 by (induct rule:list_induct2, simp_all)
807 lemma map_snd_zip[simp]:
808 "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
809 by (induct rule:list_induct2, simp_all)
812 subsubsection {* @{text rev} *}
814 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
817 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
820 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
823 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
826 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
829 lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
832 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
835 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
836 apply (induct xs arbitrary: ys, force)
837 apply (case_tac ys, simp, force)
840 lemma inj_on_rev[iff]: "inj_on rev A"
841 by(simp add:inj_on_def)
843 lemma rev_induct [case_names Nil snoc]:
844 "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
845 apply(simplesubst rev_rev_ident[symmetric])
846 apply(rule_tac list = "rev xs" in list.induct, simp_all)
849 lemma rev_exhaust [case_names Nil snoc]:
850 "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"
851 by (induct xs rule: rev_induct) auto
853 lemmas rev_cases = rev_exhaust
855 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
856 by(rule rev_cases[of xs]) auto
859 subsubsection {* @{text set} *}
861 lemma finite_set [iff]: "finite (set xs)"
864 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)"
867 lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs"
870 lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
873 lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs"
876 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
879 lemma set_empty2[iff]: "({} = set xs) = (xs = [])"
882 lemma set_rev [simp]: "set (rev xs) = set xs"
885 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
888 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
891 lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}"
892 apply (induct j, simp_all)
893 apply (erule ssubst, auto)
897 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
899 case Nil thus ?case by simp
901 case Cons thus ?case by (auto intro: Cons_eq_appendI)
904 lemma in_set_conv_decomp: "x \<in> set xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"
905 by (auto elim: split_list)
907 lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
909 case Nil thus ?case by simp
914 assume "x = a" thus ?case using Cons by fastsimp
916 assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
920 lemma in_set_conv_decomp_first:
921 "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
922 by (auto dest!: split_list_first)
924 lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
925 proof (induct xs rule:rev_induct)
926 case Nil thus ?case by simp
931 assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
933 assume "x \<noteq> a" thus ?case using snoc by fastsimp
937 lemma in_set_conv_decomp_last:
938 "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
939 by (auto dest!: split_list_last)
941 lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x"
943 case Nil thus ?case by simp
946 by(simp add:Bex_def)(metis append_Cons append.simps(1))
949 lemma split_list_propE:
950 assumes "\<exists>x \<in> set xs. P x"
951 obtains ys x zs where "xs = ys @ x # zs" and "P x"
952 using split_list_prop [OF assms] by blast
954 lemma split_list_first_prop:
955 "\<exists>x \<in> set xs. P x \<Longrightarrow>
956 \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)"
958 case Nil thus ?case by simp
965 (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
968 hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
969 thus ?thesis using `\<not> P x` Cons(1) by (metis append_Cons set_ConsD)
973 lemma split_list_first_propE:
974 assumes "\<exists>x \<in> set xs. P x"
975 obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y"
976 using split_list_first_prop [OF assms] by blast
978 lemma split_list_first_prop_iff:
979 "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
980 (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))"
981 by (rule, erule split_list_first_prop) auto
983 lemma split_list_last_prop:
984 "\<exists>x \<in> set xs. P x \<Longrightarrow>
985 \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)"
986 proof(induct xs rule:rev_induct)
987 case Nil thus ?case by simp
992 assume "P x" thus ?thesis by (metis emptyE set_empty)
995 hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
996 thus ?thesis using `\<not> P x` snoc(1) by fastsimp
1000 lemma split_list_last_propE:
1001 assumes "\<exists>x \<in> set xs. P x"
1002 obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z"
1003 using split_list_last_prop [OF assms] by blast
1005 lemma split_list_last_prop_iff:
1006 "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
1007 (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
1008 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)
1010 lemma finite_list: "finite A ==> EX xs. set xs = A"
1011 by (erule finite_induct)
1012 (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))
1014 lemma card_length: "card (set xs) \<le> length xs"
1015 by (induct xs) (auto simp add: card_insert_if)
1017 lemma set_minus_filter_out:
1018 "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
1021 subsubsection {* @{text filter} *}
1023 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
1026 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"
1027 by (induct xs) simp_all
1029 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
1032 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
1033 by (induct xs) (auto simp add: le_SucI)
1035 lemma sum_length_filter_compl:
1036 "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
1037 by(induct xs) simp_all
1039 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
1042 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
1045 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
1046 by (induct xs) simp_all
1048 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
1051 apply(cut_tac P=P and xs=xs in length_filter_le)
1056 "filter P (map f xs) = map f (filter (P o f) xs)"
1057 by (induct xs) simp_all
1059 lemma length_filter_map[simp]:
1060 "length (filter P (map f xs)) = length(filter (P o f) xs)"
1061 by (simp add:filter_map)
1063 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
1066 lemma length_filter_less:
1067 "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
1069 case Nil thus ?case by simp
1071 case (Cons x xs) thus ?case
1072 apply (auto split:split_if_asm)
1073 using length_filter_le[of P xs] apply arith
1077 lemma length_filter_conv_card:
1078 "length(filter p xs) = card{i. i < length xs & p(xs!i)}"
1080 case Nil thus ?case by simp
1083 let ?S = "{i. i < length xs & p(xs!i)}"
1084 have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)
1085 show ?case (is "?l = card ?S'")
1088 hence eq: "?S' = insert 0 (Suc ` ?S)"
1089 by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
1090 have "length (filter p (x # xs)) = Suc(card ?S)"
1091 using Cons `p x` by simp
1092 also have "\<dots> = Suc(card(Suc ` ?S))" using fin
1093 by (simp add: card_image inj_Suc)
1094 also have "\<dots> = card ?S'" using eq fin
1095 by (simp add:card_insert_if) (simp add:image_def)
1096 finally show ?thesis .
1099 hence eq: "?S' = Suc ` ?S"
1100 by(auto simp add: image_def split:nat.split elim:lessE)
1101 have "length (filter p (x # xs)) = card ?S"
1102 using Cons `\<not> p x` by simp
1103 also have "\<dots> = card(Suc ` ?S)" using fin
1104 by (simp add: card_image inj_Suc)
1105 also have "\<dots> = card ?S'" using eq fin
1106 by (simp add:card_insert_if)
1107 finally show ?thesis .
1111 lemma Cons_eq_filterD:
1112 "x#xs = filter P ys \<Longrightarrow>
1113 \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
1114 (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
1116 case Nil thus ?case by simp
1119 show ?case (is "\<exists>x. ?Q x")
1125 with Py Cons.prems have "?Q []" by simp
1126 then show ?thesis ..
1128 assume "x \<noteq> y"
1129 with Py Cons.prems show ?thesis by simp
1133 with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
1134 then have "?Q (y#us)" by simp
1135 then show ?thesis ..
1139 lemma filter_eq_ConsD:
1140 "filter P ys = x#xs \<Longrightarrow>
1141 \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
1142 by(rule Cons_eq_filterD) simp
1144 lemma filter_eq_Cons_iff:
1145 "(filter P ys = x#xs) =
1146 (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
1147 by(auto dest:filter_eq_ConsD)
1149 lemma Cons_eq_filter_iff:
1150 "(x#xs = filter P ys) =
1151 (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
1152 by(auto dest:Cons_eq_filterD)
1154 lemma filter_cong[fundef_cong, recdef_cong]:
1155 "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
1157 apply(erule thin_rl)
1158 by (induct ys) simp_all
1161 subsubsection {* List partitioning *}
1163 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
1164 "partition P [] = ([], [])"
1165 | "partition P (x # xs) =
1166 (let (yes, no) = partition P xs
1167 in if P x then (x # yes, no) else (yes, x # no))"
1169 lemma partition_filter1:
1170 "fst (partition P xs) = filter P xs"
1171 by (induct xs) (auto simp add: Let_def split_def)
1173 lemma partition_filter2:
1174 "snd (partition P xs) = filter (Not o P) xs"
1175 by (induct xs) (auto simp add: Let_def split_def)
1178 assumes "partition P xs = (yes, no)"
1179 shows "(\<forall>p \<in> set yes. P p) \<and> (\<forall>p \<in> set no. \<not> P p)"
1181 from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
1183 then show ?thesis by (simp_all add: partition_filter1 partition_filter2)
1186 lemma partition_set:
1187 assumes "partition P xs = (yes, no)"
1188 shows "set yes \<union> set no = set xs"
1190 from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
1192 then show ?thesis by (auto simp add: partition_filter1 partition_filter2)
1196 subsubsection {* @{text concat} *}
1198 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
1201 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
1202 by (induct xss) auto
1204 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
1205 by (induct xss) auto
1207 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
1210 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
1213 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
1216 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
1219 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
1223 subsubsection {* @{text nth} *}
1225 lemma nth_Cons_0 [simp]: "(x # xs)!0 = x"
1228 lemma nth_Cons_Suc [simp]: "(x # xs)!(Suc n) = xs!n"
1231 declare nth.simps [simp del]
1234 "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
1235 apply (induct xs arbitrary: n, simp)
1236 apply (case_tac n, auto)
1239 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
1242 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
1245 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
1246 apply (induct xs arbitrary: n, simp)
1247 apply (case_tac n, auto)
1250 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
1251 by(cases xs) simp_all
1254 lemma list_eq_iff_nth_eq:
1255 "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
1256 apply(induct xs arbitrary: ys)
1260 apply(simp add:nth_Cons split:nat.split)apply blast
1263 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
1264 apply (induct xs, simp, simp)
1266 apply (metis nat_case_0 nth.simps zero_less_Suc)
1267 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
1268 apply (case_tac i, simp)
1269 apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
1272 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
1273 by(auto simp:set_conv_nth)
1275 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
1276 by (auto simp add: set_conv_nth)
1278 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"
1279 by (auto simp add: set_conv_nth)
1281 lemma all_nth_imp_all_set:
1282 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"
1283 by (auto simp add: set_conv_nth)
1285 lemma all_set_conv_all_nth:
1286 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"
1287 by (auto simp add: set_conv_nth)
1290 "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
1291 proof (induct xs arbitrary: n)
1292 case Nil thus ?case by simp
1295 hence n: "n < Suc (length xs)" by simp
1297 { assume "n < length xs"
1298 with n obtain n' where "length xs - n = Suc n'"
1299 by (cases "length xs - n", auto)
1301 then have "length xs - Suc n = n'" by simp
1303 have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
1306 show ?case by (clarsimp simp add: Cons nth_append)
1309 subsubsection {* @{text list_update} *}
1311 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
1312 by (induct xs arbitrary: i) (auto split: nat.split)
1314 lemma nth_list_update:
1315 "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
1316 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
1318 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
1319 by (simp add: nth_list_update)
1321 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
1322 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
1324 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
1325 by (induct xs arbitrary: i) (simp_all split:nat.splits)
1327 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
1328 apply (induct xs arbitrary: i)
1334 lemma list_update_same_conv:
1335 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
1336 by (induct xs arbitrary: i) (auto split: nat.split)
1338 lemma list_update_append1:
1339 "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
1340 apply (induct xs arbitrary: i, simp)
1341 apply(simp split:nat.split)
1344 lemma list_update_append:
1345 "(xs @ ys) [n:= x] =
1346 (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
1347 by (induct xs arbitrary: n) (auto split:nat.splits)
1349 lemma list_update_length [simp]:
1350 "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
1351 by (induct xs, auto)
1354 "length xs = length ys ==>
1355 (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
1356 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
1358 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
1359 by (induct xs arbitrary: i) (auto split: nat.split)
1361 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
1362 by (blast dest!: set_update_subset_insert [THEN subsetD])
1364 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
1365 by (induct xs arbitrary: n) (auto split:nat.splits)
1367 lemma list_update_overwrite:
1368 "xs [i := x, i := y] = xs [i := y]"
1369 apply (induct xs arbitrary: i)
1375 lemma list_update_swap:
1376 "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
1377 apply (induct xs arbitrary: i i')
1379 apply (case_tac i, case_tac i')
1386 subsubsection {* @{text last} and @{text butlast} *}
1388 lemma last_snoc [simp]: "last (xs @ [x]) = x"
1391 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
1394 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
1395 by(simp add:last.simps)
1397 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
1398 by(simp add:last.simps)
1400 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
1401 by (induct xs) (auto)
1403 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
1404 by(simp add:last_append)
1406 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
1407 by(simp add:last_append)
1409 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
1410 by(rule rev_exhaust[of xs]) simp_all
1412 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
1413 by(cases xs) simp_all
1415 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
1418 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
1419 by (induct xs rule: rev_induct) auto
1421 lemma butlast_append:
1422 "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
1423 by (induct xs arbitrary: ys) auto
1425 lemma append_butlast_last_id [simp]:
1426 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
1429 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
1430 by (induct xs) (auto split: split_if_asm)
1432 lemma in_set_butlast_appendI:
1433 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
1434 by (auto dest: in_set_butlastD simp add: butlast_append)
1436 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
1437 apply (induct xs arbitrary: n)
1439 apply (auto split:nat.split)
1442 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
1443 by(induct xs)(auto simp:neq_Nil_conv)
1445 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
1446 by (induct xs, simp, case_tac xs, simp_all)
1449 subsubsection {* @{text take} and @{text drop} *}
1451 lemma take_0 [simp]: "take 0 xs = []"
1454 lemma drop_0 [simp]: "drop 0 xs = xs"
1457 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
1460 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
1463 declare take_Cons [simp del] and drop_Cons [simp del]
1465 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
1466 by(clarsimp simp add:neq_Nil_conv)
1468 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
1469 by(cases xs, simp_all)
1471 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
1472 by (induct xs arbitrary: n) simp_all
1474 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
1475 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
1477 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
1478 by (cases n, simp, cases xs, auto)
1480 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
1481 by (simp only: drop_tl)
1483 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
1484 apply (induct xs arbitrary: n, simp)
1485 apply(simp add:drop_Cons nth_Cons split:nat.splits)
1488 lemma take_Suc_conv_app_nth:
1489 "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
1490 apply (induct xs arbitrary: i, simp)
1491 apply (case_tac i, auto)
1494 lemma drop_Suc_conv_tl:
1495 "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
1496 apply (induct xs arbitrary: i, simp)
1497 apply (case_tac i, auto)
1500 lemma length_take [simp]: "length (take n xs) = min (length xs) n"
1501 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1503 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
1504 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1506 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
1507 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1509 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
1510 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1512 lemma take_append [simp]:
1513 "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
1514 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1516 lemma drop_append [simp]:
1517 "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
1518 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1520 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
1521 apply (induct m arbitrary: xs n, auto)
1522 apply (case_tac xs, auto)
1523 apply (case_tac n, auto)
1526 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
1527 apply (induct m arbitrary: xs, auto)
1528 apply (case_tac xs, auto)
1531 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
1532 apply (induct m arbitrary: xs n, auto)
1533 apply (case_tac xs, auto)
1536 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
1537 apply(induct xs arbitrary: m n)
1539 apply(simp add: take_Cons drop_Cons split:nat.split)
1542 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
1543 apply (induct n arbitrary: xs, auto)
1544 apply (case_tac xs, auto)
1547 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
1548 apply(induct xs arbitrary: n)
1550 apply(simp add:take_Cons split:nat.split)
1553 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
1554 apply(induct xs arbitrary: n)
1556 apply(simp add:drop_Cons split:nat.split)
1559 lemma take_map: "take n (map f xs) = map f (take n xs)"
1560 apply (induct n arbitrary: xs, auto)
1561 apply (case_tac xs, auto)
1564 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
1565 apply (induct n arbitrary: xs, auto)
1566 apply (case_tac xs, auto)
1569 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
1570 apply (induct xs arbitrary: i, auto)
1571 apply (case_tac i, auto)
1574 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
1575 apply (induct xs arbitrary: i, auto)
1576 apply (case_tac i, auto)
1579 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
1580 apply (induct xs arbitrary: i n, auto)
1581 apply (case_tac n, blast)
1582 apply (case_tac i, auto)
1585 lemma nth_drop [simp]:
1586 "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
1587 apply (induct n arbitrary: xs i, auto)
1588 apply (case_tac xs, auto)
1592 "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
1593 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
1595 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
1596 by (simp add: butlast_conv_take drop_take)
1598 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
1599 by (simp add: butlast_conv_take min_max.inf_absorb1)
1601 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
1602 by (simp add: butlast_conv_take drop_take)
1604 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
1605 by(simp add: hd_conv_nth)
1607 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
1608 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
1610 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
1611 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
1613 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
1614 using set_take_subset by fast
1616 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
1617 using set_drop_subset by fast
1619 lemma append_eq_conv_conj:
1620 "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
1621 apply (induct xs arbitrary: zs, simp, clarsimp)
1622 apply (case_tac zs, auto)
1626 "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
1627 apply (induct xs arbitrary: i, auto)
1628 apply (case_tac i, simp_all)
1631 lemma append_eq_append_conv_if:
1632 "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
1633 (if size xs\<^isub>1 \<le> size ys\<^isub>1
1634 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
1635 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)"
1636 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
1638 apply(case_tac ys\<^isub>1)
1643 "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
1644 apply(induct xs arbitrary: n)
1646 apply(simp add:drop_Cons split:nat.split)
1649 lemma id_take_nth_drop:
1650 "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs"
1652 assume si: "i < length xs"
1653 hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
1655 from si have "take (Suc i) xs = take i xs @ [xs!i]"
1656 apply (rule_tac take_Suc_conv_app_nth) by arith
1657 ultimately show ?thesis by auto
1660 lemma upd_conv_take_nth_drop:
1661 "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
1663 assume i: "i < length xs"
1664 have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"
1665 by(rule arg_cong[OF id_take_nth_drop[OF i]])
1666 also have "\<dots> = take i xs @ a # drop (Suc i) xs"
1667 using i by (simp add: list_update_append)
1668 finally show ?thesis .
1672 "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
1673 apply (induct i arbitrary: xs)
1674 apply (simp add: neq_Nil_conv)
1682 subsubsection {* @{text takeWhile} and @{text dropWhile} *}
1684 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
1687 lemma takeWhile_append1 [simp]:
1688 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"
1691 lemma takeWhile_append2 [simp]:
1692 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
1695 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
1698 lemma dropWhile_append1 [simp]:
1699 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
1702 lemma dropWhile_append2 [simp]:
1703 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
1706 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
1707 by (induct xs) (auto split: split_if_asm)
1709 lemma takeWhile_eq_all_conv[simp]:
1710 "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
1713 lemma dropWhile_eq_Nil_conv[simp]:
1714 "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
1717 lemma dropWhile_eq_Cons_conv:
1718 "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
1721 text{* The following two lemmmas could be generalized to an arbitrary
1724 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1725 takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
1726 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
1728 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1729 dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
1733 apply(subst dropWhile_append2)
1737 lemma takeWhile_not_last:
1738 "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
1745 lemma takeWhile_cong [fundef_cong, recdef_cong]:
1746 "[| l = k; !!x. x : set l ==> P x = Q x |]
1747 ==> takeWhile P l = takeWhile Q k"
1748 by (induct k arbitrary: l) (simp_all)
1750 lemma dropWhile_cong [fundef_cong, recdef_cong]:
1751 "[| l = k; !!x. x : set l ==> P x = Q x |]
1752 ==> dropWhile P l = dropWhile Q k"
1753 by (induct k arbitrary: l, simp_all)
1756 subsubsection {* @{text zip} *}
1758 lemma zip_Nil [simp]: "zip [] ys = []"
1761 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
1764 declare zip_Cons [simp del]
1767 "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
1768 by(auto split:list.split)
1770 lemma length_zip [simp]:
1771 "length (zip xs ys) = min (length xs) (length ys)"
1772 by (induct xs ys rule:list_induct2') auto
1776 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
1777 by (induct xs zs rule:list_induct2') auto
1781 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
1782 by (induct xs ys rule:list_induct2') auto
1784 lemma zip_append [simp]:
1785 "[| length xs = length us; length ys = length vs |] ==>
1786 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
1787 by (simp add: zip_append1)
1790 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
1791 by (induct rule:list_induct2, simp_all)
1794 "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
1795 apply(induct xs arbitrary:ys) apply simp
1801 "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
1802 apply(induct xs arbitrary:ys) apply simp
1807 lemma nth_zip [simp]:
1808 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
1809 apply (induct ys arbitrary: i xs, simp)
1811 apply (simp_all add: nth.simps split: nat.split)
1815 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
1816 by (simp add: set_conv_nth cong: rev_conj_cong)
1819 "length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
1820 by (rule sym, simp add: update_zip)
1822 lemma zip_replicate [simp]:
1823 "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
1824 apply (induct i arbitrary: j, auto)
1825 apply (case_tac j, auto)
1829 "take n (zip xs ys) = zip (take n xs) (take n ys)"
1830 apply (induct n arbitrary: xs ys)
1832 apply (case_tac xs, simp)
1833 apply (case_tac ys, simp_all)
1837 "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
1838 apply (induct n arbitrary: xs ys)
1840 apply (case_tac xs, simp)
1841 apply (case_tac ys, simp_all)
1844 lemma set_zip_leftD:
1845 "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
1846 by (induct xs ys rule:list_induct2') auto
1848 lemma set_zip_rightD:
1849 "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
1850 by (induct xs ys rule:list_induct2') auto
1853 "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
1854 by(blast dest: set_zip_leftD set_zip_rightD)
1856 subsubsection {* @{text list_all2} *}
1858 lemma list_all2_lengthD [intro?]:
1859 "list_all2 P xs ys ==> length xs = length ys"
1860 by (simp add: list_all2_def)
1862 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
1863 by (simp add: list_all2_def)
1865 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
1866 by (simp add: list_all2_def)
1868 lemma list_all2_Cons [iff, code]:
1869 "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
1870 by (auto simp add: list_all2_def)
1872 lemma list_all2_Cons1:
1873 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
1876 lemma list_all2_Cons2:
1877 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
1880 lemma list_all2_rev [iff]:
1881 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
1882 by (simp add: list_all2_def zip_rev cong: conj_cong)
1884 lemma list_all2_rev1:
1885 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
1886 by (subst list_all2_rev [symmetric]) simp
1888 lemma list_all2_append1:
1889 "list_all2 P (xs @ ys) zs =
1890 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
1891 list_all2 P xs us \<and> list_all2 P ys vs)"
1892 apply (simp add: list_all2_def zip_append1)
1894 apply (rule_tac x = "take (length xs) zs" in exI)
1895 apply (rule_tac x = "drop (length xs) zs" in exI)
1896 apply (force split: nat_diff_split simp add: min_def, clarify)
1897 apply (simp add: ball_Un)
1900 lemma list_all2_append2:
1901 "list_all2 P xs (ys @ zs) =
1902 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
1903 list_all2 P us ys \<and> list_all2 P vs zs)"
1904 apply (simp add: list_all2_def zip_append2)
1906 apply (rule_tac x = "take (length ys) xs" in exI)
1907 apply (rule_tac x = "drop (length ys) xs" in exI)
1908 apply (force split: nat_diff_split simp add: min_def, clarify)
1909 apply (simp add: ball_Un)
1912 lemma list_all2_append:
1913 "length xs = length ys \<Longrightarrow>
1914 list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
1915 by (induct rule:list_induct2, simp_all)
1917 lemma list_all2_appendI [intro?, trans]:
1918 "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
1919 by (simp add: list_all2_append list_all2_lengthD)
1921 lemma list_all2_conv_all_nth:
1922 "list_all2 P xs ys =
1923 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
1924 by (force simp add: list_all2_def set_zip)
1926 lemma list_all2_trans:
1927 assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
1928 shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
1929 (is "!!bs cs. PROP ?Q as bs cs")
1931 fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
1932 show "!!cs. PROP ?Q (x # xs) bs cs"
1934 fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"
1935 show "PROP ?Q (x # xs) (y # ys) cs"
1936 by (induct cs) (auto intro: tr I1 I2)
1940 lemma list_all2_all_nthI [intro?]:
1941 "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
1942 by (simp add: list_all2_conv_all_nth)
1945 "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
1946 by (simp add: list_all2_def)
1948 lemma list_all2_nthD:
1949 "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
1950 by (simp add: list_all2_conv_all_nth)
1952 lemma list_all2_nthD2:
1953 "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
1954 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
1956 lemma list_all2_map1:
1957 "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
1958 by (simp add: list_all2_conv_all_nth)
1960 lemma list_all2_map2:
1961 "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
1962 by (auto simp add: list_all2_conv_all_nth)
1964 lemma list_all2_refl [intro?]:
1965 "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
1966 by (simp add: list_all2_conv_all_nth)
1968 lemma list_all2_update_cong:
1969 "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
1970 by (simp add: list_all2_conv_all_nth nth_list_update)
1972 lemma list_all2_update_cong2:
1973 "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
1974 by (simp add: list_all2_lengthD list_all2_update_cong)
1976 lemma list_all2_takeI [simp,intro?]:
1977 "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
1978 apply (induct xs arbitrary: n ys)
1980 apply (clarsimp simp add: list_all2_Cons1)
1985 lemma list_all2_dropI [simp,intro?]:
1986 "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
1987 apply (induct as arbitrary: n bs, simp)
1988 apply (clarsimp simp add: list_all2_Cons1)
1989 apply (case_tac n, simp, simp)
1992 lemma list_all2_mono [intro?]:
1993 "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
1994 apply (induct xs arbitrary: ys, simp)
1995 apply (case_tac ys, auto)
1999 "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
2000 by (induct xs ys rule: list_induct2') auto
2003 subsubsection {* @{text foldl} and @{text foldr} *}
2005 lemma foldl_append [simp]:
2006 "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
2007 by (induct xs arbitrary: a) auto
2009 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
2012 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
2013 by(induct xs) simp_all
2015 text{* For efficient code generation: avoid intermediate list. *}
2016 lemma foldl_map[code unfold]:
2017 "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
2018 by(induct xs arbitrary:a) simp_all
2020 lemma foldl_cong [fundef_cong, recdef_cong]:
2021 "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
2022 ==> foldl f a l = foldl g b k"
2023 by (induct k arbitrary: a b l) simp_all
2025 lemma foldr_cong [fundef_cong, recdef_cong]:
2026 "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]
2027 ==> foldr f l a = foldr g k b"
2028 by (induct k arbitrary: a b l) simp_all
2030 lemma (in semigroup_add) foldl_assoc:
2031 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
2032 by (induct zs arbitrary: y) (simp_all add:add_assoc)
2034 lemma (in monoid_add) foldl_absorb0:
2035 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
2036 by (induct zs) (simp_all add:foldl_assoc)
2039 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
2041 lemma foldl_foldr1_lemma:
2042 "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
2043 by (induct xs arbitrary: a) (auto simp:add_assoc)
2045 corollary foldl_foldr1:
2046 "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
2047 by (simp add:foldl_foldr1_lemma)
2050 text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
2052 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
2055 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
2056 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
2058 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
2059 by (induct xs, auto simp add: foldl_assoc add_commute)
2062 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
2063 difficult to use because it requires an additional transitivity step.
2066 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
2067 by (induct ns arbitrary: n) auto
2069 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
2070 by (force intro: start_le_sum simp add: in_set_conv_decomp)
2072 lemma sum_eq_0_conv [iff]:
2073 "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
2074 by (induct ns arbitrary: m) auto
2076 lemma foldr_invariant:
2077 "\<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)"
2078 by (induct xs, simp_all)
2080 lemma foldl_invariant:
2081 "\<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)"
2082 by (induct xs arbitrary: x, simp_all)
2084 text{* @{const foldl} and @{text concat} *}
2086 lemma concat_conv_foldl: "concat xss = foldl op@ [] xss"
2087 by (induct xss) (simp_all add:monoid_append.foldl_absorb0)
2089 lemma foldl_conv_concat:
2090 "foldl (op @) xs xxs = xs @ (concat xxs)"
2091 by(simp add:concat_conv_foldl monoid_append.foldl_absorb0)
2093 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
2095 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
2096 by (induct xs) (simp_all add:add_assoc)
2098 lemma listsum_rev [simp]:
2099 fixes xs :: "'a\<Colon>comm_monoid_add list"
2100 shows "listsum (rev xs) = listsum xs"
2101 by (induct xs) (simp_all add:add_ac)
2103 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
2106 lemma length_concat: "length (concat xss) = listsum (map length xss)"
2107 by (induct xss) simp_all
2109 text{* For efficient code generation ---
2110 @{const listsum} is not tail recursive but @{const foldl} is. *}
2111 lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
2112 by(simp add:listsum_foldr foldl_foldr1)
2115 text{* Some syntactic sugar for summing a function over a list: *}
2118 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
2120 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
2121 syntax (HTML output)
2122 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
2124 translations -- {* Beware of argument permutation! *}
2125 "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
2126 "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
2128 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
2129 by (induct xs) (simp_all add: left_distrib)
2131 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
2132 by (induct xs) (simp_all add: left_distrib)
2134 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
2135 lemma uminus_listsum_map:
2136 fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
2137 shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
2138 by (induct xs) simp_all
2141 subsubsection {* @{text upt} *}
2143 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
2144 -- {* simp does not terminate! *}
2147 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
2148 by (subst upt_rec) simp
2150 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
2151 by(induct j)simp_all
2153 lemma upt_eq_Cons_conv:
2154 "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
2155 apply(induct j arbitrary: x xs)
2157 apply(clarsimp simp add: append_eq_Cons_conv)
2161 lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
2162 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}
2165 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
2166 by (simp add: upt_rec)
2168 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
2169 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
2172 lemma length_upt [simp]: "length [i..<j] = j - i"
2173 by (induct j) (auto simp add: Suc_diff_le)
2175 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
2177 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
2181 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
2182 by(simp add:upt_conv_Cons)
2184 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
2187 by(simp add:upt_Suc_append)
2189 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
2190 apply (induct m arbitrary: i, simp)
2191 apply (subst upt_rec)
2193 apply (subst upt_rec)
2194 apply (simp del: upt.simps)
2197 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
2202 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
2205 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
2206 apply (induct n m arbitrary: i rule: diff_induct)
2207 prefer 3 apply (subst map_Suc_upt[symmetric])
2208 apply (auto simp add: less_diff_conv nth_upt)
2211 lemma nth_take_lemma:
2212 "k <= length xs ==> k <= length ys ==>
2213 (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
2214 apply (atomize, induct k arbitrary: xs ys)
2215 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
2216 txt {* Both lists must be non-empty *}
2217 apply (case_tac xs, simp)
2218 apply (case_tac ys, clarify)
2219 apply (simp (no_asm_use))
2221 txt {* prenexing's needed, not miniscoping *}
2222 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)
2226 lemma nth_equalityI:
2227 "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
2228 apply (frule nth_take_lemma [OF le_refl eq_imp_le])
2229 apply (simp_all add: take_all)
2233 "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
2234 by (rule nth_equalityI, auto)
2236 (* needs nth_equalityI *)
2237 lemma list_all2_antisym:
2238 "\<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>
2239 \<Longrightarrow> xs = ys"
2240 apply (simp add: list_all2_conv_all_nth)
2241 apply (rule nth_equalityI, blast, simp)
2244 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
2245 -- {* The famous take-lemma. *}
2246 apply (drule_tac x = "max (length xs) (length ys)" in spec)
2247 apply (simp add: le_max_iff_disj take_all)
2252 "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
2253 by (cases n) simp_all
2256 "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
2257 by (cases n) simp_all
2259 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
2260 by (cases n) simp_all
2262 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
2263 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
2264 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
2266 declare take_Cons_number_of [simp]
2267 drop_Cons_number_of [simp]
2268 nth_Cons_number_of [simp]
2271 subsubsection {* @{text "distinct"} and @{text remdups} *}
2273 lemma distinct_append [simp]:
2274 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
2277 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
2280 lemma set_remdups [simp]: "set (remdups xs) = set xs"
2281 by (induct xs) (auto simp add: insert_absorb)
2283 lemma distinct_remdups [iff]: "distinct (remdups xs)"
2286 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
2287 by (induct xs, auto)
2289 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
2290 by (metis distinct_remdups distinct_remdups_id)
2292 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
2293 by (metis distinct_remdups finite_list set_remdups)
2295 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
2298 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
2301 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
2304 lemma length_remdups_eq[iff]:
2305 "(length (remdups xs) = length xs) = (remdups xs = xs)"
2308 apply(subgoal_tac "length (remdups xs) <= length xs")
2310 apply(rule length_remdups_leq)
2315 "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
2319 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
2322 lemma distinct_upt[simp]: "distinct[i..<j]"
2325 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
2326 apply(induct xs arbitrary: i)
2330 apply(blast dest:in_set_takeD)
2333 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
2334 apply(induct xs arbitrary: i)
2340 lemma distinct_list_update:
2341 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
2342 shows "distinct (xs[i:=a])"
2343 proof (cases "i < length xs")
2345 with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
2346 apply (drule_tac id_take_nth_drop) by simp
2347 with d True show ?thesis
2348 apply (simp add: upd_conv_take_nth_drop)
2349 apply (drule subst [OF id_take_nth_drop]) apply assumption
2350 apply simp apply (cases "a = xs!i") apply simp by blast
2352 case False with d show ?thesis by auto
2356 text {* It is best to avoid this indexed version of distinct, but
2357 sometimes it is useful. *}
2359 lemma distinct_conv_nth:
2360 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
2361 apply (induct xs, simp, simp)
2362 apply (rule iffI, clarsimp)
2364 apply (case_tac j, simp)
2365 apply (simp add: set_conv_nth)
2367 apply (clarsimp simp add: set_conv_nth, simp)
2370 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
2372 apply (clarsimp simp add: set_conv_nth)
2373 apply (erule_tac x = 0 in allE, simp)
2374 apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
2376 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
2378 apply (erule_tac x = "Suc i" in allE, simp)
2379 apply (erule_tac x = "Suc j" in allE, simp)
2382 lemma nth_eq_iff_index_eq:
2383 "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
2384 by(auto simp: distinct_conv_nth)
2386 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
2389 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
2391 case Nil thus ?case by simp
2395 proof (cases "x \<in> set xs")
2396 case False with Cons show ?thesis by simp
2398 case True with Cons.prems
2399 have "card (set xs) = Suc (length xs)"
2400 by (simp add: card_insert_if split: split_if_asm)
2401 moreover have "card (set xs) \<le> length xs" by (rule card_length)
2402 ultimately have False by simp
2407 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
2408 apply (induct n == "length ws" arbitrary:ws) apply simp
2409 apply(case_tac ws) apply simp
2410 apply (simp split:split_if_asm)
2411 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
2414 lemma length_remdups_concat:
2415 "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
2416 by(simp add: set_concat distinct_card[symmetric])
2419 subsubsection {* @{text remove1} *}
2421 lemma remove1_append:
2422 "remove1 x (xs @ ys) =
2423 (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
2426 lemma in_set_remove1[simp]:
2427 "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
2432 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
2439 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
2446 lemma length_remove1:
2447 "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
2449 apply (auto dest!:length_pos_if_in_set)
2452 lemma remove1_filter_not[simp]:
2453 "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
2456 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
2457 apply(insert set_remove1_subset)
2461 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
2462 by (induct xs) simp_all
2465 subsubsection {* @{text removeAll} *}
2467 lemma removeAll_append[simp]:
2468 "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
2471 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
2474 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
2477 (* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
2478 lemma length_removeAll:
2479 "length(removeAll x xs) = length xs - count x xs"
2482 lemma removeAll_filter_not[simp]:
2483 "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
2487 lemma distinct_remove1_removeAll:
2488 "distinct xs ==> remove1 x xs = removeAll x xs"
2489 by (induct xs) simp_all
2491 lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>
2492 map f (removeAll x xs) = removeAll (f x) (map f xs)"
2493 by (induct xs) (simp_all add:inj_on_def)
2495 lemma map_removeAll_inj: "inj f \<Longrightarrow>
2496 map f (removeAll x xs) = removeAll (f x) (map f xs)"
2497 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
2500 subsubsection {* @{text replicate} *}
2502 lemma length_replicate [simp]: "length (replicate n x) = n"
2505 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
2508 lemma replicate_app_Cons_same:
2509 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
2512 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
2513 apply (induct n, simp)
2514 apply (simp add: replicate_app_Cons_same)
2517 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
2520 text{* Courtesy of Matthias Daum: *}
2521 lemma append_replicate_commute:
2522 "replicate n x @ replicate k x = replicate k x @ replicate n x"
2523 apply (simp add: replicate_add [THEN sym])
2524 apply (simp add: add_commute)
2527 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
2530 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"
2533 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
2534 by (atomize (full), induct n) auto
2536 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
2537 apply (induct n arbitrary: i, simp)
2538 apply (simp add: nth_Cons split: nat.split)
2541 text{* Courtesy of Matthias Daum (2 lemmas): *}
2542 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
2543 apply (case_tac "k \<le> i")
2544 apply (simp add: min_def)
2545 apply (drule not_leE)
2546 apply (simp add: min_def)
2547 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
2549 apply (simp add: replicate_add [symmetric])
2552 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
2553 apply (induct k arbitrary: i)
2562 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
2565 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
2566 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
2568 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
2571 lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
2572 by (simp add: set_replicate_conv_if split: split_if_asm)
2574 lemma replicate_append_same:
2575 "replicate i x @ [x] = x # replicate i x"
2576 by (induct i) simp_all
2578 lemma map_replicate_trivial:
2579 "map (\<lambda>i. x) [0..<i] = replicate i x"
2580 by (induct i) (simp_all add: replicate_append_same)
2583 subsubsection{*@{text rotate1} and @{text rotate}*}
2585 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
2586 by(simp add:rotate1_def)
2588 lemma rotate0[simp]: "rotate 0 = id"
2589 by(simp add:rotate_def)
2591 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
2592 by(simp add:rotate_def)
2595 "rotate (m+n) = rotate m o rotate n"
2596 by(simp add:rotate_def funpow_add)
2598 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
2599 by(simp add:rotate_add)
2601 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
2602 by(simp add:rotate_def funpow_swap1)
2604 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
2605 by(cases xs) simp_all
2607 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
2610 apply (simp add:rotate_def)
2613 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
2614 by(simp add:rotate1_def split:list.split)
2616 lemma rotate_drop_take:
2617 "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
2620 apply(simp add:rotate_def)
2621 apply(cases "xs = []")
2623 apply(case_tac "n mod length xs = 0")
2624 apply(simp add:mod_Suc)
2625 apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
2626 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
2627 take_hd_drop linorder_not_le)
2630 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
2631 by(simp add:rotate_drop_take)
2633 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
2634 by(simp add:rotate_drop_take)
2636 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
2637 by(simp add:rotate1_def split:list.split)
2639 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
2640 by (induct n arbitrary: xs) (simp_all add:rotate_def)
2642 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
2643 by(simp add:rotate1_def split:list.split) blast
2645 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
2646 by (induct n) (simp_all add:rotate_def)
2648 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
2649 by(simp add:rotate_drop_take take_map drop_map)
2651 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
2652 by(simp add:rotate1_def split:list.split)
2654 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
2655 by (induct n) (simp_all add:rotate_def)
2657 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
2658 by(simp add:rotate1_def split:list.split)
2660 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
2661 by (induct n) (simp_all add:rotate_def)
2664 "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
2665 apply(simp add:rotate_drop_take rev_drop rev_take)
2666 apply(cases "length xs = 0")
2668 apply(cases "n mod length xs = 0")
2670 apply(simp add:rotate_drop_take rev_drop rev_take)
2673 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
2674 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
2675 apply(subgoal_tac "length xs \<noteq> 0")
2677 using mod_less_divisor[of "length xs" n] by arith
2680 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
2682 lemma sublist_empty [simp]: "sublist xs {} = []"
2683 by (auto simp add: sublist_def)
2685 lemma sublist_nil [simp]: "sublist [] A = []"
2686 by (auto simp add: sublist_def)
2688 lemma length_sublist:
2689 "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
2690 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
2692 lemma sublist_shift_lemma_Suc:
2693 "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
2694 map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
2695 apply(induct xs arbitrary: "is")
2697 apply (case_tac "is")
2702 lemma sublist_shift_lemma:
2703 "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
2704 map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
2705 by (induct xs rule: rev_induct) (simp_all add: add_commute)
2707 lemma sublist_append:
2708 "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
2709 apply (unfold sublist_def)
2710 apply (induct l' rule: rev_induct, simp)
2711 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
2712 apply (simp add: add_commute)
2716 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
2717 apply (induct l rule: rev_induct)
2718 apply (simp add: sublist_def)
2719 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
2722 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
2723 apply(induct xs arbitrary: I)
2724 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
2727 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
2728 by(auto simp add:set_sublist)
2730 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
2731 by(auto simp add:set_sublist)
2733 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
2734 by(auto simp add:set_sublist)
2736 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
2737 by (simp add: sublist_Cons)
2740 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
2741 apply(induct xs arbitrary: I)
2743 apply(auto simp add:sublist_Cons)
2747 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
2748 apply (induct l rule: rev_induct, simp)
2749 apply (simp split: nat_diff_split add: sublist_append)
2752 lemma filter_in_sublist:
2753 "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
2754 proof (induct xs arbitrary: s)
2755 case Nil thus ?case by simp
2758 moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
2759 ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
2763 subsubsection {* @{const splice} *}
2765 lemma splice_Nil2 [simp, code]:
2767 by (cases xs) simp_all
2769 lemma splice_Cons_Cons [simp, code]:
2770 "splice (x#xs) (y#ys) = x # y # splice xs ys"
2773 declare splice.simps(2) [simp del, code del]
2775 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
2776 apply(induct xs arbitrary: ys) apply simp
2782 subsection {*Sorting*}
2784 text{* Currently it is not shown that @{const sort} returns a
2785 permutation of its input because the nicest proof is via multisets,
2786 which are not yet available. Alternatively one could define a function
2787 that counts the number of occurrences of an element in a list and use
2788 that instead of multisets to state the correctness property. *}
2793 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
2794 apply(induct xs arbitrary: x) apply simp
2795 by simp (blast intro: order_trans)
2797 lemma sorted_append:
2798 "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
2799 by (induct xs) (auto simp add:sorted_Cons)
2801 lemma set_insort: "set(insort x xs) = insert x (set xs)"
2804 lemma set_sort[simp]: "set(sort xs) = set xs"
2805 by (induct xs) (simp_all add:set_insort)
2807 lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
2808 by(induct xs)(auto simp:set_insort)
2810 lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
2811 by(induct xs)(simp_all add:distinct_insort set_sort)
2813 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
2815 apply(auto simp:sorted_Cons set_insort)
2818 theorem sorted_sort[simp]: "sorted (sort xs)"
2819 by (induct xs) (auto simp:sorted_insort)
2821 lemma insort_is_Cons: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
2824 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
2825 by (induct xs, auto simp add: sorted_Cons)
2827 lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
2828 by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
2830 lemma sorted_remdups[simp]:
2831 "sorted l \<Longrightarrow> sorted (remdups l)"
2832 by (induct l) (auto simp: sorted_Cons)
2834 lemma sorted_distinct_set_unique:
2835 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
2838 from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
2839 from assms show ?thesis
2840 proof(induct rule:list_induct2[OF 1])
2841 case 1 show ?case by simp
2843 case 2 thus ?case by (simp add:sorted_Cons)
2844 (metis Diff_insert_absorb antisym insertE insert_iff)
2848 lemma finite_sorted_distinct_unique:
2849 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
2850 apply(drule finite_distinct_list)
2852 apply(rule_tac a="sort xs" in ex1I)
2853 apply (auto simp: sorted_distinct_set_unique)
2858 lemma sorted_upt[simp]: "sorted[i..<j]"
2859 by (induct j) (simp_all add:sorted_append)
2862 subsubsection {* @{text sorted_list_of_set} *}
2864 text{* This function maps (finite) linearly ordered sets to sorted
2865 lists. Warning: in most cases it is not a good idea to convert from
2866 sets to lists but one should convert in the other direction (via
2874 sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
2875 [code func del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
2877 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
2878 set(sorted_list_of_set A) = A &
2879 sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
2880 apply(simp add:sorted_list_of_set_def)
2882 apply(simp_all add: finite_sorted_distinct_unique)
2885 lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
2886 unfolding sorted_list_of_set_def
2887 apply(subst the_equality[of _ "[]"])
2894 subsubsection {* @{text upto}: the generic interval-list *}
2896 class finite_intvl_succ = linorder +
2897 fixes successor :: "'a \<Rightarrow> 'a"
2898 assumes finite_intvl: "finite{a..b}"
2899 and successor_incr: "a < successor a"
2900 and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
2902 context finite_intvl_succ
2906 upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
2907 "upto i j == sorted_list_of_set {i..j}"
2909 lemma upto[simp]: "set[a..b] = {a..b} & sorted[a..b] & distinct[a..b]"
2910 by(simp add:upto_def finite_intvl)
2912 lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
2913 apply(insert successor_incr[of i])
2914 apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
2915 apply(metis ord_discrete less_le not_le)
2918 lemma sorted_list_of_set_rec: "i \<le> j \<Longrightarrow>
2919 sorted_list_of_set {i..j} = i # sorted_list_of_set {successor i..j}"
2920 apply(simp add:sorted_list_of_set_def upto_def)
2921 apply (rule the1_equality[OF finite_sorted_distinct_unique])
2922 apply (simp add:finite_intvl)
2923 apply(rule the1I2[OF finite_sorted_distinct_unique])
2924 apply (simp add:finite_intvl)
2925 apply (simp add: sorted_Cons insert_intvl Ball_def)
2926 apply (metis successor_incr leD less_imp_le order_trans)
2929 lemma sorted_list_of_set_rec2: "i \<le> j \<Longrightarrow>
2930 sorted_list_of_set {i..successor j} =
2931 sorted_list_of_set {i..j} @ [successor j]"
2932 apply(simp add:sorted_list_of_set_def upto_def)
2933 apply (rule the1_equality[OF finite_sorted_distinct_unique])
2934 apply (simp add:finite_intvl)
2935 apply(rule the1I2[OF finite_sorted_distinct_unique])
2936 apply (simp add:finite_intvl)
2937 apply (simp add: sorted_append Ball_def expand_set_eq)
2939 apply (metis eq_iff leD linear not_leE ord_discrete order_trans successor_incr)
2940 apply (metis leD linear order_trans successor_incr)
2943 lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
2944 by(simp add: upto_def sorted_list_of_set_rec)
2946 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
2947 by(simp add: upto_rec)
2949 lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..successor j] = [i..j] @ [successor j]"
2950 by(simp add: upto_def sorted_list_of_set_rec2)
2954 text{* The integers are an instance of the above class: *}
2956 instantiation int:: finite_intvl_succ
2960 successor_int_def: "successor = (%i\<Colon>int. i+1)"
2963 by intro_classes (simp_all add: successor_int_def)
2967 text{* Now @{term"[i..j::int]"} is defined for integers. *}
2969 hide (open) const successor
2971 lemma upto_rec2_int: "(i::int) \<le> j \<Longrightarrow> [i..j+1] = [i..j] @ [j+1]"
2972 by(rule upto_rec2[where 'a = int, simplified successor_int_def])
2975 subsubsection {* @{text lists}: the list-forming operator over sets *}
2978 lists :: "'a set => 'a list set"
2981 Nil [intro!]: "[]: lists A"
2982 | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
2984 inductive_cases listsE [elim!,noatp]: "x#l : lists A"
2985 inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
2987 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
2988 by (rule predicate1I, erule listsp.induct, blast+)
2990 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
2993 assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
2996 lemmas lists_IntI = listsp_infI [to_set]
2998 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
2999 proof (rule mono_inf [where f=listsp, THEN order_antisym])
3000 show "mono listsp" by (simp add: mono_def listsp_mono)
3001 show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
3004 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
3006 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
3008 lemma append_in_listsp_conv [iff]:
3009 "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
3012 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
3014 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
3015 -- {* eliminate @{text listsp} in favour of @{text set} *}
3018 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
3020 lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
3021 by (rule in_listsp_conv_set [THEN iffD1])
3023 lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
3025 lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
3026 by (rule in_listsp_conv_set [THEN iffD2])
3028 lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
3030 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
3035 subsubsection{* Inductive definition for membership *}
3037 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
3039 elem: "ListMem x (x # xs)"
3040 | insert: "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
3042 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
3044 apply (induct set: ListMem)
3047 apply (auto intro: ListMem.intros)
3052 subsubsection{*Lists as Cartesian products*}
3054 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
3055 @{term A} and tail drawn from @{term Xs}.*}
3058 set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
3059 "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
3060 declare set_Cons_def [code func del]
3062 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
3063 by (auto simp add: set_Cons_def)
3065 text{*Yields the set of lists, all of the same length as the argument and
3066 with elements drawn from the corresponding element of the argument.*}
3068 consts listset :: "'a set list \<Rightarrow> 'a list set"
3071 "listset(A#As) = set_Cons A (listset As)"
3074 subsection{*Relations on Lists*}
3076 subsubsection {* Length Lexicographic Ordering *}
3078 text{*These orderings preserve well-foundedness: shorter lists
3079 precede longer lists. These ordering are not used in dictionaries.*}
3081 consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
3082 --{*The lexicographic ordering for lists of the specified length*}
3086 (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
3087 {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
3090 lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
3091 "lex r == \<Union>n. lexn r n"
3092 --{*Holds only between lists of the same length*}
3094 lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
3095 "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
3096 --{*Compares lists by their length and then lexicographically*}
3098 declare lex_def [code func del]
3101 lemma wf_lexn: "wf r ==> wf (lexn r n)"
3102 apply (induct n, simp, simp)
3103 apply(rule wf_subset)
3104 prefer 2 apply (rule Int_lower1)
3105 apply(rule wf_prod_fun_image)
3106 prefer 2 apply (rule inj_onI, auto)
3110 "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
3111 by (induct n arbitrary: xs ys) auto
3113 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
3114 apply (unfold lex_def)
3116 apply (blast intro: wf_lexn, clarify)
3117 apply (rename_tac m n)
3118 apply (subgoal_tac "m \<noteq> n")
3119 prefer 2 apply blast
3120 apply (blast dest: lexn_length not_sym)
3125 {(xs,ys). length xs = n \<and> length ys = n \<and>
3126 (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
3127 apply (induct n, simp)
3128 apply (simp add: image_Collect lex_prod_def, safe, blast)
3129 apply (rule_tac x = "ab # xys" in exI, simp)
3130 apply (case_tac xys, simp_all, blast)
3135 {(xs,ys). length xs = length ys \<and>
3136 (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
3137 by (force simp add: lex_def lexn_conv)
3139 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
3140 by (unfold lenlex_def) blast
3143 "lenlex r = {(xs,ys). length xs < length ys |
3144 length xs = length ys \<and> (xs, ys) : lex r}"
3145 by (simp add: lenlex_def diag_def lex_prod_def inv_image_def)
3147 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
3148 by (simp add: lex_conv)
3150 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
3151 by (simp add:lex_conv)
3153 lemma Cons_in_lex [simp]:
3154 "((x # xs, y # ys) : lex r) =
3155 ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
3156 apply (simp add: lex_conv)
3158 prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
3159 apply (case_tac xys, simp, simp)
3164 subsubsection {* Lexicographic Ordering *}
3166 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
3167 This ordering does \emph{not} preserve well-foundedness.
3168 Author: N. Voelker, March 2005. *}
3171 lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set"
3172 "lexord r == {(x,y). \<exists> a v. y = x @ a # v \<or>
3173 (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
3174 declare lexord_def [code func del]
3176 lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
3177 by (unfold lexord_def, induct_tac y, auto)
3179 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
3180 by (unfold lexord_def, induct_tac x, auto)
3182 lemma lexord_cons_cons[simp]:
3183 "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
3184 apply (unfold lexord_def, safe, simp_all)
3185 apply (case_tac u, simp, simp)
3186 apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
3187 apply (erule_tac x="b # u" in allE)
3190 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
3192 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
3193 by (induct_tac x, auto)
3195 lemma lexord_append_left_rightI:
3196 "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
3197 by (induct_tac u, auto)
3199 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
3202 lemma lexord_append_leftD:
3203 "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
3204 by (erule rev_mp, induct_tac x, auto)
3206 lemma lexord_take_index_conv:
3207 "((x,y) : lexord r) =
3208 ((length x < length y \<and> take (length x) y = x) \<or>
3209 (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
3210 apply (unfold lexord_def Let_def, clarsimp)
3211 apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
3213 apply (rule_tac x="hd (drop (length x) y)" in exI)
3214 apply (rule_tac x="tl (drop (length x) y)" in exI)
3215 apply (erule subst, simp add: min_def)
3216 apply (rule_tac x ="length u" in exI, simp)
3217 apply (rule_tac x ="take i x" in exI)
3218 apply (rule_tac x ="x ! i" in exI)
3219 apply (rule_tac x ="y ! i" in exI, safe)
3220 apply (rule_tac x="drop (Suc i) x" in exI)
3221 apply (drule sym, simp add: drop_Suc_conv_tl)
3222 apply (rule_tac x="drop (Suc i) y" in exI)
3223 by (simp add: drop_Suc_conv_tl)
3225 -- {* lexord is extension of partial ordering List.lex *}
3226 lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
3227 apply (rule_tac x = y in spec)
3228 apply (induct_tac x, clarsimp)
3229 by (clarify, case_tac x, simp, force)
3231 lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
3235 "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
3236 apply (erule rev_mp)+
3237 apply (rule_tac x = x in spec)
3238 apply (rule_tac x = z in spec)
3239 apply ( induct_tac y, simp, clarify)
3240 apply (case_tac xa, erule ssubst)
3241 apply (erule allE, erule allE) -- {* avoid simp recursion *}
3242 apply (case_tac x, simp, simp)
3243 apply (case_tac x, erule allE, erule allE, simp)
3244 apply (erule_tac x = listb in allE)
3245 apply (erule_tac x = lista in allE, simp)
3246 apply (unfold trans_def)
3249 lemma lexord_transI: "trans r \<Longrightarrow> trans (lexord r)"
3250 by (rule transI, drule lexord_trans, blast)
3252 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"
3253 apply (rule_tac x = y in spec)
3254 apply (induct_tac x, rule allI)
3255 apply (case_tac x, simp, simp)
3256 apply (rule allI, case_tac x, simp, simp)
3260 subsection {* Lexicographic combination of measure functions *}
3262 text {* These are useful for termination proofs *}
3265 "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
3267 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
3268 unfolding measures_def
3271 lemma in_measures[simp]:
3272 "(x, y) \<in> measures [] = False"
3273 "(x, y) \<in> measures (f # fs)
3274 = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"
3275 unfolding measures_def
3278 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
3281 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
3285 subsubsection{*Lifting a Relation on List Elements to the Lists*}
3288 listrel :: "('a * 'a)set => ('a list * 'a list)set"
3289 for r :: "('a * 'a)set"
3291 Nil: "([],[]) \<in> listrel r"
3292 | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
3294 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
3295 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
3296 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
3297 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
3300 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
3302 apply (erule listrel.induct)
3303 apply (blast intro: listrel.intros)+
3306 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
3308 apply (erule listrel.induct, auto)
3311 lemma listrel_refl: "refl A r \<Longrightarrow> refl (lists A) (listrel r)"
3312 apply (simp add: refl_def listrel_subset Ball_def)
3314 apply (induct_tac x)
3315 apply (auto intro: listrel.intros)
3318 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"
3319 apply (auto simp add: sym_def)
3320 apply (erule listrel.induct)
3321 apply (blast intro: listrel.intros)+
3324 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"
3325 apply (simp add: trans_def)
3328 apply (erule listrel.induct)
3329 apply (blast intro: listrel.intros)+
3332 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
3333 by (simp add: equiv_def listrel_refl listrel_sym listrel_trans)
3335 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
3336 by (blast intro: listrel.intros)
3339 "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
3340 by (auto simp add: set_Cons_def intro: listrel.intros)
3343 subsection{*Miscellany*}
3345 subsubsection {* Characters and strings *}
3348 Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
3349 | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
3352 "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
3353 Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
3354 proof (rule UNIV_eq_I)
3355 fix x show "x \<in> ?A" by (cases x) simp_all
3358 instance nibble :: finite
3359 by default (simp add: UNIV_nibble)
3361 datatype char = Char nibble nibble
3362 -- "Note: canonical order of character encoding coincides with standard term ordering"
3365 "UNIV = image (split Char) (UNIV \<times> UNIV)"
3366 proof (rule UNIV_eq_I)
3367 fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
3370 instance char :: finite
3371 by default (simp add: UNIV_char)
3373 lemma size_char [code, simp]:
3374 "size (c::char) = 0" by (cases c) simp
3376 lemma char_size [code, simp]:
3377 "char_size (c::char) = 0" by (cases c) simp
3379 types string = "char list"
3382 "_Char" :: "xstr => char" ("CHR _")
3383 "_String" :: "xstr => string" ("_")
3385 setup StringSyntax.setup
3388 subsection {* Size function *}
3390 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
3391 by (rule is_measure_trivial)
3393 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
3394 by (rule is_measure_trivial)
3396 lemma list_size_estimation[termination_simp]:
3397 "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
3400 lemma list_size_estimation'[termination_simp]:
3401 "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
3404 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
3407 lemma list_size_pointwise[termination_simp]:
3408 "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
3409 by (induct xs) force+
3411 subsection {* Code generator *}
3413 subsubsection {* Setup *}
3418 fun term_of_list f T = HOLogic.mk_list T o map f;
3421 fun gen_list' aG aT i j = frequency
3425 val (xs, ts) = gen_list' aG aT (i-1) j
3426 in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
3427 (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
3428 and gen_list aG aT i = gen_list' aG aT i i;
3432 val term_of_char = HOLogic.mk_char o ord;
3436 let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
3437 in (chr j, fn () => HOLogic.mk_char j) end;
3440 consts_code "Cons" ("(_ ::/ _)")
3461 open Basic_Code_Thingol;
3462 val nil' = Code_Name.const @{theory} @{const_name Nil};
3463 val cons' = Code_Name.const @{theory} @{const_name Cons};
3464 val char' = Code_Name.const @{theory} @{const_name Char}
3465 val nibbles' = map (Code_Name.const @{theory})
3466 [@{const_name Nibble0}, @{const_name Nibble1},
3467 @{const_name Nibble2}, @{const_name Nibble3},
3468 @{const_name Nibble4}, @{const_name Nibble5},
3469 @{const_name Nibble6}, @{const_name Nibble7},
3470 @{const_name Nibble8}, @{const_name Nibble9},
3471 @{const_name NibbleA}, @{const_name NibbleB},
3472 @{const_name NibbleC}, @{const_name NibbleD},
3473 @{const_name NibbleE}, @{const_name NibbleF}];
3475 fun implode_list t =
3477 fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
3481 | dest_cons _ = NONE;
3482 val (ts, t') = Code_Thingol.unfoldr dest_cons t;
3484 of IConst (c, _) => if c = nil' then SOME ts else NONE
3488 fun decode_char (IConst (c1, _), IConst (c2, _)) =
3490 fun idx c = find_index (curry (op =) c) nibbles';
3491 fun decode ~1 _ = NONE
3492 | decode _ ~1 = NONE
3493 | decode n m = SOME (chr (n * 16 + m));
3494 in decode (idx c1) (idx c2) end
3495 | decode_char _ = NONE;
3497 fun implode_string mk_char mk_string ts =
3499 fun implode_char (IConst (c, _) `$ t1 `$ t2) =
3500 if c = char' then decode_char (t1, t2) else NONE
3501 | implode_char _ = NONE;
3502 val ts' = map implode_char ts;
3503 in if forall is_some ts'
3504 then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
3508 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
3509 Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
3510 pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
3511 Code_Printer.str target_cons,
3512 pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
3515 fun pretty_list literals =
3517 val mk_list = Code_Printer.literal_list literals;
3518 fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
3519 case Option.map (cons t1) (implode_list t2)
3520 of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
3521 | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
3524 fun pretty_list_string literals =
3526 val mk_list = Code_Printer.literal_list literals;
3527 val mk_char = Code_Printer.literal_char literals;
3528 val mk_string = Code_Printer.literal_string literals;
3529 fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
3530 case Option.map (cons t1) (implode_list t2)
3531 of SOME ts => (case implode_string mk_char mk_string ts
3533 | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
3534 | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
3537 fun pretty_char literals =
3539 val mk_char = Code_Printer.literal_char literals;
3540 fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
3541 case decode_char (t1, t2)
3542 of SOME c => (Code_Printer.str o mk_char) c
3543 | NONE => Code_Printer.nerror thm "Illegal character expression";
3546 fun pretty_message literals =
3548 val mk_char = Code_Printer.literal_char literals;
3549 val mk_string = Code_Printer.literal_string literals;
3550 fun pretty _ thm _ _ _ [(t, _)] =
3552 of SOME ts => (case implode_string mk_char mk_string ts
3554 | NONE => Code_Printer.nerror thm "Illegal message expression")
3555 | NONE => Code_Printer.nerror thm "Illegal message expression";
3560 fun add_literal_list target thy =
3562 val pr = pretty_list (Code_Target.the_literals thy target);
3565 |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
3568 fun add_literal_list_string target thy =
3570 val pr = pretty_list_string (Code_Target.the_literals thy target);
3573 |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
3576 fun add_literal_char target thy =
3578 val pr = pretty_char (Code_Target.the_literals thy target);
3581 |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
3584 fun add_literal_message str target thy =
3586 val pr = pretty_message (Code_Target.the_literals thy target);
3589 |> Code_Target.add_syntax_const target str (SOME pr)
3596 fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
3599 code_instance list :: eq
3602 code_const "op = \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
3603 (Haskell infixl 4 "==")
3608 fun list_codegen thy defs gr dep thyname b t =
3610 val ts = HOLogic.dest_list t;
3611 val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
3613 val (gr'', ps) = foldl_map
3614 (Codegen.invoke_codegen thy defs dep thyname false) (gr', ts)
3615 in SOME (gr'', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
3617 fun char_codegen thy defs gr dep thyname b t =
3619 val i = HOLogic.dest_char t;
3620 val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
3622 in SOME (gr', Codegen.str (ML_Syntax.print_string (chr i)))
3623 end handle TERM _ => NONE;
3626 Codegen.add_codegen "list_codegen" list_codegen
3627 #> Codegen.add_codegen "char_codegen" char_codegen
3632 subsubsection {* Generation of efficient code *}
3635 member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
3637 "x mem [] \<longleftrightarrow> False"
3638 | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
3641 null:: "'a list \<Rightarrow> bool"
3644 | "null (x#xs) = False"
3647 list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
3649 "list_inter [] bs = []"
3650 | "list_inter (a#as) bs =
3651 (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
3654 list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
3656 "list_all P [] = True"
3657 | "list_all P (x#xs) = (P x \<and> list_all P xs)"
3660 list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
3662 "list_ex P [] = False"
3663 | "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
3666 filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
3668 "filtermap f [] = []"
3669 | "filtermap f (x#xs) =
3670 (case f x of None \<Rightarrow> filtermap f xs
3671 | Some y \<Rightarrow> y # filtermap f xs)"
3674 map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
3676 "map_filter f P [] = []"
3677 | "map_filter f P (x#xs) =
3678 (if P x then f x # map_filter f P xs else map_filter f P xs)"
3681 Only use @{text mem} for generating executable code. Otherwise use
3682 @{prop "x : set xs"} instead --- it is much easier to reason about.
3683 The same is true for @{const list_all} and @{const list_ex}: write
3684 @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
3685 quantifiers are aleady known to the automatic provers. In fact, the
3686 declarations in the code subsection make sure that @{text "\<in>"},
3687 @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} are implemented
3690 Efficient emptyness check is implemented by @{const null}.
3692 The functions @{const filtermap} and @{const map_filter} are just
3693 there to generate efficient code. Do not use
3694 them for modelling and proving.
3697 lemma rev_foldl_cons [code]:
3698 "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
3700 case Nil then show ?case by simp
3705 have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
3706 = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
3707 by (induct xs arbitrary: ys) auto
3710 show ?case by (induct xs) (auto simp add: Cons aux)
3713 lemma mem_iff [code post]:
3714 "x mem xs \<longleftrightarrow> x \<in> set xs"
3717 lemmas in_set_code [code unfold] = mem_iff [symmetric]
3719 lemma empty_null [code inline]:
3720 "xs = [] \<longleftrightarrow> null xs"
3721 by (cases xs) simp_all
3723 lemmas null_empty [code post] =
3724 empty_null [symmetric]
3726 lemma list_inter_conv:
3727 "set (list_inter xs ys) = set xs \<inter> set ys"
3730 lemma list_all_iff [code post]:
3731 "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
3734 lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
3736 lemma list_all_append [simp]:
3737 "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
3740 lemma list_all_rev [simp]:
3741 "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
3742 by (simp add: list_all_iff)
3744 lemma list_all_length:
3745 "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
3746 unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
3748 lemma list_ex_iff [code post]:
3749 "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
3750 by (induct xs) simp_all
3752 lemmas list_bex_code [code unfold] =
3753 list_ex_iff [symmetric]
3755 lemma list_ex_length:
3756 "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
3757 unfolding list_ex_iff set_conv_nth by auto
3759 lemma filtermap_conv:
3760 "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
3761 by (induct xs) (simp_all split: option.split)
3763 lemma map_filter_conv [simp]:
3764 "map_filter f P xs = map f (filter P xs)"
3768 text {* Code for bounded quantification and summation over nats. *}
3770 lemma atMost_upto [code unfold]:
3771 "{..n} = set [0..<Suc n]"
3774 lemma atLeast_upt [code unfold]:
3775 "{..<n} = set [0..<n]"
3778 lemma greaterThanLessThan_upt [code unfold]:
3779 "{n<..<m} = set [Suc n..<m]"
3782 lemma atLeastLessThan_upt [code unfold]:
3783 "{n..<m} = set [n..<m]"
3786 lemma greaterThanAtMost_upt [code unfold]:
3787 "{n<..m} = set [Suc n..<Suc m]"
3790 lemma atLeastAtMost_upt [code unfold]:
3791 "{n..m} = set [n..<Suc m]"
3794 lemma all_nat_less_eq [code unfold]:
3795 "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
3798 lemma ex_nat_less_eq [code unfold]:
3799 "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
3802 lemma all_nat_less [code unfold]:
3803 "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
3806 lemma ex_nat_less [code unfold]:
3807 "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
3810 lemma setsum_set_distinct_conv_listsum:
3811 "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
3812 by (induct xs) simp_all
3814 lemma setsum_set_upt_conv_listsum [code unfold]:
3815 "setsum f (set [m..<n]) = listsum (map f [m..<n])"
3816 by (rule setsum_set_distinct_conv_listsum) simp
3819 text {* Code for summation over ints. *}
3821 lemma greaterThanLessThan_upto [code unfold]:
3822 "{i<..<j::int} = set [i+1..j - 1]"
3825 lemma atLeastLessThan_upto [code unfold]:
3826 "{i..<j::int} = set [i..j - 1]"
3829 lemma greaterThanAtMost_upto [code unfold]:
3830 "{i<..j::int} = set [i+1..j]"
3833 lemma atLeastAtMost_upto [code unfold]:
3834 "{i..j::int} = set [i..j]"
3837 lemma setsum_set_upto_conv_listsum [code unfold]:
3838 "setsum f (set [i..j::int]) = listsum (map f [i..j])"
3839 by (rule setsum_set_distinct_conv_listsum) simp