Rat_ZF.thy

header{*The Rational Numbers as Equivalence Classes Over Pairs of Integers*}
theory Rat_ZF
imports "~~/src/ZF/Main_ZFC" "~~/src/ZF/Int_ZF" begin
definition
  ratrel :: i where
    "ratrel \<equiv> { < <x1, x2>, <y1, y2> > \<in> (int*int)*(int*int) .
                x1 $* y2 = x2 $* y1 }"
definition
  rat :: i where
    "rat \<equiv> (int*int)//ratrel - {<z, $#0> . z \<in> int}"

definition
  rat_of :: "i\<Rightarrow>i" --{*coercion fron int to rat*} ("@$ _" [80] 80) where
    "@$ m \<equiv> ratrel `` {<intify(m), 1>}"

definition 
  ratify :: "i\<Rightarrow>i" where
    "ratify(r) \<equiv> if r \<in> rat then r else @$0"

definition
  raw_qminus :: "i\<Rightarrow>i" where
    "raw_qminus(z) \<equiv> \<Union><x,y>\<in>z. ratrel `` {<$- x, y>}"

definition
  qminus :: "i\<Rightarrow>i" ("@- _" [80] 80) where
    "qminus(r) \<equiv> if r \<in> rat then raw_qminus(r) else @$0"

definition
  raw_qmult :: "[i,i]\<Rightarrow>i" where
    "raw_qmult(z1, z2) \<equiv>
     \<Union><x1, y1>\<in>z1. \<Union><x2, y2>\<in>z2. ratrel `` {<x1 $* y1, y1 $* y2>}"

definition 
  qmult :: "[i,i]\<Rightarrow>i" (infixl "@*" 70) where 
    "r1 @* r2 \<equiv> raw_qmult (ratify(r1), ratify(r2))"

definition
  raw_qadd :: "[i,i]\<Rightarrow>i" where
    "raw_qadd(z1, z2) \<equiv>
     \<Union><x1, y1> \<in> z1. \<Union><x2, y2> \<in> z2. ratrel `` { <x1 $* y2 $+ x2 $* y1, y1 $* y2> }"

definition
  qadd :: "[i,i]\<Rightarrow>i" (infixl "@+" 65) where
    "r1 @+ r2 \<equiv> raw_qadd (ratify(r1), ratify(r2))"

definition
  raw_qrecip :: "i\<Rightarrow>i" where
    "raw_qrecip(z) \<equiv> \<Union><x,y>\<in>z. ratrel `` {<y, x>}"

definition
  qrecip :: "i \<Rightarrow> i" where
    "qrecip(r) \<equiv> if r \<in> rat then (if (\<exists>y. <$#0, y> \<in> r) then @$0 else raw_qrecip(r)) else @$0"

definition
  qdiff :: "[i,i]\<Rightarrow>i" (infixl "@-" 65) where
    "z1 @- z2 \<equiv> z1 @+ qminus(z2)"

definition
  qnegative :: "i\<Rightarrow>o" where
    "qnegative(r) \<equiv> \<exists>x y. $#0 $< x & y \<in> int & znegative(y) & <y, x> \<in> r"

definition
  qdiv :: "[i,i]\<Rightarrow>i" (infixl "@/" 65) where
    "qdiv(r1, r2) \<equiv> r1 @* qrecip(r2)"

definition
  qless :: "[i,i]\<Rightarrow>o" (infixl "@<" 50) where
    "r1 @< r2 \<equiv> qnegative(r1 @- r2)"

definition
  qle :: "[i,i]\<Rightarrow>o" (infixl "@\<le>" 50) where
    "r1 @\<le> r2 \<equiv> r1 @< r2 | ratify(r1) = ratify(r2)"


end