(* testexamples for Poly, polynomials

   author: Matthias Goldgruber 2003

   (c) due to copyright terms

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

LEGEND:

WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'

          examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'

*)

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

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

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

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

"----------- fun is_polyexp --------------------------------------------------------------------";

"----------- fun has_degree_in -----------------------------------------------------------------";

"----------- fun mono_deg_in -------------------------------------------------------------------";

"----------- fun mono_deg_in -------------------------------------------------------------------";

"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";

"-------- investigate (new 2002) uniary minus -----------";

"-------- check make_polynomial with simple terms -------";

"-------- fun is_multUnordered --------------------------";

"-------- examples from textbook Schalk I ---------------";

"-------- check pbl  'polynomial simplification' --------";

"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";

"-------- interSteps for Schalk 299a --------------------";

"-------- norm_Poly NOT COMPLETE ------------------------";

"-------- ord_make_polynomial ---------------------------";

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

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

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

"----------- fun is_polyexp --------------------------------------------------------------------";

"----------- fun is_polyexp --------------------------------------------------------------------";

"----------- fun is_polyexp --------------------------------------------------------------------";

val thy = @{theory Partial_Fractions};

val ctxt = Proof_Context.init_global thy;

val t = (the o (parseNEW  ctxt)) "x / x";

if is_polyexp t then error "NOT is_polyexp (x / x)" else ();

val t = (the o (parseNEW  ctxt)) "-1 * A * 3";

if is_polyexp t then () else error "is_polyexp (-1 * A * 3)";

val t = (the o (parseNEW  ctxt)) "-1 * AA * 3";

if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)";

"----------- fun has_degree_in -----------------------------------------------------------------";

"----------- fun has_degree_in -----------------------------------------------------------------";

"----------- fun has_degree_in -----------------------------------------------------------------";

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "1";

if has_degree_in t v = 0 then () else error "has_degree_in (1) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "1";

if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";

(*----------*)

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";

if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";

if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";

(*----------*)

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";

if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";

if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";

(*----------*)

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";

if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";

if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";

(*----------*)

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";

if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";

if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";

(*----------*)

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";

if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";

if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";

(*----------*)

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";

if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";

if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";

(*----------*)

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "x";

if has_degree_in t v = 1 then () else error "has_degree_in (x) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "AA";

if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";

(*----------*)

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";

if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";

if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";

"----------- fun mono_deg_in -------------------------------------------------------------------";

"----------- fun mono_deg_in -------------------------------------------------------------------";

"----------- fun mono_deg_in -------------------------------------------------------------------";

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";

if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";

if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";

if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";

if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "x";

if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";

if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";

if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";

(*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *)

val thy = @{theory Partial_Fractions}

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";

if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";

if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";

if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";

if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "AA";

if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";

if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";

if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";

"----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";

"----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";

"----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";

val thy = @{theory Partial_Fractions}

val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";

val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;

val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";

val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;

"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";

"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";

"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";

val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";

