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