<commit_before>(*  Title:      HOL/ex/Primrec
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1997  University of Cambridge

Primitive Recursive Functions

Proof adopted from
<NAME>, 
A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.

See also <NAME>, Introduction to Mathematical Logic.
(Van Nostrand, 1964), page 250, exercise 11.

Demonstrates recursive definitions, the TFL package
*)

Primrec = WF_Rel + List +

consts ack  :: "nat * nat => nat"
recdef ack "less_than ** less_than"
    "ack (0,n) =  (n + 1)"
    "ack (Suc m,0) = (ack (m, 1))"
    "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"

consts  list_add :: nat list => nat
primrec list_add list
  "list_add []     = 0"
  "list_add (m#ms) = m + list_add ms"<commit_msg>Mended the definition of ack(0,n)<commit_after>(*  Title:      HOL/ex/Primrec
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1997  University of Cambridge

Primitive Recursive Functions

Proof adopted from
<NAME>, 
A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.

See also <NAME>, Introduction to Mathematical Logic.
(<NAME>, 1964), page 250, exercise 11.

Demonstrates recursive definitions, the TFL package
*)

Primrec = WF_Rel + List +

consts ack  :: "nat * nat => nat"
recdef ack "less_than ** less_than"
    "ack (0,n) =  Suc n"
    "ack (Suc m,0) = (ack (m, 1))"
    "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"

consts  list_add :: nat list => nat
primrec list_add list
  "list_add []     = 0"
  "list_add (m#ms) = m + list_add ms"
{'fraction_non_alphanumeric': 0.1203599550056243, 'fraction_numerical': 0.031496062992125984, 'mean_word_length': 3.4143920595533497, 'pattern_counts': {'":': 0, '<': 10, '<?xml version=': 0, '>': 14, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3673756', 'n_tokens_mistral': 695, 'n_tokens_neox': 624, 'n_words': 224}