(* started August 25, 1997 *)

(* modified May 29, 1998 for installation in algebra2.mk2 *)

(* purpose:  develop the theory of order for real numbers *)
(* this theory of order for the reals takes the common approach of
defining the notion of "less than" for real numbers in terms of the
notion of "positive" real number; the axioms for "positive" are
somewhat simpler than the axioms of order *)

(* two theorems are provided in comments which were added to older
theories in the course of development of this file; if you are
running an old version of the web page files, you may need one or
both of these theorems (ZERONOTONE and SIGNPULL) *)

(* script "algebra2"; *) (* this is how this will link in when it is
complete *)

(* this theorem has been added to naturals.mk2; it is provided
here in case you are running this file with an older version of naturals *)

(*

(*

ZERONOTONE:

0 = 1 = 

false

*)

s "0=1";
ri "(LEFT@ZERONAT)**RIGHT@ONENAT";
rri "EVALEQ"; ex();
p "ZERONOTONE";

*)

(*

(* this theorem is found in the newest version of algebra2.mk2
but reproduced here in case you are using an old version *)

(*

SIGNPULL:

?x * -?y = 

-?x * ?y

["BUILTIN","CASEINTRO","DIST","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REFLEX","TIMESCOMM","TIMESTYPE","TYPES"]

*)


s "?x* -?y";
ri "TADDTOP@TIMESTYPE"; ex();
rri "PLUSID"; ex();
left();
initializecounter();
ri "REALZERO";
rri "PLUSMINUS"; ex();
assign "?y_2" "?x*?y";
top();
ri "PLUSASSOC"; ex();
right();
rri "DIST"; ex();
right();
ri "PLUSCOMM**PLUSMINUS** $REALZERO"; ex();
up();
ri "TIMESCOMM**TIMESZERO"; ex();
up();
ri "COMMPLUSID**TREMTOP@MINUSTYPE"; ex();
prove "SIGNPULL";

*)


declareconstant "Positive";  (* predicate true of positive real numbers *)

axiom "POSTYPE" "Positive@?x" "bool:Positive@Real:?x";
axiom "POSPLUS" "(Positive@?x)&Positive@?y" "(Positive@?x+?y)&(Positive@?x)&(Positive@?y)";
axiom "POSTIMES" "(Positive@?x)&Positive@?y" "(Positive@?x*?y)&(Positive@?x)&(Positive@?y)";
axiom "TRICHOTOMY" "(Positive@?x)|(Positive@ -?x)" "~0=Real:?x";

axiom "REAL_LESS_DEF" "?x<?y" "Positive@?y-?x";

(* these definitions may end up competing with defs in student files *)

defineinfix "GREATER" "?x>?y" "?y<?x";

defineinfix "LESS_EQ_REAL" "?x=<?y" "((Real:?x)=(Real:?y))|?x<?y";

defineinfix "GREATER_EQ_REAL" "?x>=?y" "((Real:?x)=(Real:?y))|?x>?y";

defineinfix "NOT_EQ" "?x~=?y" "~?x=?y";

s "Positive@?x";
ri "POSTYPE"; ex();
right();right();
initializecounter();
rri "PLUSMINUS"; ex();
assign "?y_1" "0";
ri "PLUSCOMM**PLUSID"; ex();
top();
rri "POSTYPE";
rri "REAL_LESS_DEF"; ex();
p "ALT_POS_DEF";

(*

POSASSERT:

Positive @ ?x = 

|-Positive @ ?x

["ASSERT","POSTYPE","TYPES"]

*)

s "Positive@?x";
ri "POSTYPE";
rri "TYPES";
ri "RIGHT@ $POSTYPE"; 
ri "ASSERT2";
ex();
prove "POSASSERT";

(*

ZERONOTPOS:

Positive @ 0 = 

false

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","MINUSTYPE","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSTYPE","REFLEX","TRICHOTOMY","TYPES","XOR"]

*)