val SOME (id, t') = eval_is_expanded_in 0 0 t 0;

if UnparseC.term t' = "-8 - 2 * x + x \<up> 2 is_expanded_in x = True"

         andalso id = "-8 - 2 * x + x \<up> 2 is_expanded_in x = True"

then () else error "eval_is_expanded_in x ..changed";

val thy = @{theory Partial_Fractions}

val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";

val SOME (id, t') = eval_is_expanded_in 0 0 t 0;

if  UnparseC.term t' = "-8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"

          andalso id = "-8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"

then () else error "eval_is_expanded_in AA ..changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*x + x \<up> 2) is_poly_in x";

val SOME (id, t') = eval_is_poly_in 0 0 t 0;

if  UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"

          andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"

then () else error "is_poly_in x ..changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*AA + AA \<up> 2) is_poly_in AA";

val SOME (id, t') = eval_is_poly_in 0 0 t 0;

if  UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"

          andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"

then () else error "is_poly_in AA ..changed";

val thy = @{theory Partial_Fractions}

val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";

val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;

val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";

val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;

"-------- investigate (new 2002) uniary minus -----------";

"-------- investigate (new 2002) uniary minus -----------";

"-------- investigate (new 2002) uniary minus -----------";

(*---------------------------------------------- vvvvvvvvvvvvvv -----------------------*)

val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)

TermC.atomty t;

(*

*** Const (HOL.Trueprop, bool => prop)

*** . Const (HOL.eq, real => real => bool)

*** . . Const (Groups.minus_class.minus, real => real => real)

*** . . . Const (Groups.zero_class.zero, real)

*** . . . Var ((x, 0), real)

*** . . Const (Groups.uminus_class.uminus, real => real)

*** . . . Var ((x, 0), real)

*)

case t of

  Const ("HOL.Trueprop", _) $

    (Const ("HOL.eq", _) $ 

      (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $ 

        Var (("x", 0), _)) $

             (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()

| _ => error "internal representation of \"0 - ?x = - ?x\" changed";

(*----------------------------------- vvvv --------------------------------------------*)

val t = (Thm.term_of o the o (TermC.parse thy)) "-1";

TermC.atomty t;

(*** -------------

*** Free ( -1, real)                      *)

case t of

  Free ("-1", _) => ()

| _ => error "internal representation of \"-1\" changed";

(*----------------------------------- vvvvv -------------------------------------------*)

val t = (Thm.term_of o the o (TermC.parse thy)) "- 1";

TermC.atomty t;

(*

*** 

*** Free (-1, real)

*** 

*)

case t of

 Free ("-1", _) => ()

| _ => error "internal representation of \"- 1\" changed";

"======= these external values all have the same internal representation";

(* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)

(*----------------------------------- vvvvv -------------------------------------------*)

val t = (Thm.term_of o the o (TermC.parse thy)) "-x";

TermC.atomty t;

(**** -------------

*** Free ( -x, real)*)

case t of

  Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()

| _ => error "internal representation of \"-x\" changed";

(*----------------------------------- vvvvv -------------------------------------------*)

val t = (Thm.term_of o the o (TermC.parse thy)) "- x";

TermC.atomty t;

(**** -------------

*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)

case t of

  Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()

| _ => error "internal representation of \"- x\" changed";

(*----------------------------------- vvvvvv ------------------------------------------*)

val t = (Thm.term_of o the o (TermC.parse thy)) "-(x)";

TermC.atomty t;

(**** -------------

*** Free ( -x, real)*)

case t of

  Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()

| _ => error "internal representation of \"-(x)\" changed";

"-------- check make_polynomial with simple terms -------";

"-------- check make_polynomial with simple terms -------";

"-------- check make_polynomial with simple terms -------";

"----- check 1 ---";

val t = TermC.str2term "2*3*a";

val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";

"----- check 2 ---";

val t = TermC.str2term "2*a + 3*a";

val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";

"----- check 3 ---";

val t = TermC.str2term "2*a + 3*a + 3*a";

val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";

"----- check 4 ---";

val t = TermC.str2term "3*a - 2*a";

val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "a" then () else error "check make_polynomial 4";

"----- check 5 ---";

val t = TermC.str2term "4*(3*a - 2*a)";

val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";

"----- check 6 ---";

val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";

val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";

"-------- fun is_multUnordered --------------------------";

"-------- fun is_multUnordered --------------------------";

"-------- fun is_multUnordered --------------------------";

val thy = @{theory "Isac_Knowledge"};

"===== works for a simple example, see rewrite.sml -- fun app_rev ===";

val t = TermC.str2term "x \<up> 2 * x";

val SOME (t', _) = rewrite_set_ thy true order_mult_ t;

if UnparseC.term t' = "x * x \<up> 2" then ()

else error "poly.sml Poly.is_multUnordered doesn't work";

(* 100928 Rewrite.trace_on shows the first occurring difference in 267b:

###  rls: order_mult_ on: 5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +

 (-48 * x \<up> 4 + 8))

######  rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered

#######  try calc: Poly.is_multUnordered'

=======  calc. to: False  !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!

*)

val t = TermC.str2term "5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +  (-48 * x \<up> 4 + 8))";

"----- is_multUnordered ---";

val tsort = sort_variables t;

UnparseC.term tsort = "2 * (5 * (x \<up> 2 * x \<up> 7)) + 3 * (5 * x \<up> 2) + 6 * x \<up> 7 + 9 +\n-1 * (3 * (6 * (x \<up> 4 * x \<up> 5))) +\n-1 * (-1 * (3 * x \<up> 5)) +\n-48 * x \<up> 4 +\n8";

is_polyexp t;

tsort = t;

is_polyexp t andalso not (t = sort_variables t);

if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";

"----- eval_is_multUnordered ---";

val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +  (-48 * x \<up> 4 + 8))) is_multUnordered";

case eval_is_multUnordered "testid" "" tm thy of

    SOME (_, Const ("HOL.Trueprop", _) $ 

                   (Const ("HOL.eq", _) $

                          (Const ("Poly.is_multUnordered", _) $ _) $ 

                          Const ("HOL.True", _))) => ()

  | _ => error "poly.sml diff. eval_is_multUnordered";

"----- rewrite_set_ STILL DIDN'T WORK";

val SOME (t, _) = rewrite_set_ thy true order_mult_ t;

UnparseC.term t;

"-------- examples from textbook Schalk I ---------------";

"-------- examples from textbook Schalk I ---------------";

"-------- examples from textbook Schalk I ---------------";

"-----SPB Schalk I p.63 No.267b ---";

(*associate poly* )

val t = TermC.str2term "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "17 + 15 * x \<up> 2 + -48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 + -8 * x \<up> 9"

then () else error "poly.sml: diff.behav. in make_polynomial 1";

"-----SPB Schalk I p.63 No.275b ---";

val t = TermC.str2term "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if (UnparseC.term t) = ("3 * x \<up> 4 + -2 * x \<up> 3 * y + -5 * x \<up> 2 * y \<up> 2 + " ^

  "4 * x * y \<up> 3 +\n-2 * y \<up> 4")

then () else error "poly.sml: diff.behav. in make_polynomial 2";

"-----SPB Schalk I p.63 No.279b ---";

val t = TermC.str2term "(x-a)*(x-b)*(x-c)*(x-d)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if (UnparseC.term t) = 

  ("a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x \<up> 2 +\n" ^

  "-1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n-1 * a * x \<up> 3 +\n" ^

  "-1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n-1 * b * x \<up> 3 +\n" ^

  "c * d * x \<up> 2 +\n-1 * c * x \<up> 3 +\n-1 * d * x \<up> 3 +\nx \<up> 4")

then () else error "poly.sml: diff.behav. in make_polynomial 3";

( *associate poly*)

"-----SPB Schalk I p.63 No.291 ---";

val t = TermC.str2term "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if (UnparseC.term t) = "50 + -770 * x + 4520 * x \<up> 2 + -16320 * x \<up> 3 + -26880 * x \<up> 4"

then () else error "poly.sml: diff.behav. in make_polynomial 4";

(*associate poly* )

"-----SPB Schalk I p.64 No.295c ---";

val t = TermC.str2term "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if (UnparseC.term t) = ("169 * a \<up> 8 * b \<up> 18 * c \<up> 2 + -312 * a \<up> 7 * b \<up> 15 * c \<up> 10" ^

  " +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18")

then ()else error "poly.sml: diff.behav. in make_polynomial 5";

( *associate poly*)

"-----SPB Schalk I p.64 No.299a ---";

val t = TermC.str2term "(x - y)*(x + y)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

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

then () else error "poly.sml: diff.behav. in make_polynomial 6";

"-----SPB Schalk I p.64 No.300c ---";

val t = TermC.str2term "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if (UnparseC.term t) = "-1 + 9 * x \<up> 4 * y \<up> 2"

then () else error "poly.sml: diff.behav. in make_polynomial 7";

"-----SPB Schalk I p.64 No.302 ---";

val t = TermC.str2term

  "(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "0"

then () else error "poly.sml: diff.behav. in make_polynomial 8";

(* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)

"-----SPB Schalk I p.64 No.306a ---";

val t = TermC.str2term "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8" then ()

else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * -2 * x \<up> 4 = -2 * x \<up> 4";

(*WN071729 when reducing "rls reduce_012_" for Schaerding,

the above resulted in the term below ... but reduces from then correctly*)

val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "1 + -2 * x \<up> 4 + x \<up> 8"

then () else error "poly.sml: diff.behav. in make_polynomial 9b";

"-----SPB Schalk I p.64 No.296a ---";

val t = TermC.str2term "(x - a) \<up> 3";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "-1 * a \<up> 3 + 3 * a \<up> 2 * x + -3 * a * x \<up> 2 + x \<up> 3"

then () else error "poly.sml: diff.behav. in make_polynomial 10";

"-----SPB Schalk I p.64 No.296c ---";

val t = TermC.str2term "(-3*x - 4*y) \<up> 3";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "-27 * x \<up> 3 + -108 * x \<up> 2 * y + -144 * x * y \<up> 2 +\n-64 * y \<up> 3"

then () else error "poly.sml: diff.behav. in make_polynomial 11";

"-----SPB Schalk I p.62 No.242c ---";

val t = TermC.str2term "x \<up> (-4)*(x \<up> (-4)*y \<up> (-2)) \<up> (-1)*y \<up> (-2)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "1"

then () else error "poly.sml: diff.behav. in make_polynomial 12";

"-----SPB Schalk I p.60 No.209a ---";

val t = TermC.str2term "a \<up> (7-x) * a \<up> x";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "a \<up> 7"

then () else error "poly.sml: diff.behav. in make_polynomial 13";

"-----SPB Schalk I p.60 No.209d ---";

val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "d \<up> 3"

then () else error "poly.sml: diff.behav. in make_polynomial 14";

(*---------------------------------------------------------------------*)

(*---------------- ?RL?Bsple bei denen es Probleme gibt----------------*)

(*---------------------------------------------------------------------*)

"-----Schalk I p.64 No.303 ---";

val t = TermC.str2term "(a + 2*b)*(a \<up> 2 + 4*b \<up> 2)*(a - 2*b) - (a - 6*b)*(a \<up> 2 + 36*b \<up> 2)*(a + 6*b)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "1280 * b \<up> 4"

then () else error "poly.sml: diff.behav. in make_polynomial 14b";

(* Richtig - aber Binomische Formel wurde nicht verwendet! *)

(*--------------------------------------------------------------------*)

(*----------------------- Eigene Beispiele ---------------------------*)

(*--------------------------------------------------------------------*)

"-----SPO ---";

val t = TermC.str2term "a \<up> 2*a \<up> (-2)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "1" then ()

else error "poly.sml: diff.behav. in make_polynomial 15";

"-----SPO ---";

val t = TermC.str2term "a + a + a";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "3 * a" then ()

else error "poly.sml: diff.behav. in make_polynomial 16";

"-----SPO ---";

val t = TermC.str2term "a + b + b + b";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "a + 3 * b" then ()

else error "poly.sml: diff.behav. in make_polynomial 17";

"-----SPO ---";

val t = TermC.str2term "a \<up> 2*b*b \<up> (-1)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "a \<up> 2" then ()

else error "poly.sml: diff.behav. in make_polynomial 18";

"-----SPO ---";

val t = TermC.str2term "a \<up> 2*a \<up> (-2)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "1" then ()

else error "poly.sml: diff.behav. in make_polynomial 19";

"-----SPO ---";

val t = TermC.str2term "b + a - b";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "a" then ()

else error "poly.sml: diff.behav. in make_polynomial 20";

"-----SPO ---";

val t = TermC.str2term "b * a * a";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "a \<up> 2 * b" then ()

else error "poly.sml: diff.behav. in make_polynomial 21";

"-----SPO ---";

val t = TermC.str2term "(a \<up> 2) \<up> 3";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "a \<up> 6" then ()

else error "poly.sml: diff.behav. in make_polynomial 22";

"-----SPO ---";

val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()

else error "poly.sml: diff.behav. in make_polynomial 23";

"-----SPO ---";

val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "a \<up> 4" then ()

else error "poly.sml: diff.behav. in make_polynomial 24";

"-----SPO ---";

val t = TermC.str2term "a * b * b \<up> (-1) + a";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "2 * a" then ()

else error "poly.sml: diff.behav. in make_polynomial 25";

"-----SPO ---";

val t = TermC.str2term "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if (UnparseC.term t) = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"

then () else error "poly.sml: diff.behav. in make_polynomial 26";

(*MG030627 -------------vvv-: Verschachtelte Terme -----------*)

"-----SPO ---";

val t = TermC.str2term "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"

then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)

