src/HOL/ex/Primrec.thy
 author paulson Fri Jun 06 10:19:53 1997 +0200 (1997-06-06) changeset 3419 9092b79d86d5 parent 3335 b0139b83a5ee child 5184 9b8547a9496a permissions -rw-r--r--
Mended the definition of ack(0,n)
```     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 list_add list
```
```    29   "list_add []     = 0"
```
```    30   "list_add (m#ms) = m + list_add ms"
```
```    31
```
```    32 consts  zeroHd  :: nat list => nat
```
```    33 primrec zeroHd list
```
```    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
```