walther@60327: (* Title: test/Tools/isac/Knowledge/rational-1.sml
walther@60327:    Author: Walther Neuper
walther@60327:    Use is subject to license terms.
walther@60327: 
walther@60327: Test of basic functions and application to complex examples.
walther@60327: *)
walther@60327: 
walther@60327: "-----------------------------------------------------------------------------------------------";
walther@60327: "-----------------------------------------------------------------------------------------------";
walther@60327: "table of contents -----------------------------------------------------------------------------";
walther@60327: "-----------------------------------------------------------------------------------------------";
walther@60327: "-------- fun poly_of_term ---------------------------------------------------------------------";
walther@60327: "-------- fun is_poly --------------------------------------------------------------------------";
walther@60355: "-------- fun is_ratpolyexp --------------------------------------------------------------------";
walther@60327: "-------- fun term_of_poly ---------------------------------------------------------------------";
walther@60347: "-------- fun cancel_p special cases -----------------------------------------------------------";
walther@60327: "-------- complex examples: rls norm_Rational --------------------------------------------------";
walther@60327: "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
walther@60327: "-----------------------------------------------------------------------------------------------";
walther@60327: "-----------------------------------------------------------------------------------------------";
walther@60327: 
walther@60327: 
walther@60327: "-------- fun poly_of_term ---------------------------------------------------------------------";
walther@60327: "-------- fun poly_of_term ---------------------------------------------------------------------";
walther@60327: "-------- fun poly_of_term ---------------------------------------------------------------------";
walther@60348: val thy = @{theory Isac_Knowledge};
Walther@60565: val vs = TermC.vars_of (TermC.parse_test @{context} "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");
walther@60327: 
Walther@60565: val t = TermC.parse_test @{context} "0 ::real";
walther@60347: if  poly_of_term vs t = SOME [(0, [0, 0, 0])] 
walther@60347: then () else error "poly_of_term 0 changed";
walther@60347: 
Walther@60565: val t = TermC.parse_test @{context} "-3 + - 2 * x ::real";
walther@60327: if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]
walther@60327: then () else error "poly_of_term uminus changed";
walther@60327: 
Walther@60565: if poly_of_term vs (TermC.parse_test @{context} "12::real") = SOME [(12, [0, 0, 0])]
walther@60327: then () else error "poly_of_term 1 changed";
walther@60327: 
Walther@60565: if poly_of_term vs (TermC.parse_test @{context} "x::real") = SOME [(1, [1, 0, 0])]
walther@60327: then () else error "poly_of_term 2 changed";
walther@60327: 
Walther@60565: if         poly_of_term vs (TermC.parse_test @{context} "12 * x \<up> 3") = SOME [(12, [3, 0, 0])]
walther@60327: then () else error "poly_of_term 3 changed";
walther@60327: "~~~~~ fun poly_of_term , args:"; val (vs, t) =
Walther@60565:   (vs, (TermC.parse_test @{context} "12 * x \<up> 3"));
walther@60327: 
walther@60327:            monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with x \<up> 3*)
walther@60336: "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2)) =
walther@60327:   (vs, (1, replicate (length vs) 0), t);
walther@60327:     val (c', es') =
walther@60327: 
walther@60327:            monom_of_term vs (c, es) m1;
wenzelm@60405: "~~~~~ 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)) ) =
walther@60327:   (vs, (c', es'), m2);
walther@60327: (*+*)c = 12;
walther@60327: (*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0];
walther@60327: 
walther@60327: if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [3, 0, 0])
wenzelm@60405: then () else error "monom_of_term (realpow): return value CHANGED";
walther@60327: 
Walther@60565: if poly_of_term vs (TermC.parse_test @{context} "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]
walther@60327: then () else error "poly_of_term 4 changed";
walther@60327: 
Walther@60565: if poly_of_term vs (TermC.parse_test @{context} "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") =
walther@60327:   SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]
walther@60327: then () else error "poly_of_term 5 changed";
walther@60327: 
walther@60327: (*poly_of_term is quite liberal:*)
walther@60327: (*the coefficient may be somewhere, the order of variables and the parentheses 
walther@60327:   within a monomial are arbitrary*)
Walther@60565: if poly_of_term vs (TermC.parse_test @{context} "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
walther@60327: then () else error "poly_of_term 6 changed";
walther@60327: 
walther@60327: (*there may even be more than 1 coefficient:*)
Walther@60565: 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])]
walther@60327: then () else error "poly_of_term 7 changed";
walther@60327: 
walther@60327: (*the order and the parentheses within monomials are arbitrary:*)
Walther@60565: if poly_of_term vs (TermC.parse_test @{context} "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)")
walther@60327:   = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
walther@60327: then () else error "poly_of_term 8 changed";
walther@60327: 
walther@60327: (*from --- rls norm_Rational downto fun gcd_poly ---*)
Walther@60565: val t = TermC.parse_test @{context} (*copy from above: "::real" is not required due to " \<up> "*)
walther@60329:   ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^
walther@60329:   "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");
walther@60327: "~~~~~ fun cancel_p_, args:"; val (t) = (t);
walther@60327: val opt = check_fraction t;
walther@60327: val SOME (numerator, denominator) = opt;
walther@60327: (*+*)UnparseC.term numerator = "- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)"; (*isa -- isa2*);
walther@60327: (*+*)UnparseC.term denominator = "- 18 + - 9 * x + 2 * y \<up> 2 + x * y \<up> 2";     (*isa -- isa2*);
walther@60327:        val vs = TermC.vars_of t;
walther@60327: (*+*)UnparseC.terms vs = "[\"x\", \"y\"]";
walther@60327:        val baseT = type_of numerator
walther@60327:        val expT = HOLogic.realT;
walther@60327: val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator);  (*isa <> isa2*)
walther@60327: 
walther@60327: "-------- fun is_poly --------------------------------------------------------------------------";
walther@60327: "-------- fun is_poly --------------------------------------------------------------------------";
walther@60327: "-------- fun is_poly --------------------------------------------------------------------------";
Walther@60565: if is_poly (TermC.parse_test @{context} "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1")
walther@60327: then () else error "is_poly 1 changed";
Walther@60565: if not (is_poly (TermC.parse_test @{context} "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))
walther@60327: then () else error "is_poly 2 changed";
walther@60327: 
walther@60355: "-------- fun is_ratpolyexp --------------------------------------------------------------------";
walther@60355: "-------- fun is_ratpolyexp --------------------------------------------------------------------";
walther@60355: "-------- fun is_ratpolyexp --------------------------------------------------------------------";
walther@60355: if is_ratpolyexp @{term "14 * x * y / (x * y)"}
walther@60355: then () else error "is_ratpolyexp (14 * x * y / (x * y)) CHANGED";
walther@60355: if is_ratpolyexp @{term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"}
walther@60355: then () else error "is_ratpolyexp (2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1) CHANGED";
walther@60355: 
walther@60355: if is_ratpolyexp @{term "((sin x) \<up> 2 - (cos x) \<up> 2)/ ((sin x)+ (cos x))"}
walther@60355: then error "is_ratpolyexp (((sin x) \<up> 2 - (cos x) \<up> 2)/ ((sin x)+ (cos x)) CHANGED" else ();
walther@60355: if is_ratpolyexp @{term "1 + sqrt x + sqrt y"}
walther@60355: then error "is_ratpolyexp (1 + sqrt x + sqrt y) CHANGED" else ();
walther@60355: 
walther@60355: 
walther@60327: "-------- fun term_of_poly ---------------------------------------------------------------------";
walther@60327: "-------- fun term_of_poly ---------------------------------------------------------------------";
walther@60327: "-------- fun term_of_poly ---------------------------------------------------------------------";
walther@60327: val expT = HOLogic.realT
Walther@60565: val Free (_, baseT) = (hd o vars o TermC.parse_test @{context}) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";
walther@60327: val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]
walther@60327: val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))
walther@60327: (*precondition for [(c, es),...]: legth es = length vs*)
walther@60327: ;
walther@60327: 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"
walther@60327: then () else error "term_of_poly 1 changed";
walther@60327: 
walther@60347: "-------- fun cancel_p special cases -----------------------------------------------------------";
walther@60347: "-------- fun cancel_p special cases -----------------------------------------------------------";
walther@60347: "-------- fun cancel_p special cases -----------------------------------------------------------";
walther@60349: val thy = @{theory Isac_Knowledge};
Walther@60500: val ctxt = Proof_Context.init_global thy
walther@60349: 
walther@60347: (*------- standard case: *)
Walther@60565: val t = TermC.parse_test @{context} "2 / 3 + 1 / 6 ::real";
walther@60347: "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);
walther@60347: val SOME ((n1, d1), (n2, d2)) =
walther@60347:      (*case*) check_frac_sum t (*of*);
walther@60347:       val vs = TermC.vars_of t;
walther@60347: (*+*)val [] = vs;
walther@60347: val (SOME n1', SOME a, SOME n2', SOME b) =
walther@60347:    (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
walther@60347:             val ((a', b'), c) = gcd_poly a b
walther@60347:             val (baseT, expT) = (type_of n1, HOLogic.realT);
walther@60347: (*+*)val [(1, [])] = a'; (* 6 * _1_ = 6 *)
walther@60347: (*+*)val [(2, [])] = b'; (* 3 * _2_ = 6 *)
walther@60347: (*+*)val [(3, [])] = c;  (* 3 / 6 \<and> 3 / 3 ..gcd *)
walther@60347: 
walther@60347:             val nomin = term_of_poly baseT expT vs
walther@60347:               (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
walther@60347: 
walther@60347: (*+*)val "5" = UnparseC.term nomin; (* = "3" ERROR*)
walther@60347: 
walther@60347: (*+*)val [(2, [])] =   the (poly_of_term vs n1);            (*---v----------------------v----*)
walther@60347: (*+*)val [(4, [])] = ((the (poly_of_term vs n1)) %%*%% b'); (* = 2 * _2_  new nomin for 2 / 3*)
walther@60347: 
walther@60347: (*+*)val [(1, [])] =   the (poly_of_term vs n2);            (*---v----------------------v----*)
walther@60347: (*+*)val [(1, [])] = ((the (poly_of_term vs n2)) %%*%% a'); (* = 1 * _1_  new nomin for 1 / 6*)
walther@60347: 
walther@60347: (*+*)val [(5, [])] =                                        (* = 4 + 1    new nomin for sum  *)
walther@60347:             (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
walther@60347: 
walther@60347:             val denom =                                     (* = 3 * 1 * 2 new denom for sum *)
walther@60347:                         term_of_poly baseT expT vs ((c %%*%% a') %%*%% b');
walther@60347: (*+*)val "6" = UnparseC.term denom;
walther@60347: 
walther@60347:             val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom);
walther@60347: (*+*)val "5 / 6" = UnparseC.term t'
walther@60347: 
walther@60347: 
walther@60347: (*------- 0 / m + 0 / n
walther@60347:              20 years old bug found here: *)
Walther@60565: 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)";
Walther@60500: val SOME (t', _) = rewrite_set_ ctxt true norm_Rational t;
walther@60347: (*
walther@60347: :
walther@60347: ##  rls: cancel_p_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24) 
walther@60347: ###  rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24) 
walther@60347: ------------------------------------------------------------these are missing now -----\
walther@60347: /##  rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 1)  from isa2: strange behaviour
walther@60347: /##  rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 1 + 0 / 1)   from isa2: strange behaviour
walther@60347: ------------------------------------------------------------these are missing now -----/
walther@60347: ##  rls: norm_Rational_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24) 
walther@60347: ###  rls: add_fractions_p_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24) 
walther@60347: ####  rls: add_fractions_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
walther@60347: --------------------------------------------------^v^v^v^v^v^v^v^v^--undetected bug
walther@60347: ####  rls: add_fractions_p on: 0 = c_2 + 1 / EI * (3 / 24)  =3: ERROR
walther@60347: ###  rls: rat_mult_div_pow on: 0 = c_2 + 1 / EI * (3 / 24) 
walther@60347: :
walther@60347: *)
walther@60347: if UnparseC.term t' = "0 = c_2" then () else error "norm_Rational CHANGED"; (*isa2*)
walther@60347: 
Walther@60565: val t = TermC.parse_test @{context} "0 / 12 + 0 / 24 ::real";
walther@60347:        add_fraction_p_ @{theory} t;
walther@60347: "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);
walther@60347: val SOME ((n1, d1), (n2, d2)) =
walther@60347:      (*case*) check_frac_sum t (*of*);
walther@60347: 
walther@60347: (*+*)val Const ("Groups.zero_class.zero", _) = n1;
walther@60347: (*+*)val Const ("Groups.zero_class.zero", _) = n2;
walther@60347: 
walther@60347:       val vs = TermC.vars_of t;
walther@60347: (*+*)val [] = vs;
walther@60347: 
walther@60347: val (SOME n1', SOME a, SOME n2', SOME b) =
walther@60347:    (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
walther@60347: 
walther@60347: (*+*)if n1' = [(0, [])] then () else error "correction w.r.t zero polynomial CHANGED";
walther@60347: 
walther@60347:             val ((a', b'), c) = gcd_poly a b
walther@60347:             val (baseT, expT) = (type_of n1, HOLogic.realT);
walther@60347: (*+*)val [(1, [])] = a'; (* 1 * _1_ = 24 *)          
walther@60347: (*+*)val [(2, [])] = b'; (* 2 * _2_ = 12 *)          
walther@60347: (*+*)val [(12, [])] = c; (* 12 / 24 \<and> 12 / 12 ..gcd *)  
walther@60347: 
walther@60347:             val nomin = term_of_poly baseT expT vs
walther@60347:               (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
walther@60347: 
walther@60347: (*+*)UnparseC.term nomin; (* = "3" ERROR*)
walther@60347: (* correct ERROR ------------------------------------------------------------------\\*)
walther@60347: (*+*)val SOME [(0, [])] = poly_of_term vs n1 (* ERROR WAS [(1, [])] *)
walther@60347: (* correct ERROR ------------------------------------------------------------------//*)
walther@60347: 
walther@60347: (*+*)val [(0, [])] =   the (poly_of_term vs n1);            (*---v----------------------v-----*)
walther@60347: (*+*)val [(0, [])] = ((the (poly_of_term vs n1)) %%*%% b'); (* = 0 * _0_  new nomin for 0 / 12*)
walther@60347: 
walther@60347: (*+*)val [(0, [])] =   the (poly_of_term vs n2);            (*---v----------------------v-----*)
walther@60347: (*+*)val [(0, [])] = ((the (poly_of_term vs n2)) %%*%% a'); (* = 0 * _0_  new nomin for 0 / 24*)
walther@60347: 
walther@60347: (*+*)val [(0, [])] =                                        (* = 0 + 0    new nomin for sum   *)
walther@60347:         (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
walther@60347: 
walther@60347:             val denom =                                     (* = 12 * 1 * 2 new denom for sum *)
walther@60347:                         term_of_poly baseT expT vs ((c %%*%% a') %%*%% b');
walther@60347: (*+*)val "24" =  UnparseC.term denom;
walther@60347: 
walther@60347:             val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom);
walther@60347: (*+*)val "0 / 24" =  UnparseC.term t'
walther@60347: 
walther@60347: (*---------- fun cancel_p with Const AA *)
walther@60347: val thy = @{theory Partial_Fractions};
walther@60347: val ctxt = Proof_Context.init_global @{theory}
walther@60347: val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)
walther@60347: 
Walther@60500: val SOME (t', _) = rewrite_set_ ctxt true cancel_p t;
walther@60347: case t' of
walther@60347:   Const (\<^const_name>\<open>divide\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $
walther@60347:     Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
walther@60347: | _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";
walther@60347: 
walther@60347: "~~~~~ fun cancel_p , args:"; val (t) = (t);
walther@60347: val opt = check_fraction t
walther@60347: val SOME (numerator, denominator) = (*case*) opt (*of*);
walther@60347: 
walther@60347: if UnparseC.term numerator = "2 * AA" andalso UnparseC.term denominator = "2"
walther@60347: then () else error "check_fraction (2 * AA / 2) changed";
walther@60347:         val vs = TermC.vars_of t;
walther@60347: case vs of
walther@60347:   [Const (\<^const_name>\<open>AA\<close>, _)] => ()
walther@60347: | _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1  changed";
walther@60347: 
walther@60347: 
walther@60327: "-------- complex examples: rls norm_Rational --------------------------------------------------";
walther@60327: "-------- complex examples: rls norm_Rational --------------------------------------------------";
walther@60327: "-------- complex examples: rls norm_Rational --------------------------------------------------";
Walther@60565: val t = TermC.parse_test @{context} "(3*x+5)/18 - x/2  - -(3*x - 2)/9 = 0";
Walther@60500: val SOME (t', _) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';
walther@60327: if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";
walther@60327: 
Walther@60565: val t = TermC.parse_test @{context} "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
Walther@60500: val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';
walther@60327: if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then () 
walther@60327: else error "rational.sml 2";
walther@60327: 
Walther@60565: 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";
Walther@60500: val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';
walther@60327: if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then ()
walther@60327: else error "rational.sml 3";
walther@60327: 
walther@60327: "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
walther@60327: "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
walther@60327: "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
walther@60327: (*Schalk I, p.60 Nr. 215c *)
Walther@60565: val t = TermC.parse_test @{context} "(a + b) \<up> 4 * (x - y)  /  ((x - y) \<up> 3 * (a + b) \<up> 2)";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;
walther@60327: if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
walther@60327: then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";
walther@60327: 
walther@60327: (*SRC Schalk I, p.66 Nr. 381b *)
Walther@60565: val t = TermC.parse_test @{context} 
walther@60327: "(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;
walther@60327: if UnparseC.term t = "1 / (- 5 + 2 * x)"
walther@60327: then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
walther@60327: 
walther@60327: (*Schalk I, p.60 Nr. 215c *)
Walther@60565: val t = TermC.parse_test @{context} "(a + b) \<up> 4 * (x - y)  /  ((x - y) \<up> 3 * (a + b) \<up> 2)";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;
walther@60327: if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
walther@60327: then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";
walther@60327: