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