$$$ackb.pvs
%%%
%%% Author: Paul Y Gloess
%%% http://www.enseirb.fr/~gloess/
%%%
%%% Created Monday December 17, 2001,
%%% last update Thursday 30 October 2008
%%%
%%% 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.
%%%
%%% Remark: This theory is a variant of "ackerman" theory, built in
%%% class, 30 October 2008, for pedagogical purposes:
%%% 1- instead of merely using the "lex" combinator defined
%%% in "wf@well_founded_lex" theory, the students try to
%%% design an appropriate well founded relation, and come
%%% up with their own explicit definition of << (which
%%% was initially declared;
%%% 2- all the TCCs are proved automatically, except the
%%% wellfoundedness of <<: hence the idea of importing
%%% the "wf@well_founded_lex" theory, which provides the
%%% relevant "lex_well_founded" theorem;
%%% 3- the proof of << wellfoundedness boils down to proving
%%% that << = lex(<, <), where < is restricted to natural
%%% numbers, and using "lex_well_founded" theorem and
%%% "wf_nat" prelude axiom (stating the wellfoundedness
%%% of < nat restriction).
%%%
ackb: THEORY
BEGIN
wf: LIBRARY = "../wf"
IMPORTING wf@well_founded_lex[nat, nat]
<<: (well_founded?[[nat, nat]])
= (LAMBDA (x1y1, x2y2: [nat, nat]):
LET (x1, y1) = x1y1, (x2, y2) = x2y2
IN x1 < x2
OR x1 = x2 AND y1 < y2)
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 ackb
$$$ackb.prf
(|ackb|
(|doublelessp_TCC1| ""
(CASE "lex((lambda (m, n: nat): m