s "Positive@0";
ri "POSASSERT** $DIDEM"; ex();
right();right();
rri "MINUSZERO"; ex();
top();
ri "TRICHOTOMY"; ex();
right();right();
rri "REALZERO"; ex();
up();
ri "REFLEX"; ex();
up();
rri "FDEF";ex();
p "ZERONOTPOS";

(*

NOTBOTHPOS:

(Positive @ ?x) & Positive @ -?x = 

false

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","MINUSTYPE","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSPLUS","POSTYPE","REFLEX","TRICHOTOMY","TYPES","XOR"]

*)

s "(Positive@?x)&Positive@ -?x";
ri "POSPLUS"; ex();
left();right();
ri "PLUSCOMM**PLUSMINUS"; ex();
up();
ri "POSTYPE**(EVERYWHERE@TYPES)** $POSTYPE"; ex();
ri "ZERONOTPOS"; ex();
up();
ri "CSYM**CZER"; ex();
p "NOTBOTHPOS";


s "(0=Real:?x)|Positive@?x*?x";
ri "MAKE_CASE"; ex();
ri "OR_EXP"; ex();
rri "NOT_EXP"; ex();
left();
rri "TRICHOTOMY"; ex();
top();
ri "OR_EXP"; ex();
ri "EVERYWHERE2@ODDCHOICE"; ex();
downtoleft "false";
ri "FDEF"; ex();
right();
ri "($AT)** $CIDEM"; ex();
ri "RL@0|-|1"; ex();
ri "POSTIMES"; ex();
left();
ri "POSASSERT** $ASSERT_UNEXP"; ex();
ri "ODDCHOICE**1|-|2"; ex();
up();up();
ri "NEWTAUT"; ex();
up();up();up();
downtoright "false";
ri "FDEF"; ex();
right();
ri "($AT)** $CIDEM"; ex();
ri "RL@0|-|2"; ex();
ri "POSTIMES"; ex();
left();right();
ri "SIGNPULL**RIGHT@TIMESCOMM**SIGNPULL"; ex();
ri "MINUSMINUS"; ex();
up();
ri "POSTYPE**(EVERYWHERE@TYPES)** $POSTYPE"; ex();
ri "POSASSERT** $ASSERT_UNEXP"; ex();
ri "ODDCHOICE**1|-|3"; ex();
up();up();
ri "NEWTAUT"; ex();
top();
ri "EVERYWHERE@ $CASEINTRO"; ex();
prove "SQUARE_POS";

(*

POS_ONE:

Positive @ 1 = 

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","DIST","EQUATION","EVALEQ","IF","IFF","MINUSTYPE","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSTIMES","POSTYPE","REFLEX","TIMESCOMM","TIMESID","TIMESTYPE","TRICHOTOMY","TYPES","XOR"]

*)

s "Positive@1";
ri "POSTYPE"; ex();
ri "EVERYWHERE@ $TIMESID"; ex();
ri "ASSERT2"; ex();
ri "($DID)**DSYM"; ex();
left();
rri "ZERONOTONE"; ex();
right();
ri "ONENAT**REALNAT**RIGHT@ $BUILTIN"; ex();
top();
ri "SQUARE_POS"; ex();
p "POS_ONE"; 

(*

POS_ZERO:

Positive @ 0 = 

false

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","MINUSTYPE","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSTYPE","REFLEX","TRICHOTOMY","TYPES","XOR"]

*)

s "Positive@0";
ri "POSASSERT"; ex();
rri "DIDEM"; ex();
right();right();
rri "MINUSZERO"; ex();
up();up();
ri "TRICHOTOMY"; ex();
right();left();
ri "REALZERO"; ex();
up();
ri "REFLEX"; ex();
top();
ri "NEWTAUT"; ex();
p "POS_ZERO";


(*

REAL_LESS_TRANS:

(?x < ?y) & ?y < ?z = 

(?x < ?z) & (?x < ?y) & ?y < ?z

["BUILTIN","CASEINTRO","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSPLUS","REAL_LESS_DEF","REFLEX","TYPES"]

*)

