src/HOL/List.thy

A few new lemmas

(*  Title:      HOL/List.thy
    ID:         $Id$
    Author:     Tobias Nipkow
*)

header {* The datatype of finite lists *}

theory List
imports PreList
begin

datatype 'a list =
    Nil    ("[]")
  | Cons 'a  "'a list"    (infixr "#" 65)

subsection{*Basic list processing functions*}

consts
  "@" :: "'a list => 'a list => 'a list"    (infixr 65)
  filter:: "('a => bool) => 'a list => 'a list"
  concat:: "'a list list => 'a list"
  foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
  foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
  hd:: "'a list => 'a"
  tl:: "'a list => 'a list"
  last:: "'a list => 'a"
  butlast :: "'a list => 'a list"
  set :: "'a list => 'a set"
  list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool"
  map :: "('a=>'b) => ('a list => 'b list)"
  nth :: "'a list => nat => 'a"    (infixl "!" 100)
  list_update :: "'a list => nat => 'a => 'a list"
  take:: "nat => 'a list => 'a list"
  drop:: "nat => 'a list => 'a list"
  takeWhile :: "('a => bool) => 'a list => 'a list"
  dropWhile :: "('a => bool) => 'a list => 'a list"
  rev :: "'a list => 'a list"
  zip :: "'a list => 'b list => ('a * 'b) list"
  upt :: "nat => nat => nat list" ("(1[_..</_'])")
  remdups :: "'a list => 'a list"
  remove1 :: "'a => 'a list => 'a list"
  null:: "'a list => bool"
  "distinct":: "'a list => bool"
  replicate :: "nat => 'a => 'a list"
  rotate1 :: "'a list \<Rightarrow> 'a list"
  rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
  sublist :: "'a list => nat set => 'a list"
(* For efficiency *)
  mem :: "'a => 'a list => bool"    (infixl 55)
  list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
  list_all:: "('a => bool) => ('a list => bool)"
  itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
  map_filter :: "('a => 'b) => ('a => bool) => 'a list => 'b list"


nonterminals lupdbinds lupdbind

syntax
  -- {* list Enumeration *}
  "@list" :: "args => 'a list"    ("[(_)]")

  -- {* Special syntax for filter *}
  "@filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_:_./ _])")

  -- {* list update *}
  "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")
  "" :: "lupdbind => lupdbinds"    ("_")
  "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")
  "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)

  upto:: "nat => nat => nat list"    ("(1[_../_])")

translations
  "[x, xs]" == "x#[xs]"
  "[x]" == "x#[]"
  "[x:xs . P]"== "filter (%x. P) xs"