%------------------------------------------------------------------------------
% Negation
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

neg: THEORY

BEGIN

  IMPORTING cauchy

  cx: VAR cauchy_real
  x:  VAR real
  p:  VAR nat
  nzcx: VAR cauchy_nzreal
  pcx: VAR cauchy_posreal
  ncx: VAR cauchy_negreal

  cauchy_neg(cx): cauchy_real = (LAMBDA p: -cx(p))

  neg_lemma: LEMMA cauchy_prop(x,cx) IFF cauchy_prop(-x, cauchy_neg(cx))

  neg_cauchy_nzreal_is_cauchy_nzreal:
    JUDGEMENT cauchy_neg(nzcx) HAS_TYPE cauchy_nzreal

  neg_cauchy_posreal_is_cauchy_negreal:
    JUDGEMENT cauchy_neg(pcx) HAS_TYPE cauchy_negreal

  neg_cauchy_negreal_is_cauchy_posreal:
    JUDGEMENT cauchy_neg(ncx) HAS_TYPE cauchy_posreal

END neg