src/HOL/List.thy
author nipkow
Fri, 22 Dec 1995 12:25:20 +0100
changeset 1419 a6a034a47a71
parent 1370 7361ac9b024d
child 1475 7f5a4cd08209
permissions -rw-r--r--
defined take/drop by induction over list rather than nat.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title:      HOL/List.thy
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994 TU Muenchen
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
Definition of type 'a list as a datatype. This allows primrec to work.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
List = Arith +
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
977
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 965
diff changeset
    12
datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
consts
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
1370
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    16
  "@"	    :: ['a list, 'a list] => 'a list		(infixr 65)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    17
  drop      :: [nat, 'a list] => 'a list
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    18
  filter    :: ['a => bool, 'a list] => 'a list
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    19
  flat      :: 'a list list => 'a list
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    20
  foldl     :: [['b,'a] => 'b, 'b, 'a list] => 'b
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    21
  hd        :: 'a list => 'a
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    22
  length    :: 'a list => nat
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    23
  list_all  :: ('a => bool) => ('a list => bool)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    24
  map       :: ('a=>'b) => ('a list => 'b list)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    25
  mem       :: ['a, 'a list] => bool			(infixl 55)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    26
  nth       :: [nat, 'a list] => 'a
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    27
  take      :: [nat, 'a list] => 'a list
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    28
  tl,ttl    :: 'a list => 'a list
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    29
  rev       :: 'a list => 'a list
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
syntax
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    32
  (* list Enumeration *)
1370
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    33
  "@list"   :: args => 'a list                        ("[(_)]")
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    34
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    35
  (* Special syntax for list_all and filter *)
1370
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    36
  "@Alls"	:: [idt, 'a list, bool] => bool	("(2Alls _:_./ _)" 10)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1327
diff changeset
    37
  "@filter"	:: [idt, 'a list, bool] => 'a list	("(1[_:_ ./ _])")
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    39
translations
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    40
  "[x, xs]"     == "x#[xs]"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
  "[x]"         == "x#[]"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
  "[x:xs . P]"	== "filter (%x.P) xs"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    44
  "Alls x:xs.P"	== "list_all (%x.P) xs"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
primrec hd list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
  hd_Nil  "hd([]) = (@x.False)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
  hd_Cons "hd(x#xs) = x"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    49
primrec tl list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    50
  tl_Nil  "tl([]) = (@x.False)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
  tl_Cons "tl(x#xs) = xs"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    52
primrec ttl list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    53
  (* a "total" version of tl: *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    54
  ttl_Nil  "ttl([]) = []"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    55
  ttl_Cons "ttl(x#xs) = xs"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    56
primrec "op mem" list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    57
  mem_Nil  "x mem [] = False"
965
24eef3860714 changed syntax of "if"
clasohm
parents: 923
diff changeset
    58
  mem_Cons "x mem (y#ys) = (if y=x then True else x mem ys)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    59
primrec list_all list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    60
  list_all_Nil  "list_all P [] = True"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    61
  list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    62
primrec map list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    63
  map_Nil  "map f [] = []"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    64
  map_Cons "map f (x#xs) = f(x)#map f xs"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
primrec "op @" list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    66
  append_Nil  "[] @ ys = ys"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    67
  append_Cons "(x#xs)@ys = x#(xs@ys)"
1169
5873833cf37f Added function rev and its properties length_rev, etc.
lcp
parents: 977
diff changeset
    68
primrec rev list
5873833cf37f Added function rev and its properties length_rev, etc.
lcp
parents: 977
diff changeset
    69
  rev_Nil  "rev([]) = []"
5873833cf37f Added function rev and its properties length_rev, etc.
lcp
parents: 977
diff changeset
    70
  rev_Cons "rev(x#xs) = rev(xs) @ [x]"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    71
primrec filter list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    72
  filter_Nil  "filter P [] = []"
965
24eef3860714 changed syntax of "if"
clasohm
parents: 923
diff changeset
    73
  filter_Cons "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    74
primrec foldl list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
  foldl_Nil  "foldl f a [] = a"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
  foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
primrec length list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
  length_Nil  "length([]) = 0"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    79
  length_Cons "length(x#xs) = Suc(length(xs))"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    80
primrec flat list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    81
  flat_Nil  "flat([]) = []"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
  flat_Cons "flat(x#xs) = x @ flat(xs)"
1419
a6a034a47a71 defined take/drop by induction over list rather than nat.
nipkow
parents: 1370
diff changeset
    83
primrec drop list
a6a034a47a71 defined take/drop by induction over list rather than nat.
nipkow
parents: 1370
diff changeset
    84
  drop_Nil  "drop n [] = []"
a6a034a47a71 defined take/drop by induction over list rather than nat.
nipkow
parents: 1370
diff changeset
    85
  drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
a6a034a47a71 defined take/drop by induction over list rather than nat.
nipkow
parents: 1370
diff changeset
    86
primrec take list
a6a034a47a71 defined take/drop by induction over list rather than nat.
nipkow
parents: 1370
diff changeset
    87
  take_Nil  "take n [] = []"
a6a034a47a71 defined take/drop by induction over list rather than nat.
nipkow
parents: 1370
diff changeset
    88
  take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    89
defs
1327
6c29cfab679c added new arithmetic lemmas and the functions take and drop.
nipkow
parents: 1169
diff changeset
    90
  nth_def  "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    91
end