5 header {* The datatype of finite lists *}
8 imports Plain Quotient Presburger Code_Numeral Sledgehammer Recdef
9 uses ("Tools/list_code.ML")
14 | Cons 'a "'a list" (infixr "#" 65)
17 -- {* list Enumeration *}
18 "_list" :: "args => 'a list" ("[(_)]")
25 subsection {* Basic list processing functions *}
28 hd :: "'a list \<Rightarrow> 'a" where
32 tl :: "'a list \<Rightarrow> 'a list" where
37 last :: "'a list \<Rightarrow> 'a" where
38 "last (x # xs) = (if xs = [] then x else last xs)"
41 butlast :: "'a list \<Rightarrow> 'a list" where
43 | "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
46 set :: "'a list \<Rightarrow> 'a set" where
48 | "set (x # xs) = insert x (set xs)"
51 map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
53 | "map f (x # xs) = f x # map f xs"
56 append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
57 append_Nil:"[] @ ys = ys"
58 | append_Cons: "(x#xs) @ ys = x # xs @ ys"
61 rev :: "'a list \<Rightarrow> 'a list" where
63 | "rev (x # xs) = rev xs @ [x]"
66 filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
68 | "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
71 -- {* Special syntax for filter *}
72 "_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
75 "[x<-xs . P]"== "CONST filter (%x. P) xs"
78 "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
80 "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
83 foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
84 foldl_Nil: "foldl f a [] = a"
85 | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
88 foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
90 | "foldr f (x # xs) a = f x (foldr f xs a)"
93 concat:: "'a list list \<Rightarrow> 'a list" where
95 | "concat (x # xs) = x @ concat xs"
97 primrec (in monoid_add)
98 listsum :: "'a list \<Rightarrow> 'a" where
100 | "listsum (x # xs) = x + listsum xs"
103 drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
104 drop_Nil: "drop n [] = []"
105 | drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
106 -- {*Warning: simpset does not contain this definition, but separate
107 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
110 take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
111 take_Nil:"take n [] = []"
112 | take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"
113 -- {*Warning: simpset does not contain this definition, but separate
114 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
117 nth :: "'a list => nat => 'a" (infixl "!" 100) where
118 nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
119 -- {*Warning: simpset does not contain this definition, but separate
120 theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
123 list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
124 "list_update [] i v = []"
125 | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
127 nonterminals lupdbinds lupdbind
130 "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")
131 "" :: "lupdbind => lupdbinds" ("_")
132 "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")
133 "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900)
136 "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
137 "xs[i:=x]" == "CONST list_update xs i x"
140 takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
141 "takeWhile P [] = []"
142 | "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
145 dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
146 "dropWhile P [] = []"
147 | "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"
150 zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
152 | zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"
153 -- {*Warning: simpset does not contain this definition, but separate
154 theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
157 upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
158 upt_0: "[i..<0] = []"
159 | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
162 distinct :: "'a list \<Rightarrow> bool" where
163 "distinct [] \<longleftrightarrow> True"
164 | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
167 remdups :: "'a list \<Rightarrow> 'a list" where
169 | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
172 insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
173 "insert x xs = (if x \<in> set xs then xs else x # xs)"
175 hide_const (open) insert
176 hide_fact (open) insert_def
179 remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
181 | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
184 removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
185 "removeAll x [] = []"
186 | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
189 replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
190 replicate_0: "replicate 0 x = []"
191 | replicate_Suc: "replicate (Suc n) x = x # replicate n x"
194 Function @{text size} is overloaded for all datatypes. Users may
195 refer to the list version as @{text length}. *}
198 length :: "'a list \<Rightarrow> nat" where
199 "length \<equiv> size"
202 rotate1 :: "'a list \<Rightarrow> 'a list" where
203 "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
206 rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
207 "rotate n = rotate1 ^^ n"
210 list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
212 (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
215 sublist :: "'a list => nat set => 'a list" where
216 "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
219 splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
221 | "splice (x # xs) ys = (if ys = [] then x # xs else x # hd ys # splice xs (tl ys))"
222 -- {*Warning: simpset does not contain the second eqn but a derived one. *}
228 @{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\
229 @{lemma "length [a,b,c] = 3" by simp}\\
230 @{lemma "set [a,b,c] = {a,b,c}" by simp}\\
231 @{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\
232 @{lemma "rev [a,b,c] = [c,b,a]" by simp}\\
233 @{lemma "hd [a,b,c,d] = a" by simp}\\
234 @{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\
235 @{lemma "last [a,b,c,d] = d" by simp}\\
236 @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
237 @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
238 @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
239 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
240 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
241 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
242 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
243 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
244 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
245 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
246 @{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
247 @{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\
248 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\
249 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
250 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
251 @{lemma "distinct [2,0,1::nat]" by simp}\\
252 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
253 @{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\
254 @{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\
255 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
256 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
257 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
258 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
259 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
260 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
261 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\
262 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\
263 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\
264 @{lemma "listsum [1,2,3::nat] = 6" by simp}
266 \caption{Characteristic examples}
267 \label{fig:Characteristic}
269 Figure~\ref{fig:Characteristic} shows characteristic examples
270 that should give an intuitive understanding of the above functions.
273 text{* The following simple sort functions are intended for proofs,
274 not for efficient implementations. *}
279 fun sorted :: "'a list \<Rightarrow> bool" where
280 "sorted [] \<longleftrightarrow> True" |
281 "sorted [x] \<longleftrightarrow> True" |
282 "sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
284 primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
285 "insort_key f x [] = [x]" |
286 "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
288 definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
289 "sort_key f xs = foldr (insort_key f) xs []"
291 abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
292 abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
294 definition insort_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
295 "insort_insert x xs = (if x \<in> set xs then xs else insort x xs)"
300 subsubsection {* List comprehension *}
302 text{* Input syntax for Haskell-like list comprehension notation.
303 Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
304 the list of all pairs of distinct elements from @{text xs} and @{text ys}.
305 The syntax is as in Haskell, except that @{text"|"} becomes a dot
306 (like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
307 \verb![e| x <- xs, ...]!.
309 The qualifiers after the dot are
311 \item[generators] @{text"p \<leftarrow> xs"},
312 where @{text p} is a pattern and @{text xs} an expression of list type, or
313 \item[guards] @{text"b"}, where @{text b} is a boolean expression.
314 %\item[local bindings] @ {text"let x = e"}.
317 Just like in Haskell, list comprehension is just a shorthand. To avoid
318 misunderstandings, the translation into desugared form is not reversed
319 upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is
320 optmized to @{term"map (%x. e) xs"}.
322 It is easy to write short list comprehensions which stand for complex
323 expressions. During proofs, they may become unreadable (and
324 mangled). In such cases it can be advisable to introduce separate
325 definitions for the list comprehensions in question. *}
328 Proper theorem proving support would be nice. For example, if
329 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
330 produced something like
331 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
334 nonterminals lc_qual lc_quals
337 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __")
338 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
339 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
340 (*"_lc_let" :: "letbinds => lc_qual" ("let _")*)
341 "_lc_end" :: "lc_quals" ("]")
342 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
343 "_lc_abs" :: "'a => 'b list => 'b list"
345 (* These are easier than ML code but cannot express the optimized
346 translation of [e. p<-xs]
348 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
349 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
350 => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
351 "[e. P]" => "if P then [e] else []"
352 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
353 => "if P then (_listcompr e Q Qs) else []"
354 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
355 => "_Let b (_listcompr e Q Qs)"
359 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
361 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
363 parse_translation (advanced) {*
365 val NilC = Syntax.const @{const_syntax Nil};
366 val ConsC = Syntax.const @{const_syntax Cons};
367 val mapC = Syntax.const @{const_syntax map};
368 val concatC = Syntax.const @{const_syntax concat};
369 val IfC = Syntax.const @{const_syntax If};
371 fun singl x = ConsC $ x $ NilC;
373 fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
375 val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
376 val e = if opti then singl e else e;
377 val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
379 Syntax.const @{syntax_const "_case1"} $
380 Syntax.const @{const_syntax dummy_pattern} $ NilC;
381 val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
382 val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];
385 fun abs_tr ctxt (p as Free (s, T)) e opti =
387 val thy = ProofContext.theory_of ctxt;
388 val s' = Sign.intern_const thy s;
390 if Sign.declared_const thy s'
391 then (pat_tr ctxt p e opti, false)
392 else (lambda p e, true)
394 | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
396 fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
400 Const (@{syntax_const "_lc_end"}, _) => singl e
401 | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
402 in IfC $ b $ res $ NilC end
404 [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
405 Const(@{syntax_const "_lc_end"}, _)] =
406 (case abs_tr ctxt p e true of
407 (f, true) => mapC $ f $ es
408 | (f, false) => concatC $ (mapC $ f $ es))
410 [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
411 Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
412 let val e' = lc_tr ctxt [e, q, qs];
413 in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
415 in [(@{syntax_const "_listcompr"}, lc_tr)] end
419 term "[(x,y,z). x\<leftarrow>xs]"
420 term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
421 term "[(x,y,z). x<a, x>b]"
422 term "[(x,y,z). x\<leftarrow>xs, x>b]"
423 term "[(x,y,z). x<a, x\<leftarrow>xs]"
424 term "[(x,y). Cons True x \<leftarrow> xs]"
425 term "[(x,y,z). Cons x [] \<leftarrow> xs]"
426 term "[(x,y,z). x<a, x>b, x=d]"
427 term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
428 term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
429 term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
430 term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
431 term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
432 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
433 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
435 term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
439 subsubsection {* @{const Nil} and @{const Cons} *}
441 lemma not_Cons_self [simp]:
445 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]
447 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
451 "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
452 by (rule measure_induct [of length]) iprover
454 lemma list_nonempty_induct [consumes 1, case_names single cons]:
455 assumes "xs \<noteq> []"
456 assumes single: "\<And>x. P [x]"
457 assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"
459 using `xs \<noteq> []` proof (induct xs)
460 case Nil then show ?case by simp
462 case (Cons x xs) show ?case proof (cases xs)
463 case Nil with single show ?thesis by simp
465 case Cons then have "xs \<noteq> []" by simp
466 moreover with Cons.hyps have "P xs" .
467 ultimately show ?thesis by (rule cons)
472 subsubsection {* @{const length} *}
475 Needs to come before @{text "@"} because of theorem @{text
476 append_eq_append_conv}.
479 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"
482 lemma length_map [simp]: "length (map f xs) = length xs"
485 lemma length_rev [simp]: "length (rev xs) = length xs"
488 lemma length_tl [simp]: "length (tl xs) = length xs - 1"
491 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
494 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])"
497 lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0"
500 lemma length_Suc_conv:
501 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
504 lemma Suc_length_conv:
505 "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
506 apply (induct xs, simp, simp)
510 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"
513 lemma list_induct2 [consumes 1, case_names Nil Cons]:
514 "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>
515 (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys))
516 \<Longrightarrow> P xs ys"
517 proof (induct xs arbitrary: ys)
518 case Nil then show ?case by simp
520 case (Cons x xs ys) then show ?case by (cases ys) simp_all
523 lemma list_induct3 [consumes 2, case_names Nil Cons]:
524 "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow>
525 (\<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))
526 \<Longrightarrow> P xs ys zs"
527 proof (induct xs arbitrary: ys zs)
528 case Nil then show ?case by simp
530 case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)
534 lemma list_induct4 [consumes 3, case_names Nil Cons]:
535 "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow>
536 P [] [] [] [] \<Longrightarrow> (\<And>x xs y ys z zs w ws. length xs = length ys \<Longrightarrow>
537 length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> P xs ys zs ws \<Longrightarrow>
538 P (x#xs) (y#ys) (z#zs) (w#ws)) \<Longrightarrow> P xs ys zs ws"
539 proof (induct xs arbitrary: ys zs ws)
540 case Nil then show ?case by simp
542 case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)
547 \<And>x xs. P (x#xs) [];
548 \<And>y ys. P [] (y#ys);
549 \<And>x xs y ys. P xs ys \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
550 \<Longrightarrow> P xs ys"
551 by (induct xs arbitrary: ys) (case_tac x, auto)+
553 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
554 by (rule Eq_FalseI) auto
556 simproc_setup list_neq ("(xs::'a list) = ys") = {*
558 Reduces xs=ys to False if xs and ys cannot be of the same length.
559 This is the case if the atomic sublists of one are a submultiset
560 of those of the other list and there are fewer Cons's in one than the other.
565 fun len (Const(@{const_name Nil},_)) acc = acc
566 | len (Const(@{const_name Cons},_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
567 | len (Const(@{const_name append},_) $ xs $ ys) acc = len xs (len ys acc)
568 | len (Const(@{const_name rev},_) $ xs) acc = len xs acc
569 | len (Const(@{const_name map},_) $ _ $ xs) acc = len xs acc
570 | len t (ts,n) = (t::ts,n);
572 fun list_neq _ ss ct =
574 val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
575 val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
578 val Type(_,listT::_) = eqT;
579 val size = HOLogic.size_const listT;
580 val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
581 val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
582 val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
583 (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));
584 in SOME (thm RS @{thm neq_if_length_neq}) end
586 if m < n andalso submultiset (op aconv) (ls,rs) orelse
587 n < m andalso submultiset (op aconv) (rs,ls)
588 then prove_neq() else NONE
594 subsubsection {* @{text "@"} -- append *}
596 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
599 lemma append_Nil2 [simp]: "xs @ [] = xs"
602 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
605 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])"
608 lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"
611 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
614 lemma append_eq_append_conv [simp, no_atp]:
615 "length xs = length ys \<or> length us = length vs
616 ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
617 apply (induct xs arbitrary: ys)
618 apply (case_tac ys, simp, force)
619 apply (case_tac ys, force, simp)
622 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
623 (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
624 apply (induct xs arbitrary: ys zs ts)
631 lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"
634 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"
637 lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)"
640 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"
641 using append_same_eq [of _ _ "[]"] by auto
643 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
644 using append_same_eq [of "[]"] by auto
646 lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
649 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
652 lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"
653 by (simp add: hd_append split: list.split)
655 lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"
656 by (simp split: list.split)
658 lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"
659 by (simp add: tl_append split: list.split)
662 lemma Cons_eq_append_conv: "x#xs = ys@zs =
663 (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"
666 lemma append_eq_Cons_conv: "(ys@zs = x#xs) =
667 (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
671 text {* Trivial rules for solving @{text "@"}-equations automatically. *}
673 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
676 lemma Cons_eq_appendI:
677 "[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"
680 lemma append_eq_appendI:
681 "[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"
686 Simplification procedure for all list equalities.
687 Currently only tries to rearrange @{text "@"} to see if
688 - both lists end in a singleton list,
689 - or both lists end in the same list.
695 fun last (cons as Const(@{const_name Cons},_) $ _ $ xs) =
696 (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)
697 | last (Const(@{const_name append},_) $ _ $ ys) = last ys
700 fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
703 fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
704 (case xs of Const(@{const_name Nil},_) => xs | _ => cons $ butlast xs)
705 | butlast ((app as Const(@{const_name append},_) $ xs) $ ys) = app $ butlast ys
706 | butlast xs = Const(@{const_name Nil},fastype_of xs);
708 val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
709 @{thm append_Nil}, @{thm append_Cons}];
711 fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
713 val lastl = last lhs and lastr = last rhs;
716 val lhs1 = butlast lhs and rhs1 = butlast rhs;
717 val Type(_,listT::_) = eqT
718 val appT = [listT,listT] ---> listT
719 val app = Const(@{const_name append},appT)
720 val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
721 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
722 val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
723 (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
724 in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
727 if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
728 else if lastl aconv lastr then rearr @{thm append_same_eq}
734 val list_eq_simproc =
735 Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
739 Addsimprocs [list_eq_simproc];
743 subsubsection {* @{text map} *}
745 lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
746 by (induct xs) simp_all
748 lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)"
749 by (rule ext, induct_tac xs) auto
751 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"
754 lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs"
757 lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)"
762 lemma rev_map: "rev (map f xs) = map f (rev xs)"
765 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
768 lemma map_cong [fundef_cong, recdef_cong]:
769 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
770 -- {* a congruence rule for @{text map} *}
773 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
776 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
779 lemma map_eq_Cons_conv:
780 "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
783 lemma Cons_eq_map_conv:
784 "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
787 lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]
788 lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]
789 declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!]
792 "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
793 by(induct ys, auto simp add: Cons_eq_map_conv)
795 lemma map_eq_imp_length_eq:
796 assumes "map f xs = map g ys"
797 shows "length xs = length ys"
798 using assms proof (induct ys arbitrary: xs)
799 case Nil then show ?case by simp
801 case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
802 from Cons xs have "map f zs = map g ys" by simp
803 moreover with Cons have "length zs = length ys" by blast
804 with xs show ?case by simp
808 "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
810 apply(frule map_eq_imp_length_eq)
812 apply(induct rule:list_induct2)
815 apply (blast intro:sym)
818 lemma inj_on_map_eq_map:
819 "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
820 by(blast dest:map_inj_on)
823 "map f xs = map f ys ==> inj f ==> xs = ys"
824 by (induct ys arbitrary: xs) (auto dest!:injD)
826 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
827 by(blast dest:map_injective)
829 lemma inj_mapI: "inj f ==> inj (map f)"
830 by (iprover dest: map_injective injD intro: inj_onI)
832 lemma inj_mapD: "inj (map f) ==> inj f"
833 apply (unfold inj_on_def, clarify)
834 apply (erule_tac x = "[x]" in ballE)
835 apply (erule_tac x = "[y]" in ballE, simp, blast)
839 lemma inj_map[iff]: "inj (map f) = inj f"
840 by (blast dest: inj_mapD intro: inj_mapI)
842 lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
844 apply(erule map_inj_on)
845 apply(blast intro:inj_onI dest:inj_onD)
848 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
851 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
854 lemma map_fst_zip[simp]:
855 "length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs"
856 by (induct rule:list_induct2, simp_all)
858 lemma map_snd_zip[simp]:
859 "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
860 by (induct rule:list_induct2, simp_all)
863 subsubsection {* @{text rev} *}
865 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
868 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
871 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
874 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
877 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
880 lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
883 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
886 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
887 apply (induct xs arbitrary: ys, force)
888 apply (case_tac ys, simp, force)
891 lemma inj_on_rev[iff]: "inj_on rev A"
892 by(simp add:inj_on_def)
894 lemma rev_induct [case_names Nil snoc]:
895 "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
896 apply(simplesubst rev_rev_ident[symmetric])
897 apply(rule_tac list = "rev xs" in list.induct, simp_all)
900 lemma rev_exhaust [case_names Nil snoc]:
901 "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"
902 by (induct xs rule: rev_induct) auto
904 lemmas rev_cases = rev_exhaust
906 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
907 by(rule rev_cases[of xs]) auto
910 subsubsection {* @{text set} *}
912 lemma finite_set [iff]: "finite (set xs)"
915 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)"
918 lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs"
921 lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
924 lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs"
927 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
930 lemma set_empty2[iff]: "({} = set xs) = (xs = [])"
933 lemma set_rev [simp]: "set (rev xs) = set xs"
936 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
939 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
942 lemma set_upt [simp]: "set[i..<j] = {i..<j}"
943 by (induct j) (simp_all add: atLeastLessThanSuc)
946 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
948 case Nil thus ?case by simp
950 case Cons thus ?case by (auto intro: Cons_eq_appendI)
953 lemma in_set_conv_decomp: "x \<in> set xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"
954 by (auto elim: split_list)
956 lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
958 case Nil thus ?case by simp
963 assume "x = a" thus ?case using Cons by fastsimp
965 assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
969 lemma in_set_conv_decomp_first:
970 "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
971 by (auto dest!: split_list_first)
973 lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
974 proof (induct xs rule:rev_induct)
975 case Nil thus ?case by simp
980 assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
982 assume "x \<noteq> a" thus ?case using snoc by fastsimp
986 lemma in_set_conv_decomp_last:
987 "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
988 by (auto dest!: split_list_last)
990 lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x"
992 case Nil thus ?case by simp
995 by(simp add:Bex_def)(metis append_Cons append.simps(1))
998 lemma split_list_propE:
999 assumes "\<exists>x \<in> set xs. P x"
1000 obtains ys x zs where "xs = ys @ x # zs" and "P x"
1001 using split_list_prop [OF assms] by blast
1003 lemma split_list_first_prop:
1004 "\<exists>x \<in> set xs. P x \<Longrightarrow>
1005 \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)"
1007 case Nil thus ?case by simp
1013 thus ?thesis by simp
1014 (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
1017 hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
1018 thus ?thesis using `\<not> P x` Cons(1) by (metis append_Cons set_ConsD)
1022 lemma split_list_first_propE:
1023 assumes "\<exists>x \<in> set xs. P x"
1024 obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y"
1025 using split_list_first_prop [OF assms] by blast
1027 lemma split_list_first_prop_iff:
1028 "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
1029 (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))"
1030 by (rule, erule split_list_first_prop) auto
1032 lemma split_list_last_prop:
1033 "\<exists>x \<in> set xs. P x \<Longrightarrow>
1034 \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)"
1035 proof(induct xs rule:rev_induct)
1036 case Nil thus ?case by simp
1041 assume "P x" thus ?thesis by (metis emptyE set_empty)
1044 hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
1045 thus ?thesis using `\<not> P x` snoc(1) by fastsimp
1049 lemma split_list_last_propE:
1050 assumes "\<exists>x \<in> set xs. P x"
1051 obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z"
1052 using split_list_last_prop [OF assms] by blast
1054 lemma split_list_last_prop_iff:
1055 "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
1056 (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
1057 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)
1059 lemma finite_list: "finite A ==> EX xs. set xs = A"
1060 by (erule finite_induct)
1061 (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))
1063 lemma card_length: "card (set xs) \<le> length xs"
1064 by (induct xs) (auto simp add: card_insert_if)
1066 lemma set_minus_filter_out:
1067 "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
1071 subsubsection {* @{text filter} *}
1073 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
1076 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"
1077 by (induct xs) simp_all
1079 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
1082 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
1083 by (induct xs) (auto simp add: le_SucI)
1085 lemma sum_length_filter_compl:
1086 "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
1087 by(induct xs) simp_all
1089 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
1092 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
1095 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
1096 by (induct xs) simp_all
1098 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
1101 apply(cut_tac P=P and xs=xs in length_filter_le)
1106 "filter P (map f xs) = map f (filter (P o f) xs)"
1107 by (induct xs) simp_all
1109 lemma length_filter_map[simp]:
1110 "length (filter P (map f xs)) = length(filter (P o f) xs)"
1111 by (simp add:filter_map)
1113 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
1116 lemma length_filter_less:
1117 "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
1119 case Nil thus ?case by simp
1121 case (Cons x xs) thus ?case
1122 apply (auto split:split_if_asm)
1123 using length_filter_le[of P xs] apply arith
1127 lemma length_filter_conv_card:
1128 "length(filter p xs) = card{i. i < length xs & p(xs!i)}"
1130 case Nil thus ?case by simp
1133 let ?S = "{i. i < length xs & p(xs!i)}"
1134 have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)
1135 show ?case (is "?l = card ?S'")
1138 hence eq: "?S' = insert 0 (Suc ` ?S)"
1139 by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
1140 have "length (filter p (x # xs)) = Suc(card ?S)"
1141 using Cons `p x` by simp
1142 also have "\<dots> = Suc(card(Suc ` ?S))" using fin
1143 by (simp add: card_image inj_Suc)
1144 also have "\<dots> = card ?S'" using eq fin
1145 by (simp add:card_insert_if) (simp add:image_def)
1146 finally show ?thesis .
1149 hence eq: "?S' = Suc ` ?S"
1150 by(auto simp add: image_def split:nat.split elim:lessE)
1151 have "length (filter p (x # xs)) = card ?S"
1152 using Cons `\<not> p x` by simp
1153 also have "\<dots> = card(Suc ` ?S)" using fin
1154 by (simp add: card_image inj_Suc)
1155 also have "\<dots> = card ?S'" using eq fin
1156 by (simp add:card_insert_if)
1157 finally show ?thesis .
1161 lemma Cons_eq_filterD:
1162 "x#xs = filter P ys \<Longrightarrow>
1163 \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
1164 (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
1166 case Nil thus ?case by simp
1169 show ?case (is "\<exists>x. ?Q x")
1175 with Py Cons.prems have "?Q []" by simp
1176 then show ?thesis ..
1178 assume "x \<noteq> y"
1179 with Py Cons.prems show ?thesis by simp
1183 with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
1184 then have "?Q (y#us)" by simp
1185 then show ?thesis ..
1189 lemma filter_eq_ConsD:
1190 "filter P ys = x#xs \<Longrightarrow>
1191 \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
1192 by(rule Cons_eq_filterD) simp
1194 lemma filter_eq_Cons_iff:
1195 "(filter P ys = x#xs) =
1196 (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
1197 by(auto dest:filter_eq_ConsD)
1199 lemma Cons_eq_filter_iff:
1200 "(x#xs = filter P ys) =
1201 (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
1202 by(auto dest:Cons_eq_filterD)
1204 lemma filter_cong[fundef_cong, recdef_cong]:
1205 "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
1207 apply(erule thin_rl)
1208 by (induct ys) simp_all
1211 subsubsection {* List partitioning *}
1213 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
1214 "partition P [] = ([], [])"
1215 | "partition P (x # xs) =
1216 (let (yes, no) = partition P xs
1217 in if P x then (x # yes, no) else (yes, x # no))"
1219 lemma partition_filter1:
1220 "fst (partition P xs) = filter P xs"
1221 by (induct xs) (auto simp add: Let_def split_def)
1223 lemma partition_filter2:
1224 "snd (partition P xs) = filter (Not o P) xs"
1225 by (induct xs) (auto simp add: Let_def split_def)
1228 assumes "partition P xs = (yes, no)"
1229 shows "(\<forall>p \<in> set yes. P p) \<and> (\<forall>p \<in> set no. \<not> P p)"
1231 from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
1233 then show ?thesis by (simp_all add: partition_filter1 partition_filter2)
1236 lemma partition_set:
1237 assumes "partition P xs = (yes, no)"
1238 shows "set yes \<union> set no = set xs"
1240 from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
1242 then show ?thesis by (auto simp add: partition_filter1 partition_filter2)
1245 lemma partition_filter_conv[simp]:
1246 "partition f xs = (filter f xs,filter (Not o f) xs)"
1247 unfolding partition_filter2[symmetric]
1248 unfolding partition_filter1[symmetric] by simp
1250 declare partition.simps[simp del]
1253 subsubsection {* @{text concat} *}
1255 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
1258 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
1259 by (induct xss) auto
1261 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
1262 by (induct xss) auto
1264 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
1267 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
1270 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
1273 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
1276 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
1280 subsubsection {* @{text nth} *}
1282 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
1285 lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
1288 declare nth.simps [simp del]
1291 "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
1292 apply (induct xs arbitrary: n, simp)
1293 apply (case_tac n, auto)
1296 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
1299 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
1302 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
1303 apply (induct xs arbitrary: n, simp)
1304 apply (case_tac n, auto)
1307 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
1308 by(cases xs) simp_all
1311 lemma list_eq_iff_nth_eq:
1312 "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
1313 apply(induct xs arbitrary: ys)
1317 apply(simp add:nth_Cons split:nat.split)apply blast
1320 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
1321 apply (induct xs, simp, simp)
1323 apply (metis nat_case_0 nth.simps zero_less_Suc)
1324 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
1325 apply (case_tac i, simp)
1326 apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
1329 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
1330 by(auto simp:set_conv_nth)
1332 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
1333 by (auto simp add: set_conv_nth)
1335 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"
1336 by (auto simp add: set_conv_nth)
1338 lemma all_nth_imp_all_set:
1339 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"
1340 by (auto simp add: set_conv_nth)
1342 lemma all_set_conv_all_nth:
1343 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"
1344 by (auto simp add: set_conv_nth)
1347 "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
1348 proof (induct xs arbitrary: n)
1349 case Nil thus ?case by simp
1352 hence n: "n < Suc (length xs)" by simp
1354 { assume "n < length xs"
1355 with n obtain n' where "length xs - n = Suc n'"
1356 by (cases "length xs - n", auto)
1358 then have "length xs - Suc n = n'" by simp
1360 have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
1363 show ?case by (clarsimp simp add: Cons nth_append)
1366 lemma Skolem_list_nth:
1367 "(ALL i<k. EX x. P i x) = (EX xs. size xs = k & (ALL i<k. P i (xs!i)))"
1368 (is "_ = (EX xs. ?P k xs)")
1370 case 0 show ?case by simp
1373 show ?case (is "?L = ?R" is "_ = (EX xs. ?P' xs)")
1375 assume "?R" thus "?L" using Suc by auto
1378 with Suc obtain x xs where "?P k xs & P k x" by (metis less_Suc_eq)
1379 hence "?P'(xs@[x])" by(simp add:nth_append less_Suc_eq)
1385 subsubsection {* @{text list_update} *}
1387 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
1388 by (induct xs arbitrary: i) (auto split: nat.split)
1390 lemma nth_list_update:
1391 "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
1392 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
1394 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
1395 by (simp add: nth_list_update)
1397 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
1398 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
1400 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
1401 by (induct xs arbitrary: i) (simp_all split:nat.splits)
1403 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
1404 apply (induct xs arbitrary: i)
1410 lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"
1411 by(metis length_0_conv length_list_update)
1413 lemma list_update_same_conv:
1414 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
1415 by (induct xs arbitrary: i) (auto split: nat.split)
1417 lemma list_update_append1:
1418 "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
1419 apply (induct xs arbitrary: i, simp)
1420 apply(simp split:nat.split)
1423 lemma list_update_append:
1424 "(xs @ ys) [n:= x] =
1425 (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
1426 by (induct xs arbitrary: n) (auto split:nat.splits)
1428 lemma list_update_length [simp]:
1429 "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
1430 by (induct xs, auto)
1432 lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"
1433 by(induct xs arbitrary: k)(auto split:nat.splits)
1436 "k < length xs \<Longrightarrow> rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"
1437 by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
1440 "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
1441 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
1443 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
1444 by (induct xs arbitrary: i) (auto split: nat.split)
1446 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
1447 by (blast dest!: set_update_subset_insert [THEN subsetD])
1449 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
1450 by (induct xs arbitrary: n) (auto split:nat.splits)
1452 lemma list_update_overwrite[simp]:
1453 "xs [i := x, i := y] = xs [i := y]"
1454 apply (induct xs arbitrary: i) apply simp
1455 apply (case_tac i, simp_all)
1458 lemma list_update_swap:
1459 "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
1460 apply (induct xs arbitrary: i i')
1462 apply (case_tac i, case_tac i')
1468 lemma list_update_code [code]:
1470 "(x # xs)[0 := y] = y # xs"
1471 "(x # xs)[Suc i := y] = x # xs[i := y]"
1475 subsubsection {* @{text last} and @{text butlast} *}
1477 lemma last_snoc [simp]: "last (xs @ [x]) = x"
1480 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
1483 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
1484 by(simp add:last.simps)
1486 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
1487 by(simp add:last.simps)
1489 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
1490 by (induct xs) (auto)
1492 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
1493 by(simp add:last_append)
1495 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
1496 by(simp add:last_append)
1498 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
1499 by(rule rev_exhaust[of xs]) simp_all
1501 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
1502 by(cases xs) simp_all
1504 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
1507 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
1508 by (induct xs rule: rev_induct) auto
1510 lemma butlast_append:
1511 "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
1512 by (induct xs arbitrary: ys) auto
1514 lemma append_butlast_last_id [simp]:
1515 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
1518 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
1519 by (induct xs) (auto split: split_if_asm)
1521 lemma in_set_butlast_appendI:
1522 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
1523 by (auto dest: in_set_butlastD simp add: butlast_append)
1525 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
1526 apply (induct xs arbitrary: n)
1528 apply (auto split:nat.split)
1531 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
1532 by(induct xs)(auto simp:neq_Nil_conv)
1534 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
1535 by (induct xs, simp, case_tac xs, simp_all)
1537 lemma last_list_update:
1538 "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
1539 by (auto simp: last_conv_nth)
1541 lemma butlast_list_update:
1542 "butlast(xs[k:=x]) =
1543 (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"
1544 apply(cases xs rule:rev_cases)
1546 apply(simp add:list_update_append split:nat.splits)
1550 "xs \<noteq> [] \<Longrightarrow> last (map f xs) = f (last xs)"
1551 by (cases xs rule: rev_cases) simp_all
1554 "map f (butlast xs) = butlast (map f xs)"
1555 by (induct xs) simp_all
1558 subsubsection {* @{text take} and @{text drop} *}
1560 lemma take_0 [simp]: "take 0 xs = []"
1563 lemma drop_0 [simp]: "drop 0 xs = xs"
1566 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
1569 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
1572 declare take_Cons [simp del] and drop_Cons [simp del]
1574 lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"
1575 unfolding One_nat_def by simp
1577 lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"
1578 unfolding One_nat_def by simp
1580 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
1581 by(clarsimp simp add:neq_Nil_conv)
1583 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
1584 by(cases xs, simp_all)
1586 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
1587 by (induct xs arbitrary: n) simp_all
1589 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
1590 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
1592 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
1593 by (cases n, simp, cases xs, auto)
1595 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
1596 by (simp only: drop_tl)
1598 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
1599 apply (induct xs arbitrary: n, simp)
1600 apply(simp add:drop_Cons nth_Cons split:nat.splits)
1603 lemma take_Suc_conv_app_nth:
1604 "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
1605 apply (induct xs arbitrary: i, simp)
1606 apply (case_tac i, auto)
1609 lemma drop_Suc_conv_tl:
1610 "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
1611 apply (induct xs arbitrary: i, simp)
1612 apply (case_tac i, auto)
1615 lemma length_take [simp]: "length (take n xs) = min (length xs) n"
1616 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1618 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
1619 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1621 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
1622 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1624 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
1625 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1627 lemma take_append [simp]:
1628 "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
1629 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1631 lemma drop_append [simp]:
1632 "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
1633 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1635 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
1636 apply (induct m arbitrary: xs n, auto)
1637 apply (case_tac xs, auto)
1638 apply (case_tac n, auto)
1641 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
1642 apply (induct m arbitrary: xs, auto)
1643 apply (case_tac xs, auto)
1646 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
1647 apply (induct m arbitrary: xs n, auto)
1648 apply (case_tac xs, auto)
1651 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
1652 apply(induct xs arbitrary: m n)
1654 apply(simp add: take_Cons drop_Cons split:nat.split)
1657 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
1658 apply (induct n arbitrary: xs, auto)
1659 apply (case_tac xs, auto)
1662 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
1663 apply(induct xs arbitrary: n)
1665 apply(simp add:take_Cons split:nat.split)
1668 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
1669 apply(induct xs arbitrary: n)
1671 apply(simp add:drop_Cons split:nat.split)
1674 lemma take_map: "take n (map f xs) = map f (take n xs)"
1675 apply (induct n arbitrary: xs, auto)
1676 apply (case_tac xs, auto)
1679 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
1680 apply (induct n arbitrary: xs, auto)
1681 apply (case_tac xs, auto)
1684 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
1685 apply (induct xs arbitrary: i, auto)
1686 apply (case_tac i, auto)
1689 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
1690 apply (induct xs arbitrary: i, auto)
1691 apply (case_tac i, auto)
1694 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
1695 apply (induct xs arbitrary: i n, auto)
1696 apply (case_tac n, blast)
1697 apply (case_tac i, auto)
1700 lemma nth_drop [simp]:
1701 "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
1702 apply (induct n arbitrary: xs i, auto)
1703 apply (case_tac xs, auto)
1707 "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
1708 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
1710 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
1711 by (simp add: butlast_conv_take drop_take add_ac)
1713 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
1714 by (simp add: butlast_conv_take min_max.inf_absorb1)
1716 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
1717 by (simp add: butlast_conv_take drop_take add_ac)
1719 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
1720 by(simp add: hd_conv_nth)
1722 lemma set_take_subset_set_take:
1723 "m <= n \<Longrightarrow> set(take m xs) <= set(take n xs)"
1724 by(induct xs arbitrary: m n)(auto simp:take_Cons split:nat.split)
1726 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
1727 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
1729 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
1730 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
1732 lemma set_drop_subset_set_drop:
1733 "m >= n \<Longrightarrow> set(drop m xs) <= set(drop n xs)"
1734 apply(induct xs arbitrary: m n)
1735 apply(auto simp:drop_Cons split:nat.split)
1736 apply (metis set_drop_subset subset_iff)
1739 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
1740 using set_take_subset by fast
1742 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
1743 using set_drop_subset by fast
1745 lemma append_eq_conv_conj:
1746 "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
1747 apply (induct xs arbitrary: zs, simp, clarsimp)
1748 apply (case_tac zs, auto)
1752 "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
1753 apply (induct xs arbitrary: i, auto)
1754 apply (case_tac i, simp_all)
1757 lemma append_eq_append_conv_if:
1758 "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
1759 (if size xs\<^isub>1 \<le> size ys\<^isub>1
1760 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
1761 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)"
1762 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
1764 apply(case_tac ys\<^isub>1)
1769 "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs"
1770 apply(induct xs arbitrary: n)
1772 apply(simp add:drop_Cons split:nat.split)
1775 lemma id_take_nth_drop:
1776 "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs"
1778 assume si: "i < length xs"
1779 hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
1781 from si have "take (Suc i) xs = take i xs @ [xs!i]"
1782 apply (rule_tac take_Suc_conv_app_nth) by arith
1783 ultimately show ?thesis by auto
1786 lemma upd_conv_take_nth_drop:
1787 "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
1789 assume i: "i < length xs"
1790 have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"
1791 by(rule arg_cong[OF id_take_nth_drop[OF i]])
1792 also have "\<dots> = take i xs @ a # drop (Suc i) xs"
1793 using i by (simp add: list_update_append)
1794 finally show ?thesis .
1798 "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
1799 apply (induct i arbitrary: xs)
1800 apply (simp add: neq_Nil_conv)
1808 subsubsection {* @{text takeWhile} and @{text dropWhile} *}
1810 lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
1813 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
1816 lemma takeWhile_append1 [simp]:
1817 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"
1820 lemma takeWhile_append2 [simp]:
1821 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
1824 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
1827 lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> takeWhile P xs ! j = xs ! j"
1828 apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
1830 lemma dropWhile_nth: "j < length (dropWhile P xs) \<Longrightarrow> dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))"
1831 apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
1833 lemma length_dropWhile_le: "length (dropWhile P xs) \<le> length xs"
1836 lemma dropWhile_append1 [simp]:
1837 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
1840 lemma dropWhile_append2 [simp]:
1841 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
1844 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
1845 by (induct xs) (auto split: split_if_asm)
1847 lemma takeWhile_eq_all_conv[simp]:
1848 "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
1851 lemma dropWhile_eq_Nil_conv[simp]:
1852 "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
1855 lemma dropWhile_eq_Cons_conv:
1856 "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
1859 lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
1860 by (induct xs) (auto dest: set_takeWhileD)
1862 lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
1865 lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \<circ> f) xs)"
1868 lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \<circ> f) xs)"
1871 lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"
1874 lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"
1878 "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
1879 using assms by (induct xs) auto
1881 lemma takeWhile_eq_filter:
1882 assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
1883 shows "takeWhile P xs = filter P xs"
1885 have A: "filter P xs = filter P (takeWhile P xs @ dropWhile P xs)"
1887 have B: "filter P (dropWhile P xs) = []"
1888 unfolding filter_empty_conv using assms by blast
1889 have "filter P xs = takeWhile P xs"
1890 unfolding A filter_append B
1891 by (auto simp add: filter_id_conv dest: set_takeWhileD)
1895 lemma takeWhile_eq_take_P_nth:
1896 "\<lbrakk> \<And> i. \<lbrakk> i < n ; i < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) ; n < length xs \<Longrightarrow> \<not> P (xs ! n) \<rbrakk> \<Longrightarrow>
1897 takeWhile P xs = take n xs"
1898 proof (induct xs arbitrary: n)
1902 case (Suc n') note this[simp]
1903 have "P x" using Cons.prems(1)[of 0] by simp
1904 moreover have "takeWhile P xs = take n' xs"
1905 proof (rule Cons.hyps)
1906 case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
1907 next case goal2 thus ?case using Cons by auto
1909 ultimately show ?thesis by simp
1913 lemma nth_length_takeWhile:
1914 "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
1917 lemma length_takeWhile_less_P_nth:
1918 assumes all: "\<And> i. i < j \<Longrightarrow> P (xs ! i)" and "j \<le> length xs"
1919 shows "j \<le> length (takeWhile P xs)"
1920 proof (rule classical)
1921 assume "\<not> ?thesis"
1922 hence "length (takeWhile P xs) < length xs" using assms by simp
1923 thus ?thesis using all `\<not> ?thesis` nth_length_takeWhile[of P xs] by auto
1926 text{* The following two lemmmas could be generalized to an arbitrary
1929 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1930 takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
1931 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
1933 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1934 dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
1938 apply(subst dropWhile_append2)
1942 lemma takeWhile_not_last:
1943 "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
1950 lemma takeWhile_cong [fundef_cong, recdef_cong]:
1951 "[| l = k; !!x. x : set l ==> P x = Q x |]
1952 ==> takeWhile P l = takeWhile Q k"
1953 by (induct k arbitrary: l) (simp_all)
1955 lemma dropWhile_cong [fundef_cong, recdef_cong]:
1956 "[| l = k; !!x. x : set l ==> P x = Q x |]
1957 ==> dropWhile P l = dropWhile Q k"
1958 by (induct k arbitrary: l, simp_all)
1961 subsubsection {* @{text zip} *}
1963 lemma zip_Nil [simp]: "zip [] ys = []"
1966 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
1969 declare zip_Cons [simp del]
1974 "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
1975 by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+
1978 "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
1979 by(auto split:list.split)
1981 lemma length_zip [simp]:
1982 "length (zip xs ys) = min (length xs) (length ys)"
1983 by (induct xs ys rule:list_induct2') auto
1985 lemma zip_obtain_same_length:
1986 assumes "\<And>zs ws n. length zs = length ws \<Longrightarrow> n = min (length xs) (length ys)
1987 \<Longrightarrow> zs = take n xs \<Longrightarrow> ws = take n ys \<Longrightarrow> P (zip zs ws)"
1988 shows "P (zip xs ys)"
1990 let ?n = "min (length xs) (length ys)"
1991 have "P (zip (take ?n xs) (take ?n ys))"
1992 by (rule assms) simp_all
1993 moreover have "zip xs ys = zip (take ?n xs) (take ?n ys)"
1994 proof (induct xs arbitrary: ys)
1995 case Nil then show ?case by simp
1997 case (Cons x xs) then show ?case by (cases ys) simp_all
1999 ultimately show ?thesis by simp
2004 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
2005 by (induct xs zs rule:list_induct2') auto
2009 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
2010 by (induct xs ys rule:list_induct2') auto
2012 lemma zip_append [simp]:
2013 "[| length xs = length us; length ys = length vs |] ==>
2014 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
2015 by (simp add: zip_append1)
2018 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
2019 by (induct rule:list_induct2, simp_all)
2022 "zip (map f xs) (map g ys) = map (\<lambda> (x, y). (f x, g y)) (zip xs ys)"
2023 proof (induct xs arbitrary: ys)
2024 case (Cons x xs) note Cons_x_xs = Cons.hyps
2028 show ?thesis unfolding Cons using Cons_x_xs by simp
2033 "zip (map f xs) ys = map (\<lambda>(x, y). (f x, y)) (zip xs ys)"
2034 using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
2037 "zip xs (map f ys) = map (\<lambda>(x, y). (x, f y)) (zip xs ys)"
2038 using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
2041 "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
2042 unfolding zip_map1 by auto
2045 "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
2046 unfolding zip_map2 by auto
2048 text{* Courtesy of Andreas Lochbihler: *}
2049 lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
2052 lemma nth_zip [simp]:
2053 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
2054 apply (induct ys arbitrary: i xs, simp)
2056 apply (simp_all add: nth.simps split: nat.split)
2060 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
2061 by(simp add: set_conv_nth cong: rev_conj_cong)
2063 lemma zip_same: "((a,b) \<in> set (zip xs xs)) = (a \<in> set xs \<and> a = b)"
2067 "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
2068 by(rule sym, simp add: update_zip)
2070 lemma zip_replicate [simp]:
2071 "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
2072 apply (induct i arbitrary: j, auto)
2073 apply (case_tac j, auto)
2077 "take n (zip xs ys) = zip (take n xs) (take n ys)"
2078 apply (induct n arbitrary: xs ys)
2080 apply (case_tac xs, simp)
2081 apply (case_tac ys, simp_all)
2085 "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
2086 apply (induct n arbitrary: xs ys)
2088 apply (case_tac xs, simp)
2089 apply (case_tac ys, simp_all)
2092 lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \<circ> fst) (zip xs ys)"
2093 proof (induct xs arbitrary: ys)
2094 case (Cons x xs) thus ?case by (cases ys) auto
2097 lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \<circ> snd) (zip xs ys)"
2098 proof (induct xs arbitrary: ys)
2099 case (Cons x xs) thus ?case by (cases ys) auto
2102 lemma set_zip_leftD:
2103 "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
2104 by (induct xs ys rule:list_induct2') auto
2106 lemma set_zip_rightD:
2107 "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
2108 by (induct xs ys rule:list_induct2') auto
2111 "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
2112 by(blast dest: set_zip_leftD set_zip_rightD)
2114 lemma zip_map_fst_snd:
2115 "zip (map fst zs) (map snd zs) = zs"
2116 by (induct zs) simp_all
2119 "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
2120 by (auto simp add: zip_map_fst_snd)
2122 lemma distinct_zipI1:
2123 "distinct xs \<Longrightarrow> distinct (zip xs ys)"
2124 proof (induct xs arbitrary: ys)
2129 have "(x, y) \<notin> set (zip xs ys')"
2130 using Cons.prems by (auto simp: set_zip)
2132 unfolding Cons zip_Cons_Cons distinct.simps
2133 using Cons.hyps Cons.prems by simp
2137 lemma distinct_zipI2:
2138 "distinct xs \<Longrightarrow> distinct (zip xs ys)"
2139 proof (induct xs arbitrary: ys)
2144 have "(x, y) \<notin> set (zip xs ys')"
2145 using Cons.prems by (auto simp: set_zip)
2147 unfolding Cons zip_Cons_Cons distinct.simps
2148 using Cons.hyps Cons.prems by simp
2153 subsubsection {* @{text list_all2} *}
2155 lemma list_all2_lengthD [intro?]:
2156 "list_all2 P xs ys ==> length xs = length ys"
2157 by (simp add: list_all2_def)
2159 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
2160 by (simp add: list_all2_def)
2162 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
2163 by (simp add: list_all2_def)
2165 lemma list_all2_Cons [iff, code]:
2166 "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
2167 by (auto simp add: list_all2_def)
2169 lemma list_all2_Cons1:
2170 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
2173 lemma list_all2_Cons2:
2174 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
2177 lemma list_all2_rev [iff]:
2178 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
2179 by (simp add: list_all2_def zip_rev cong: conj_cong)
2181 lemma list_all2_rev1:
2182 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
2183 by (subst list_all2_rev [symmetric]) simp
2185 lemma list_all2_append1:
2186 "list_all2 P (xs @ ys) zs =
2187 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
2188 list_all2 P xs us \<and> list_all2 P ys vs)"
2189 apply (simp add: list_all2_def zip_append1)
2191 apply (rule_tac x = "take (length xs) zs" in exI)
2192 apply (rule_tac x = "drop (length xs) zs" in exI)
2193 apply (force split: nat_diff_split simp add: min_def, clarify)
2194 apply (simp add: ball_Un)
2197 lemma list_all2_append2:
2198 "list_all2 P xs (ys @ zs) =
2199 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
2200 list_all2 P us ys \<and> list_all2 P vs zs)"
2201 apply (simp add: list_all2_def zip_append2)
2203 apply (rule_tac x = "take (length ys) xs" in exI)
2204 apply (rule_tac x = "drop (length ys) xs" in exI)
2205 apply (force split: nat_diff_split simp add: min_def, clarify)
2206 apply (simp add: ball_Un)
2209 lemma list_all2_append:
2210 "length xs = length ys \<Longrightarrow>
2211 list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
2212 by (induct rule:list_induct2, simp_all)
2214 lemma list_all2_appendI [intro?, trans]:
2215 "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
2216 by (simp add: list_all2_append list_all2_lengthD)
2218 lemma list_all2_conv_all_nth:
2219 "list_all2 P xs ys =
2220 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
2221 by (force simp add: list_all2_def set_zip)
2223 lemma list_all2_trans:
2224 assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
2225 shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
2226 (is "!!bs cs. PROP ?Q as bs cs")
2228 fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
2229 show "!!cs. PROP ?Q (x # xs) bs cs"
2231 fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"
2232 show "PROP ?Q (x # xs) (y # ys) cs"
2233 by (induct cs) (auto intro: tr I1 I2)
2237 lemma list_all2_all_nthI [intro?]:
2238 "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
2239 by (simp add: list_all2_conv_all_nth)
2242 "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
2243 by (simp add: list_all2_def)
2245 lemma list_all2_nthD:
2246 "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
2247 by (simp add: list_all2_conv_all_nth)
2249 lemma list_all2_nthD2:
2250 "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
2251 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
2253 lemma list_all2_map1:
2254 "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
2255 by (simp add: list_all2_conv_all_nth)
2257 lemma list_all2_map2:
2258 "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
2259 by (auto simp add: list_all2_conv_all_nth)
2261 lemma list_all2_refl [intro?]:
2262 "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
2263 by (simp add: list_all2_conv_all_nth)
2265 lemma list_all2_update_cong:
2266 "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
2267 by (simp add: list_all2_conv_all_nth nth_list_update)
2269 lemma list_all2_update_cong2:
2270 "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
2271 by (simp add: list_all2_lengthD list_all2_update_cong)
2273 lemma list_all2_takeI [simp,intro?]:
2274 "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
2275 apply (induct xs arbitrary: n ys)
2277 apply (clarsimp simp add: list_all2_Cons1)
2282 lemma list_all2_dropI [simp,intro?]:
2283 "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
2284 apply (induct as arbitrary: n bs, simp)
2285 apply (clarsimp simp add: list_all2_Cons1)
2286 apply (case_tac n, simp, simp)
2289 lemma list_all2_mono [intro?]:
2290 "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
2291 apply (induct xs arbitrary: ys, simp)
2292 apply (case_tac ys, auto)
2296 "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
2297 by (induct xs ys rule: list_induct2') auto
2300 subsubsection {* @{text foldl} and @{text foldr} *}
2302 lemma foldl_append [simp]:
2303 "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
2304 by (induct xs arbitrary: a) auto
2306 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
2309 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
2310 by(induct xs) simp_all
2312 text{* For efficient code generation: avoid intermediate list. *}
2313 lemma foldl_map[code_unfold]:
2314 "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
2315 by(induct xs arbitrary:a) simp_all
2318 assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"
2319 shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
2320 by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: expand_fun_eq)
2322 lemma foldl_cong [fundef_cong, recdef_cong]:
2323 "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
2324 ==> foldl f a l = foldl g b k"
2325 by (induct k arbitrary: a b l) simp_all
2327 lemma foldr_cong [fundef_cong, recdef_cong]:
2328 "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]
2329 ==> foldr f l a = foldr g k b"
2330 by (induct k arbitrary: a b l) simp_all
2332 lemma foldl_fun_comm:
2333 assumes "\<And>x y s. f (f s x) y = f (f s y) x"
2334 shows "f (foldl f s xs) x = foldl f (f s x) xs"
2335 by (induct xs arbitrary: s)
2336 (simp_all add: assms)
2338 lemma (in semigroup_add) foldl_assoc:
2339 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
2340 by (induct zs arbitrary: y) (simp_all add:add_assoc)
2342 lemma (in monoid_add) foldl_absorb0:
2343 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
2344 by (induct zs) (simp_all add:foldl_assoc)
2347 assumes "\<And>x y s. f (f s x) y = f (f s y) x"
2348 shows "foldl f s (rev xs) = foldl f s xs"
2349 proof (induct xs arbitrary: s)
2350 case Nil then show ?case by simp
2352 case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
2355 lemma rev_foldl_cons [code]:
2356 "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
2358 case Nil then show ?case by simp
2363 have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
2364 = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
2365 by (induct xs arbitrary: ys) auto
2368 show ?case by (induct xs) (auto simp add: Cons aux)
2372 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
2374 lemma foldl_foldr1_lemma:
2375 "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
2376 by (induct xs arbitrary: a) (auto simp:add_assoc)
2378 corollary foldl_foldr1:
2379 "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
2380 by (simp add:foldl_foldr1_lemma)
2383 text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
2385 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
2388 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
2389 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
2391 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
2392 by (induct xs, auto simp add: foldl_assoc add_commute)
2395 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
2396 difficult to use because it requires an additional transitivity step.
2399 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
2400 by (induct ns arbitrary: n) auto
2402 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
2403 by (force intro: start_le_sum simp add: in_set_conv_decomp)
2405 lemma sum_eq_0_conv [iff]:
2406 "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
2407 by (induct ns arbitrary: m) auto
2409 lemma foldr_invariant:
2410 "\<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)"
2411 by (induct xs, simp_all)
2413 lemma foldl_invariant:
2414 "\<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)"
2415 by (induct xs arbitrary: x, simp_all)
2417 lemma foldl_weak_invariant:
2419 and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)"
2420 shows "P (foldl f s xs)"
2421 using assms by (induct xs arbitrary: s) simp_all
2423 text {* @{const foldl} and @{const concat} *}
2425 lemma foldl_conv_concat:
2426 "foldl (op @) xs xss = xs @ concat xss"
2427 proof (induct xss arbitrary: xs)
2428 case Nil show ?case by simp
2430 interpret monoid_add "op @" "[]" proof qed simp_all
2431 case Cons then show ?case by (simp add: foldl_absorb0)
2434 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
2435 by (simp add: foldl_conv_concat)
2437 text {* @{const Finite_Set.fold} and @{const foldl} *}
2439 lemma (in fun_left_comm) fold_set_remdups:
2440 "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
2441 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
2443 lemma (in fun_left_comm_idem) fold_set:
2444 "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
2445 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
2447 lemma (in ab_semigroup_idem_mult) fold1_set:
2448 assumes "xs \<noteq> []"
2449 shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"
2451 interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
2452 from assms obtain y ys where xs: "xs = y # ys"
2455 proof (cases "set ys = {}")
2456 case True with xs show ?thesis by simp
2459 then have "fold1 times (insert y (set ys)) = fold times y (set ys)"
2460 by (simp only: finite_set fold1_eq_fold_idem)
2461 with xs show ?thesis by (simp add: fold_set mult_commute)
2465 lemma (in lattice) Inf_fin_set_fold [code_unfold]:
2466 "Inf_fin (set (x # xs)) = foldl inf x xs"
2468 interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
2469 by (fact ab_semigroup_idem_mult_inf)
2471 by (simp add: Inf_fin_def fold1_set del: set.simps)
2474 lemma (in lattice) Sup_fin_set_fold [code_unfold]:
2475 "Sup_fin (set (x # xs)) = foldl sup x xs"
2477 interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
2478 by (fact ab_semigroup_idem_mult_sup)
2480 by (simp add: Sup_fin_def fold1_set del: set.simps)
2483 lemma (in linorder) Min_fin_set_fold [code_unfold]:
2484 "Min (set (x # xs)) = foldl min x xs"
2486 interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
2487 by (fact ab_semigroup_idem_mult_min)
2489 by (simp add: Min_def fold1_set del: set.simps)
2492 lemma (in linorder) Max_fin_set_fold [code_unfold]:
2493 "Max (set (x # xs)) = foldl max x xs"
2495 interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
2496 by (fact ab_semigroup_idem_mult_max)
2498 by (simp add: Max_def fold1_set del: set.simps)
2501 lemma (in complete_lattice) Inf_set_fold [code_unfold]:
2502 "Inf (set xs) = foldl inf top xs"
2504 interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
2505 by (fact fun_left_comm_idem_inf)
2506 show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
2509 lemma (in complete_lattice) Sup_set_fold [code_unfold]:
2510 "Sup (set xs) = foldl sup bot xs"
2512 interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
2513 by (fact fun_left_comm_idem_sup)
2514 show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
2517 lemma (in complete_lattice) INFI_set_fold:
2518 "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
2519 unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map
2520 by (simp add: inf_commute)
2522 lemma (in complete_lattice) SUPR_set_fold:
2523 "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
2524 unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
2525 by (simp add: sup_commute)
2528 subsubsection {* @{text upt} *}
2530 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
2531 -- {* simp does not terminate! *}
2534 lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]
2536 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
2537 by (subst upt_rec) simp
2539 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
2540 by(induct j)simp_all
2542 lemma upt_eq_Cons_conv:
2543 "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
2544 apply(induct j arbitrary: x xs)
2546 apply(clarsimp simp add: append_eq_Cons_conv)
2550 lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
2551 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}
2554 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
2555 by (simp add: upt_rec)
2557 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
2558 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
2561 lemma length_upt [simp]: "length [i..<j] = j - i"
2562 by (induct j) (auto simp add: Suc_diff_le)
2564 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
2566 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
2570 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
2571 by(simp add:upt_conv_Cons)
2573 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
2576 by(simp add:upt_Suc_append)
2578 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
2579 apply (induct m arbitrary: i, simp)
2580 apply (subst upt_rec)
2582 apply (subst upt_rec)
2583 apply (simp del: upt.simps)
2586 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
2591 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
2594 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
2595 apply (induct n m arbitrary: i rule: diff_induct)
2596 prefer 3 apply (subst map_Suc_upt[symmetric])
2597 apply (auto simp add: less_diff_conv nth_upt)
2600 lemma nth_take_lemma:
2601 "k <= length xs ==> k <= length ys ==>
2602 (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
2603 apply (atomize, induct k arbitrary: xs ys)
2604 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
2605 txt {* Both lists must be non-empty *}
2606 apply (case_tac xs, simp)
2607 apply (case_tac ys, clarify)
2608 apply (simp (no_asm_use))
2610 txt {* prenexing's needed, not miniscoping *}
2611 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)
2615 lemma nth_equalityI:
2616 "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
2617 apply (frule nth_take_lemma [OF le_refl eq_imp_le])
2618 apply (simp_all add: take_all)
2622 "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
2623 by (rule nth_equalityI, auto)
2625 (* needs nth_equalityI *)
2626 lemma list_all2_antisym:
2627 "\<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>
2628 \<Longrightarrow> xs = ys"
2629 apply (simp add: list_all2_conv_all_nth)
2630 apply (rule nth_equalityI, blast, simp)
2633 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
2634 -- {* The famous take-lemma. *}
2635 apply (drule_tac x = "max (length xs) (length ys)" in spec)
2636 apply (simp add: le_max_iff_disj take_all)
2641 "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
2642 by (cases n) simp_all
2645 "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
2646 by (cases n) simp_all
2648 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
2649 by (cases n) simp_all
2651 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
2652 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
2653 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
2655 declare take_Cons_number_of [simp]
2656 drop_Cons_number_of [simp]
2657 nth_Cons_number_of [simp]
2660 subsubsection {* @{text upto}: interval-list on @{typ int} *}
2662 (* FIXME make upto tail recursive? *)
2664 function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
2665 "upto i j = (if i \<le> j then i # [i+1..j] else [])"
2668 by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
2670 declare upto.simps[code, simp del]
2672 lemmas upto_rec_number_of[simp] =
2673 upto.simps[of "number_of m" "number_of n", standard]
2675 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
2676 by(simp add: upto.simps)
2678 lemma set_upto[simp]: "set[i..j] = {i..j}"
2679 apply(induct i j rule:upto.induct)
2680 apply(simp add: upto.simps simp_from_to)
2684 subsubsection {* @{text "distinct"} and @{text remdups} *}
2686 lemma distinct_append [simp]:
2687 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
2690 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
2693 lemma set_remdups [simp]: "set (remdups xs) = set xs"
2694 by (induct xs) (auto simp add: insert_absorb)
2696 lemma distinct_remdups [iff]: "distinct (remdups xs)"
2699 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
2700 by (induct xs, auto)
2702 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
2703 by (metis distinct_remdups distinct_remdups_id)
2705 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
2706 by (metis distinct_remdups finite_list set_remdups)
2708 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
2711 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
2714 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
2717 lemma length_remdups_eq[iff]:
2718 "(length (remdups xs) = length xs) = (remdups xs = xs)"
2721 apply(subgoal_tac "length (remdups xs) <= length xs")
2723 apply(rule length_remdups_leq)
2726 lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
2732 "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
2736 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
2739 lemma distinct_upt[simp]: "distinct[i..<j]"
2742 lemma distinct_upto[simp]: "distinct[i..j]"
2743 apply(induct i j rule:upto.induct)
2744 apply(subst upto.simps)
2748 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
2749 apply(induct xs arbitrary: i)
2753 apply(blast dest:in_set_takeD)
2756 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
2757 apply(induct xs arbitrary: i)
2763 lemma distinct_list_update:
2764 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
2765 shows "distinct (xs[i:=a])"
2766 proof (cases "i < length xs")
2768 with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
2769 apply (drule_tac id_take_nth_drop) by simp
2770 with d True show ?thesis
2771 apply (simp add: upd_conv_take_nth_drop)
2772 apply (drule subst [OF id_take_nth_drop]) apply assumption
2773 apply simp apply (cases "a = xs!i") apply simp by blast
2775 case False with d show ?thesis by auto
2778 lemma distinct_concat:
2779 assumes "distinct xs"
2780 and "\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys"
2781 and "\<And> ys zs. \<lbrakk> ys \<in> set xs ; zs \<in> set xs ; ys \<noteq> zs \<rbrakk> \<Longrightarrow> set ys \<inter> set zs = {}"
2782 shows "distinct (concat xs)"
2783 using assms by (induct xs) auto
2785 text {* It is best to avoid this indexed version of distinct, but
2786 sometimes it is useful. *}
2788 lemma distinct_conv_nth:
2789 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
2790 apply (induct xs, simp, simp)
2791 apply (rule iffI, clarsimp)
2793 apply (case_tac j, simp)
2794 apply (simp add: set_conv_nth)
2796 apply (clarsimp simp add: set_conv_nth, simp)
2799 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
2801 apply (clarsimp simp add: set_conv_nth)
2802 apply (erule_tac x = 0 in allE, simp)
2803 apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
2805 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
2807 apply (erule_tac x = "Suc i" in allE, simp)
2808 apply (erule_tac x = "Suc j" in allE, simp)
2811 lemma nth_eq_iff_index_eq:
2812 "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
2813 by(auto simp: distinct_conv_nth)
2815 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
2818 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
2820 case Nil thus ?case by simp
2824 proof (cases "x \<in> set xs")
2825 case False with Cons show ?thesis by simp
2827 case True with Cons.prems
2828 have "card (set xs) = Suc (length xs)"
2829 by (simp add: card_insert_if split: split_if_asm)
2830 moreover have "card (set xs) \<le> length xs" by (rule card_length)
2831 ultimately have False by simp
2836 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
2837 apply (induct n == "length ws" arbitrary:ws) apply simp
2838 apply(case_tac ws) apply simp
2839 apply (simp split:split_if_asm)
2840 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
2843 lemma length_remdups_concat:
2844 "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
2845 by(simp add: set_concat distinct_card[symmetric])
2847 lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"
2849 have xs: "concat[xs] = xs" by simp
2850 from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
2853 lemma remdups_remdups:
2854 "remdups (remdups xs) = remdups xs"
2855 by (induct xs) simp_all
2857 lemma distinct_butlast:
2858 assumes "xs \<noteq> []" and "distinct xs"
2859 shows "distinct (butlast xs)"
2861 from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
2862 with `distinct xs` show ?thesis by simp
2866 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
2868 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
2869 by (induct xs) (simp_all add:add_assoc)
2871 lemma listsum_rev [simp]:
2872 fixes xs :: "'a\<Colon>comm_monoid_add list"
2873 shows "listsum (rev xs) = listsum xs"
2874 by (induct xs) (simp_all add:add_ac)
2876 lemma listsum_map_remove1:
2877 fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
2878 shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
2879 by (induct xs)(auto simp add:add_ac)
2881 lemma list_size_conv_listsum:
2882 "list_size f xs = listsum (map f xs) + size xs"
2885 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
2888 lemma length_concat: "length (concat xss) = listsum (map length xss)"
2889 by (induct xss) simp_all
2891 lemma listsum_map_filter:
2892 fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
2893 assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
2894 shows "listsum (map f (filter P xs)) = listsum (map f xs)"
2895 using assms by (induct xs) auto
2897 text{* For efficient code generation ---
2898 @{const listsum} is not tail recursive but @{const foldl} is. *}
2899 lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
2900 by(simp add:listsum_foldr foldl_foldr1)
2902 lemma distinct_listsum_conv_Setsum:
2903 "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
2904 by (induct xs) simp_all
2906 lemma listsum_eq_0_nat_iff_nat[simp]:
2907 "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
2908 by(simp add: listsum)
2910 lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)"
2911 apply(induct ns arbitrary: k)
2913 apply(fastsimp simp add:nth_Cons split: nat.split)
2916 lemma listsum_update_nat: "k<size ns \<Longrightarrow>
2917 listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"
2918 apply(induct ns arbitrary:k)
2919 apply (auto split:nat.split)
2920 apply(drule elem_le_listsum_nat)
2924 text{* Some syntactic sugar for summing a function over a list: *}
2927 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
2929 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
2930 syntax (HTML output)
2931 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
2933 translations -- {* Beware of argument permutation! *}
2934 "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
2935 "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
2937 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
2938 by (induct xs) (simp_all add: left_distrib)
2940 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
2941 by (induct xs) (simp_all add: left_distrib)
2943 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
2944 lemma uminus_listsum_map:
2945 fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
2946 shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
2947 by (induct xs) simp_all
2950 fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
2951 shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
2952 by (induct xs) (simp_all add: algebra_simps)
2954 lemma listsum_subtractf:
2955 fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
2956 shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
2957 by (induct xs) simp_all
2959 lemma listsum_const_mult:
2960 fixes f :: "'a \<Rightarrow> 'b::semiring_0"
2961 shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
2962 by (induct xs, simp_all add: algebra_simps)
2964 lemma listsum_mult_const:
2965 fixes f :: "'a \<Rightarrow> 'b::semiring_0"
2966 shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
2967 by (induct xs, simp_all add: algebra_simps)
2970 fixes xs :: "'a::ordered_ab_group_add_abs list"
2971 shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
2972 by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
2975 fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"
2976 shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"
2977 by (induct xs, simp, simp add: add_mono)
2979 lemma listsum_distinct_conv_setsum_set:
2980 "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
2981 by (induct xs) simp_all
2983 lemma interv_listsum_conv_setsum_set_nat:
2984 "listsum (map f [m..<n]) = setsum f (set [m..<n])"
2985 by (simp add: listsum_distinct_conv_setsum_set)
2987 lemma interv_listsum_conv_setsum_set_int:
2988 "listsum (map f [k..l]) = setsum f (set [k..l])"
2989 by (simp add: listsum_distinct_conv_setsum_set)
2991 text {* General equivalence between @{const listsum} and @{const setsum} *}
2992 lemma listsum_setsum_nth:
2993 "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
2994 using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
2997 subsubsection {* @{const insert} *}
2999 lemma in_set_insert [simp]:
3000 "x \<in> set xs \<Longrightarrow> List.insert x xs = xs"
3001 by (simp add: List.insert_def)
3003 lemma not_in_set_insert [simp]:
3004 "x \<notin> set xs \<Longrightarrow> List.insert x xs = x # xs"
3005 by (simp add: List.insert_def)
3007 lemma insert_Nil [simp]:
3008 "List.insert x [] = [x]"
3011 lemma set_insert [simp]:
3012 "set (List.insert x xs) = insert x (set xs)"
3013 by (auto simp add: List.insert_def)
3015 lemma distinct_insert [simp]:
3016 "distinct xs \<Longrightarrow> distinct (List.insert x xs)"
3017 by (simp add: List.insert_def)
3019 lemma insert_remdups:
3020 "List.insert x (remdups xs) = remdups (List.insert x xs)"
3021 by (simp add: List.insert_def)
3023 lemma distinct_induct [consumes 1, case_names Nil insert]:
3024 assumes "distinct xs"
3026 assumes insert: "\<And>x xs. distinct xs \<Longrightarrow> x \<notin> set xs
3027 \<Longrightarrow> P xs \<Longrightarrow> P (List.insert x xs)"
3029 using `distinct xs` proof (induct xs)
3030 case Nil from `P []` show ?case .
3033 then have "distinct xs" and "x \<notin> set xs" and "P xs" by simp_all
3034 with insert have "P (List.insert x xs)" .
3035 with `x \<notin> set xs` show ?case by simp
3039 subsubsection {* @{text remove1} *}
3041 lemma remove1_append:
3042 "remove1 x (xs @ ys) =
3043 (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
3046 lemma remove1_commute: "remove1 x (remove1 y zs) = remove1 y (remove1 x zs)"
3049 lemma in_set_remove1[simp]:
3050 "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
3055 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
3062 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
3069 lemma length_remove1:
3070 "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
3072 apply (auto dest!:length_pos_if_in_set)
3075 lemma remove1_filter_not[simp]:
3076 "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
3079 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
3080 apply(insert set_remove1_subset)
3084 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
3085 by (induct xs) simp_all
3087 lemma remove1_remdups:
3088 "distinct xs \<Longrightarrow> remove1 x (remdups xs) = remdups (remove1 x xs)"
3089 by (induct xs) simp_all
3092 assumes "x \<notin> set xs"
3093 shows "remove1 x xs = xs"
3094 using assms by (induct xs) simp_all
3097 subsubsection {* @{text removeAll} *}
3099 lemma removeAll_filter_not_eq:
3100 "removeAll x = filter (\<lambda>y. x \<noteq> y)"
3103 show "removeAll x xs = filter (\<lambda>y. x \<noteq> y) xs"
3107 lemma removeAll_append[simp]:
3108 "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
3111 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
3114 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
3117 (* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
3118 lemma length_removeAll:
3119 "length(removeAll x xs) = length xs - count x xs"
3122 lemma removeAll_filter_not[simp]:
3123 "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
3126 lemma distinct_removeAll:
3127 "distinct xs \<Longrightarrow> distinct (removeAll x xs)"
3128 by (simp add: removeAll_filter_not_eq)
3130 lemma distinct_remove1_removeAll:
3131 "distinct xs ==> remove1 x xs = removeAll x xs"
3132 by (induct xs) simp_all
3134 lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>
3135 map f (removeAll x xs) = removeAll (f x) (map f xs)"
3136 by (induct xs) (simp_all add:inj_on_def)
3138 lemma map_removeAll_inj: "inj f \<Longrightarrow>
3139 map f (removeAll x xs) = removeAll (f x) (map f xs)"
3140 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
3143 subsubsection {* @{text replicate} *}
3145 lemma length_replicate [simp]: "length (replicate n x) = n"
3148 lemma Ex_list_of_length: "\<exists>xs. length xs = n"
3149 by (rule exI[of _ "replicate n undefined"]) simp
3151 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
3154 lemma map_replicate_const:
3155 "map (\<lambda> x. k) lst = replicate (length lst) k"
3156 by (induct lst) auto
3158 lemma replicate_app_Cons_same:
3159 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
3162 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
3163 apply (induct n, simp)
3164 apply (simp add: replicate_app_Cons_same)
3167 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
3170 text{* Courtesy of Matthias Daum: *}
3171 lemma append_replicate_commute:
3172 "replicate n x @ replicate k x = replicate k x @ replicate n x"
3173 apply (simp add: replicate_add [THEN sym])
3174 apply (simp add: add_commute)
3177 text{* Courtesy of Andreas Lochbihler: *}
3178 lemma filter_replicate:
3179 "filter P (replicate n x) = (if P x then replicate n x else [])"
3182 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
3185 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"
3188 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
3189 by (atomize (full), induct n) auto
3191 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
3192 apply (induct n arbitrary: i, simp)
3193 apply (simp add: nth_Cons split: nat.split)
3196 text{* Courtesy of Matthias Daum (2 lemmas): *}
3197 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
3198 apply (case_tac "k \<le> i")
3199 apply (simp add: min_def)
3200 apply (drule not_leE)
3201 apply (simp add: min_def)
3202 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
3204 apply (simp add: replicate_add [symmetric])
3207 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
3208 apply (induct k arbitrary: i)
3217 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
3220 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
3221 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
3223 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
3226 lemma in_set_replicate[simp]: "(x : set (replicate n y)) = (x = y & n \<noteq> 0)"
3227 by (simp add: set_replicate_conv_if)
3229 lemma Ball_set_replicate[simp]:
3230 "(ALL x : set(replicate n a). P x) = (P a | n=0)"
3231 by(simp add: set_replicate_conv_if)
3233 lemma Bex_set_replicate[simp]:
3234 "(EX x : set(replicate n a). P x) = (P a & n\<noteq>0)"
3235 by(simp add: set_replicate_conv_if)
3237 lemma replicate_append_same:
3238 "replicate i x @ [x] = x # replicate i x"
3239 by (induct i) simp_all
3241 lemma map_replicate_trivial:
3242 "map (\<lambda>i. x) [0..<i] = replicate i x"
3243 by (induct i) (simp_all add: replicate_append_same)
3245 lemma concat_replicate_trivial[simp]:
3246 "concat (replicate i []) = []"
3247 by (induct i) (auto simp add: map_replicate_const)
3249 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
3252 lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"
3255 lemma replicate_eq_replicate[simp]:
3256 "(replicate m x = replicate n y) \<longleftrightarrow> (m=n & (m\<noteq>0 \<longrightarrow> x=y))"
3257 apply(induct m arbitrary: n)
3264 subsubsection{*@{text rotate1} and @{text rotate}*}
3266 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
3267 by(simp add:rotate1_def)
3269 lemma rotate0[simp]: "rotate 0 = id"
3270 by(simp add:rotate_def)
3272 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
3273 by(simp add:rotate_def)
3276 "rotate (m+n) = rotate m o rotate n"
3277 by(simp add:rotate_def funpow_add)
3279 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
3280 by(simp add:rotate_add)
3282 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
3283 by(simp add:rotate_def funpow_swap1)
3285 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
3286 by(cases xs) simp_all
3288 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
3291 apply (simp add:rotate_def)
3294 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
3295 by(simp add:rotate1_def split:list.split)
3297 lemma rotate_drop_take:
3298 "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
3301 apply(simp add:rotate_def)
3302 apply(cases "xs = []")
3304 apply(case_tac "n mod length xs = 0")
3305 apply(simp add:mod_Suc)
3306 apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
3307 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
3308 take_hd_drop linorder_not_le)
3311 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
3312 by(simp add:rotate_drop_take)
3314 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
3315 by(simp add:rotate_drop_take)
3317 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
3318 by(simp add:rotate1_def split:list.split)
3320 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
3321 by (induct n arbitrary: xs) (simp_all add:rotate_def)
3323 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
3324 by(simp add:rotate1_def split:list.split) blast
3326 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
3327 by (induct n) (simp_all add:rotate_def)
3329 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
3330 by(simp add:rotate_drop_take take_map drop_map)
3332 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
3333 by(simp add:rotate1_def split:list.split)
3335 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
3336 by (induct n) (simp_all add:rotate_def)
3338 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
3339 by(simp add:rotate1_def split:list.split)
3341 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
3342 by (induct n) (simp_all add:rotate_def)
3345 "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
3346 apply(simp add:rotate_drop_take rev_drop rev_take)
3347 apply(cases "length xs = 0")
3349 apply(cases "n mod length xs = 0")
3351 apply(simp add:rotate_drop_take rev_drop rev_take)
3354 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
3355 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
3356 apply(subgoal_tac "length xs \<noteq> 0")
3358 using mod_less_divisor[of "length xs" n] by arith
3361 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
3363 lemma sublist_empty [simp]: "sublist xs {} = []"
3364 by (auto simp add: sublist_def)
3366 lemma sublist_nil [simp]: "sublist [] A = []"
3367 by (auto simp add: sublist_def)
3369 lemma length_sublist:
3370 "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
3371 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
3373 lemma sublist_shift_lemma_Suc:
3374 "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
3375 map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
3376 apply(induct xs arbitrary: "is")
3378 apply (case_tac "is")
3383 lemma sublist_shift_lemma:
3384 "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
3385 map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
3386 by (induct xs rule: rev_induct) (simp_all add: add_commute)
3388 lemma sublist_append:
3389 "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
3390 apply (unfold sublist_def)
3391 apply (induct l' rule: rev_induct, simp)
3392 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
3393 apply (simp add: add_commute)
3397 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
3398 apply (induct l rule: rev_induct)
3399 apply (simp add: sublist_def)
3400 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
3403 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
3404 apply(induct xs arbitrary: I)
3405 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
3408 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
3409 by(auto simp add:set_sublist)
3411 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
3412 by(auto simp add:set_sublist)
3414 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
3415 by(auto simp add:set_sublist)
3417 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
3418 by (simp add: sublist_Cons)
3421 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
3422 apply(induct xs arbitrary: I)
3424 apply(auto simp add:sublist_Cons)
3428 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
3429 apply (induct l rule: rev_induct, simp)
3430 apply (simp split: nat_diff_split add: sublist_append)
3433 lemma filter_in_sublist:
3434 "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
3435 proof (induct xs arbitrary: s)
3436 case Nil thus ?case by simp
3439 moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
3440 ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
3444 subsubsection {* @{const splice} *}
3446 lemma splice_Nil2 [simp, code]:
3448 by (cases xs) simp_all
3450 lemma splice_Cons_Cons [simp, code]:
3451 "splice (x#xs) (y#ys) = x # y # splice xs ys"
3454 declare splice.simps(2) [simp del, code del]
3456 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
3457 apply(induct xs arbitrary: ys) apply simp
3463 subsubsection {* Transpose *}
3465 function transpose where
3466 "transpose [] = []" |
3467 "transpose ([] # xss) = transpose xss" |
3468 "transpose ((x#xs) # xss) =
3469 (x # [h. (h#t) \<leftarrow> xss]) # transpose (xs # [t. (h#t) \<leftarrow> xss])"
3470 by pat_completeness auto
3472 lemma transpose_aux_filter_head:
3473 "concat (map (list_case [] (\<lambda>h t. [h])) xss) =
3474 map (\<lambda>xs. hd xs) [ys\<leftarrow>xss . ys \<noteq> []]"
3475 by (induct xss) (auto split: list.split)
3477 lemma transpose_aux_filter_tail:
3478 "concat (map (list_case [] (\<lambda>h t. [t])) xss) =
3479 map (\<lambda>xs. tl xs) [ys\<leftarrow>xss . ys \<noteq> []]"
3480 by (induct xss) (auto split: list.split)
3482 lemma transpose_aux_max:
3483 "max (Suc (length xs)) (foldr (\<lambda>xs. max (length xs)) xss 0) =
3484 Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) [ys\<leftarrow>xss . ys\<noteq>[]] 0))"
3485 (is "max _ ?foldB = Suc (max _ ?foldA)")
3486 proof (cases "[ys\<leftarrow>xss . ys\<noteq>[]] = []")
3488 hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
3491 moreover hence "x = []" by (cases x) auto
3492 ultimately show ?case by auto
3494 thus ?thesis using True by simp
3498 have foldA: "?foldA = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0 - 1"
3499 by (induct xss) auto
3500 have foldB: "?foldB = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0"
3501 by (induct xss) auto
3506 obtain z zs where zs: "[ys\<leftarrow>xss . ys \<noteq> []] = z#zs" by (auto simp: neq_Nil_conv)
3507 hence "z \<in> set ([ys\<leftarrow>xss . ys \<noteq> []])" by auto
3508 hence "z \<noteq> []" by auto
3511 by (auto simp: max_def intro: less_le_trans)
3514 unfolding foldA foldB max_Suc_Suc[symmetric]
3518 termination transpose
3519 by (relation "measure (\<lambda>xs. foldr (\<lambda>xs. max (length xs)) xs 0 + length xs)")
3520 (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max less_Suc_eq_le)
3522 lemma transpose_empty: "(transpose xs = []) \<longleftrightarrow> (\<forall>x \<in> set xs. x = [])"
3523 by (induct rule: transpose.induct) simp_all
3525 lemma length_transpose:
3526 fixes xs :: "'a list list"
3527 shows "length (transpose xs) = foldr (\<lambda>xs. max (length xs)) xs 0"
3528 by (induct rule: transpose.induct)
3529 (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max
3530 max_Suc_Suc[symmetric] simp del: max_Suc_Suc)
3532 lemma nth_transpose:
3533 fixes xs :: "'a list list"
3534 assumes "i < length (transpose xs)"
3535 shows "transpose xs ! i = map (\<lambda>xs. xs ! i) [ys \<leftarrow> xs. i < length ys]"
3536 using assms proof (induct arbitrary: i rule: transpose.induct)
3538 def XS == "(x # xs) # xss"
3539 hence [simp]: "XS \<noteq> []" by auto
3543 thus ?thesis by (simp add: transpose_aux_filter_head hd_conv_nth)
3546 have *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp
3547 have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp
3548 { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"
3549 by (cases x) simp_all
3552 have j_less: "j < length (transpose (xs # concat (map (list_case [] (\<lambda>h t. [t])) xss)))"
3553 using "3.prems" by (simp add: transpose_aux_filter_tail length_transpose Suc)
3556 unfolding transpose.simps `i = Suc j` nth_Cons_Suc "3.hyps"[OF j_less]
3557 apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
3558 apply (rule_tac y=x in list.exhaust)
3563 lemma transpose_map_map:
3564 "transpose (map (map f) xs) = map (map f) (transpose xs)"
3565 proof (rule nth_equalityI, safe)
3566 have [simp]: "length (transpose (map (map f) xs)) = length (transpose xs)"
3567 by (simp add: length_transpose foldr_map comp_def)
3568 show "length (transpose (map (map f) xs)) = length (map (map f) (transpose xs))" by simp
3570 fix i assume "i < length (transpose (map (map f) xs))"
3571 thus "transpose (map (map f) xs) ! i = map (map f) (transpose xs) ! i"
3572 by (simp add: nth_transpose filter_map comp_def)
3576 subsubsection {* (In)finiteness *}
3578 lemma finite_maxlen:
3579 "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
3580 proof (induct rule: finite.induct)
3581 case emptyI show ?case by simp
3584 then obtain n where "\<forall>s\<in>M. length s < n" by blast
3585 hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
3589 lemma finite_lists_length_eq:
3591 shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")
3593 case 0 show ?case by simp
3596 have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
3597 by (auto simp:length_Suc_conv)
3598 then show ?case using `finite A`
3599 by (auto intro: finite_imageI Suc) (* FIXME metis? *)
3602 lemma finite_lists_length_le:
3603 assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
3606 have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
3607 thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
3610 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
3612 apply(drule finite_maxlen)
3613 apply (metis UNIV_I length_replicate less_not_refl)
3617 subsection {* Sorting *}
3619 text{* Currently it is not shown that @{const sort} returns a
3620 permutation of its input because the nicest proof is via multisets,
3621 which are not yet available. Alternatively one could define a function
3622 that counts the number of occurrences of an element in a list and use
3623 that instead of multisets to state the correctness property. *}
3628 lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
3629 by (induct xs, auto)
3631 lemma insort_left_comm:
3632 "insort x (insort y xs) = insort y (insort x xs)"
3635 lemma fun_left_comm_insort:
3636 "fun_left_comm insort"
3638 qed (fact insort_left_comm)
3640 lemma sort_key_simps [simp]:
3641 "sort_key f [] = []"
3642 "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
3643 by (simp_all add: sort_key_def)
3645 lemma sort_foldl_insort:
3646 "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"
3647 by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)
3649 lemma length_sort[simp]: "length (sort_key f xs) = length xs"
3650 by (induct xs, auto)
3652 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
3653 apply(induct xs arbitrary: x) apply simp
3654 by simp (blast intro: order_trans)
3656 lemma sorted_append:
3657 "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
3658 by (induct xs) (auto simp add:sorted_Cons)
3660 lemma sorted_nth_mono:
3661 "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
3662 by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
3664 lemma sorted_rev_nth_mono:
3665 "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
3666 using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
3667 rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
3670 lemma sorted_nth_monoI:
3671 "(\<And> i j. \<lbrakk> i \<le> j ; j < length xs \<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j) \<Longrightarrow> sorted xs"
3675 proof (rule Cons.hyps)
3676 fix i j assume "i \<le> j" and "j < length xs"
3677 with Cons.prems[of "Suc i" "Suc j"]
3678 show "xs ! i \<le> xs ! j" by auto
3682 fix y assume "y \<in> set xs"
3683 then obtain j where "j < length xs" and "xs ! j = y"
3684 unfolding in_set_conv_nth by blast
3685 with Cons.prems[of 0 "Suc j"]
3691 unfolding sorted_Cons by auto
3694 lemma sorted_equals_nth_mono:
3695 "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
3696 by (auto intro: sorted_nth_monoI sorted_nth_mono)
3698 lemma set_insort: "set(insort_key f x xs) = insert x (set xs)"
3701 lemma set_sort[simp]: "set(sort_key f xs) = set xs"
3702 by (induct xs) (simp_all add:set_insort)
3704 lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
3705 by(induct xs)(auto simp:set_insort)
3707 lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
3708 by(induct xs)(simp_all add:distinct_insort set_sort)
3710 lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
3711 by(induct xs)(auto simp:sorted_Cons set_insort)
3713 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
3714 using sorted_insort_key[where f="\<lambda>x. x"] by simp
3716 theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))"
3717 by(induct xs)(auto simp:sorted_insort_key)
3719 theorem sorted_sort[simp]: "sorted (sort xs)"
3720 by(induct xs)(auto simp:sorted_insort)
3722 lemma sorted_butlast:
3723 assumes "xs \<noteq> []" and "sorted xs"
3724 shows "sorted (butlast xs)"
3726 from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
3727 with `sorted xs` show ?thesis by (simp add: sorted_append)
3730 lemma insort_not_Nil [simp]:
3731 "insort_key f a xs \<noteq> []"
3732 by (induct xs) simp_all
3734 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
3737 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
3738 by(induct xs)(auto simp add: sorted_Cons)
3740 lemma insort_key_remove1: "\<lbrakk> a \<in> set xs; sorted (map f xs) ; inj_on f (set xs) \<rbrakk>
3741 \<Longrightarrow> insort_key f a (remove1 a xs) = xs"
3745 proof (cases "x = a")
3747 hence "f x \<noteq> f a" using Cons.prems by auto
3748 hence "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
3749 thus ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
3750 qed (auto simp: sorted_Cons insort_is_Cons)
3753 lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
3754 using insort_key_remove1[where f="\<lambda>x. x"] by simp
3756 lemma sorted_remdups[simp]:
3757 "sorted l \<Longrightarrow> sorted (remdups l)"
3758 by (induct l) (auto simp: sorted_Cons)
3760 lemma sorted_distinct_set_unique:
3761 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
3764 from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
3765 from assms show ?thesis
3766 proof(induct rule:list_induct2[OF 1])
3767 case 1 show ?case by simp
3769 case 2 thus ?case by (simp add:sorted_Cons)
3770 (metis Diff_insert_absorb antisym insertE insert_iff)
3774 lemma map_sorted_distinct_set_unique:
3775 assumes "inj_on f (set xs \<union> set ys)"
3776 assumes "sorted (map f xs)" "distinct (map f xs)"
3777 "sorted (map f ys)" "distinct (map f ys)"
3778 assumes "set xs = set ys"
3781 from assms have "map f xs = map f ys"
3782 by (simp add: sorted_distinct_set_unique)
3783 moreover with `inj_on f (set xs \<union> set ys)` show "xs = ys"
3784 by (blast intro: map_inj_on)
3787 lemma finite_sorted_distinct_unique:
3788 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
3789 apply(drule finite_distinct_list)
3791 apply(rule_tac a="sort xs" in ex1I)
3792 apply (auto simp: sorted_distinct_set_unique)
3796 "sorted xs \<Longrightarrow> sorted (take n xs)"
3797 proof (induct xs arbitrary: n rule: sorted.induct)
3798 case 1 show ?case by simp
3800 case 2 show ?case by (cases n) simp_all
3803 then have "x \<le> y" by simp
3804 show ?case proof (cases n)
3805 case 0 then show ?thesis by simp
3808 with 3 have "sorted (take m (y # xs))" by simp
3809 with Suc `x \<le> y` show ?thesis by (cases m) simp_all
3814 "sorted xs \<Longrightarrow> sorted (drop n xs)"
3815 proof (induct xs arbitrary: n rule: sorted.induct)
3816 case 1 show ?case by simp
3818 case 2 show ?case by (cases n) simp_all
3820 case 3 then show ?case by (cases n) simp_all
3823 lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
3824 unfolding dropWhile_eq_drop by (rule sorted_drop)
3826 lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
3827 apply (subst takeWhile_eq_take) by (rule sorted_take)
3829 lemma sorted_filter:
3830 "sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
3831 by (induct xs) (simp_all add: sorted_Cons)
3833 lemma foldr_max_sorted:
3834 assumes "sorted (rev xs)"
3835 shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"
3836 using assms proof (induct xs)
3838 moreover hence "sorted (rev xs)" using sorted_append by auto
3839 ultimately show ?case
3840 by (cases xs, auto simp add: sorted_append max_def)
3843 lemma filter_equals_takeWhile_sorted_rev:
3844 assumes sorted: "sorted (rev (map f xs))"
3845 shows "[x \<leftarrow> xs. t < f x] = takeWhile (\<lambda> x. t < f x) xs"
3846 (is "filter ?P xs = ?tW")
3847 proof (rule takeWhile_eq_filter[symmetric])
3848 let "?dW" = "dropWhile ?P xs"
3849 fix x assume "x \<in> set ?dW"
3850 then obtain i where i: "i < length ?dW" and nth_i: "x = ?dW ! i"
3851 unfolding in_set_conv_nth by auto
3852 hence "length ?tW + i < length (?tW @ ?dW)"
3853 unfolding length_append by simp
3854 hence i': "length (map f ?tW) + i < length (map f xs)" by simp
3855 have "(map f ?tW @ map f ?dW) ! (length (map f ?tW) + i) \<le>
3856 (map f ?tW @ map f ?dW) ! (length (map f ?tW) + 0)"
3857 using sorted_rev_nth_mono[OF sorted _ i', of "length ?tW"]
3858 unfolding map_append[symmetric] by simp
3859 hence "f x \<le> f (?dW ! 0)"
3860 unfolding nth_append_length_plus nth_i
3861 using i preorder_class.le_less_trans[OF le0 i] by simp
3862 also have "... \<le> t"
3863 using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i]
3864 using hd_conv_nth[of "?dW"] by simp
3865 finally show "\<not> t < f x" by simp
3868 lemma set_insort_insert:
3869 "set (insort_insert x xs) = insert x (set xs)"
3870 by (auto simp add: insort_insert_def set_insort)
3872 lemma distinct_insort_insert:
3873 assumes "distinct xs"
3874 shows "distinct (insort_insert x xs)"
3875 using assms by (induct xs) (auto simp add: insort_insert_def set_insort)
3877 lemma sorted_insort_insert:
3879 shows "sorted (insort_insert x xs)"
3880 using assms by (simp add: insort_insert_def sorted_insort)
3882 lemma filter_insort_key_triv:
3883 "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
3884 by (induct xs) simp_all
3886 lemma filter_insort_key:
3887 "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
3888 using assms by (induct xs)
3889 (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
3891 lemma filter_sort_key:
3892 "filter P (sort_key f xs) = sort_key f (filter P xs)"
3893 by (induct xs) (simp_all add: filter_insort_key_triv filter_insort_key)
3895 lemma sorted_same [simp]:
3896 "sorted [x\<leftarrow>xs. x = f xs]"
3897 proof (induct xs arbitrary: f)
3898 case Nil then show ?case by simp
3901 then have "sorted [y\<leftarrow>xs . y = (\<lambda>xs. x) xs]" .
3902 moreover from Cons have "sorted [y\<leftarrow>xs . y = (f \<circ> Cons x) xs]" .
3903 ultimately show ?case by (simp_all add: sorted_Cons)
3906 lemma remove1_insort [simp]:
3907 "remove1 x (insort x xs) = xs"
3908 by (induct xs) simp_all
3912 lemma sorted_upt[simp]: "sorted[i..<j]"
3913 by (induct j) (simp_all add:sorted_append)
3915 lemma sorted_upto[simp]: "sorted[i..j]"
3916 apply(induct i j rule:upto.induct)
3917 apply(subst upto.simps)
3918 apply(simp add:sorted_Cons)
3922 subsubsection {* @{const transpose} on sorted lists *}
3924 lemma sorted_transpose[simp]:
3925 shows "sorted (rev (map length (transpose xs)))"
3926 by (auto simp: sorted_equals_nth_mono rev_nth nth_transpose
3927 length_filter_conv_card intro: card_mono)
3929 lemma transpose_max_length:
3930 "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length [x \<leftarrow> xs. x \<noteq> []]"
3932 proof (cases "transpose xs = []")
3934 have "?L = foldr max (map length (transpose xs)) 0"
3935 by (simp add: foldr_map comp_def)
3936 also have "... = length (transpose xs ! 0)"
3937 using False sorted_transpose by (simp add: foldr_max_sorted)
3938 finally show ?thesis
3939 using False by (simp add: nth_transpose)
3942 hence "[x \<leftarrow> xs. x \<noteq> []] = []"
3943 by (auto intro!: filter_False simp: transpose_empty)
3944 thus ?thesis by (simp add: transpose_empty True)
3947 lemma length_transpose_sorted:
3948 fixes xs :: "'a list list"
3949 assumes sorted: "sorted (rev (map length xs))"
3950 shows "length (transpose xs) = (if xs = [] then 0 else length (xs ! 0))"
3951 proof (cases "xs = []")
3954 using foldr_max_sorted[OF sorted] False
3955 unfolding length_transpose foldr_map comp_def
3959 lemma nth_nth_transpose_sorted[simp]:
3960 fixes xs :: "'a list list"
3961 assumes sorted: "sorted (rev (map length xs))"
3962 and i: "i < length (transpose xs)"
3963 and j: "j < length [ys \<leftarrow> xs. i < length ys]"
3964 shows "transpose xs ! i ! j = xs ! j ! i"
3965 using j filter_equals_takeWhile_sorted_rev[OF sorted, of i]
3966 nth_transpose[OF i] nth_map[OF j]
3967 by (simp add: takeWhile_nth)
3969 lemma transpose_column_length:
3970 fixes xs :: "'a list list"
3971 assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
3972 shows "length (filter (\<lambda>ys. i < length ys) (transpose xs)) = length (xs ! i)"
3974 have "xs \<noteq> []" using `i < length xs` by auto
3975 note filter_equals_takeWhile_sorted_rev[OF sorted, simp]
3976 { fix j assume "j \<le> i"
3977 note sorted_rev_nth_mono[OF sorted, of j i, simplified, OF this `i < length xs`]
3978 } note sortedE = this[consumes 1]
3980 have "{j. j < length (transpose xs) \<and> i < length (transpose xs ! j)}
3981 = {..< length (xs ! i)}"
3984 assume "j < length (transpose xs)" and "i < length (transpose xs ! j)"
3985 with this(2) nth_transpose[OF this(1)]
3986 have "i < length (takeWhile (\<lambda>ys. j < length ys) xs)" by simp
3987 from nth_mem[OF this] takeWhile_nth[OF this]
3988 show "j < length (xs ! i)" by (auto dest: set_takeWhileD)
3990 fix j assume "j < length (xs ! i)"
3991 thus "j < length (transpose xs)"
3992 using foldr_max_sorted[OF sorted] `xs \<noteq> []` sortedE[OF le0]
3993 by (auto simp: length_transpose comp_def foldr_map)
3995 have "Suc i \<le> length (takeWhile (\<lambda>ys. j < length ys) xs)"
3996 using `i < length xs` `j < length (xs ! i)` less_Suc_eq_le
3997 by (auto intro!: length_takeWhile_less_P_nth dest!: sortedE)
3998 with nth_transpose[OF `j < length (transpose xs)`]
3999 show "i < length (transpose xs ! j)" by simp
4001 thus ?thesis by (simp add: length_filter_conv_card)
4004 lemma transpose_column:
4005 fixes xs :: "'a list list"
4006 assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
4007 shows "map (\<lambda>ys. ys ! i) (filter (\<lambda>ys. i < length ys) (transpose xs))
4008 = xs ! i" (is "?R = _")
4009 proof (rule nth_equalityI, safe)
4010 show length: "length ?R = length (xs ! i)"
4011 using transpose_column_length[OF assms] by simp
4013 fix j assume j: "j < length ?R"
4014 note * = less_le_trans[OF this, unfolded length_map, OF length_filter_le]
4015 from j have j_less: "j < length (xs ! i)" using length by simp
4016 have i_less_tW: "Suc i \<le> length (takeWhile (\<lambda>ys. Suc j \<le> length ys) xs)"
4017 proof (rule length_takeWhile_less_P_nth)
4018 show "Suc i \<le> length xs" using `i < length xs` by simp
4019 fix k assume "k < Suc i"
4020 hence "k \<le> i" by auto
4021 with sorted_rev_nth_mono[OF sorted this] `i < length xs`
4022 have "length (xs ! i) \<le> length (xs ! k)" by simp
4023 thus "Suc j \<le> length (xs ! k)" using j_less by simp
4025 have i_less_filter: "i < length [ys\<leftarrow>xs . j < length ys]"
4026 unfolding filter_equals_takeWhile_sorted_rev[OF sorted, of j]
4027 using i_less_tW by (simp_all add: Suc_le_eq)
4028 from j show "?R ! j = xs ! i ! j"
4029 unfolding filter_equals_takeWhile_sorted_rev[OF sorted_transpose, of i]
4030 by (simp add: takeWhile_nth nth_nth_transpose_sorted[OF sorted * i_less_filter])
4033 lemma transpose_transpose:
4034 fixes xs :: "'a list list"
4035 assumes sorted: "sorted (rev (map length xs))"
4036 shows "transpose (transpose xs) = takeWhile (\<lambda>x. x \<noteq> []) xs" (is "?L = ?R")
4038 have len: "length ?L = length ?R"
4039 unfolding length_transpose transpose_max_length
4040 using filter_equals_takeWhile_sorted_rev[OF sorted, of 0]
4043 { fix i assume "i < length ?R"
4044 with less_le_trans[OF _ length_takeWhile_le[of _ xs]]
4045 have "i < length xs" by simp
4048 by (rule nth_equalityI)
4049 (simp_all add: len nth_transpose transpose_column[OF sorted] * takeWhile_nth)
4052 theorem transpose_rectangle:
4053 assumes "xs = [] \<Longrightarrow> n = 0"
4054 assumes rect: "\<And> i. i < length xs \<Longrightarrow> length (xs ! i) = n"
4055 shows "transpose xs = map (\<lambda> i. map (\<lambda> j. xs ! j ! i) [0..<length xs]) [0..<n]"
4056 (is "?trans = ?map")
4057 proof (rule nth_equalityI)
4058 have "sorted (rev (map length xs))"
4059 by (auto simp: rev_nth rect intro!: sorted_nth_monoI)
4060 from foldr_max_sorted[OF this] assms
4061 show len: "length ?trans = length ?map"
4062 by (simp_all add: length_transpose foldr_map comp_def)
4064 { fix i assume "i < n" hence "[ys\<leftarrow>xs . i < length ys] = xs"
4065 using rect by (auto simp: in_set_conv_nth intro!: filter_True) }
4066 ultimately show "\<forall>i < length ?trans. ?trans ! i = ?map ! i"
4067 by (auto simp: nth_transpose intro: nth_equalityI)
4071 subsubsection {* @{text sorted_list_of_set} *}
4073 text{* This function maps (finite) linearly ordered sets to sorted
4074 lists. Warning: in most cases it is not a good idea to convert from
4075 sets to lists but one should convert in the other direction (via
4081 definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
4082 "sorted_list_of_set = Finite_Set.fold insort []"
4084 lemma sorted_list_of_set_empty [simp]:
4085 "sorted_list_of_set {} = []"
4086 by (simp add: sorted_list_of_set_def)
4088 lemma sorted_list_of_set_insert [simp]:
4090 shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
4092 interpret fun_left_comm insort by (fact fun_left_comm_insort)
4093 with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
4096 lemma sorted_list_of_set [simp]:
4097 "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
4098 \<and> distinct (sorted_list_of_set A)"
4099 by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
4101 lemma sorted_list_of_set_sort_remdups:
4102 "sorted_list_of_set (set xs) = sort (remdups xs)"
4104 interpret fun_left_comm insort by (fact fun_left_comm_insort)
4105 show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
4108 lemma sorted_list_of_set_remove:
4110 shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
4111 proof (cases "x \<in> A")
4112 case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
4113 with False show ?thesis by (simp add: remove1_idem)
4115 case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
4116 with assms show ?thesis by simp
4121 lemma sorted_list_of_set_range [simp]:
4122 "sorted_list_of_set {m..<n} = [m..<n]"
4123 by (rule sorted_distinct_set_unique) simp_all
4127 subsubsection {* @{text lists}: the list-forming operator over sets *}
4130 lists :: "'a set => 'a list set"
4133 Nil [intro!]: "[]: lists A"
4134 | Cons [intro!,no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
4136 inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
4137 inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
4139 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
4140 by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
4142 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
4145 assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
4148 lemmas lists_IntI = listsp_infI [to_set]
4150 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
4151 proof (rule mono_inf [where f=listsp, THEN order_antisym])
4152 show "mono listsp" by (simp add: mono_def listsp_mono)
4153 show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
4156 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
4158 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
4160 lemma append_in_listsp_conv [iff]:
4161 "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
4164 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
4166 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
4167 -- {* eliminate @{text listsp} in favour of @{text set} *}
4170 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
4172 lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
4173 by (rule in_listsp_conv_set [THEN iffD1])
4175 lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
4177 lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
4178 by (rule in_listsp_conv_set [THEN iffD2])
4180 lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
4182 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
4186 subsubsection {* Inductive definition for membership *}
4188 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
4190 elem: "ListMem x (x # xs)"
4191 | insert: "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
4193 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
4195 apply (induct set: ListMem)
4198 apply (auto intro: ListMem.intros)
4202 subsubsection {* Lists as Cartesian products *}
4204 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
4205 @{term A} and tail drawn from @{term Xs}.*}
4208 set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
4209 "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
4211 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
4212 by (auto simp add: set_Cons_def)
4214 text{*Yields the set of lists, all of the same length as the argument and
4215 with elements drawn from the corresponding element of the argument.*}
4218 listset :: "'a set list \<Rightarrow> 'a list set" where
4220 | "listset (A # As) = set_Cons A (listset As)"
4223 subsection {* Relations on Lists *}
4225 subsubsection {* Length Lexicographic Ordering *}
4227 text{*These orderings preserve well-foundedness: shorter lists
4228 precede longer lists. These ordering are not used in dictionaries.*}
4230 primrec -- {*The lexicographic ordering for lists of the specified length*}
4231 lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
4233 | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
4234 {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
4237 lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
4238 "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
4241 lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
4242 "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
4243 -- {*Compares lists by their length and then lexicographically*}
4245 lemma wf_lexn: "wf r ==> wf (lexn r n)"
4246 apply (induct n, simp, simp)
4247 apply(rule wf_subset)
4248 prefer 2 apply (rule Int_lower1)
4249 apply(rule wf_prod_fun_image)
4250 prefer 2 apply (rule inj_onI, auto)
4254 "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
4255 by (induct n arbitrary: xs ys) auto
4257 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
4258 apply (unfold lex_def)
4260 apply (blast intro: wf_lexn, clarify)
4261 apply (rename_tac m n)
4262 apply (subgoal_tac "m \<noteq> n")
4263 prefer 2 apply blast
4264 apply (blast dest: lexn_length not_sym)
4269 {(xs,ys). length xs = n \<and> length ys = n \<and>
4270 (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
4271 apply (induct n, simp)
4272 apply (simp add: image_Collect lex_prod_def, safe, blast)
4273 apply (rule_tac x = "ab # xys" in exI, simp)
4274 apply (case_tac xys, simp_all, blast)
4279 {(xs,ys). length xs = length ys \<and>
4280 (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
4281 by (force simp add: lex_def lexn_conv)
4283 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
4284 by (unfold lenlex_def) blast
4287 "lenlex r = {(xs,ys). length xs < length ys |
4288 length xs = length ys \<and> (xs, ys) : lex r}"
4289 by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def)
4291 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
4292 by (simp add: lex_conv)
4294 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
4295 by (simp add:lex_conv)
4297 lemma Cons_in_lex [simp]:
4298 "((x # xs, y # ys) : lex r) =
4299 ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
4300 apply (simp add: lex_conv)
4302 prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
4303 apply (case_tac xys, simp, simp)
4308 subsubsection {* Lexicographic Ordering *}
4310 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
4311 This ordering does \emph{not} preserve well-foundedness.
4312 Author: N. Voelker, March 2005. *}
4315 lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
4316 "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
4317 (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
4319 lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
4320 by (unfold lexord_def, induct_tac y, auto)
4322 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
4323 by (unfold lexord_def, induct_tac x, auto)
4325 lemma lexord_cons_cons[simp]:
4326 "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
4327 apply (unfold lexord_def, safe, simp_all)
4328 apply (case_tac u, simp, simp)
4329 apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
4330 apply (erule_tac x="b # u" in allE)
4333 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
4335 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
4336 by (induct_tac x, auto)
4338 lemma lexord_append_left_rightI:
4339 "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
4340 by (induct_tac u, auto)
4342 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
4345 lemma lexord_append_leftD:
4346 "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
4347 by (erule rev_mp, induct_tac x, auto)
4349 lemma lexord_take_index_conv:
4350 "((x,y) : lexord r) =
4351 ((length x < length y \<and> take (length x) y = x) \<or>
4352 (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
4353 apply (unfold lexord_def Let_def, clarsimp)
4354 apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
4356 apply (rule_tac x="hd (drop (length x) y)" in exI)
4357 apply (rule_tac x="tl (drop (length x) y)" in exI)
4358 apply (erule subst, simp add: min_def)
4359 apply (rule_tac x ="length u" in exI, simp)
4360 apply (rule_tac x ="take i x" in exI)
4361 apply (rule_tac x ="x ! i" in exI)
4362 apply (rule_tac x ="y ! i" in exI, safe)
4363 apply (rule_tac x="drop (Suc i) x" in exI)
4364 apply (drule sym, simp add: drop_Suc_conv_tl)
4365 apply (rule_tac x="drop (Suc i) y" in exI)
4366 by (simp add: drop_Suc_conv_tl)
4368 -- {* lexord is extension of partial ordering List.lex *}
4369 lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
4370 apply (rule_tac x = y in spec)
4371 apply (induct_tac x, clarsimp)
4372 by (clarify, case_tac x, simp, force)
4374 lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
4378 "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
4379 apply (erule rev_mp)+
4380 apply (rule_tac x = x in spec)
4381 apply (rule_tac x = z in spec)
4382 apply ( induct_tac y, simp, clarify)
4383 apply (case_tac xa, erule ssubst)
4384 apply (erule allE, erule allE) -- {* avoid simp recursion *}
4385 apply (case_tac x, simp, simp)
4386 apply (case_tac x, erule allE, erule allE, simp)
4387 apply (erule_tac x = listb in allE)
4388 apply (erule_tac x = lista in allE, simp)
4389 apply (unfold trans_def)
4392 lemma lexord_transI: "trans r \<Longrightarrow> trans (lexord r)"
4393 by (rule transI, drule lexord_trans, blast)
4395 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"
4396 apply (rule_tac x = y in spec)
4397 apply (induct_tac x, rule allI)
4398 apply (case_tac x, simp, simp)
4399 apply (rule allI, case_tac x, simp, simp)
4403 subsection {* Lexicographic combination of measure functions *}
4405 text {* These are useful for termination proofs *}
4408 "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
4410 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
4411 unfolding measures_def
4414 lemma in_measures[simp]:
4415 "(x, y) \<in> measures [] = False"
4416 "(x, y) \<in> measures (f # fs)
4417 = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"
4418 unfolding measures_def
4421 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
4424 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
4428 subsubsection {* Lifting a Relation on List Elements to the Lists *}
4431 listrel :: "('a * 'a)set => ('a list * 'a list)set"
4432 for r :: "('a * 'a)set"
4434 Nil: "([],[]) \<in> listrel r"
4435 | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
4437 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
4438 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
4439 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
4440 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
4443 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
4445 apply (erule listrel.induct)
4446 apply (blast intro: listrel.intros)+
4449 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
4451 apply (erule listrel.induct, auto)
4454 lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)"
4455 apply (simp add: refl_on_def listrel_subset Ball_def)
4457 apply (induct_tac x)
4458 apply (auto intro: listrel.intros)
4461 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"
4462 apply (auto simp add: sym_def)
4463 apply (erule listrel.induct)
4464 apply (blast intro: listrel.intros)+
4467 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"
4468 apply (simp add: trans_def)
4471 apply (erule listrel.induct)
4472 apply (blast intro: listrel.intros)+
4475 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
4476 by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans)
4478 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
4479 by (blast intro: listrel.intros)
4482 "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
4483 by (auto simp add: set_Cons_def intro: listrel.intros)
4486 subsection {* Size function *}
4488 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
4489 by (rule is_measure_trivial)
4491 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
4492 by (rule is_measure_trivial)
4494 lemma list_size_estimation[termination_simp]:
4495 "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
4498 lemma list_size_estimation'[termination_simp]:
4499 "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
4502 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
4505 lemma list_size_pointwise[termination_simp]:
4506 "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
4507 by (induct xs) force+
4510 subsection {* Transfer *}
4513 embed_list :: "nat list \<Rightarrow> int list"
4515 "embed_list l = map int l"
4518 nat_list :: "int list \<Rightarrow> bool"
4520 "nat_list l = nat_set (set l)"
4523 return_list :: "int list \<Rightarrow> nat list"
4525 "return_list l = map nat l"
4527 lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
4528 embed_list (return_list l) = l"
4529 unfolding embed_list_def return_list_def nat_list_def nat_set_def
4534 lemma transfer_nat_int_list_functions:
4535 "l @ m = return_list (embed_list l @ embed_list m)"
4536 "[] = return_list []"
4537 unfolding return_list_def embed_list_def
4539 apply (induct l, auto)
4540 apply (induct m, auto)
4544 lemma transfer_nat_int_fold1: "fold f l x =
4545 fold (%x. f (nat x)) (embed_list l) x";
4549 subsection {* Code generation *}
4551 subsubsection {* Counterparts for set-related operations *}
4553 definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
4554 [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
4557 Only use @{text member} for generating executable code. Otherwise use
4558 @{prop "x \<in> set xs"} instead --- it is much easier to reason about.
4563 by (simp add: expand_fun_eq member_def mem_def)
4565 lemma member_rec [code]:
4566 "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
4567 "member [] y \<longleftrightarrow> False"
4568 by (auto simp add: member_def)
4570 lemma in_set_member [code_unfold]:
4571 "x \<in> set xs \<longleftrightarrow> member xs x"
4572 by (simp add: member_def)
4574 declare INFI_def [code_unfold]
4575 declare SUPR_def [code_unfold]
4577 declare set_map [symmetric, code_unfold]
4579 definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
4580 list_all_iff [code_post]: "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
4582 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
4583 list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
4586 Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
4587 over @{const list_all} and @{const list_ex} in specifications.
4590 lemma list_all_simps [simp, code]:
4591 "list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs"
4592 "list_all P [] \<longleftrightarrow> True"
4593 by (simp_all add: list_all_iff)
4595 lemma list_ex_simps [simp, code]:
4596 "list_ex P (x # xs) \<longleftrightarrow> P x \<or> list_ex P xs"
4597 "list_ex P [] \<longleftrightarrow> False"
4598 by (simp_all add: list_ex_iff)
4600 lemma Ball_set_list_all [code_unfold]:
4601 "Ball (set xs) P \<longleftrightarrow> list_all P xs"
4602 by (simp add: list_all_iff)
4604 lemma Bex_set_list_ex [code_unfold]:
4605 "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
4606 by (simp add: list_ex_iff)
4608 lemma list_all_append [simp]:
4609 "list_all P (xs @ ys) \<longleftrightarrow> list_all P xs \<and> list_all P ys"
4610 by (auto simp add: list_all_iff)
4612 lemma list_ex_append [simp]:
4613 "list_ex P (xs @ ys) \<longleftrightarrow> list_ex P xs \<or> list_ex P ys"
4614 by (auto simp add: list_ex_iff)
4616 lemma list_all_rev [simp]:
4617 "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
4618 by (simp add: list_all_iff)
4620 lemma list_ex_rev [simp]:
4621 "list_ex P (rev xs) \<longleftrightarrow> list_ex P xs"
4622 by (simp add: list_ex_iff)
4624 lemma list_all_length:
4625 "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
4626 by (auto simp add: list_all_iff set_conv_nth)
4628 lemma list_ex_length:
4629 "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
4630 by (auto simp add: list_ex_iff set_conv_nth)
4632 lemma list_all_cong [fundef_cong]:
4633 "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
4634 by (simp add: list_all_iff)
4636 lemma list_any_cong [fundef_cong]:
4637 "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
4638 by (simp add: list_ex_iff)
4640 text {* Bounded quantification and summation over nats. *}
4642 lemma atMost_upto [code_unfold]:
4643 "{..n} = set [0..<Suc n]"
4646 lemma atLeast_upt [code_unfold]:
4647 "{..<n} = set [0..<n]"
4650 lemma greaterThanLessThan_upt [code_unfold]:
4651 "{n<..<m} = set [Suc n..<m]"
4654 lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
4656 lemma greaterThanAtMost_upt [code_unfold]:
4657 "{n<..m} = set [Suc n..<Suc m]"
4660 lemma atLeastAtMost_upt [code_unfold]:
4661 "{n..m} = set [n..<Suc m]"
4664 lemma all_nat_less_eq [code_unfold]:
4665 "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
4668 lemma ex_nat_less_eq [code_unfold]:
4669 "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
4672 lemma all_nat_less [code_unfold]:
4673 "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
4676 lemma ex_nat_less [code_unfold]:
4677 "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
4680 lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
4681 "setsum f (set [m..<n]) = listsum (map f [m..<n])"
4682 by (simp add: interv_listsum_conv_setsum_set_nat)
4684 text {* Summation over ints. *}
4686 lemma greaterThanLessThan_upto [code_unfold]:
4687 "{i<..<j::int} = set [i+1..j - 1]"
4690 lemma atLeastLessThan_upto [code_unfold]:
4691 "{i..<j::int} = set [i..j - 1]"
4694 lemma greaterThanAtMost_upto [code_unfold]:
4695 "{i<..j::int} = set [i+1..j]"
4698 lemmas atLeastAtMost_upto [code_unfold] = set_upto [symmetric]
4700 lemma setsum_set_upto_conv_listsum_int [code_unfold]:
4701 "setsum f (set [i..j::int]) = listsum (map f [i..j])"
4702 by (simp add: interv_listsum_conv_setsum_set_int)
4705 subsubsection {* Optimizing by rewriting *}
4707 definition null :: "'a list \<Rightarrow> bool" where
4708 [code_post]: "null xs \<longleftrightarrow> xs = []"
4711 Efficient emptyness check is implemented by @{const null}.
4714 lemma null_rec [code]:
4715 "null (x # xs) \<longleftrightarrow> False"
4716 "null [] \<longleftrightarrow> True"
4717 by (simp_all add: null_def)
4719 lemma eq_Nil_null [code_unfold]:
4720 "xs = [] \<longleftrightarrow> null xs"
4721 by (simp add: null_def)
4723 lemma equal_Nil_null [code_unfold]:
4724 "HOL.equal xs [] \<longleftrightarrow> null xs"
4725 by (simp add: equal eq_Nil_null)
4727 definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
4728 [code_post]: "maps f xs = concat (map f xs)"
4730 definition map_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
4731 [code_post]: "map_filter f xs = map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> None) xs)"
4734 Operations @{const maps} and @{const map_filter} avoid
4735 intermediate lists on execution -- do not use for proving.
4738 lemma maps_simps [code]:
4739 "maps f (x # xs) = f x @ maps f xs"
4741 by (simp_all add: maps_def)
4743 lemma map_filter_simps [code]:
4744 "map_filter f (x # xs) = (case f x of None \<Rightarrow> map_filter f xs | Some y \<Rightarrow> y # map_filter f xs)"
4745 "map_filter f [] = []"
4746 by (simp_all add: map_filter_def split: option.split)
4748 lemma concat_map_maps [code_unfold]:
4749 "concat (map f xs) = maps f xs"
4750 by (simp add: maps_def)
4752 lemma map_filter_map_filter [code_unfold]:
4753 "map f (filter P xs) = map_filter (\<lambda>x. if P x then Some (f x) else None) xs"
4754 by (simp add: map_filter_def)
4756 text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
4757 and similiarly for @{text"\<exists>"}. *}
4759 definition all_interval_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
4760 "all_interval_nat P i j \<longleftrightarrow> (\<forall>n \<in> {i..<j}. P n)"
4763 "all_interval_nat P i j \<longleftrightarrow> i \<ge> j \<or> P i \<and> all_interval_nat P (Suc i) j"
4765 have *: "\<And>n. P i \<Longrightarrow> \<forall>n\<in>{Suc i..<j}. P n \<Longrightarrow> i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n"
4768 assume "P i" "\<forall>n\<in>{Suc i..<j}. P n" "i \<le> n" "n < j"
4769 then show "P n" by (cases "n = i") simp_all
4771 show ?thesis by (auto simp add: all_interval_nat_def intro: *)
4774 lemma list_all_iff_all_interval_nat [code_unfold]:
4775 "list_all P [i..<j] \<longleftrightarrow> all_interval_nat P i j"
4776 by (simp add: list_all_iff all_interval_nat_def)
4778 lemma list_ex_iff_not_all_inverval_nat [code_unfold]:
4779 "list_ex P [i..<j] \<longleftrightarrow> \<not> (all_interval_nat (Not \<circ> P) i j)"
4780 by (simp add: list_ex_iff all_interval_nat_def)
4782 definition all_interval_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
4783 "all_interval_int P i j \<longleftrightarrow> (\<forall>k \<in> {i..j}. P k)"
4786 "all_interval_int P i j \<longleftrightarrow> i > j \<or> P i \<and> all_interval_int P (i + 1) j"
4788 have *: "\<And>k. P i \<Longrightarrow> \<forall>k\<in>{i+1..j}. P k \<Longrightarrow> i \<le> k \<Longrightarrow> k \<le> j \<Longrightarrow> P k"
4791 assume "P i" "\<forall>k\<in>{i+1..j}. P k" "i \<le> k" "k \<le> j"
4792 then show "P k" by (cases "k = i") simp_all
4794 show ?thesis by (auto simp add: all_interval_int_def intro: *)
4797 lemma list_all_iff_all_interval_int [code_unfold]:
4798 "list_all P [i..j] \<longleftrightarrow> all_interval_int P i j"
4799 by (simp add: list_all_iff all_interval_int_def)
4801 lemma list_ex_iff_not_all_inverval_int [code_unfold]:
4802 "list_ex P [i..j] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> P) i j)"
4803 by (simp add: list_ex_iff all_interval_int_def)
4805 hide_const (open) member null maps map_filter all_interval_nat all_interval_int
4808 subsubsection {* Pretty lists *}
4810 use "Tools/list_code.ML"
4824 code_instance list :: equal
4827 code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
4828 (Haskell infixl 4 "==")
4839 fun term_of_list f T = HOLogic.mk_list T o map f;
4842 fun gen_list' aG aT i j = frequency
4846 val (xs, ts) = gen_list' aG aT (i-1) j
4847 in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
4848 (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
4849 and gen_list aG aT i = gen_list' aG aT i i;
4852 consts_code Cons ("(_ ::/ _)")
4856 fun list_codegen thy defs dep thyname b t gr =
4858 val ts = HOLogic.dest_list t;
4859 val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
4861 val (ps, gr'') = fold_map
4862 (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
4863 in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
4865 fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]
4866 #> Codegen.add_codegen "list_codegen" list_codegen
4871 subsubsection {* Use convenient predefined operations *}
4875 (OCaml infixr 6 "@")
4876 (Haskell infixr 5 "++")
4877 (Scala infixl 7 "++")
4888 code_const List.maps
4889 (Haskell "concatMap")
4897 code_const List.null
4900 code_const takeWhile
4901 (Haskell "takeWhile")
4903 code_const dropWhile
4904 (Haskell "dropWhile")