val t = TermC.str2term "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"

then () else error "poly.sml: diff.behav. in make_polynomial 28";

"-------- check pbl  'polynomial simplification' --------";

"-------- check pbl  'polynomial simplification' --------";

"-------- check pbl  'polynomial simplification' --------";

val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];

"-----0 ---";

case Refine.refine fmz ["polynomial", "simplification"]of

    [M_Match.Matches (["polynomial", "simplification"], _)] => ()

  | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";

(*...if there is an error, then ...*)

"-----1 ---";

(*default_print_depth 7;*)

val pbt = Problem.from_store ["polynomial", "simplification"];

(*default_print_depth 3;*)

(*if there is ...

> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;

... then Rewrite.trace_on:*)

"-----2 ---";

Rewrite.trace_on := false;

M_Match.match_pbl fmz pbt;

Rewrite.trace_on := false;

(*... if there is no rewrite, then there is something wrong with prls*)

"-----3 ---";

(*default_print_depth 7;*)

val prls = (#prls o Problem.from_store) ["polynomial", "simplification"];

(*default_print_depth 3;*)

val t = TermC.str2term "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";

val SOME (t',_) = rewrite_set_ thy false prls t;

if t' = @{term True} then () 

else error "poly.sml: diff.behav. in check pbl 'polynomial..";

(*... if this works, but --1-- does still NOT work, check types:*)

"-----4 ---";

(*show_types:=true;*)

(*

> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;

val wh = [False "(t_::real => real) (is_polyexp::real)"]

...................... \<up> \<up> \<up>  \<up> ............... \<up> ^*)

val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;

(*show_types:=false;*)

"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";

"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";

"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";

val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];

val (dI',pI',mI') =

  ("Poly",["polynomial", "simplification"],

   ["simplification", "for_polynomials"]);

val p = e_pos'; val c = []; 

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Given "Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n  (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1))"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)

(*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =

(*+*)  "[\n(0 ,[] ,false ,#Find ,Inc ??.Simplify.normalform ,(??.empty, [])), \n(1 ,[1] ,true ,#Given ,Cor ??.Simplify.Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n  (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)) ,(t_t, [(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)]))]"

(*+*)then () else error "No.267b: I_Model.T CHANGED";

( *+ ...could not be repaired in child of 7e314dd233fd ?!?*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*)

(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*)

(*+*)if f2str f = "(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)"

(*+*)then () else error "";

(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)

(*+*)if f2str f = "17 + 15 * x \<up> 2 + -48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n-8 * x \<up> 9"

(*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b -1";

(*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)

"-------- interSteps for Schalk 299a --------------------";

"-------- interSteps for Schalk 299a --------------------";

"-------- interSteps for Schalk 299a --------------------";

reset_states ();

CalcTree

[(["Term ((x - y)*(x + (y::real)))", "normalform N"], 

  ("Poly",["polynomial", "simplification"],

  ["simplification", "for_polynomials"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;

interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);

val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;

if existpt' ([1,1], Frm) pt then ()

else error "poly.sml: interSteps doesnt work again 1";

interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);

val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;

(*============ inhibit exn WN120316 ==============================================

if existpt' ([1,1,1], Frm) pt then ()

else error "poly.sml: interSteps doesnt work again 2";

============ inhibit exn WN120316 ==============================================*)

"-------- norm_Poly NOT COMPLETE ------------------------";

"-------- norm_Poly NOT COMPLETE ------------------------";

"-------- norm_Poly NOT COMPLETE ------------------------";

val thy = @{theory AlgEin};

val SOME (f',_) = rewrite_set_ thy false norm_Poly

(TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");

if UnparseC.term f' = "L = senkrecht + oben + 2 * 2 * k + 2 * -4 * q"

then ((*norm_Poly NOT COMPLETE -- TODO MG*))

else error "norm_Poly changed behavior";

"-------- ord_make_polynomial ---------------------------";

"-------- ord_make_polynomial ---------------------------";

"-------- ord_make_polynomial ---------------------------";

val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";

val t2 = TermC.str2term "3 * a + 3 * b + 2 * b";

if ord_make_polynomial true thy [] (t1, t2) then ()

else error "poly.sml: diff.behav. in ord_make_polynomial";

(*WN071202: \<up> why then is there no rewriting ...*)

val term = TermC.str2term "2*b + (3*a + 3*b)";

val NONE = rewrite_set_ (@{theory "Isac_Knowledge"}) false order_add_mult term;

(*or why is there no rewriting this way...*)

val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";

val t2 = TermC.str2term "3 * a + (2 * b + 3 * b)";