src/HOL/List.thy
author nipkow
Wed Jul 09 12:57:04 1997 +0200 (1997-07-09)
changeset 3507 157be29ad5ba
parent 3465 e85c24717cad
child 3584 8f9ee0f79d9a
permissions -rw-r--r--
Improved length = size translation.
     1 (*  Title:      HOL/List.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     5 
     6 The datatype of finite lists.
     7 *)
     8 
     9 List = Divides +
    10 
    11 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
    12 
    13 consts
    14   "@"         :: ['a list, 'a list] => 'a list            (infixr 65)
    15   filter      :: ['a => bool, 'a list] => 'a list
    16   concat      :: 'a list list => 'a list
    17   foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
    18   hd          :: 'a list => 'a
    19   set         :: 'a list => 'a set
    20   list_all    :: ('a => bool) => ('a list => bool)
    21   map         :: ('a=>'b) => ('a list => 'b list)
    22   mem         :: ['a, 'a list] => bool                    (infixl 55)
    23   nth         :: [nat, 'a list] => 'a
    24   take, drop  :: [nat, 'a list] => 'a list
    25   takeWhile,
    26   dropWhile   :: ('a => bool) => 'a list => 'a list
    27   tl,ttl      :: 'a list => 'a list
    28   rev         :: 'a list => 'a list
    29 
    30 syntax
    31   (* list Enumeration *)
    32   "@list"     :: args => 'a list                          ("[(_)]")
    33 
    34   (* Special syntax for filter *)
    35   "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_:_ ./ _])")
    36 
    37 translations
    38   "[x, xs]"     == "x#[xs]"
    39   "[x]"         == "x#[]"
    40   "[x:xs . P]"  == "filter (%x.P) xs"
    41 
    42 syntax (symbols)
    43   "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_\\<in>_ ./ _])")
    44 
    45 
    46 consts
    47   lists        :: 'a set => 'a list set
    48 
    49   inductive "lists A"
    50   intrs
    51     Nil  "[]: lists A"
    52     Cons "[| a: A;  l: lists A |] ==> a#l : lists A"
    53 
    54 
    55 (*Function "size" is overloaded for all datatypes.  Users may refer to the
    56   list version as "length".*)
    57 syntax   length :: 'a list => nat
    58 translations  "length"  =>  "size:: _ list => nat"
    59 
    60 primrec hd list
    61   "hd([]) = arbitrary"
    62   "hd(x#xs) = x"
    63 primrec tl list
    64   "tl([]) = arbitrary"
    65   "tl(x#xs) = xs"
    66 primrec ttl list
    67   (* a "total" version of tl: *)
    68   "ttl([]) = []"
    69   "ttl(x#xs) = xs"
    70 primrec "op mem" list
    71   "x mem [] = False"
    72   "x mem (y#ys) = (if y=x then True else x mem ys)"
    73 primrec set list
    74   "set [] = {}"
    75   "set (x#xs) = insert x (set xs)"
    76 primrec list_all list
    77   list_all_Nil  "list_all P [] = True"
    78   list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
    79 primrec map list
    80   "map f [] = []"
    81   "map f (x#xs) = f(x)#map f xs"
    82 primrec "op @" list
    83   "[] @ ys = ys"
    84   "(x#xs)@ys = x#(xs@ys)"
    85 primrec rev list
    86   "rev([]) = []"
    87   "rev(x#xs) = rev(xs) @ [x]"
    88 primrec filter list
    89   "filter P [] = []"
    90   "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
    91 primrec foldl list
    92   "foldl f a [] = a"
    93   "foldl f a (x#xs) = foldl f (f a x) xs"
    94 primrec concat list
    95   "concat([]) = []"
    96   "concat(x#xs) = x @ concat(xs)"
    97 primrec drop list
    98   drop_Nil  "drop n [] = []"
    99   drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
   100 primrec take list
   101   take_Nil  "take n [] = []"
   102   take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
   103 primrec nth nat
   104   "nth 0 xs = hd xs"
   105   "nth (Suc n) xs = nth n (tl xs)"
   106 primrec takeWhile list
   107   "takeWhile P [] = []"
   108   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
   109 primrec dropWhile list
   110   "dropWhile P [] = []"
   111   "dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)"
   112 
   113 end
   114 
   115 ML
   116 
   117 local
   118 
   119 (* translating size::list -> length *)
   120 
   121 fun size_tr' (Type ("fun", (Type ("list", _) :: _))) [t] =
   122       Syntax.const "length" $ t
   123   | size_tr'   _ _ = raise Match;
   124 
   125 in
   126 
   127 val typed_print_translation = [("size", size_tr')];
   128 
   129 end;