src/HOL/List.thy
changeset 23096 423ad2fe9f76
parent 23060 0c0b03d0ec7e
child 23192 ec73b9707d48
     1.1 --- a/src/HOL/List.thy	Thu May 24 16:52:54 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Thu May 24 22:55:53 2007 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4    butlast :: "'a list => 'a list"
     1.5    set :: "'a list => 'a set"
     1.6    map :: "('a=>'b) => ('a list => 'b list)"
     1.7 +  listsum ::  "'a list => 'a::monoid_add"
     1.8    nth :: "'a list => nat => 'a"    (infixl "!" 100)
     1.9    list_update :: "'a list => nat => 'a => 'a list"
    1.10    take:: "nat => 'a list => 'a list"
    1.11 @@ -134,6 +135,10 @@
    1.12    "concat(x#xs) = x @ concat(xs)"
    1.13  
    1.14  primrec
    1.15 +"listsum [] = 0"
    1.16 +"listsum (x # xs) = x + listsum xs"
    1.17 +
    1.18 +primrec
    1.19    drop_Nil:"drop n [] = []"
    1.20    drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
    1.21    -- {*Warning: simpset does not contain this definition, but separate
    1.22 @@ -1417,6 +1422,20 @@
    1.23  "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
    1.24  by (induct rule:list_induct2, simp_all)
    1.25  
    1.26 +lemma map_zip_map:
    1.27 + "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
    1.28 +apply(induct xs arbitrary:ys) apply simp
    1.29 +apply(case_tac ys)
    1.30 +apply simp_all
    1.31 +done
    1.32 +
    1.33 +lemma map_zip_map2:
    1.34 + "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
    1.35 +apply(induct xs arbitrary:ys) apply simp
    1.36 +apply(case_tac ys)
    1.37 +apply simp_all
    1.38 +done
    1.39 +
    1.40  lemma nth_zip [simp]:
    1.41  "!!i xs. [| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
    1.42  apply (induct ys, simp)
    1.43 @@ -1618,6 +1637,12 @@
    1.44  lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
    1.45  by (induct xs) auto
    1.46  
    1.47 +lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
    1.48 +by(induct xs) simp_all
    1.49 +
    1.50 +lemma foldl_map: "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
    1.51 +by(induct xs arbitrary:a) simp_all
    1.52 +
    1.53  lemma foldl_cong [fundef_cong, recdef_cong]:
    1.54    "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
    1.55    ==> foldl f a l = foldl g b k"
    1.56 @@ -1628,6 +1653,19 @@
    1.57    ==> foldr f l a = foldr g k b"
    1.58    by (induct k arbitrary: a b l) simp_all
    1.59  
    1.60 +text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
    1.61 +
    1.62 +lemma foldl_foldr1_lemma:
    1.63 + "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
    1.64 +by (induct xs arbitrary: a) (auto simp:add_assoc)
    1.65 +
    1.66 +corollary foldl_foldr1:
    1.67 + "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
    1.68 +by (simp add:foldl_foldr1_lemma)
    1.69 +
    1.70 +
    1.71 +text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
    1.72 +
    1.73  lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
    1.74  by (induct xs) auto
    1.75  
    1.76 @@ -1649,6 +1687,37 @@
    1.77  "!!m::nat. (foldl (op +) m ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
    1.78  by (induct ns) auto
    1.79  
    1.80 +subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
    1.81 +
    1.82 +lemma listsum_foldr:
    1.83 + "listsum xs = foldr (op +) xs 0"
    1.84 +by(induct xs) auto
    1.85 +
    1.86 +(* for efficient code generation *)
    1.87 +lemma listsum[code]: "listsum xs = foldl (op +) 0 xs"
    1.88 +by(simp add:listsum_foldr foldl_foldr1)
    1.89 +
    1.90 +text{* Some syntactic sugar for summing a function over a list: *}
    1.91 +
    1.92 +syntax
    1.93 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
    1.94 +syntax (xsymbols)
    1.95 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    1.96 +syntax (HTML output)
    1.97 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    1.98 +
    1.99 +translations -- {* Beware of argument permutation! *}
   1.100 +  "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
   1.101 +  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
   1.102 +
   1.103 +lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
   1.104 +by (induct xs) simp_all
   1.105 +
   1.106 +text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
   1.107 +lemma uminus_listsum_map:
   1.108 + "- listsum (map f xs) = (listsum (map (uminus o f) xs) :: 'a::ab_group_add)"
   1.109 +by(induct xs) simp_all
   1.110 +
   1.111  
   1.112  subsubsection {* @{text upto} *}
   1.113  
   1.114 @@ -2763,6 +2832,7 @@
   1.115    "map_filter f P (x#xs) =
   1.116       (if P x then f x # map_filter f P xs else map_filter f P xs)"
   1.117  
   1.118 +
   1.119  text {*
   1.120    Only use @{text mem} for generating executable code.  Otherwise use
   1.121    @{prop "x : set xs"} instead --- it is much easier to reason about.
   1.122 @@ -2850,8 +2920,11 @@
   1.123    "map_filter f P xs = map f (filter P xs)"
   1.124    by (induct xs) auto
   1.125  
   1.126 -
   1.127 -text {* code for bounded quantification over nats *}
   1.128 +lemma [code inline]: "listsum (map f xs) = foldl (%n x. n + f x) 0 xs"
   1.129 +by(simp add:listsum_foldr foldl_map[symmetric] foldl_foldr1)
   1.130 +
   1.131 +
   1.132 +text {* Code for bounded quantification over nats. *}
   1.133  
   1.134  lemma atMost_upto [code unfold]:
   1.135    "{..n} = set [0..n]"