module induction.

import lists, control.
import goals, tacticals.
import fol, folpn, lj, parser, printer.
import nats.

type nat_r   goal -> goal -> o.

nat_r (Vs | Delta --> (nat z)) tt.
nat_r (Vs | Delta --> (nat (s N))) (Vs | Delta --> (nat N)).

type nat_l   string -> int -> goal -> goal -> o.

nat_l Str N 
  (Vs | Delta --> C)
  ( (Vs | Delta' --> (Inv z)) cc
    (all i\ ((pr i "i" :: Vs) | ((Inv i)::Delta') --> (Inv (s i)))) cc
    (Vs | ((Inv Term)::Delta') --> C)) :- 
  load_pnames Vs (read_abstraction Str Inv),
  nth_and_replace N (nat Term) Delta nil Delta'.

% type hopea  goal -> o.
% type hopeb  goal -> o.
% type hopec  goal -> o.
% 
% hopea Out :-
%    tl_loop (nil | nil  --> (forall "u" u\ (nat u imp plus u zero u))) Out.
% 
% hopeb Out :-
%    tl_loop (nil | nil  --> 
%             (forall "u" u\ forall "v" v\ forall "w" w\ 
%                (nat u and nat v and plus u v w) imp plus v u w)) Out.
% 
% hopec Out :-
%   tl_loop 
%     (nil | nil  --> (plus (succ (succ zero)) zero (succ (succ zero)))) 
%     Out.