(*
 * nat.txt (2011/11/01 版)
 *   [注意] 2011/10/25 に配布した版は、バグがあって正く動かない !!
 *		- zadd の定義に誤り
 *
 * ペアノの公理による自然数の定義
 *	0) 0 は自然数
 *	1) x が自然数ならば s[x] ( = x + 1 ) は自然数
 *	2) 上記の規則でできる物だけが自然数である
 *
 *)

(*
 * コード化 ( 数字列 0, 1, 2 ) 、ペアノ形式 ( 0, s[0], s[s[0]] ) 間の変換
 *	ntop : N -> P
 *	pton : P -> N
 *)

ntop[0] := 0
ntop[x_] := s[ntop[x - 1]]

pton[0] := 0
pton[s[x_]] := pton[x] + 1

(*
 * ペアノ形式での和
 *
 *	   0    + x =       x
 *	(x + 1) + y = ( x + y ) + 1
 *)

padd[0, x_] := x
padd[s[x_], y_] := s[padd[x, y]]

(*
 * ペアノ形式での積
 *
 *	   0    * x =       0
 *	(x + 1) * y = ( x * y ) + y
 *)

pmul[0,_] := 0
pmul[s[x_], y_] := padd[pmul[x, y], y]

(*
 * ペアノ形式での部分差 ( x > y => x-y, x < y => 0 )
 *
 *	  0   -*-   x   =     0
 *	  x   -*-   0   =     x
 *	(x+1) -*- (y+1) =  x -*- y
 *)

psub[0, _] := 0
psub[x_, 0] := x
psub[s[x_], s[y_]] := psub[x, y]

(*
 * ペアノ形式で整数を扱う
 *
 *)

bar[pp[0, x_]] := pp[0, x]
bar[pp[x_, 0]] := pp[x, 0]
bar[pp[s[x_], s[y_]]] := bar[pp[x, y]]

(*
 * 整数とそのペアノ形式の変換
 *)

ntoz[z_] := pp[ntop[z], 0] /; z >= 0
ntoz[z_] := pp[0, ntop[-z]] /; z < 0

zton[pp[0, x_]] := -pton[x]
zton[pp[x_, 0]] := pton[x]
zton[x_] := zton[bar[x]]

(*
 * if then else 関数
 *)

pifz[0, x_, _] := x
pifz[_, _, y_] := y

(*
 * 大小比較
 *)

pgt[x_, y_] := pifz[psub[x, y], y, x]

plt[x_, y_] := pifz[psub[x, y], x, y]

(*
 * 最大公約数
 *)

pgcm[0, x_] := x
pgcm[x_, y_] := pgcm[psub[pgt[x, y], plt[x, y]], plt[x, y]]

(*
 * 割り算
 *)

pdiv[0, _] := 0
pdiv[x_, y_] := pifz[psub[s[x],y],0,s[pdiv[psub[x, y], y]]]

(*
 * 余り
 *)

prem[x_, y_] := psub[x, pmul[y, pdiv[x, y]]]

(*
 * 符号の変更
 *)

zminus[pp[x_,y_]] := pp[y,x]

 (*
  * 絶対値
  *)

zabs[pp[0,x_]] := pp[x,0]
zabs[z_] := z

 (*
  * 整数のペアノ形式
  *)

ztop[pp[x_,0]] := x
ztop[pp[0,y_]] := y

ptoz[x_] := pp[x,0]

 (*
  * 整数のペアノ形式での計算
  *)

zadd[pp[x_,y_],pp[u_,v_]] := bar[pp[padd[x,u],padd[y,v]]]

zsub[x_,y_] := zadd[x,zminus[y]]

zmul[pp[x_,y_],pp[u_,v_]] := pp[padd[pmul[x,u],pmul[y,v]],padd[pmul[x,v],pmul[y,u]]]
zpmul[pp[x_,y_],z_] := pp[pmul[x,z],pmul[y,z]]

zpdiv[pp[x_,y_],z_] := pp[pdiv[x,z],pdiv[y,z]]

(*
 * 有理数のペアノ形式での計算
 *)

qbar[qq[x_,y_]] := qq[zpdiv[x,pgcm[ztop[x],y]],pdiv[y,pgcm[ztop[x],y]]]

ntoq[{x_,y_}] := qbar[qq[ntoz[x],ntop[y]]]
qton[qq[x_,y_]] := {zton[x],pton[y]}

qmul[qq[x_,y_],qq[u_,v_]] := qbar[qq[zmul[x,u],pmul[y,v]]]

qadd[qq[x_,y_],qq[u_,v_]] := qbar[qq[zadd[zpmul[x,v],zpmul[u,y]],pmul[y,v]]]