1.1 --- a/src/Tools/isac/ProgLang/Calculate.thy Mon Sep 13 16:01:48 2021 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy Tue Sep 14 12:22:57 2021 +0200
1.3 @@ -24,36 +24,54 @@
1.4 \<close> ML \<open>
1.5 (*** evaluate binary associative operations ***)
1.6
1.7 -fun eval_binop _ _
1.8 - (t as ((opp as Const (op0, _)) $ (Const (op0', _) $ v $ t1) $ t2)) _ =(* binary . (v.n1).n2 *)
1.9 - if op0 = op0' andalso TermC.is_num t1 andalso TermC.is_num t2 then
1.10 - let
1.11 - val op' = if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0
1.12 - val res = Eval.calcul op' (t1, t2);
1.13 - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ v $ res));
1.14 - in SOME ("#: " ^ UnparseC.term prop, prop) end
1.15 - else NONE
1.16 - | eval_binop _ (_ : string)
1.17 - (t as ((opp as Const (op0, _)) $ t1 $ (Const (op0', _) $ t2 $ v))) _ =(* binary . n1.(n2.v) *)
1.18 - if op0 = op0' andalso op0 <> "Groups.minus_class.minus"
1.19 - andalso TermC.is_num t1 andalso TermC.is_num t2 then
1.20 - let
1.21 - val res = Eval.calcul op0 (t1, t2);
1.22 - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ res $ v));
1.23 - in
1.24 - SOME ("#: " ^ UnparseC.term prop, prop)
1.25 - end
1.26 - else NONE
1.27 - | eval_binop _ _ (t as (Const (op0, _) $ t1 $ t2)) _ = (* binary . n1.n2 *)
1.28 - if TermC.is_num t1 andalso TermC.is_num t2 then
1.29 - let
1.30 - val res = Eval.calcul op0 (t1, t2);
1.31 - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
1.32 - in
1.33 - SOME ("#: " ^ UnparseC.term prop, prop)
1.34 - end
1.35 - else NONE
1.36 - | eval_binop _ _ _ _ = NONE;
1.37 +val is_num = can HOLogic.dest_number;
1.38 +
1.39 +val is_calcul_op =
1.40 + member (op =) [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>, \<^const_name>\<open>times\<close>, \<^const_name>\<open>powr\<close>];
1.41 +
1.42 +fun calcul thy lhs =
1.43 + let
1.44 + val _ = tracing ("-----calcul: lhs = " ^ UnparseC.term lhs)
1.45 + val simp_ctxt =
1.46 + Proof_Context.init_global thy
1.47 + |> put_simpset (Simplifier.simpset_of @{theory_context Complex_Main});
1.48 + val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
1.49 + val rhs = Thm.term_of (Thm.rhs_of eq);
1.50 + val _ = tracing ("=====calcul: rhs = " ^ UnparseC.term rhs)(* \<^assert> (is_num rhs);*)
1.51 + in rhs end;
1.52 +
1.53 +fun eval_binop (_: string) (_: string) t thy =
1.54 + (case t of
1.55 + (opp as Const (c1, T)) $ (Const (c2, _) $ v $ t1) $ t2 => (* binary \<circ> (v \<circ> n1) \<circ> n2 *)
1.56 + if c1 = c2 andalso is_calcul_op c1 andalso is_num t1 andalso is_num t2 then
1.57 + let
1.58 + val opp' = Const (if c1 = \<^const_name>\<open>minus\<close> then \<^const_name>\<open>plus\<close> else c1, T);
1.59 + val res = calcul thy (opp' $ t1 $ t2);
1.60 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ v $ res));
1.61 + in SOME ("#: " ^ UnparseC.term prop, prop) end
1.62 + else NONE
1.63 + | (opp as Const (c1, _)) $ t1 $ (Const (c2, _) $ t2 $ v) => (* binary \<circ> n1 \<circ> (n2 \<circ> v) *)
1.64 + if c1 = c2 andalso is_calcul_op c1 andalso c1 <> \<^const_name>\<open>minus\<close>
1.65 + andalso is_num t1 andalso is_num t2
1.66 + then
1.67 + let
1.68 + val res = calcul thy (opp $ t1 $ t2);
1.69 + val prop = HOLogic.Trueprop $ HOLogic.mk_eq (t, opp $ res $ v);
1.70 + in
1.71 + SOME ("#: " ^ UnparseC.term prop, prop)
1.72 + end
1.73 + else NONE
1.74 + | Const (c, _) $ t1 $ t2 => (* binary \<circ> n1 \<circ> n2 *)
1.75 + if is_calcul_op c andalso is_num t1 andalso is_num t2 then
1.76 + let
1.77 + val res = calcul thy t;
1.78 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
1.79 + in
1.80 + SOME ("#: " ^ UnparseC.term prop, prop)
1.81 + end
1.82 + else NONE
1.83 + | _ => NONE);
1.84 +
1.85 \<close> ML \<open>
1.86 \<close> ML \<open>
1.87 \<close>
2.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Mon Sep 13 16:01:48 2021 +0200
2.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Tue Sep 14 12:22:57 2021 +0200
2.3 @@ -18,7 +18,6 @@
2.4 val adhoc_thm1_: theory -> Eval_Def.cal -> term -> (string * thm) option
2.5 val norm: term -> term
2.6 val popt2str: ('a * term) option -> string
2.7 - val calcul: string -> term * term -> term
2.8 val trace_on: bool Unsynchronized.ref
2.9 val int_of_numeral: term -> int
2.10 \<^isac_test>\<open>
2.11 @@ -110,7 +109,7 @@
2.12 fun trace_calc4 str t1 t2 =
2.13 if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
2.14
2.15 -fun get_pair (*1*)thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
2.16 +fun get_pair (*1*)thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
2.17 if op_ = op0 then
2.18 let val popt = ef op_ t thy
2.19 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end
2.20 @@ -127,7 +126,7 @@
2.21 let
2.22 val popt = get_pair thy op_ ef t1
2.23 val _ = trace_calc2 "3.. get_pair: " t1 popt
2.24 - in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end
2.25 + in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end (* search subterms *)
2.26 end
2.27 else (* search subterms *)
2.28 let
2.29 @@ -194,8 +193,6 @@
2.30 else (*3*) mk_rule (prems, concl, @{term True})
2.31 end;
2.32
2.33 -(*** handle numerals in eval_binop ***)
2.34 -
2.35 (* preliminary HACK *)
2.36 fun int_of_numeral (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = 0
2.37 | int_of_numeral (Const (\<^const_name>\<open>one_class.one\<close>, _)) = 1
2.38 @@ -203,19 +200,6 @@
2.39 | int_of_numeral (Const (\<^const_name>\<open>numeral\<close>, _) $ n) = HOLogic.dest_numeral n
2.40 | int_of_numeral t = raise TERM ("int_of_numeral", [t]);
2.41
2.42 -fun calcul op_ (t1, t2) =
2.43 - let
2.44 - val (T, _) = HOLogic.dest_number t1
2.45 - val (i1, i2) = (int_of_numeral t1, int_of_numeral t2)
2.46 - val result =
2.47 - case op_ of
2.48 - "Groups.plus_class.plus" => i1 + i2 (* preliminary HACK *)
2.49 - | "Groups.minus_class.minus" => i1 - i2 (* preliminary HACK *)
2.50 - | "Groups.times_class.times" => i1 * i2 (* preliminary HACK *)
2.51 - | "Transcendental.powr" => power i1 i2 (* preliminary HACK *)
2.52 - | str => raise ERROR ("calcul not impl.for op_ " ^ str)
2.53 - in HOLogic.mk_number T result end;
2.54 -
2.55 end
2.56
2.57
3.1 --- a/test/Tools/isac/ProgLang/calculate.sml Mon Sep 13 16:01:48 2021 +0200
3.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Sep 14 12:22:57 2021 +0200
3.3 @@ -14,25 +14,18 @@
3.4 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
3.5 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
3.6 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
3.7 -val (t1, t2) = (@{term 3}, @{term "2::real"});
3.8 -val t = HOLogic.mk_binop "Groups.plus_class.plus" (t1, t2);
3.9
3.10 - eval_binop "" "" t "";
3.11 -"~~~~~ fun eval_binop , args:"; val (_, _, (t as (Const (op0, t0) $ t1 $ t2)), _) =(* binary . n1.n2 *)
3.12 - ((), (), t, ());
3.13 - (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*);
3.14 - val res = calcul op0 (t1, t2);
3.15 - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
3.16 - (*in*)
3.17 - val xxx = SOME ("#: " ^ UnparseC.term prop, prop);
3.18 - (*end*)
3.19 +fun test thy t = writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul thy t)));
3.20
3.21 -case xxx of
3.22 - SOME
3.23 - ("#: (3::'a) + 2 = (5::'a)",
3.24 - Const (\<^const_name>\<open>Trueprop\<close>, _) $
3.25 - (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
3.26 - (Const (\<^const_name>\<open>plus_class.plus\<close>, _) $ _ $
3.27 - (Const (\<^const_name>\<open>numeral\<close>, _) $ _ )) $
3.28 - _ )) => ()
3.29 -| _ => error "eval_binop #: (3::'a) + 2 = (5::'a) CHANGED"
3.30 +test \<^theory> \<^term>\<open>10 + 20 :: real\<close>;
3.31 +test \<^theory> \<^term>\<open>10 - 20 :: real\<close>;
3.32 +test \<^theory> \<^term>\<open>10 * 20 :: real\<close>;
3.33 +test \<^theory> \<^term>\<open>10 powr 20 :: real\<close>;
3.34 +
3.35 +test \<^theory> \<^term>\<open>10 + 20 :: int\<close>;
3.36 +test \<^theory> \<^term>\<open>10 - 20 :: int\<close>;
3.37 +test \<^theory> \<^term>\<open>10 * 20 :: int\<close>;
3.38 +
3.39 +test \<^theory> \<^term>\<open>10 + 20 :: nat\<close>;
3.40 +test \<^theory> \<^term>\<open>10 - 20 :: nat\<close>;
3.41 +test \<^theory> \<^term>\<open>10 * 20 :: nat\<close>;
4.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Sep 13 16:01:48 2021 +0200
4.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Tue Sep 14 12:22:57 2021 +0200
4.3 @@ -300,41 +300,21 @@
4.4 "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
4.5 "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
4.6 "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
4.7 -val (t1, t2) = (@{term 3}, @{term "2::real"});
4.8 +val t = @{term "2 + 3 ::real"};
4.9
4.10 -"~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2));
4.11 - val (Const (\<^const_name>\<open>numeral\<close>, _) $ n1) = t1;
4.12 - val (Const (\<^const_name>\<open>numeral\<close>, _) $ n2) = t2;
4.13 - val (T, _) = HOLogic.dest_number t1
4.14 - val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2)
4.15 - val result =
4.16 - case op_ of
4.17 - "Groups.plus_class.plus" => i1 + i2
4.18 - | "Groups.minus_class.minus" => i1 - i2
4.19 - | "Groups.times_class.times" => i1 * i2
4.20 - | "Transcendental.powr" => power i1 i2
4.21 - | str => raise ERROR ("calcul not impl.for op_ " ^ str)
4.22 - (*in*)
4.23 - val xxx = HOLogic.mk_number T result;
4.24 - (*end*)
4.25 -case HOLogic.dest_number xxx of
4.26 - (_, 5) => ()
4.27 -| _ => error "calcul + 2 3 CHANGED";
4.28 +"~~~~~ fun calcul , args:"; val (thy, lhs) = (@{theory}, t);
4.29 + val simp_ctxt =
4.30 + Proof_Context.init_global thy
4.31 + |> put_simpset (Simplifier.simpset_of @{theory_context Complex_Main});
4.32 + val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
4.33
4.34 -case HOLogic.dest_number (calcul "Groups.minus_class.minus" (t1, t2)) of
4.35 - (_, 1) => xxx
4.36 -| _ => error "calcul - 2 3 CHANGED";
4.37 +if ThmC.string_of_thm eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";
4.38
4.39 -case HOLogic.dest_number (calcul "Groups.times_class.times" (t1, t2)) of
4.40 - (_, 6) => xxx
4.41 -| _ => error "calcul - 2 3 CHANGED";
4.42 + val rhs = Thm.term_of (Thm.rhs_of eq);
4.43 + val _ = \<^assert> (is_num rhs);
4.44
4.45 -(* (calcul "Rings.divide_class.divide" (t1, t2)
4.46 -ERROR: calcul not impl.for op_ Rings.divide_class.divide*)
4.47 -
4.48 -case HOLogic.dest_number (calcul "Transcendental.powr" (t1, t2)) of
4.49 - (_, 9) => xxx
4.50 -| _ => error "calcul - 2 3 CHANGED";
4.51 +(*return value*) rhs;
4.52 +if TermC.to_string rhs = "5" then () else error "calcul 2";
4.53
4.54
4.55 "----------- get_pair with 3 args --------------------------------";
5.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Mon Sep 13 16:01:48 2021 +0200
5.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Tue Sep 14 12:22:57 2021 +0200
5.3 @@ -424,21 +424,22 @@
5.4 val t = (Thm.term_of o the o (TermC.parse thy)) "2 * 3";
5.5 (*val SOME (thmid,t') = *)get_pair thy op_ ef t;
5.6 ;
5.7 -"~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
5.8 +"~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
5.9 (thy, op_, ef, t);
5.10 -op_ = op0 = true;val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
5.11 -val t = (Thm.term_of o the o (TermC.parse thy)) "2 * 3";
5.12 -
5.13 + (*if*) op_ = op0; (*then*)
5.14 + val popt =
5.15 ef op_ t thy;
5.16 -"~~~~~ fun eval_binop , args:"; val ((thmid : string), (op_: string),
5.17 - (t as (Const (op0, _) $ t1 $ t2)), _) =
5.18 - ("#mult_", op_, t, thy); (* binary . n1.n2 *)
5.19 - (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*);
5.20 - val res = Eval.calcul op0 (t1, t2);
5.21 - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
5.22 -val SOME (thmid, tm) = SOME ("#: " ^ UnparseC.term prop, prop)
5.23 +"~~~~~ fun eval_binop , args:"; val ((_ : string), (_: string),
5.24 + (t as (Const (op0, _) $ t1 $ t2)), thy) =
5.25 + ("#mult_", op_, t, thy);
5.26 +val Const (c, _) $ t1 $ t2 = (* binary \<circ> n1 \<circ> n2 *)
5.27 + (*case*) t (*of*);
5.28 + (*if*) is_calcul_op c andalso is_num t1 andalso is_num t2 (*then*);
5.29 + val res = calcul thy t;
5.30 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
5.31 + SOME ("#: " ^ UnparseC.term prop, prop) (*return value*);
5.32 ;
5.33 -if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
5.34 +if "#: " ^ UnparseC.term prop = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
5.35 else error "eval_binop changed"
5.36 ;
5.37 val SOME (thmid, tm) = eval_binop "#mult_" op_ t thy;
6.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Sep 13 16:01:48 2021 +0200
6.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Sep 14 12:22:57 2021 +0200
6.3 @@ -293,6 +293,18 @@
6.4 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
6.5 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
6.6 ML_file "Knowledge/polyeq-1.sml"
6.7 +ML \<open>
6.8 +\<close> ML \<open>
6.9 +\<close> ML \<open>
6.10 +\<close> ML \<open>
6.11 +\<close> ML \<open>
6.12 +\<close> ML \<open>
6.13 +\<close> ML \<open>
6.14 +\<close> ML \<open>
6.15 +\<close> ML \<open>
6.16 +\<close> ML \<open>
6.17 +\<close> ML \<open>
6.18 +\<close>
6.19 (*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*)
6.20 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
6.21 ML_file "Knowledge/calculus.sml"
7.1 --- a/test/Tools/isac/Test_Some.thy Mon Sep 13 16:01:48 2021 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Tue Sep 14 12:22:57 2021 +0200
7.3 @@ -107,6 +107,1145 @@
7.4 section \<open>===================================================================================\<close>
7.5 ML \<open>
7.6 \<close> ML \<open>
7.7 +(* Title: Knowledge/polyeq-1.sml
7.8 + testexamples for PolyEq, poynomial equations and equational systems
7.9 + Author: Richard Lang 2003
7.10 + (c) due to copyright terms
7.11 +
7.12 +Separation into polyeq-1.sml and polyeq-1a.sml due to
7.13 +*)
7.14 +
7.15 +"-----------------------------------------------------------------";
7.16 +"table of contents -----------------------------------------------";
7.17 +"-----------------------------------------------------------------";
7.18 +"------ polyeq-1.sml ---------------------------------------------";
7.19 +"----------- tests on predicates in problems ---------------------";
7.20 +"----------- test matching problems ------------------------------";
7.21 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
7.22 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
7.23 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
7.24 +"----------- lin.eq degree_0 -------------------------------------";
7.25 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
7.26 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
7.27 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
7.28 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
7.29 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
7.30 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
7.31 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
7.32 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
7.33 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
7.34 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
7.35 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
7.36 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
7.37 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
7.38 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
7.39 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
7.40 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.41 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
7.42 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
7.43 +"-----------------------------------------------------------------";
7.44 +"------ polyeq-2.sml ---------------------------------------------";
7.45 +"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
7.46 +"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
7.47 +"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
7.48 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
7.49 +"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
7.50 +"----------- rls make_polynomial_in ------------------------------";
7.51 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
7.52 +"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
7.53 +"-----------------------------------------------------------------";
7.54 +"-----------------------------------------------------------------";
7.55 +
7.56 +"----------- tests on predicates in problems ---------------------";
7.57 +"----------- tests on predicates in problems ---------------------";
7.58 +"----------- tests on predicates in problems ---------------------";
7.59 +val thy = @{theory};
7.60 +Rewrite.trace_on:=false; (*true false*)
7.61 +
7.62 + val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
7.63 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
7.64 + if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
7.65 + else error "polyeq.sml: diff.behav. in lhs";
7.66 +
7.67 +\<close> ML \<open>
7.68 + val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
7.69 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
7.70 + if (UnparseC.term t) = "True" then ()
7.71 + else error "polyeq.sml: diff.behav. 1 in is_expended_in";
7.72 +
7.73 + val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
7.74 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
7.75 + if (UnparseC.term t) = "False" then ()
7.76 + else error "polyeq.sml: diff.behav. 2 in is_poly_in";
7.77 +
7.78 + val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
7.79 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
7.80 + if (UnparseC.term t) = "True" then ()
7.81 + else error "polyeq.sml: diff.behav. 3 in is_poly_in";
7.82 +
7.83 + val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
7.84 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
7.85 + if (UnparseC.term t) = "True" then ()
7.86 + else error "polyeq.sml: diff.behav. 4 in is_expended_in";
7.87 +
7.88 + val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
7.89 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
7.90 + if (UnparseC.term t) = "True" then ()
7.91 + else error "polyeq.sml: diff.behav. 5 in is_expended_in";
7.92 +
7.93 + val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
7.94 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
7.95 + if (UnparseC.term t) = "True" then ()
7.96 + else error "polyeq.sml: diff.behav. in has_degree_in_in";
7.97 +
7.98 + val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
7.99 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
7.100 + if (UnparseC.term t) = "False" then ()
7.101 + else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
7.102 +
7.103 + val t4 = (Thm.term_of o the o (TermC.parse thy))
7.104 + "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
7.105 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
7.106 + if (UnparseC.term t) = "False" then ()
7.107 + else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
7.108 +
7.109 +val t5 = (Thm.term_of o the o (TermC.parse thy))
7.110 + "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
7.111 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
7.112 + if (UnparseC.term t) = "True" then ()
7.113 + else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
7.114 +
7.115 +\<close> ML \<open>
7.116 +"----------- test matching problems --------------------------0---";
7.117 +"----------- test matching problems --------------------------0---";
7.118 +"----------- test matching problems --------------------------0---";
7.119 +val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.120 +if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
7.121 + M_Match.Matches' {Find = [Correct "solutions L"],
7.122 + With = [],
7.123 + Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
7.124 + Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
7.125 + Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
7.126 + Relate = []}
7.127 +then () else error "M_Match.match_pbl [expanded,univariate,equation]";
7.128 +
7.129 +if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
7.130 + M_Match.Matches' {Find = [Correct "solutions L"],
7.131 + With = [],
7.132 + Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
7.133 + Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
7.134 + Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
7.135 +then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
7.136 +
7.137 +
7.138 +\<close> ML \<open>
7.139 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
7.140 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
7.141 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
7.142 +(*##################################################################################
7.143 +----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
7.144 +
7.145 + (*Aufgabe zum Einstieg in die Arbeit...*)
7.146 + val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
7.147 + (*ein 'ruleset' aus Poly.ML wird angewandt...*)
7.148 + val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
7.149 + UnparseC.term t;
7.150 + "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
7.151 + val SOME (t,_) =
7.152 + rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
7.153 + UnparseC.term t;
7.154 + "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
7.155 +(* bei Verwendung von "size_of-term" nach MG :*)
7.156 +(*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
7.157 +
7.158 + (*wir holen 'a' wieder aus der Klammerung heraus...*)
7.159 + val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
7.160 + UnparseC.term t;
7.161 + "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
7.162 +(* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
7.163 +
7.164 + val SOME (t,_) =
7.165 + rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
7.166 + UnparseC.term t;
7.167 + "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
7.168 + (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
7.169 + "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
7.170 +
7.171 + (*das rewriting l"asst sich beobachten mit
7.172 +Rewrite.trace_on := false; (*true false*)
7.173 + *)
7.174 +
7.175 +"------ 15.11.02 --------------------------";
7.176 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
7.177 + val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
7.178 + val a = (Thm.term_of o the o (TermC.parse thy)) "a";
7.179 +
7.180 +Rewrite.trace_on := false; (*true false*)
7.181 + (* Anwenden einer Regelmenge aus Termorder.ML: *)
7.182 + val SOME (t,_) =
7.183 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
7.184 + UnparseC.term t;
7.185 + val SOME (t,_) =
7.186 + rewrite_set_ thy false discard_parentheses t;
7.187 + UnparseC.term t;
7.188 +"1 + b * x + x * a";
7.189 +
7.190 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
7.191 + val SOME (t,_) =
7.192 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
7.193 + UnparseC.term t;
7.194 + val SOME (t,_) =
7.195 + rewrite_set_ thy false discard_parentheses t;
7.196 + UnparseC.term t;
7.197 +"1 + (x + b * x) * a + a \<up> 2";
7.198 +
7.199 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
7.200 + val SOME (t,_) =
7.201 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
7.202 + UnparseC.term t;
7.203 + val SOME (t,_) =
7.204 + rewrite_set_ thy false discard_parentheses t;
7.205 + UnparseC.term t;
7.206 +"1 + b * a + (7 + x) * a \<up> 2";
7.207 +
7.208 +(* MG2003
7.209 + Prog_Expr.thy grundlegende Algebra
7.210 + Poly.thy Polynome
7.211 + Rational.thy Br"uche
7.212 + Root.thy Wurzeln
7.213 + RootRat.thy Wurzen + Br"uche
7.214 + Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
7.215 +
7.216 + get_thm Termorder.thy "bdv_n_collect";
7.217 + get_thm (theory "Isac_Knowledge") "bdv_n_collect";
7.218 +*)
7.219 + val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
7.220 + val SOME (t,_) =
7.221 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
7.222 + UnparseC.term t;
7.223 + val SOME (t,_) =
7.224 + rewrite_set_ thy false discard_parentheses t;
7.225 + UnparseC.term t;
7.226 +"(7 + x) * a \<up> 2";
7.227 +
7.228 + val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
7.229 +
7.230 + val t = (Thm.term_of o the o (parseold thy)) "7";
7.231 +##################################################################################*)
7.232 +
7.233 +
7.234 +\<close> ML \<open>
7.235 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
7.236 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
7.237 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
7.238 +(* termorder hacked by MG, adapted later by WN *)
7.239 +(** )local ( *. for make_polynomial_in .*)
7.240 +
7.241 +open Term; (* for type order = EQUAL | LESS | GREATER *)
7.242 +
7.243 +fun pr_ord EQUAL = "EQUAL"
7.244 + | pr_ord LESS = "LESS"
7.245 + | pr_ord GREATER = "GREATER";
7.246 +
7.247 +fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
7.248 + | dest_hd' x (t as Free (a, T)) =
7.249 + if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
7.250 + else (((a, 0), T), 1)
7.251 + | dest_hd' _ (Var v) = (v, 2)
7.252 + | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
7.253 + | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
7.254 + | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
7.255 +
7.256 +fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
7.257 + Free (var, _) $ Free (pot, _)) =
7.258 + (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
7.259 + case x of (*WN*)
7.260 + (Free (xstr, _)) =>
7.261 + if xstr = var
7.262 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
7.263 + 1000 * (the (TermC.int_opt_of_string pot)))
7.264 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
7.265 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
7.266 + | size_of_term' i pr x (t as Abs (_, _, body)) =
7.267 + (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
7.268 + 1 + size_of_term' (i + 1) pr x body)
7.269 + | size_of_term' i pr x (f $ t) =
7.270 + let
7.271 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
7.272 + val s1 = size_of_term' (i + 1) pr x f
7.273 + val s2 = size_of_term' (i + 1) pr x t
7.274 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
7.275 + in (s1 + s2) end
7.276 + | size_of_term' i pr x t =
7.277 + (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
7.278 + case t of
7.279 + Free (subst, _) =>
7.280 + (case x of
7.281 + Free (xstr, _) =>
7.282 + if xstr = subst
7.283 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
7.284 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
7.285 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
7.286 + | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
7.287 +
7.288 +fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
7.289 + let
7.290 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
7.291 + val ord =
7.292 + case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
7.293 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
7.294 + in ord end
7.295 + | term_ord' i pr x _ (t, u) =
7.296 + let
7.297 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
7.298 + val ord =
7.299 + case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
7.300 + EQUAL =>
7.301 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u
7.302 + in
7.303 + (case hd_ord (i + 1) pr x (f, g) of
7.304 + EQUAL => (terms_ord x (i + 1) pr) (ts, us)
7.305 + | ord => ord)
7.306 + end
7.307 + | ord => ord
7.308 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
7.309 + in ord end
7.310 +and hd_ord i pr x (f, g) = (* ~ term.ML *)
7.311 + let
7.312 + val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
7.313 + val ord = prod_ord
7.314 + (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
7.315 + (dest_hd' x f, dest_hd' x g)
7.316 + val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
7.317 + in ord end
7.318 +and terms_ord x i pr (ts, us) =
7.319 + let
7.320 + val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
7.321 + val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
7.322 + val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
7.323 + in ord end
7.324 +
7.325 +(** )in( *local*)
7.326 +
7.327 +fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
7.328 + ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
7.329 + case subst of
7.330 + (_, x) :: _ =>
7.331 + term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
7.332 + | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
7.333 +
7.334 +(** )end;( *local*)
7.335 +
7.336 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
7.337 +if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then () else error "still GREATER?";
7.338 +
7.339 +val x = TermC.str2term "x ::real";
7.340 +
7.341 +val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
7.342 +if 2006 = size_of_term' 1 false(*true*) x t1
7.343 +then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
7.344 +
7.345 +val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
7.346 +if 3004 = size_of_term' 1 false(*true*) x t2
7.347 +then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
7.348 +
7.349 +
7.350 +\<close> ML \<open>
7.351 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
7.352 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
7.353 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
7.354 + val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
7.355 + val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
7.356 + val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
7.357 +
7.358 + val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
7.359 + val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
7.360 + val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
7.361 + val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
7.362 +
7.363 +if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then ()
7.364 +else error "termorder.sml diff.behav ord_make_polynomial_in #1";
7.365 +
7.366 +if ord_make_polynomial_in false(*true*) thy substa (x1,x2) = true(*LESS *) then ()
7.367 +else error "termorder.sml diff.behav ord_make_polynomial_in #2";
7.368 +
7.369 +if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then ()
7.370 +else error "termorder.sml diff.behav ord_make_polynomial_in #3";
7.371 +
7.372 + val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
7.373 + val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
7.374 + ord_make_polynomial_in false(*true*) thy substx (aa, bb);
7.375 + true; (* => LESS *)
7.376 +
7.377 + val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
7.378 + val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
7.379 + ord_make_polynomial_in false(*true*) thy substa (aa, bb);
7.380 + false; (* => GREATER *)
7.381 +
7.382 +(* und nach dem Re-engineering der Termorders in den 'rulesets'
7.383 + kannst Du die 'gr"osste' Variable frei w"ahlen: *)
7.384 + val bdv= TermC.str2term "bdv ::real";
7.385 + val x = TermC.str2term "x ::real";
7.386 + val a = TermC.str2term "a ::real";
7.387 + val b = TermC.str2term "b ::real";
7.388 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
7.389 +if UnparseC.term t' = "b + x + a" then ()
7.390 +else error "termorder.sml diff.behav ord_make_polynomial_in #11";
7.391 +
7.392 +val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
7.393 +
7.394 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
7.395 +if UnparseC.term t' = "a + b + x" then ()
7.396 +else error "termorder.sml diff.behav ord_make_polynomial_in #13";
7.397 +
7.398 + val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
7.399 + val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
7.400 +val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
7.401 +if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
7.402 +else error "termorder.sml diff.behav ord_make_polynomial_in #15";
7.403 +
7.404 + val ttt' = "(3*x + 5)/18 ::real";
7.405 + val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
7.406 +val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
7.407 +if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
7.408 +else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
7.409 +
7.410 +val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
7.411 +if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
7.412 +else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
7.413 +
7.414 +\<close> ML \<open>
7.415 +"----------- lin.eq degree_0 -------------------------------------";
7.416 +"----------- lin.eq degree_0 -------------------------------------";
7.417 +"----------- lin.eq degree_0 -------------------------------------";
7.418 +"----- d0_false ------";
7.419 +val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
7.420 +val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
7.421 + ["PolyEq", "solve_d0_polyeq_equation"]);
7.422 +(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
7.423 +TODO: change to "equality (x + - 1*x = (0::real))"
7.424 + and search for an appropriate problem and method.
7.425 +
7.426 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.427 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.428 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.429 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.430 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.431 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.432 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.433 +case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
7.434 + | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
7.435 +
7.436 +"----- d0_true ------";
7.437 +val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
7.438 +val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
7.439 + ["PolyEq", "solve_d0_polyeq_equation"]);
7.440 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.441 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.442 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.443 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.444 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.445 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.446 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.447 +case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
7.448 + | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
7.449 +============ inhibit exn WN110914 ============================================*)
7.450 +
7.451 +\<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)
7.452 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
7.453 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
7.454 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
7.455 +"----- d2_pqformula1 ------!!!!";
7.456 +val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
7.457 +val (dI',pI',mI') =
7.458 + ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
7.459 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.460 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.461 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.462 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.463 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.464 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.465 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.466 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
7.467 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.468 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.469 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.470 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.471 +
7.472 +(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
7.473 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
7.474 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.475 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.476 +
7.477 +if p = ([], Res) andalso
7.478 + f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
7.479 + case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
7.480 +else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
7.481 +
7.482 +\<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)
7.483 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
7.484 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
7.485 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
7.486 +"----- d2_pqformula1_neg ------";
7.487 +val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
7.488 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.489 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.490 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.491 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.492 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.493 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.494 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.495 +(*### or2list False
7.496 + ([1],Res) False Or_to_List)*)
7.497 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.498 +(*### or2list False
7.499 + ([2],Res) [] Check_elementwise "Assumptions"*)
7.500 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.501 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.502 +val asm = Ctree.get_assumptions pt p;
7.503 +if f2str f = "[]" andalso
7.504 + UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
7.505 + "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
7.506 +else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
7.507 +
7.508 +\<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)
7.509 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
7.510 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
7.511 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
7.512 +"----- d2_pqformula2 ------";
7.513 +val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.514 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.515 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.516 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.517 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.518 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.519 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.520 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.521 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.522 +
7.523 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.524 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.525 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.526 +case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
7.527 + | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
7.528 +
7.529 +
7.530 +\<close> ML \<open>
7.531 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
7.532 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
7.533 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
7.534 +"----- d2_pqformula3 ------";
7.535 +(*EP-9*)
7.536 +val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.537 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.538 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.539 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.540 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.541 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.542 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.543 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.544 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.545 +
7.546 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.547 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.548 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.549 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
7.550 + | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
7.551 +
7.552 +
7.553 +\<close> ML \<open>
7.554 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
7.555 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
7.556 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
7.557 +"----- d2_pqformula3_neg ------";
7.558 +val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.559 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.560 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.561 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.562 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.563 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.564 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.565 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.566 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.567 +
7.568 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.569 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.570 +"TODO 2 + x + x \<up> 2 = 0";
7.571 +"TODO 2 + x + x \<up> 2 = 0";
7.572 +"TODO 2 + x + x \<up> 2 = 0";
7.573 +
7.574 +\<close> ML \<open>
7.575 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
7.576 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
7.577 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
7.578 +"----- d2_pqformula4 ------";
7.579 +val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.580 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.581 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.582 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.583 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.584 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.585 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.586 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.587 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.588 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.589 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.590 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.591 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
7.592 + | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
7.593 +
7.594 +\<close> ML \<open>
7.595 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
7.596 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
7.597 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
7.598 +"----- d2_pqformula5 ------";
7.599 +val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.600 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.601 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.602 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.603 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.604 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.605 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.606 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.607 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.608 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.609 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.610 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.611 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.612 + | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
7.613 +
7.614 +\<close> ML \<open>
7.615 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
7.616 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
7.617 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
7.618 +"----- d2_pqformula6 ------";
7.619 +val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.620 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.621 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.622 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.623 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.624 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.625 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.626 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.627 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.628 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.629 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.630 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.631 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.632 + | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
7.633 +
7.634 +\<close> text \<open> (*=====calcul: rhs = (1::?'a) - (0::?'a) *)
7.635 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
7.636 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
7.637 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
7.638 +"----- d2_pqformula7 ------";
7.639 +(*EP- 10*)
7.640 +val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.641 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.642 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.643 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.644 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.645 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.646 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.647 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.648 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.649 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.650 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.651 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.652 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.653 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
7.654 +
7.655 +\<close> text \<open> (*=====calcul: rhs = (1::?'b) - (0::?'b) *)
7.656 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
7.657 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
7.658 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
7.659 +"----- d2_pqformula8 ------";
7.660 +val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.661 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.662 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.663 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.664 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.665 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.666 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.667 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.668 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.669 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.670 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.671 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.672 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.673 + | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
7.674 +
7.675 +\<close> ML \<open>
7.676 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
7.677 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
7.678 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
7.679 +"----- d2_pqformula9 ------";
7.680 +val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.681 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.682 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.683 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.684 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.685 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.686 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.687 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.688 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.689 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.690 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.691 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
7.692 + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
7.693 +
7.694 +
7.695 +\<close> ML \<open>
7.696 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
7.697 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
7.698 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
7.699 +"----- d2_pqformula9_neg ------";
7.700 +val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.701 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.702 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.703 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.704 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.705 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.706 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.707 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.708 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.709 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.710 +"TODO 4 + 1*x \<up> 2 = 0";
7.711 +"TODO 4 + 1*x \<up> 2 = 0";
7.712 +"TODO 4 + 1*x \<up> 2 = 0";
7.713 +
7.714 +\<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)
7.715 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
7.716 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
7.717 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
7.718 +val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.719 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.720 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.721 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.722 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.723 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.724 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.725 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.726 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.727 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.728 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.729 +case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
7.730 + | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
7.731 +
7.732 +\<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)
7.733 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
7.734 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
7.735 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
7.736 +val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.737 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.738 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.739 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.740 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.741 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.742 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.743 +
7.744 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.745 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.746 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.747 +"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
7.748 +"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
7.749 +"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
7.750 +
7.751 +
7.752 +\<close> ML \<open>
7.753 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
7.754 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
7.755 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
7.756 +(*EP- 11*)
7.757 +val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.758 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.759 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.760 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.761 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.762 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.763 +
7.764 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.765 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.766 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.767 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.768 +
7.769 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.770 +case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
7.771 + | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
7.772 +
7.773 +
7.774 +\<close> text \<open> (*=====calcul: rhs = (1::?'c) - (0::?'c) *)
7.775 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
7.776 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
7.777 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
7.778 +val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.779 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.780 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.781 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.782 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.783 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.784 +
7.785 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.786 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.787 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.788 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.789 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.790 +"TODO 1 + x + 2*x \<up> 2 = 0";
7.791 +"TODO 1 + x + 2*x \<up> 2 = 0";
7.792 +"TODO 1 + x + 2*x \<up> 2 = 0";
7.793 +
7.794 +
7.795 +val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.796 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.797 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.798 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.799 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.800 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.801 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.802 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.803 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.804 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.805 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.806 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
7.807 + | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
7.808 +
7.809 +val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.810 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.811 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.812 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.813 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.814 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.815 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.816 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.817 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.818 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.819 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.820 +"TODO 2 + 1*x + x \<up> 2 = 0";
7.821 +"TODO 2 + 1*x + x \<up> 2 = 0";
7.822 +"TODO 2 + 1*x + x \<up> 2 = 0";
7.823 +
7.824 +(*EP- 12*)
7.825 +val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.826 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.827 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.828 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.829 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.830 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.831 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.832 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.833 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.834 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.835 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.836 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
7.837 + | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
7.838 +
7.839 +val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.840 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.841 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.842 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.843 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.844 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.845 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.846 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.847 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.848 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.849 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.850 +"TODO 2 + x + x \<up> 2 = 0";
7.851 +"TODO 2 + x + x \<up> 2 = 0";
7.852 +"TODO 2 + x + x \<up> 2 = 0";
7.853 +
7.854 +(*EP- 13*)
7.855 +val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.856 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.857 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.858 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.859 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.860 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.861 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.862 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.863 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.864 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.865 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.866 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
7.867 + | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
7.868 +
7.869 +val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.870 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.871 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.872 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.873 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.874 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.875 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.876 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.877 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.878 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.879 +"TODO 8+ 2*x \<up> 2 = 0";
7.880 +"TODO 8+ 2*x \<up> 2 = 0";
7.881 +"TODO 8+ 2*x \<up> 2 = 0";
7.882 +
7.883 +(*EP- 14*)
7.884 +val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.885 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.886 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.887 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.888 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.889 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.890 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.891 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.892 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.893 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.894 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
7.895 + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
7.896 +
7.897 +
7.898 +val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.899 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.900 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.901 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.902 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.903 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.904 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.905 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.906 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.907 +"TODO 4+ x \<up> 2 = 0";
7.908 +"TODO 4+ x \<up> 2 = 0";
7.909 +"TODO 4+ x \<up> 2 = 0";
7.910 +
7.911 +(*EP- 15*)
7.912 +val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.913 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.914 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.915 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.916 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.917 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.918 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.919 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.920 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.921 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.922 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.923 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.924 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
7.925 +
7.926 +val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.927 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.928 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.929 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.930 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.931 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.932 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.933 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.934 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.935 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.936 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.937 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.938 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
7.939 +
7.940 +(*EP- 16*)
7.941 +val fmz = ["equality (x + 2 * x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];
7.942 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.943 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.944 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.945 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.946 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.947 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.948 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.949 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.950 +
7.951 +(*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f;
7.952 +(*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt
7.953 +
7.954 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)
7.955 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.956 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.957 +case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
7.958 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
7.959 +
7.960 +(*EP-//*)
7.961 +val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.962 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.963 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.964 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.965 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.966 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.967 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.968 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.969 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.970 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.971 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.972 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.973 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
7.974 +
7.975 +
7.976 +\<close> ML \<open>
7.977 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.978 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.979 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.980 +(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
7.981 +see --- val rls = calculate_RootRat > calculate_Rational ---
7.982 +calculate_RootRat was a TODO with 2002, requires re-design.
7.983 +see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
7.984 +*)
7.985 + val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
7.986 + "solveFor x", "solutions L"];
7.987 + val (dI',pI',mI') =
7.988 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
7.989 + ["PolyEq", "complete_square"]);
7.990 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.991 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.992 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.993 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.994 +
7.995 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.996 +(*Apply_Method ("PolyEq", "complete_square")*)
7.997 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.998 +(*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
7.999 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1000 +(*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
7.1001 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1002 +(*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
7.1003 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1004 +(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
7.1005 + 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
7.1006 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1007 +(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
7.1008 + - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
7.1009 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1010 +(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
7.1011 + - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
7.1012 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1013 +(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
7.1014 + x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
7.1015 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1016 +(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
7.1017 + x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
7.1018 + NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
7.1019 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1020 +(*"x = - 2 | x = 4" nxt = Or_to_List*)
7.1021 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1022 +(*"[x = - 2, x = 4]" nxt = Check_Postcond*)
7.1023 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
7.1024 +(* FIXXXME
7.1025 + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
7.1026 + | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
7.1027 +*)
7.1028 +if f2str f =
7.1029 + "[x = - 1 * - 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))]"
7.1030 +(*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
7.1031 +then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
7.1032 +
7.1033 +
7.1034 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
7.1035 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
7.1036 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
7.1037 +(*stopped due to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
7.1038 +see --- val rls = calculate_RootRat > calculate_Rational ---*)
7.1039 +val thy = @{theory PolyEq};
7.1040 +val ctxt = Proof_Context.init_global thy;
7.1041 +val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
7.1042 +val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
7.1043 +
7.1044 +val rls = complete_square;
7.1045 +val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
7.1046 +if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2"
7.1047 +then () else error "rls complete_square CHANGED";
7.1048 +
7.1049 +val thm = @{thm square_explicit1};
7.1050 +val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
7.1051 +if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
7.1052 +then () else error "thm square_explicit1 CHANGED";
7.1053 +
7.1054 +val thm = @{thm root_plus_minus};
7.1055 +val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
7.1056 +if UnparseC.term t =
7.1057 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
7.1058 +then () else error "thm root_plus_minus CHANGED";
7.1059 +
7.1060 +(*the thm bdv_explicit2* here required to be constrained to ::real*)
7.1061 +val thm = @{thm bdv_explicit2};
7.1062 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
7.1063 +if UnparseC.term t =
7.1064 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
7.1065 +then () else error "thm bdv_explicit2 CHANGED";
7.1066 +
7.1067 +val thm = @{thm bdv_explicit3};
7.1068 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
7.1069 +if UnparseC.term t =
7.1070 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
7.1071 +then () else error "thm bdv_explicit3 CHANGED";
7.1072 +
7.1073 +val thm = @{thm bdv_explicit2};
7.1074 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
7.1075 +if UnparseC.term t =
7.1076 +"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
7.1077 +then () else error "thm bdv_explicit2 CHANGED";
7.1078 +
7.1079 +val rls = calculate_RootRat;
7.1080 +val SOME (t,asm) = rewrite_set_ thy true rls t;
7.1081 +if UnparseC.term t =
7.1082 + "- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - - 8) \<or>\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))"
7.1083 +(*"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"..isabisac15*)
7.1084 +then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
7.1085 +(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
7.1086 +
7.1087 +
7.1088 +"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
7.1089 +"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
7.1090 +"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
7.1091 +"---- test the erls ----";
7.1092 + val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
7.1093 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
7.1094 + val t' = UnparseC.term t;
7.1095 + (*if t'= \<^const_name>\<open>True\<close> then ()
7.1096 + else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
7.1097 +(* *)
7.1098 + val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
7.1099 + "solveFor x", "solutions L"];
7.1100 + val (dI',pI',mI') =
7.1101 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
7.1102 + ["PolyEq", "complete_square"]);
7.1103 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.1104 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1105 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1106 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1107 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1108 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1109 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1110 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1111 + (*Apply_Method ("PolyEq", "complete_square")*)
7.1112 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
7.1113 +
7.1114 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
7.1115 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
7.1116 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
7.1117 + val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
7.1118 + "solveFor x", "solutions L"];
7.1119 + val (dI',pI',mI') =
7.1120 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
7.1121 + ["PolyEq", "complete_square"]);
7.1122 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.1123 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1124 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1125 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1126 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1127 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1128 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1129 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1130 + (*Apply_Method ("PolyEq", "complete_square")*)
7.1131 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1132 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1133 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1134 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1135 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1136 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1137 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1138 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1139 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1140 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1141 +(* FIXXXXME n1.,
7.1142 + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
7.1143 + | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
7.1144 +*)
7.1145 +
7.1146 \<close> ML \<open>
7.1147 \<close> ML \<open>
7.1148 \<close>