$$$ackerman.pvs
%%%
%%% Author: Paul Y Gloess
%%% http://www.enseirb.fr/~gloess/
%%%
%%% Created Monday December 17, 2001,
%%% last update Wednesday November 19, 2003
%%%
%%% The "ack" function below (Ackerman function) is given in PVS Language
%%% Reference Manual (see Figure 3.3, Page 19), to illustrate recursive
%%% functions: the "ackmeas" measure used in the manual is based upon
%%% ordinal numbers, with their builtin well founded relation.
%%%
%%% Our "ack" function below is based on the "identity" measure, and the
%%% lexical combination of "<" and "<" well founded relation in "nat".
%%%
%%% We use our "wf" library, whose "well_founded_lex" theory establishes
%%% the wellfoundedness of the lexical combination of two well founded
%%% relations: all TCCs, except the wellfoundedness TCC, are automatically
%%% discharged by "subtype-tcc" and "termination-tcc" PVS strategies.
%%%
ackerman: THEORY
BEGIN
<: (well_founded?[nat]) % should belong to prelude!
= < ;
wf: LIBRARY = "../wf" ;
IMPORTING wf@well_founded_lex[nat, nat]
<<: (well_founded?[[nat, nat]])
= lex(<, <) ;
ack(m, n: nat): RECURSIVE nat
= IF m = 0 THEN n+1
ELSIF n = 0 THEN ack(m-1, 1)
ELSE ack(m-1, ack(m, n-1))
ENDIF
MEASURE identity
BY << ;
END ackerman
$$$ackerman.prf
(|ackerman|
(|lessp_TCC1| "" (LEMMA "wf_nat")
(("" (EXPAND "restrict")
(("" (ASSERT)
((""
(CASE "(LAMBDA (i, j: nat): i < j) = (LAMBDA (s: [nat, nat]): <(s))")
(("1" (ASSERT) NIL NIL)
("2" (HIDE-ALL-BUT 1) (("2" (APPLY-EXTENSIONALITY) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|ack_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|ack_TCC2| "" (TERMINATION-TCC) NIL NIL)
(|ack_TCC3| "" (SUBTYPE-TCC) NIL NIL)
(|ack_TCC4| "" (SUBTYPE-TCC) NIL NIL)
(|ack_TCC5| "" (TERMINATION-TCC) NIL NIL)
(|ack_TCC6| "" (TERMINATION-TCC) NIL NIL))