s "(?x<?y)&?y<?z";
ri "RL@REAL_LESS_DEF";ex();
ri "POSPLUS"; ex();
left();right();
ri "ALL_CANCEL"; ex();
ri "PLUSCOMM"; ex();
rri "BREAKMINUS"; ex();
top();
ri "EVERYWHERE@ $REAL_LESS_DEF"; ex(); 
p "REAL_LESS_TRANS"; 

(*

REAL_LESS_CANCEL:

(?z + ?x) < ?z + ?y = 

?x < ?y

["BUILTIN","CASEINTRO","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REAL_LESS_DEF","REFLEX","TYPES"]

*)


s "(?z+?x)<?z+?y";
ri "REAL_LESS_DEF"; ex();
right();
ri "ALL_CANCEL"; ex();
rri "BREAKMINUS"; ex();
top();
rri "REAL_LESS_DEF"; ex();
p "REAL_LESS_CANCEL";

(*

POS_SIGN:

(0 ~= Real : ?x) & Positive @ - ?x = 

(0 ~= Real : ?x) & ~ Positive @ ?x

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","MINUSTYPE","NONTRIV","NOT","NOT_EQ","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSPLUS","POSTYPE","REFLEX","TRICHOTOMY","TYPES","XOR"]

*)

s "(0~=Real:?x)&Positive@ -?x";
ri "EVERYWHERE@NOT_EQ";
ri "NEWTAUT"; ex();
right();right();
ri "ODDCHOICE**PCASEINTRO@true=Positive@?x";ex();
right();left();
right();left();
ri "($AT)**($CIDEM)"; ex();
ri "(LEFT@0|-|2)**RIGHT@0|-|3"; ex();
ri "NOTBOTHPOS"; ex();
up();up();
rri "CASEINTRO"; ex();
top();
ri "EVERYWHERE2@ $ODDCHOICE"; ex();
right();right();right();right();right();right();
rri "(2|-|2)@true"; ex();
right();right();
rri "(2|-|3)@true"; ex();
up();up();
rri "OR_EXP";
ri "LEFT@TRICHOTOMY"; ex();
ri "NOT_EXP**1|-|1"; ex();
up();up();
rri "CASEINTRO"; ex();
up();up();
rri "NOT_EXP"; ex();
top();
rri "NOT_EXP"; rri "AND_EXP";ex();
ri "EVERYWHERE2@ $NOT_EQ"; ex();
ri "ASSERT_UNEXP"; ex();
ri "CRULE1"; ex();
p "POS_SIGN";

(*

DIFF_EQ:

0 = ?y - ?x = 

(Real : ?x) = Real : ?y

["BUILTIN","CASEINTRO","EQUATION","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REFLEX","TYPES"]

*)

s "0=?y-?x";
ri "REAL_TYPE"; ex();
initializecounter();
rri "ADD_CANCEL"; ex();
assign "?z_1" "?x";
ri "REAL_UNTYPE"; ex();
ri "ALL_CANCEL";
ri "LEFT@PLUSCOMM**PLUSID"; ex();
p "DIFF_EQ";

(*

REAL_NOT_LESS:

~ ?x < ?y = 

((Real : ?x) = Real : ?y) | ?y < ?x

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","MINUSTYPE","NONTRIV","NOT","NOT_EQ","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSPLUS","POSTYPE","REAL_LESS_DEF","REFLEX","TRICHOTOMY","TYPES","XOR"]

*)

