(* Title: test/Tools/isac/Knowledge/rational-1.sml

   Author: Walther Neuper

   Use is subject to license terms.

Test of basic functions and application to complex examples.

*)

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-------- fun poly_of_term ---------------------------------------------------------------------";

"-------- fun is_poly --------------------------------------------------------------------------";

"-------- fun is_ratpolyexp --------------------------------------------------------------------";

"-------- fun term_of_poly ---------------------------------------------------------------------";

"-------- fun cancel_p special cases -----------------------------------------------------------";

"-------- complex examples: rls norm_Rational --------------------------------------------------";

"-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-------- fun poly_of_term ---------------------------------------------------------------------";

"-------- fun poly_of_term ---------------------------------------------------------------------";

"-------- fun poly_of_term ---------------------------------------------------------------------";

val thy = @{theory Isac_Knowledge};

val vs = TermC.vars_of (TermC.parse_test @{context} "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");

val t = TermC.parse_test @{context} "0 ::real";

if  poly_of_term vs t = SOME [(0, [0, 0, 0])] 

then () else error "poly_of_term 0 changed";

val t = TermC.parse_test @{context} "-3 + - 2 * x ::real";

if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]

then () else error "poly_of_term uminus changed";

if poly_of_term vs (TermC.parse_test @{context} "12::real") = SOME [(12, [0, 0, 0])]

then () else error "poly_of_term 1 changed";

if poly_of_term vs (TermC.parse_test @{context} "x::real") = SOME [(1, [1, 0, 0])]

then () else error "poly_of_term 2 changed";

if         poly_of_term vs (TermC.parse_test @{context} "12 * x \<up> 3") = SOME [(12, [3, 0, 0])]

then () else error "poly_of_term 3 changed";

"~~~~~ fun poly_of_term , args:"; val (vs, t) =

  (vs, (TermC.parse_test @{context} "12 * x \<up> 3"));

           monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with x \<up> 3*)

"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2)) =

  (vs, (1, replicate (length vs) 0), t);

    val (c', es') =

           monom_of_term vs (c, es) m1;

"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>realpow\<close>, _) $ (t as Free _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ num)) ) =

  (vs, (c', es'), m2);

(*+*)c = 12;

(*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0];

if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [3, 0, 0])

then () else error "monom_of_term (realpow): return value CHANGED";

if poly_of_term vs (TermC.parse_test @{context} "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]

then () else error "poly_of_term 4 changed";

if poly_of_term vs (TermC.parse_test @{context} "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") =

  SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]

then () else error "poly_of_term 5 changed";

(*poly_of_term is quite liberal:*)

(*the coefficient may be somewhere, the order of variables and the parentheses 

  within a monomial are arbitrary*)

if poly_of_term vs (TermC.parse_test @{context} "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])]

then () else error "poly_of_term 6 changed";

(*there may even be more than 1 coefficient:*)

if poly_of_term vs (TermC.parse_test @{context} "2 * y \<up> 4 * (x \<up> 3 * 6 * z \<up> 6)") = SOME [(12, [3, 4, 6])]

then () else error "poly_of_term 7 changed";

(*the order and the parentheses within monomials are arbitrary:*)

if poly_of_term vs (TermC.parse_test @{context} "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)")

  = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]

then () else error "poly_of_term 8 changed";

(*from --- rls norm_Rational downto fun gcd_poly ---*)

val t = TermC.parse_test @{context} (*copy from above: "::real" is not required due to " \<up> "*)

  ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^

  "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");

"~~~~~ fun cancel_p_, args:"; val (t) = (t);

val opt = check_fraction t;

val SOME (numerator, denominator) = opt;

(*+*)UnparseC.term numerator = "- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)"; (*isa -- isa2*);

(*+*)UnparseC.term denominator = "- 18 + - 9 * x + 2 * y \<up> 2 + x * y \<up> 2";     (*isa -- isa2*);

       val vs = TermC.vars_of t;

(*+*)UnparseC.terms vs = "[\"x\", \"y\"]";

       val baseT = type_of numerator

       val expT = HOLogic.realT;

val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator);  (*isa <> isa2*)

"-------- fun is_poly --------------------------------------------------------------------------";

"-------- fun is_poly --------------------------------------------------------------------------";

"-------- fun is_poly --------------------------------------------------------------------------";

if is_poly (TermC.parse_test @{context} "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1")

then () else error "is_poly 1 changed";

