(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)
(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)
(* ****** ****** *)
(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/arith_prf.atxt
** Time of generation: Thu Jan 11 11:00:02 2018
*)
(* ****** ****** *)
(* Author: Hongwei Xi *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: September, 2011 *)
(* ****** ****** *)

#if(0)
//
// It is available in [basic_dyn.sats]
//
dataprop
MUL_prop
(
  int, int, int
) = // MUL_prop
  | {n:int}
    MULbas (0, n, 0)
  | {m:nat}{n:int}{p:int}
    MULind (m+1, n, p+n) of MUL_prop (m, n, p)
  | {m:pos}{n:int}{p:int}
    MULneg (~(m), n, ~(p)) of MUL_prop (m, n, p)
//
propdef MUL = MUL_prop
//
#endif
(* ****** ****** *)
praxi mul_make : { m, n : int } () -<prf> MUL(m, n, m*n)

praxi mul_elim :
  { m, n : int } {p:int} MUL(m, n, p) -<prf> [p == m*n] void

(* ****** ****** *)
//
prfun mul_istot { m, n : int } () :<prf> [p:int] MUL(m, n, p)

//
prfun mul_isfun { m, n : int }{ p1, p2 : int } ( MUL(m,n,p1)
                                               , MUL(m,n,p2)
                                               ) :<prf> [p1 == p2] void

// endfun
prfun mul_isfun2 { m, n : int }{ p1, p2 : int } ( MUL(m,n,p1)
                                                , MUL(m,n,p2)
                                                ) :<prf> EQINT(p1, p2)

//
(* ****** ****** *)
//
// HX: (m+i)*n = m*n+i*n
//
praxi mul_add_const {i:int}{ m, n : int }{p:int} (pf : MUL(m, n, p)) 
  :<prf> MUL(m+i, n, p+i*n)

// end of [mul_add_const]
//
(* ****** ****** *)
//
// HX: (ax+b)*(cy+d) = ac*xy + ad*x + bc*y + bd
//
praxi mul_expand_linear
{ a, b : int }{ c, d : int }{ x, y : int }{xy:int} (pf : MUL(x, y, xy)) 
  :<prf> MUL(a*x+b, c*y+d, a*c*xy+a*d*x+b*c*y+b*d)

// end of [mul_expand_linear]
(* ****** ****** *)
//
// HX: (a1x1+a2x2+b)*(c1y1+c2y2+d) = ...
//
praxi mul_expand2_linear
{ a1, a2, b : int }{ c1, c2, d : int }{ x1, x2 : int }{ y1, y2 : int }{ x1y1, x1y2, x2y1, x2y2 : int }
(MUL(x1,y1,x1y1), MUL(x1,y2,x1y2), MUL(x2,y1,x2y1), MUL(x2,y2,x2y2)) 
  :<prf>
  MUL_prop(a1*x1+a2*x2+b, c1*y1+c2*y2+d, a1*c1*x1y1+a1*c2*x1y2+a2*c1*x2y1+a2*c2*x2y2+a1*d*x1+a2*d*x2+b*c1*y1+b*c2*y2+b*d)

(* end of [mul_expand2_linear] *)
(* ****** ****** *)
//
prfun mul_gte_gte_gte :
  { m, n : int | m >= 0; n >= 0 } () -<prf> [m*n >= 0] void

prfun mul_lte_gte_lte :
  { m, n : int | m <= 0; n >= 0 } () -<prf> [m*n <= 0] void

prfun mul_gte_lte_lte :
  { m, n : int | m >= 0; n <= 0 } () -<prf> [m*n <= 0] void

prfun mul_lte_lte_gte :
  { m, n : int | m <= 0; n <= 0 } () -<prf> [m*n >= 0] void

//
(* ****** ****** *)
//
prfun mul_nat_nat_nat :
  { m, n : nat } {p:int} MUL(m, n, p) -<prf> [p >= 0] void

prfun mul_pos_pos_pos :
  { m, n : pos } {p:int} MUL(m, n, p) -<prf> [p >= m+n-1] void

//
(* ****** ****** *)
//
prfun mul_negate { m, n : int }{p:int} (pf : MUL(m, n, p)) :<prf>
  MUL(~m, n, ~p)

prfun mul_negate2 { m, n : int }{p:int} (pf : MUL(m, n, p)) :<prf>
  MUL(m, ~n, ~p)

//
(* ****** ****** *)
//
// HX: m*n = n*m
//
prfun mul_commute { m, n : int }{p:int} (pf : MUL(m, n, p)) :<prf>
  MUL(n, m, p)

prfun mul_is_commutative { m, n : int }{ p, q : int }
(pf1 : MUL(m, n, p), pf2 : MUL(n, m, q)) : [p == q] void

//
(* ****** ****** *)
//
// HX: m*(n1+n2) = m*n1+m*n2
//
prfun mul_distribute {m:int}{ n1, n2 : int }{ p1, p2 : int }
(pf1 : MUL(m, n1, p1), pf2 : MUL(m, n2, p2)) :<prf> MUL(m, n1+n2, p1+p2)

//
// HX: (m1+m2)*n = m1*n + m2*n
//
prfun mul_distribute2 { m1, m2 : int }{n:int}{ p1, p2 : int }
(pf1 : MUL(m1, n, p1), pf2 : MUL(m2, n, p2)) :<prf> MUL(m1+m2, n, p1+p2)

