Implement rational calculation routine RAT_MUL_CONV

With tests.

More operations to follow of course.

src/rational/Holmakefile

@@ -1,7 +1,15 @@
+EXTRA_CLEANS = selftest.exe
+BOOLLIB = $(dprot $(SIGOBJ)/boolLib.ui)
+NUMTHY = $(dprot $(SIGOBJ)/numeralTheory.uo)
+
 THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
-TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
+TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
+TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))
 
-all: $(TARGETS)
+all: $(TARGETS) selftest.exe
 .PHONY: all
 
+selftest.exe : selftest.uo ratLib.uo ratTheory.uo ratReduce.uo
+	$(HOLMOSMLC) -o $@ $<
+
 intExtensionTheory.sml: $(dprot $(SIGOBJ)/int_arithTheory.uo)

src/rational/ratLib.sml

@@ -463,6 +463,58 @@ val RAT_BASIC_ARITH_CONV =
 val RAT_BASIC_ARITH_TAC =
 	CONV_TAC RAT_BASIC_ARITH_CONV;
 
+(* generic normalisation *)
+open ratSyntax
+fun mk_rvar s = mk_var(s, rat)
+val x = mk_rvar "x"
+val y = mk_rvar "y"
+val z = mk_rvar "z"
+val l_asscomm = prove(
+  mk_eq(mk_rat_add(mk_rat_add(x,y), z),
+        mk_rat_add(mk_rat_add(x,z), y)),
+  CONV_TAC (BINOP_CONV (REWR_CONV (GSYM ratTheory.RAT_ADD_ASSOC))) >>
+  CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV ratTheory.RAT_ADD_COMM))) >>
+  REFL_TAC);
+val r_asscomm = prove(
+  mk_eq(mk_rat_add(x, mk_rat_add(y, z)),
+        mk_rat_add(y, mk_rat_add(x,z))),
+  CONV_TAC (BINOP_CONV (REWR_CONV ratTheory.RAT_ADD_ASSOC)) >>
+  CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV ratTheory.RAT_ADD_COMM))) >>
+  REFL_TAC);
+
+val one_r = ratSyntax.mk_rat_of_num (numSyntax.mk_numeral Arbnum.one)
+
+fun non_coeff t =
+  let
+    open ratSyntax
+  in
+    case Lib.total dest_rat_mul t of
+        SOME (c,x) => if is_literal c then x
+                      else if is_literal x then c
+                      else t
+      | NONE => if is_literal t then one_r else t
+  end
+
+(*
+val merge = REWR_CONV (GSYM ratTheory.RAT_RDISTRIB) THENC
+            LAND_CONV RAT_ADD_CONV
+  let
+    open ratSyntax
+    val (t1,t2) = dest_rat_add t
+
+val RAT_SUM_CANON = GenPolyCanon.gencanon {
+  dest = ratSyntax.dest_rat_add,
+  is_literal = ratSyntax.is_literal,
+  assoc_mode = GenPolyCanon.L,
+  assoc = SPEC_ALL ratTheory.RAT_ADD_ASSOC,
+  symassoc = SYM (SPEC_ALL ratTheory.RAT_ADD_ASSOC),
+  comm = SPEC_ALL ratTheory.RAT_ADD_COMM,
+  l_asscom = l_asscomm,
+  r_asscomm = r_asscomm,
+  non_coeff = non_coeff,
+  merge = merge,
+*)
+
 (*==========================================================================
  * end of structure
  *==========================================================================*)

src/rational/ratReduce.sig

@@ -0,0 +1,8 @@
+signature ratReduce =
+sig
+
+  include Abbrev
+  val RAT_ADD_CONV : conv
+  val RAT_MUL_CONV : conv
+
+end

src/rational/ratReduce.sml

@@ -0,0 +1,152 @@
+structure ratReduce :> ratReduce =
+struct
+
+open HolKernel boolLib Abbrev ratSyntax ratTheory
+
+val zero = mk_rat_of_num (numSyntax.mk_numeral Arbnum.zero)
+val one = mk_rat_of_num (numSyntax.mk_numeral Arbnum.one)
+
+val neg1 = mk_rat_ainv one
+val neg1neg1 = mk_rat_div(neg1, neg1)
+
+val ratmul_thms = CONJUNCTS RAT_MUL_NUM_CALCULATE
+val ratmul_convs = map REWR_CONV ratmul_thms
+val rateq_thms = CONJUNCTS RAT_EQ_NUM_CALCULATE
+val rateq_convs = map REWR_CONV rateq_thms
+
+fun expose_num t =
+  if is_rat_ainv t then expose_num (rand t)
+  else if is_rat_of_num t then expose_num (rand t)
+  else t
+fun expose_num_conv c t =
+  if is_rat_ainv t then RAND_CONV (expose_num_conv c) t
+  else if is_rat_of_num t then RAND_CONV (expose_num_conv c) t
+  else c t
+
+val NOT_F = last (CONJUNCTS boolTheory.NOT_CLAUSES)
+val T_AND = hd (CONJUNCTS (SPEC_ALL boolTheory.AND_CLAUSES))
+
+(* given term of form
+     (n1 / d1) * (n2 / d2)
+   where n's and d's are either &n, or -&n, returns theorem saying
+     |- t = n' / d'
+   with n' and d' similarly literal-shaped. No normalisation is done on result
+*)
+fun coremul_conv t =
+  let
+    val (t1,t2) = dest_rat_mul t
+    val th0 = PART_MATCH (lhand o lhs o rand) RAT_DIVDIV_MUL t1
+    val th1 = PART_MATCH (rand o lhs o rand) th0 t2
+    val th2 =
+      CONV_RULE (RAND_CONV
+                   (RAND_CONV
+                      (BINOP_CONV
+                         (FIRST_CONV ratmul_convs THENC
+                          expose_num_conv reduceLib.REDUCE_CONV))) THENC
+                 (* deal with non-zero preconditions *)
+                 LAND_CONV (BINOP_CONV
+                              (RAND_CONV
+                                 (FIRST_CONV rateq_convs THENC
+                                  EVERY_CONJ_CONV reduceLib.REDUCE_CONV) THENC
+                               REWR_CONV NOT_F) THENC
+                            REWR_CONV T_AND))
+                th1
+  in
+    MP th2 TRUTH
+  end handle HOL_ERR _ =>
+  raise mk_HOL_ERR "ratReduce" "coremul_conv" "denominator probably not zero"
+
+val denom1_conv = REWR_CONV (GSYM RAT_DIV_1)
+fun maybe_denom1_conv t =
+  if is_rat_div t then ALL_CONV t
+  else denom1_conv t
+
+val neg1_neq0 =
+    (RAND_CONV (FIRST_CONV rateq_convs THENC
+                EVERY_CONJ_CONV reduceLib.REDUCE_CONV) THENC
+     REWR_CONV NOT_F) (mk_neg(mk_eq(neg1,zero))) |> EQT_ELIM
+val mul_n1n1_id = MATCH_MP (GEN_ALL RAT_DIV_INV) neg1_neq0
+
+(* ensures that a fraction has positive denominator by multiplying with -1/-1
+   if necessary *)
+fun posdenom_conv t =
+  let
+    val (n,d) = ratSyntax.dest_rat_div t
+  in
+    if is_rat_ainv d then
+      REWR_CONV (GSYM RAT_MUL_RID) THENC
+      RAND_CONV (REWR_CONV (GSYM mul_n1n1_id)) THENC
+      coremul_conv
+    else ALL_CONV
+  end t
+
+val anymul_conv =
+    BINOP_CONV (maybe_denom1_conv THENC posdenom_conv) THENC coremul_conv
+
+val xn = mk_var("x", numSyntax.num)
+val nb1_x = mk_rat_of_num (mk_comb(numSyntax.numeral_tm, numSyntax.mk_bit1 xn))
+val nb2_x = mk_rat_of_num (mk_comb(numSyntax.numeral_tm, numSyntax.mk_bit2 xn))
+
+fun mk_div_eq1 t =
+  TAC_PROOF(([], mk_eq(mk_rat_div(t,t), one)),
+            MATCH_MP_TAC RAT_DIV_INV >>
+            REWRITE_TAC [RAT_EQ_NUM_CALCULATE] >>
+            REWRITE_TAC [arithmeticTheory.NUMERAL_DEF,
+                         arithmeticTheory.BIT2,
+                         arithmeticTheory.BIT1, numTheory.NOT_SUC,
+                         arithmeticTheory.ADD_CLAUSES])
+
+val div_eq_1 = map mk_div_eq1 [nb1_x, nb2_x]
+
+val elim_neg0_conv = LAND_CONV (REWR_CONV RAT_AINV_0)
+
+fun elim_common_factor t = let
+  open Arbint
+  val (n,d) = dest_rat_div t
+  val n_i = int_of_term n
+in
+  if n_i = zero then REWR_CONV RAT_DIV_0 t
+  else let
+      val d_i = int_of_term d
+      val _ = d_i > zero orelse
+              raise mk_HOL_ERR "realSimps" "elim_common_factor"
+                               "denominator must be positive"
+      val g = fromNat (Arbnum.gcd (toNat (abs n_i), toNat (abs d_i)))
+      val _ = g <> one orelse
+              raise mk_HOL_ERR "ratReduce" "elim_common_factor"
+                               "No common factor"
+      val frac_1 = mk_rat_div(term_of_int g, term_of_int g)
+      val frac_new_t =
+          mk_rat_div(term_of_int (n_i div g), term_of_int (d_i div g))
+      val mul_t = mk_rat_mul(frac_new_t, frac_1)
+      val eqn1 = coremul_conv mul_t
+      val frac_1_eq_1 = FIRST_CONV (map REWR_CONV div_eq_1) frac_1
+      val eqn2 =
+          TRANS (SYM eqn1)
+                (AP_TERM(mk_comb(rat_mul_tm, frac_new_t)) frac_1_eq_1)
+    in
+      CONV_RULE (RAND_CONV (REWR_CONV RAT_MUL_RID THENC
+                            TRY_CONV (REWR_CONV RAT_DIV_1)))
+                eqn2
+    end
+end
+
+val RAT_MUL_CONV = anymul_conv THENC TRY_CONV elim_neg0_conv THENC
+                   TRY_CONV elim_common_factor THENC
+                   EVERY_CONV
+                     (map (TRY_CONV o REWR_CONV) [RAT_DIV_1, RAT_DIV_0])
+
+(* given fraction; finds gcd of numerator and denominator (as Arbnum.num) *)
+fun find_gcd t =
+  let
+    val (n,d) = dest_rat_div t
+    val num1 = numSyntax.dest_numeral (expose_num n)
+    val num2 = numSyntax.dest_numeral (expose_num d)
+  in
+    Arbnum.gcd(num1,num2)
+  end
+
+fun RAT_ADD_CONV t =
+  raise mk_HOL_ERR "ratReduce" "RAT_ADD_CONV" "Not implemented yet"
+
+end (* struct *)

src/rational/selftest.sml

@@ -0,0 +1,17 @@
+open testutils
+open ratLib ratReduce
+
+val _ = List.app convtest [
+  ("RAT_MUL_CONV(01)", RAT_MUL_CONV, ``2q * 3``, ``6q``),
+  ("RAT_MUL_CONV(02)", RAT_MUL_CONV, ``2q * -3``, ``-6q``),
+  ("RAT_MUL_CONV(03)", RAT_MUL_CONV, ``-2q * 3``, ``-6q``),
+  ("RAT_MUL_CONV(04)", RAT_MUL_CONV, ``-2q * -3``, ``6q``),
+  ("RAT_MUL_CONV(05)", RAT_MUL_CONV, ``2q/3 * 10``, ``20q/3``),
+  ("RAT_MUL_CONV(06)", RAT_MUL_CONV, ``2q/3 * -10``, ``-20q/3``),
+  ("RAT_MUL_CONV(07)", RAT_MUL_CONV, ``2q/3 * 9``, ``6q``),
+  ("RAT_MUL_CONV(08)", RAT_MUL_CONV, ``2q/3 * -9``, ``-6q``),
+  ("RAT_MUL_CONV(09)", RAT_MUL_CONV, ``2q/3 * -9``, ``-6q``),
+  ("RAT_MUL_CONV(10)", RAT_MUL_CONV, ``2q/3 * (3/4)``, ``1q/2``),
+  ("RAT_MUL_CONV(11)", RAT_MUL_CONV, ``2q/-3 * (3/4)``, ``-1q/2``),
+  ("RAT_MUL_CONV(12)", RAT_MUL_CONV, ``2q/-3 * 0``, ``0q``)
+]