src/HOL/ex/Primrec.thy
author berghofe
Fri Jul 24 13:19:38 1998 +0200 (1998-07-24)
changeset 5184 9b8547a9496a
parent 3419 9092b79d86d5
child 5717 0d28dbe484b6
permissions -rw-r--r--
Adapted to new datatype package.
paulson@3335
     1
(*  Title:      HOL/ex/Primrec
paulson@3335
     2
    ID:         $Id$
paulson@3335
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3335
     4
    Copyright   1997  University of Cambridge
paulson@3335
     5
paulson@3335
     6
Primitive Recursive Functions
paulson@3335
     7
paulson@3335
     8
Proof adopted from
paulson@3335
     9
Nora Szasz, 
paulson@3335
    10
A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
paulson@3335
    11
In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
paulson@3335
    12
paulson@3335
    13
See also E. Mendelson, Introduction to Mathematical Logic.
paulson@3335
    14
(Van Nostrand, 1964), page 250, exercise 11.
paulson@3335
    15
paulson@3335
    16
Demonstrates recursive definitions, the TFL package
paulson@3335
    17
*)
paulson@3335
    18
paulson@3335
    19
Primrec = WF_Rel + List +
paulson@3335
    20
paulson@3335
    21
consts ack  :: "nat * nat => nat"
paulson@3335
    22
recdef ack "less_than ** less_than"
paulson@3419
    23
    "ack (0,n) =  Suc n"
paulson@3335
    24
    "ack (Suc m,0) = (ack (m, 1))"
paulson@3335
    25
    "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
paulson@3335
    26
paulson@3335
    27
consts  list_add :: nat list => nat
berghofe@5184
    28
primrec
paulson@3335
    29
  "list_add []     = 0"
paulson@3335
    30
  "list_add (m#ms) = m + list_add ms"
paulson@3335
    31
paulson@3335
    32
consts  zeroHd  :: nat list => nat
berghofe@5184
    33
primrec
paulson@3335
    34
  "zeroHd []     = 0"
paulson@3335
    35
  "zeroHd (m#ms) = m"
paulson@3335
    36
paulson@3335
    37
paulson@3335
    38
(** The set of primitive recursive functions of type  nat list => nat **)
paulson@3335
    39
consts
paulson@3335
    40
    PRIMREC :: (nat list => nat) set
paulson@3335
    41
    SC      :: nat list => nat
paulson@3335
    42
    CONST   :: [nat, nat list] => nat
paulson@3335
    43
    PROJ    :: [nat, nat list] => nat
paulson@3335
    44
    COMP    :: [nat list => nat, (nat list => nat)list, nat list] => nat
paulson@3335
    45
    PREC    :: [nat list => nat, nat list => nat, nat list] => nat
paulson@3335
    46
paulson@3335
    47
defs
paulson@3335
    48
paulson@3335
    49
  SC_def    "SC l        == Suc (zeroHd l)"
paulson@3335
    50
paulson@3335
    51
  CONST_def "CONST k l   == k"
paulson@3335
    52
paulson@3335
    53
  PROJ_def  "PROJ i l    == zeroHd (drop i l)"
paulson@3335
    54
paulson@3335
    55
  COMP_def  "COMP g fs l == g (map (%f. f l) fs)"
paulson@3335
    56
paulson@3335
    57
  (*Note that g is applied first to PREC f g y and then to y!*)
paulson@3335
    58
  PREC_def  "PREC f g l == case l of
paulson@3335
    59
                             []   => 0
paulson@3335
    60
                           | x#l' => nat_rec (f l') (%y r. g (r#y#l')) x"
paulson@3335
    61
paulson@3335
    62
  
paulson@3335
    63
inductive PRIMREC
paulson@3335
    64
  intrs
paulson@3335
    65
    SC       "SC : PRIMREC"
paulson@3335
    66
    CONST    "CONST k : PRIMREC"
paulson@3335
    67
    PROJ     "PROJ i : PRIMREC"
paulson@3335
    68
    COMP     "[| g: PRIMREC; fs: lists PRIMREC |] ==> COMP g fs : PRIMREC"
paulson@3335
    69
    PREC     "[| f: PRIMREC; g: PRIMREC |] ==> PREC f g: PRIMREC"
paulson@3335
    70
  monos      "[lists_mono]"
paulson@3335
    71
paulson@3335
    72
end