//
(* ****** ****** *)
prfun mul_is_associative
{ x, y, z : int }{ xy, yz : int }{ xy_z, x_yz : int }
( pf1 : MUL(x, y, xy)
, pf2 : MUL(y, z, yz)
, pf3 : MUL(xy, z, xy_z)
, pf4 : MUL(x, yz, x_yz)
) :<prf> [xy_z == x_yz] void

(* ****** ****** *)
//
praxi div_istot { x, y : int | x >= 0; y > 0 } () : DIV(x, y, x / y)

//
praxi divmod_istot { x, y : int | x >= 0; y > 0 } () :
  [ q, r : nat | r < y ] DIVMOD(x, y, q, r)

//
(* ****** ****** *)
praxi divmod_isfun
{ x, y : int | x >= 0; y > 0 }{ q1, q2 : int }{ r1, r2 : int }
(pf1 : DIVMOD(x, y, q1, r1), pf2 : DIVMOD(x, y, q2, r2)) :
  [q1 == q2; r1 == r2] void

// end of [divmod_isfun]
(* ****** ****** *)
praxi divmod_elim { x, y : int | x >= 0; y > 0 }{ q, r : int }
(pf : DIVMOD(x, y, q, r)) :
  [ qy : nat | 0 <= r; r < y; x == qy+r ] MUL(q, y, qy)

praxi divmod_mul_elim { x, y : int | x >= 0; y > 0 }{ q, r : int }
(pf : DIVMOD(x, y, q, r)) :
  [0 <= q; 0 <= r; r < y; q == ndiv_int_int(x,y); x == q*y+r] void

// end of [divmod_mul_elim]
(* ****** ****** *)
//
dataprop EXP2(int, int) =
  | EXP2bas((0, 1))
  | {n:nat}{p:nat} EXP2ind((n + 1, 2 * p)) of EXP2((n, p))

prfun lemma_exp2_param :
  {n:int} {p:int} EXP2(n, p) -<prf> [n >= 0; p >= 1] void

// end of [lemma_exp2_param]
//
prfun exp2_istot {n:nat} () : [p:nat] EXP2(n, p)

prfun exp2_isfun {n:nat}{ p1, p2 : int } ( pf1 : EXP2(n, p1)
                                         , pf2 : EXP2(n, p2)
                                         ) : [p1 == p2] void

// end of [exp2_isfun]
//
// HX: proven in [arith_prf.dats]
//
prfun exp2_ispos {n:nat}{p:int} (pf : EXP2(n, p)) : [p >= 1] void

// end of [exp2_ispos]
//
// HX: proven in [arith_prf.dats]
//
prfun exp2_is_mono { n1, n2 : nat | n1 <= n2 }{ p1, p2 : int }
(pf1 : EXP2(n1, p1), pf2 : EXP2(n2, p2)) : [p1 <= p2] void

// end of [exp2_is_mono]
//
// HX: proven in [arith_prf.dats]
//
prfun exp2_muladd { n1, n2 : nat | n1 <= n2 }{ p1, p2 : int }{p:int}
(pf1 : EXP2(n1, p1), pf2 : EXP2(n2, p2), pf3 : MUL(p1, p2, p)) :
  EXP2(n1+n2, p)

// end of [exp2_muladd]
//
(* ****** ****** *)
absprop EXP (int, int, int)

praxi lemma_exp_param {b:int}{n:int}{p:int} (pf : EXP(b, n, p)) :
  [n >= 0] void

// end of [lemma_exp_param]
praxi exp_istot {b:int}{n:nat} () : [p:nat] EXP(b, n, p)

praxi exp_isfun {b:int}{n:int}{ p1, p2 : int } ( pf1 : EXP(b, n, p1)
                                               , pf2 : EXP(b, n, p2)
                                               ) : [p1 == p2] void

// end of [exp_isfun]
praxi exp_elim_0 {n:pos}{p:int} (pf : EXP(0, n, p)) : [p == 0] void

praxi exp_elim_1 {n:int}{p:int} (pf : EXP(1, n, p)) : [p == 1] void

praxi exp_elim_2 {n:int}{p:int} (pf : EXP(2, n, p)) : EXP2(n, p)

praxi exp_elim_b_0 {b:int}{p:int} (pf : EXP(b, 0, p)) : [p == 1] void

praxi exp_elim_b_1 {b:int}{p:int} (pf : EXP(b, 1, p)) : [p == b] void

praxi exp_elim_b_2 {b:int}{p:int} (pf : EXP(b, 2, p)) : MUL(b, b, p)

praxi exp_muladd {b:int}{ n1, n2 : int }{ p1, p2 : int }{p:int}
(pf1 : EXP(b, n1, p1), pf2 : EXP(b, n2, p2)) : EXP(b, n1+n2, p1*p2)

// end of [exp_muladd]
praxi exp_expmul {b:int}{ n1, n2 : int }{bn1:int}{bn1n2:int}
(pf1 : EXP(b, n1, bn1), pf2 : EXP(bn1, n2, bn1n2)) :
  EXP(b, n1*n2, bn1n2)

// end of [exp_muladd]
(* ****** ****** *)
(* end of [arith_prf.sats] *)