s "~?x<?y";
ri "RIGHT@REAL_LESS_DEF"; ex();
ri "PCASEINTRO@0=Real:?y-?x";ex();
right();left();
right();right();
ri "TADDTOP@MINUSTYPE"; ex();
rri "0|-|1"; ex();
up();
ri "POS_ZERO"; ex();
up();
ri "NEWTAUT"; ex();
up();right();
ri "MAKE_CASE"; ex();
rri "(2|-|1)@true"; ex();
rri "OR_EXP"; ex();
left();left();
ri "(ASRTEQ) ** $DUBNEG2"; ex();
up();
ri "DEMa"; ex();
ri "EVERYWHERE@ $NOT_EQ";ex();
right();right();right();
ri "TADDTOP@MINUSTYPE"; ex();
ri "($MINUSMINUS)**RIGHT@ALL_CANCEL";ex();
ri "(RIGHT @ PLUSCOMM ** $ BREAKMINUS)"; ex();
up();up();
left();
ri "NOT_EQ"; ex();
right();
ri "RIGHT@TREMTOP@MINUSTYPE"; ex();
ri "DIFF_EQ**EQSYMM** $DIFF_EQ"; ex();
ri "RIGHT@TADDTOP@MINUSTYPE"; ex();

up();
rri "NOT_EQ"; ex();
up();
ri "POS_SIGN"; ex();
left();
ri "NOT_EQ";ex();
right();
ri "RIGHT@TREMTOP@MINUSTYPE"; ex();
ri "DIFF_EQ**EQSYMM** $DIFF_EQ"; ex();
ri "RIGHT@TADDTOP@MINUSTYPE"; ex();
ri "EQUATION**1|-|1"; ex();
up();up();up();
ri "NEWTAUT"; ex();
up();
ri "UNPACK"; ex();
top();
rri "OR_EXP"; ex();
ri "ASSERT_UNEXP"; ex();
ri "DRULE1"; ex();
ri "RIGHT@ $REAL_LESS_DEF"; ex();
ri "LEFT@REAL_UNTYPE**DIFF_EQ"; ex();
ri "(LEFT@EQSYMM)** $LESS_EQ_REAL"; ex();
p "REAL_NOT_LESS";

(* theorems for integration with natorder.mk2 *)

s "(Nat:?x)>=Nat:?y";
ri "GREATER_EQ_REAL"; ex();
ri "EVERYWHERE@ $REALNAT"; ex();
ri "DSYM"; ex();
p "GREATER_OR_EQ";

s "(Nat:?x)=<Nat:?y";
ri "LESS_EQ_REAL"; ex();
ri "EVERYWHERE@ $REALNAT"; ex();
ri "DSYM"; ex();
p "LESS_OR_EQ";


quit();

(* rule of signs theorem under construction *)

s "(0~=Real:?x)&(0~=Real:?y)&Positive@?x*?y";
ri "EVERYWHERE@NOT_EQ"; ex();
ri "NEWTAUT"; ex();
right();right();right();right();
ri "PCASEINTRO@true=Positive@?x";
ri "PCASEINTRO@true=Positive@?y"; ex();
(* 4 cases need to be handled *)

(*case 1*)
right();left();right();left();
right();right();
ri "FDEF"; ex();
right();
ri "($AT)**($CIDEM)"; ex();
ri "(LEFT@0|-|4)**RIGHT@0|-|3"; ex();
ri "POSTIMES"; ex();
left();
ri "POSASSERT**($ASSERT_UNEXP)**1|-|5"; ex();
up();up();
ri "NEWTAUT"; ex();
up();up();
rri "CASEINTRO"; ex();
up();right();

(*case 2*)

right();left();

rri "(2|-|4)@false"; ex();
rri "ODDCHOICE"; ex();
rri "NOT_EXP"; ex();

rri "(2|-|1)@false"; ex();
rri "NOT_EXP"; ex();
rri "AND_EXP"; ex();
ri "ASSERT_UNEXP"; ex();
ri "CRULE1"; ex();
ri "LEFT@ $NOT_EQ"; ex();
rri "POS_SIGN"; ex();

(* cancellation rule for * and <, under construction *)

s "(?z*?x)<?z*?y"; 
ri "REAL_LESS_DEF"; ex();
right();
ri "BREAKMINUS"; ex();
ri "RIGHT@ $SIGNPULL"; ex();
rri "DIST"; ex();
ri "RIGHT@ $BREAKMINUS"; ex();


(* a type of integers *)






quit();