(* This is a test file on induction proofs.  It uses
restricted quantifiers (so we don't have the issue of talking about
addition and multiplication of things which are not numbers).  *)

(* There are some slightly odd behaviors of restricted
quantifiers and sets which require attention -- these are best
seen by running through the examples *)

(* declarations *)

DeclareFunction "Nat" [0];

DeclareFunction "+" [0,0,0];

DeclareFunction "*" [0,0,0];

(* order of operations *)

Spra "*" "+";

(* axioms *)

Axiom "ZeroNat" nil ["0 E Nat"];

Axiom "OneNat" nil ["1ENat"];

(* the next two axioms look different because I write successor
as x+1 (not as a separate operation) so closure under successor is
a special case of closure under addition and I need to "define"
1 as 0+1 *)

(* Axiom "OneDef" nil ["0+1=1"]; *)

Axiom "SumNat" ["a1ENat","a2ENat"] ["a1+a2ENat"];

Axiom "ZeroNotSucc" ["a1ENat","a1+1=0"] nil;

Axiom "SameSucc" ["a1ENat","a2ENat","a1+1=a2+1"] ["a1=a2"];

(* notice use of a restricted quantifier *)

Axiom "Induction" ["0Ea1","(Ax1:Nat.x1Ea1->x1+1Ea1)","a2ENat"] ["a2Ea1"];

(* additional axioms to handle recursive definition of addition
and multiplication *)

Axiom "PlusZero" ["a1ENat"] ["a1+0=a1"];

Axiom "PlusSucc" ["a1ENat","a2ENat"] ["a1+[a2+1]=[a1+a2]+1"];

Axiom "TimesZero" ["a1ENat"] ["a1*0=a1"];

Axiom "TimesSucc" ["a1ENat","a2ENat"] ["a1*[a2+1]=a1*a2+a1"];

(* a very easy theorem *)

(* an odd feature of this theorem is that the ind hyp
is never used *)

Start "a1ENat -> a1=0 v (Ex1:Nat.x1+1=a1)";
ThmCut "Induction";
su 2 "{x1:Nat|x1=0v(Ex2:Nat.x2+1=x1)}";
r();(* r(); *) UseThm "ZeroNat" nil [1];
r();r();

(* proof of induction step starts *)

r();r();r();(* r(); *)
ThmCut "OneNat"; UseThm "SumNat" [3,1] [1];
r(); gr 2; r(); Triv 2 1; r();

(* from here on seems to be tidying up ThmCut *)

su 3 "a1"; Gr 2; Triv 1 2;

l(); (* rf(); *) r(); Triv 3 1;

Prove 1 "ZeroOrSucc";

(* a less trivial theorem *)

(* but still pretty easy *)

Start "a1ENat -> 0+a1=a1";

r();

ThmCut "Induction";

su 2 "{x1:Nat|0+x1=x1}";

r();(*r();*) UseThm "ZeroNat" nil [1];

ThmCut "ZeroNat";

UseThm "PlusZero" [1] [1];

(* finished basis step *)

r();r();l();(* rf(); *)
r();(*r();*) ThmCut "OneNat"; UseThm "SumNat" [2,1] [1];

ThmCut "PlusSucc";

su 5 "0"; UseThm "ZeroNat" nil [1]; Done();

rwr nil;

gl 3; rwr nil; r();

Done();  l(); (* rf(); *) Triv 2 1;

Prove 2 "ZeroPlusLeft";

(* suggested next step:  try to prove commutativity of addition *)

(* the basic idea is to prove that the set

{x1:Nat | (Ax2:Nat.x1+x2=x2+x1)} is inductive (contains 0
and is closed under successor) and so contains
all natural numbers *)