if not (is_poly (TermC.parse_test @{context} "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))

then () else error "is_poly 2 changed";

"-------- fun is_ratpolyexp --------------------------------------------------------------------";

"-------- fun is_ratpolyexp --------------------------------------------------------------------";

"-------- fun is_ratpolyexp --------------------------------------------------------------------";

if is_ratpolyexp @{term "14 * x * y / (x * y)"}

then () else error "is_ratpolyexp (14 * x * y / (x * y)) CHANGED";

if is_ratpolyexp @{term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"}

then () else error "is_ratpolyexp (2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1) CHANGED";

if is_ratpolyexp @{term "((sin x) \<up> 2 - (cos x) \<up> 2)/ ((sin x)+ (cos x))"}

then error "is_ratpolyexp (((sin x) \<up> 2 - (cos x) \<up> 2)/ ((sin x)+ (cos x)) CHANGED" else ();

if is_ratpolyexp @{term "1 + sqrt x + sqrt y"}

then error "is_ratpolyexp (1 + sqrt x + sqrt y) CHANGED" else ();

"-------- fun term_of_poly ---------------------------------------------------------------------";

"-------- fun term_of_poly ---------------------------------------------------------------------";

"-------- fun term_of_poly ---------------------------------------------------------------------";

val expT = HOLogic.realT

val Free (_, baseT) = (hd o vars o TermC.parse_test @{context}) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";

val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]

val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))

(*precondition for [(c, es),...]: legth es = length vs*)

;

if UnparseC.term (term_of_poly baseT expT vs p) = "1 + 7 * y \<up> 8 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 5"

then () else error "term_of_poly 1 changed";

"-------- fun cancel_p special cases -----------------------------------------------------------";

"-------- fun cancel_p special cases -----------------------------------------------------------";

"-------- fun cancel_p special cases -----------------------------------------------------------";

val thy = @{theory Isac_Knowledge};

val ctxt = Proof_Context.init_global thy

(*------- standard case: *)

val t = TermC.parse_test @{context} "2 / 3 + 1 / 6 ::real";

"~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);

val SOME ((n1, d1), (n2, d2)) =

     (*case*) check_frac_sum t (*of*);

      val vs = TermC.vars_of t;

(*+*)val [] = vs;

val (SOME n1', SOME a, SOME n2', SOME b) =

   (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);

            val ((a', b'), c) = gcd_poly a b

            val (baseT, expT) = (type_of n1, HOLogic.realT);

(*+*)val [(1, [])] = a'; (* 6 * _1_ = 6 *)

(*+*)val [(2, [])] = b'; (* 3 * _2_ = 6 *)

(*+*)val [(3, [])] = c;  (* 3 / 6 \<and> 3 / 3 ..gcd *)

            val nomin = term_of_poly baseT expT vs

              (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));

(*+*)val "5" = UnparseC.term nomin; (* = "3" ERROR*)

(*+*)val [(2, [])] =   the (poly_of_term vs n1);            (*---v----------------------v----*)

(*+*)val [(4, [])] = ((the (poly_of_term vs n1)) %%*%% b'); (* = 2 * _2_  new nomin for 2 / 3*)

(*+*)val [(1, [])] =   the (poly_of_term vs n2);            (*---v----------------------v----*)

(*+*)val [(1, [])] = ((the (poly_of_term vs n2)) %%*%% a'); (* = 1 * _1_  new nomin for 1 / 6*)

(*+*)val [(5, [])] =                                        (* = 4 + 1    new nomin for sum  *)

            (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));

            val denom =                                     (* = 3 * 1 * 2 new denom for sum *)

                        term_of_poly baseT expT vs ((c %%*%% a') %%*%% b');

(*+*)val "6" = UnparseC.term denom;

            val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom);

(*+*)val "5 / 6" = UnparseC.term t'

(*------- 0 / m + 0 / n

             20 years old bug found here: *)

val t = TermC.parse_test @{context} "0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + - 1 * q_0 / 24 * 0 \<up> 4)";

val SOME (t', _) = rewrite_set_ ctxt true norm_Rational t;

(*

:

##  rls: cancel_p_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24) 

###  rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24) 

------------------------------------------------------------these are missing now -----\

/##  rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 1)  from isa2: strange behaviour

/##  rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 1 + 0 / 1)   from isa2: strange behaviour

------------------------------------------------------------these are missing now -----/

##  rls: norm_Rational_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24) 

###  rls: add_fractions_p_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24) 

####  rls: add_fractions_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)

--------------------------------------------------^v^v^v^v^v^v^v^v^--undetected bug

####  rls: add_fractions_p on: 0 = c_2 + 1 / EI * (3 / 24)  =3: ERROR

###  rls: rat_mult_div_pow on: 0 = c_2 + 1 / EI * (3 / 24) 

:

*)

if UnparseC.term t' = "0 = c_2" then () else error "norm_Rational CHANGED"; (*isa2*)

val t = TermC.parse_test @{context} "0 / 12 + 0 / 24 ::real";

       add_fraction_p_ @{theory} t;

"~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);

val SOME ((n1, d1), (n2, d2)) =

     (*case*) check_frac_sum t (*of*);

(*+*)val Const ("Groups.zero_class.zero", _) = n1;

(*+*)val Const ("Groups.zero_class.zero", _) = n2;

      val vs = TermC.vars_of t;

(*+*)val [] = vs;

val (SOME n1', SOME a, SOME n2', SOME b) =

   (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);

(*+*)if n1' = [(0, [])] then () else error "correction w.r.t zero polynomial CHANGED";

            val ((a', b'), c) = gcd_poly a b

            val (baseT, expT) = (type_of n1, HOLogic.realT);

(*+*)val [(1, [])] = a'; (* 1 * _1_ = 24 *)          

(*+*)val [(2, [])] = b'; (* 2 * _2_ = 12 *)          

(*+*)val [(12, [])] = c; (* 12 / 24 \<and> 12 / 12 ..gcd *)  

            val nomin = term_of_poly baseT expT vs

              (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));

(*+*)UnparseC.term nomin; (* = "3" ERROR*)

(* correct ERROR ------------------------------------------------------------------\\*)

(*+*)val SOME [(0, [])] = poly_of_term vs n1 (* ERROR WAS [(1, [])] *)

(* correct ERROR ------------------------------------------------------------------//*)

(*+*)val [(0, [])] =   the (poly_of_term vs n1);            (*---v----------------------v-----*)

(*+*)val [(0, [])] = ((the (poly_of_term vs n1)) %%*%% b'); (* = 0 * _0_  new nomin for 0 / 12*)

(*+*)val [(0, [])] =   the (poly_of_term vs n2);            (*---v----------------------v-----*)

(*+*)val [(0, [])] = ((the (poly_of_term vs n2)) %%*%% a'); (* = 0 * _0_  new nomin for 0 / 24*)

(*+*)val [(0, [])] =                                        (* = 0 + 0    new nomin for sum   *)

        (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));

            val denom =                                     (* = 12 * 1 * 2 new denom for sum *)

                        term_of_poly baseT expT vs ((c %%*%% a') %%*%% b');

(*+*)val "24" =  UnparseC.term denom;

            val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom);

(*+*)val "0 / 24" =  UnparseC.term t'

(*---------- fun cancel_p with Const AA *)

val thy = @{theory Partial_Fractions};

val ctxt = Proof_Context.init_global @{theory}

val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)

val SOME (t', _) = rewrite_set_ ctxt true cancel_p t;

case t' of

  Const (\<^const_name>\<open>divide\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $

    Const (\<^const_name>\<open>one_class.one\<close>, _) => ()

| _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";

"~~~~~ fun cancel_p , args:"; val (t) = (t);

val opt = check_fraction t

val SOME (numerator, denominator) = (*case*) opt (*of*);

if UnparseC.term numerator = "2 * AA" andalso UnparseC.term denominator = "2"

then () else error "check_fraction (2 * AA / 2) changed";

        val vs = TermC.vars_of t;

case vs of

  [Const (\<^const_name>\<open>AA\<close>, _)] => ()

| _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1  changed";

"-------- complex examples: rls norm_Rational --------------------------------------------------";

"-------- complex examples: rls norm_Rational --------------------------------------------------";

"-------- complex examples: rls norm_Rational --------------------------------------------------";

val t = TermC.parse_test @{context} "(3*x+5)/18 - x/2  - -(3*x - 2)/9 = 0";

val SOME (t', _) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';

if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";

val t = TermC.parse_test @{context} "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";

val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';

if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then () 

else error "rational.sml 2";

val t = TermC.parse_test @{context} "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";

val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';

if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then ()

else error "rational.sml 3";

"-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";

"-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";

"-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";

(*Schalk I, p.60 Nr. 215c *)

val t = TermC.parse_test @{context} "(a + b) \<up> 4 * (x - y)  /  ((x - y) \<up> 3 * (a + b) \<up> 2)";

val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;

if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"

then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";

(*SRC Schalk I, p.66 Nr. 381b *)

val t = TermC.parse_test @{context} 

"(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3";

val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;

if UnparseC.term t = "1 / (- 5 + 2 * x)"

then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";

(*Schalk I, p.60 Nr. 215c *)

val t = TermC.parse_test @{context} "(a + b) \<up> 4 * (x - y)  /  ((x - y) \<up> 3 * (a + b) \<up> 2)";

val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;

if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"

then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";