# HG changeset patch # User wneuper # Date 1631614977 -7200 # Node ID 54d17d6d42450e8d0f7728d43c41f73783273563 # Parent 2d97d160a183826d150157c61723e87b5c0a7166 \\adopt Isabelles calculation of numerals, some cases are missing diff -r 2d97d160a183 -r 54d17d6d4245 src/Tools/isac/ProgLang/Calculate.thy --- a/src/Tools/isac/ProgLang/Calculate.thy Mon Sep 13 16:01:48 2021 +0200 +++ b/src/Tools/isac/ProgLang/Calculate.thy Tue Sep 14 12:22:57 2021 +0200 @@ -24,36 +24,54 @@ \ ML \ (*** evaluate binary associative operations ***) -fun eval_binop _ _ - (t as ((opp as Const (op0, _)) $ (Const (op0', _) $ v $ t1) $ t2)) _ =(* binary . (v.n1).n2 *) - if op0 = op0' andalso TermC.is_num t1 andalso TermC.is_num t2 then - let - val op' = if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0 - val res = Eval.calcul op' (t1, t2); - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ v $ res)); - in SOME ("#: " ^ UnparseC.term prop, prop) end - else NONE - | eval_binop _ (_ : string) - (t as ((opp as Const (op0, _)) $ t1 $ (Const (op0', _) $ t2 $ v))) _ =(* binary . n1.(n2.v) *) - if op0 = op0' andalso op0 <> "Groups.minus_class.minus" - andalso TermC.is_num t1 andalso TermC.is_num t2 then - let - val res = Eval.calcul op0 (t1, t2); - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ res $ v)); - in - SOME ("#: " ^ UnparseC.term prop, prop) - end - else NONE - | eval_binop _ _ (t as (Const (op0, _) $ t1 $ t2)) _ = (* binary . n1.n2 *) - if TermC.is_num t1 andalso TermC.is_num t2 then - let - val res = Eval.calcul op0 (t1, t2); - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res)); - in - SOME ("#: " ^ UnparseC.term prop, prop) - end - else NONE - | eval_binop _ _ _ _ = NONE; +val is_num = can HOLogic.dest_number; + +val is_calcul_op = + member (op =) [\<^const_name>\plus\, \<^const_name>\minus\, \<^const_name>\times\, \<^const_name>\powr\]; + +fun calcul thy lhs = + let + val _ = tracing ("-----calcul: lhs = " ^ UnparseC.term lhs) + val simp_ctxt = + Proof_Context.init_global thy + |> put_simpset (Simplifier.simpset_of @{theory_context Complex_Main}); + val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs); + val rhs = Thm.term_of (Thm.rhs_of eq); + val _ = tracing ("=====calcul: rhs = " ^ UnparseC.term rhs)(* \<^assert> (is_num rhs);*) + in rhs end; + +fun eval_binop (_: string) (_: string) t thy = + (case t of + (opp as Const (c1, T)) $ (Const (c2, _) $ v $ t1) $ t2 => (* binary \ (v \ n1) \ n2 *) + if c1 = c2 andalso is_calcul_op c1 andalso is_num t1 andalso is_num t2 then + let + val opp' = Const (if c1 = \<^const_name>\minus\ then \<^const_name>\plus\ else c1, T); + val res = calcul thy (opp' $ t1 $ t2); + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ v $ res)); + in SOME ("#: " ^ UnparseC.term prop, prop) end + else NONE + | (opp as Const (c1, _)) $ t1 $ (Const (c2, _) $ t2 $ v) => (* binary \ n1 \ (n2 \ v) *) + if c1 = c2 andalso is_calcul_op c1 andalso c1 <> \<^const_name>\minus\ + andalso is_num t1 andalso is_num t2 + then + let + val res = calcul thy (opp $ t1 $ t2); + val prop = HOLogic.Trueprop $ HOLogic.mk_eq (t, opp $ res $ v); + in + SOME ("#: " ^ UnparseC.term prop, prop) + end + else NONE + | Const (c, _) $ t1 $ t2 => (* binary \ n1 \ n2 *) + if is_calcul_op c andalso is_num t1 andalso is_num t2 then + let + val res = calcul thy t; + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res)); + in + SOME ("#: " ^ UnparseC.term prop, prop) + end + else NONE + | _ => NONE); + \ ML \ \ ML \ \ diff -r 2d97d160a183 -r 54d17d6d4245 src/Tools/isac/ProgLang/evaluate.sml --- a/src/Tools/isac/ProgLang/evaluate.sml Mon Sep 13 16:01:48 2021 +0200 +++ b/src/Tools/isac/ProgLang/evaluate.sml Tue Sep 14 12:22:57 2021 +0200 @@ -18,7 +18,6 @@ val adhoc_thm1_: theory -> Eval_Def.cal -> term -> (string * thm) option val norm: term -> term val popt2str: ('a * term) option -> string - val calcul: string -> term * term -> term val trace_on: bool Unsynchronized.ref val int_of_numeral: term -> int \<^isac_test>\ @@ -110,7 +109,7 @@ fun trace_calc4 str t1 t2 = if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else () -fun get_pair (*1*)thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *) +fun get_pair (*1*)thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *) if op_ = op0 then let val popt = ef op_ t thy in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end @@ -127,7 +126,7 @@ let val popt = get_pair thy op_ ef t1 val _ = trace_calc2 "3.. get_pair: " t1 popt - in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end + in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end (* search subterms *) end else (* search subterms *) let @@ -194,8 +193,6 @@ else (*3*) mk_rule (prems, concl, @{term True}) end; -(*** handle numerals in eval_binop ***) - (* preliminary HACK *) fun int_of_numeral (Const (\<^const_name>\zero_class.zero\, _)) = 0 | int_of_numeral (Const (\<^const_name>\one_class.one\, _)) = 1 @@ -203,19 +200,6 @@ | int_of_numeral (Const (\<^const_name>\numeral\, _) $ n) = HOLogic.dest_numeral n | int_of_numeral t = raise TERM ("int_of_numeral", [t]); -fun calcul op_ (t1, t2) = - let - val (T, _) = HOLogic.dest_number t1 - val (i1, i2) = (int_of_numeral t1, int_of_numeral t2) - val result = - case op_ of - "Groups.plus_class.plus" => i1 + i2 (* preliminary HACK *) - | "Groups.minus_class.minus" => i1 - i2 (* preliminary HACK *) - | "Groups.times_class.times" => i1 * i2 (* preliminary HACK *) - | "Transcendental.powr" => power i1 i2 (* preliminary HACK *) - | str => raise ERROR ("calcul not impl.for op_ " ^ str) - in HOLogic.mk_number T result end; - end diff -r 2d97d160a183 -r 54d17d6d4245 test/Tools/isac/ProgLang/calculate.sml --- a/test/Tools/isac/ProgLang/calculate.sml Mon Sep 13 16:01:48 2021 +0200 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Sep 14 12:22:57 2021 +0200 @@ -14,25 +14,18 @@ "----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; "----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; "----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; -val (t1, t2) = (@{term 3}, @{term "2::real"}); -val t = HOLogic.mk_binop "Groups.plus_class.plus" (t1, t2); - eval_binop "" "" t ""; -"~~~~~ fun eval_binop , args:"; val (_, _, (t as (Const (op0, t0) $ t1 $ t2)), _) =(* binary . n1.n2 *) - ((), (), t, ()); - (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*); - val res = calcul op0 (t1, t2); - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res)); - (*in*) - val xxx = SOME ("#: " ^ UnparseC.term prop, prop); - (*end*) +fun test thy t = writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul thy t))); -case xxx of - SOME - ("#: (3::'a) + 2 = (5::'a)", - Const (\<^const_name>\Trueprop\, _) $ - (Const (\<^const_name>\HOL.eq\, _) $ - (Const (\<^const_name>\plus_class.plus\, _) $ _ $ - (Const (\<^const_name>\numeral\, _) $ _ )) $ - _ )) => () -| _ => error "eval_binop #: (3::'a) + 2 = (5::'a) CHANGED" +test \<^theory> \<^term>\10 + 20 :: real\; +test \<^theory> \<^term>\10 - 20 :: real\; +test \<^theory> \<^term>\10 * 20 :: real\; +test \<^theory> \<^term>\10 powr 20 :: real\; + +test \<^theory> \<^term>\10 + 20 :: int\; +test \<^theory> \<^term>\10 - 20 :: int\; +test \<^theory> \<^term>\10 * 20 :: int\; + +test \<^theory> \<^term>\10 + 20 :: nat\; +test \<^theory> \<^term>\10 - 20 :: nat\; +test \<^theory> \<^term>\10 * 20 :: nat\; diff -r 2d97d160a183 -r 54d17d6d4245 test/Tools/isac/ProgLang/evaluate.sml --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Sep 13 16:01:48 2021 +0200 +++ b/test/Tools/isac/ProgLang/evaluate.sml Tue Sep 14 12:22:57 2021 +0200 @@ -300,41 +300,21 @@ "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; -val (t1, t2) = (@{term 3}, @{term "2::real"}); +val t = @{term "2 + 3 ::real"}; -"~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2)); - val (Const (\<^const_name>\numeral\, _) $ n1) = t1; - val (Const (\<^const_name>\numeral\, _) $ n2) = t2; - val (T, _) = HOLogic.dest_number t1 - val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2) - val result = - case op_ of - "Groups.plus_class.plus" => i1 + i2 - | "Groups.minus_class.minus" => i1 - i2 - | "Groups.times_class.times" => i1 * i2 - | "Transcendental.powr" => power i1 i2 - | str => raise ERROR ("calcul not impl.for op_ " ^ str) - (*in*) - val xxx = HOLogic.mk_number T result; - (*end*) -case HOLogic.dest_number xxx of - (_, 5) => () -| _ => error "calcul + 2 3 CHANGED"; +"~~~~~ fun calcul , args:"; val (thy, lhs) = (@{theory}, t); + val simp_ctxt = + Proof_Context.init_global thy + |> put_simpset (Simplifier.simpset_of @{theory_context Complex_Main}); + val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs); -case HOLogic.dest_number (calcul "Groups.minus_class.minus" (t1, t2)) of - (_, 1) => xxx -| _ => error "calcul - 2 3 CHANGED"; +if ThmC.string_of_thm eq = "2 + 3 \ 5" then () else error "calcul 1"; -case HOLogic.dest_number (calcul "Groups.times_class.times" (t1, t2)) of - (_, 6) => xxx -| _ => error "calcul - 2 3 CHANGED"; + val rhs = Thm.term_of (Thm.rhs_of eq); + val _ = \<^assert> (is_num rhs); -(* (calcul "Rings.divide_class.divide" (t1, t2) -ERROR: calcul not impl.for op_ Rings.divide_class.divide*) - -case HOLogic.dest_number (calcul "Transcendental.powr" (t1, t2)) of - (_, 9) => xxx -| _ => error "calcul - 2 3 CHANGED"; +(*return value*) rhs; +if TermC.to_string rhs = "5" then () else error "calcul 2"; "----------- get_pair with 3 args --------------------------------"; diff -r 2d97d160a183 -r 54d17d6d4245 test/Tools/isac/ProgLang/prog_expr.sml --- a/test/Tools/isac/ProgLang/prog_expr.sml Mon Sep 13 16:01:48 2021 +0200 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Tue Sep 14 12:22:57 2021 +0200 @@ -424,21 +424,22 @@ val t = (Thm.term_of o the o (TermC.parse thy)) "2 * 3"; (*val SOME (thmid,t') = *)get_pair thy op_ ef t; ; -"~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) = +"~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) = (thy, op_, ef, t); -op_ = op0 = true;val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES")); -val t = (Thm.term_of o the o (TermC.parse thy)) "2 * 3"; - + (*if*) op_ = op0; (*then*) + val popt = ef op_ t thy; -"~~~~~ fun eval_binop , args:"; val ((thmid : string), (op_: string), - (t as (Const (op0, _) $ t1 $ t2)), _) = - ("#mult_", op_, t, thy); (* binary . n1.n2 *) - (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*); - val res = Eval.calcul op0 (t1, t2); - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res)); -val SOME (thmid, tm) = SOME ("#: " ^ UnparseC.term prop, prop) +"~~~~~ fun eval_binop , args:"; val ((_ : string), (_: string), + (t as (Const (op0, _) $ t1 $ t2)), thy) = + ("#mult_", op_, t, thy); +val Const (c, _) $ t1 $ t2 = (* binary \ n1 \ n2 *) + (*case*) t (*of*); + (*if*) is_calcul_op c andalso is_num t1 andalso is_num t2 (*then*); + val res = calcul thy t; + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res)); + SOME ("#: " ^ UnparseC.term prop, prop) (*return value*); ; -if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then () +if "#: " ^ UnparseC.term prop = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then () else error "eval_binop changed" ; val SOME (thmid, tm) = eval_binop "#mult_" op_ t thy; diff -r 2d97d160a183 -r 54d17d6d4245 test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Mon Sep 13 16:01:48 2021 +0200 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Sep 14 12:22:57 2021 +0200 @@ -293,6 +293,18 @@ ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*) ML_file "Knowledge/polyeq-1.sml" +ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ (*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*) (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *) ML_file "Knowledge/calculus.sml" diff -r 2d97d160a183 -r 54d17d6d4245 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Mon Sep 13 16:01:48 2021 +0200 +++ b/test/Tools/isac/Test_Some.thy Tue Sep 14 12:22:57 2021 +0200 @@ -107,6 +107,1145 @@ section \===================================================================================\ ML \ \ ML \ +(* Title: Knowledge/polyeq-1.sml + testexamples for PolyEq, poynomial equations and equational systems + Author: Richard Lang 2003 + (c) due to copyright terms + +Separation into polyeq-1.sml and polyeq-1a.sml due to +*) + +"-----------------------------------------------------------------"; +"table of contents -----------------------------------------------"; +"-----------------------------------------------------------------"; +"------ polyeq-1.sml ---------------------------------------------"; +"----------- tests on predicates in problems ---------------------"; +"----------- test matching problems ------------------------------"; +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; +"----------- open local of fun ord_make_polynomial_in ------------------------------------------"; +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; +"----------- lin.eq degree_0 -------------------------------------"; +"----------- test thm's d2_pq_formulsxx[_neg]---------------------"; +"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; +"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; +"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; +"----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; +"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; +"----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; +"----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; +"----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; +"----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; +"----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; +"----------- equality (4 + 1*x \ 2 = 0) -------------------------------------------------------"; +"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; +"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; +"----------- equality (1 + x + 2*x \ 2 = 0) --------------------------------------------------"; +"----------- (-8 - 2*x + x \ 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; +"----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; +"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; +"-----------------------------------------------------------------"; +"------ polyeq-2.sml ---------------------------------------------"; +"----------- (a*b - (a+b)*x + x \ 2 = 0), (*Schalk 2,S.68Nr.44.a*)"; +"----------- (-64 + x \ 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; +"----------- (- 147 + 3*x \ 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5"; +"----------- ((x+1)*(x+2) - (3*x - 2) \ 2=.. Schalk II s.68 Bsp 37"; +"----------- rls make_polynomial_in ------------------------------"; +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; +"----------- rls d2_polyeq_bdv_only_simplify ---------------------"; +"-----------------------------------------------------------------"; +"-----------------------------------------------------------------"; + +"----------- tests on predicates in problems ---------------------"; +"----------- tests on predicates in problems ---------------------"; +"----------- tests on predicates in problems ---------------------"; +val thy = @{theory}; +Rewrite.trace_on:=false; (*true false*) + + val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \ 2 = 0)"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1; + if ((UnparseC.term t) = "- 8 - 2 * x + x \ 2") then () + else error "polyeq.sml: diff.behav. in lhs"; + +\ ML \ + val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \ 2) is_expanded_in x"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2; + if (UnparseC.term t) = "True" then () + else error "polyeq.sml: diff.behav. 1 in is_expended_in"; + + val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0; + if (UnparseC.term t) = "False" then () + else error "polyeq.sml: diff.behav. 2 in is_poly_in"; + + val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \ 2) is_poly_in x"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; + if (UnparseC.term t) = "True" then () + else error "polyeq.sml: diff.behav. 3 in is_poly_in"; + + val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \ 2 = 0)) is_expanded_in x"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; + if (UnparseC.term t) = "True" then () + else error "polyeq.sml: diff.behav. 4 in is_expended_in"; + + val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \ 2 = 0)) is_expanded_in x"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6; + if (UnparseC.term t) = "True" then () + else error "polyeq.sml: diff.behav. 5 in is_expended_in"; + + val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \ 2) has_degree_in x) = 2"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; + if (UnparseC.term t) = "True" then () + else error "polyeq.sml: diff.behav. in has_degree_in_in"; + + val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; + if (UnparseC.term t) = "False" then () + else error "polyeq.sml: diff.behav. 6 in has_degree_in_in"; + + val t4 = (Thm.term_of o the o (TermC.parse thy)) + "((-8 - 2*x + x \ 2) has_degree_in x) = 1"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; + if (UnparseC.term t) = "False" then () + else error "polyeq.sml: diff.behav. 7 in has_degree_in_in"; + +val t5 = (Thm.term_of o the o (TermC.parse thy)) + "((-8 - 2*x + x \ 2) has_degree_in x) = 2"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5; + if (UnparseC.term t) = "True" then () + else error "polyeq.sml: diff.behav. 8 in has_degree_in_in"; + +\ ML \ +"----------- test matching problems --------------------------0---"; +"----------- test matching problems --------------------------0---"; +"----------- test matching problems --------------------------0---"; +val fmz = ["equality (-8 - 2*x + x \ 2 = 0)", "solveFor x", "solutions L"]; +if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) = + M_Match.Matches' {Find = [Correct "solutions L"], + With = [], + Given = [Correct "equality (- 8 - 2 * x + x \ 2 = 0)", Correct "solveFor x"], + Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \ 2 = 0)", + Correct "lhs (- 8 - 2 * x + x \ 2 = 0) is_expanded_in x"], + Relate = []} +then () else error "M_Match.match_pbl [expanded,univariate,equation]"; + +if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) = + M_Match.Matches' {Find = [Correct "solutions L"], + With = [], + Given = [Correct "equality (- 8 - 2 * x + x \ 2 = 0)", Correct "solveFor x"], + Where = [Correct "lhs (- 8 - 2 * x + x \ 2 = 0) has_degree_in x = 2"], + Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*) +then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]"; + + +\ ML \ +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; +(*################################################################################## +----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy + + (*Aufgabe zum Einstieg in die Arbeit...*) + val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \ 2 = 0"; + (*ein 'ruleset' aus Poly.ML wird angewandt...*) + val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t; + UnparseC.term t; + "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \ 2)) = 0"; + val SOME (t,_) = + rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t; + UnparseC.term t; + "x \ 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0"; +(* bei Verwendung von "size_of-term" nach MG :*) +(*"x \ 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *) + + (*wir holen 'a' wieder aus der Klammerung heraus...*) + val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t; + UnparseC.term t; + "x \ 2 + - 1 * b * x + - 1 * x * a + b * a = 0"; +(* "x \ 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *) + + val SOME (t,_) = + rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t; + UnparseC.term t; + "x \ 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0"; + (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben + "x \ 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*) + + (*das rewriting l"asst sich beobachten mit +Rewrite.trace_on := false; (*true false*) + *) + +"------ 15.11.02 --------------------------"; + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x"; + val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv"; + val a = (Thm.term_of o the o (TermC.parse thy)) "a"; + +Rewrite.trace_on := false; (*true false*) + (* Anwenden einer Regelmenge aus Termorder.ML: *) + val SOME (t,_) = + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; + UnparseC.term t; + val SOME (t,_) = + rewrite_set_ thy false discard_parentheses t; + UnparseC.term t; +"1 + b * x + x * a"; + + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \ 2"; + val SOME (t,_) = + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; + UnparseC.term t; + val SOME (t,_) = + rewrite_set_ thy false discard_parentheses t; + UnparseC.term t; +"1 + (x + b * x) * a + a \ 2"; + + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \ 2 * x + b * a + 7*a \ 2"; + val SOME (t,_) = + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; + UnparseC.term t; + val SOME (t,_) = + rewrite_set_ thy false discard_parentheses t; + UnparseC.term t; +"1 + b * a + (7 + x) * a \ 2"; + +(* MG2003 + Prog_Expr.thy grundlegende Algebra + Poly.thy Polynome + Rational.thy Br"uche + Root.thy Wurzeln + RootRat.thy Wurzen + Br"uche + Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03) + + get_thm Termorder.thy "bdv_n_collect"; + get_thm (theory "Isac_Knowledge") "bdv_n_collect"; +*) + val t = (Thm.term_of o the o (TermC.parse thy)) "a \ 2 * x + 7 * a \ 2"; + val SOME (t,_) = + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; + UnparseC.term t; + val SOME (t,_) = + rewrite_set_ thy false discard_parentheses t; + UnparseC.term t; +"(7 + x) * a \ 2"; + + val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi"; + + val t = (Thm.term_of o the o (parseold thy)) "7"; +##################################################################################*) + + +\ ML \ +"----------- open local of fun ord_make_polynomial_in ------------------------------------------"; +"----------- open local of fun ord_make_polynomial_in ------------------------------------------"; +"----------- open local of fun ord_make_polynomial_in ------------------------------------------"; +(* termorder hacked by MG, adapted later by WN *) +(** )local ( *. for make_polynomial_in .*) + +open Term; (* for type order = EQUAL | LESS | GREATER *) + +fun pr_ord EQUAL = "EQUAL" + | pr_ord LESS = "LESS" + | pr_ord GREATER = "GREATER"; + +fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0) + | dest_hd' x (t as Free (a, T)) = + if x = t then ((("|||||||||||||", 0), T), 0) (*WN*) + else (((a, 0), T), 1) + | dest_hd' _ (Var v) = (v, 2) + | dest_hd' _ (Bound i) = ((("", i), dummyT), 3) + | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4) + | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def."; + +fun size_of_term' i pr x (t as Const (\<^const_name>\powr\, _) $ + Free (var, _) $ Free (pot, _)) = + (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else (); + case x of (*WN*) + (Free (xstr, _)) => + if xstr = var + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else (); + 1000 * (the (TermC.int_opt_of_string pot))) + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3) + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x)) + | size_of_term' i pr x (t as Abs (_, _, body)) = + (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else (); + 1 + size_of_term' (i + 1) pr x body) + | size_of_term' i pr x (f $ t) = + let + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else (); + val s1 = size_of_term' (i + 1) pr x f + val s2 = size_of_term' (i + 1) pr x t + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else (); + in (s1 + s2) end + | size_of_term' i pr x t = + (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else (); + case t of + Free (subst, _) => + (case x of + Free (xstr, _) => + if xstr = subst + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000) + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1) + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x)) + | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1)); + +fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) + let + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else (); + val ord = + case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else () + in ord end + | term_ord' i pr x _ (t, u) = + let + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else (); + val ord = + case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of + EQUAL => + let val (f, ts) = strip_comb t and (g, us) = strip_comb u + in + (case hd_ord (i + 1) pr x (f, g) of + EQUAL => (terms_ord x (i + 1) pr) (ts, us) + | ord => ord) + end + | ord => ord + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else () + in ord end +and hd_ord i pr x (f, g) = (* ~ term.ML *) + let + val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else (); + val ord = prod_ord + (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord + (dest_hd' x f, dest_hd' x g) + val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else (); + in ord end +and terms_ord x i pr (ts, us) = + let + val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else (); + val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us); + val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else (); + in ord end + +(** )in( *local*) + +fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) = + ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **) + case subst of + (_, x) :: _ => + term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS + | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst)) + +(** )end;( *local*) + +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; +if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then () else error "still GREATER?"; + +val x = TermC.str2term "x ::real"; + +val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \ 2 / 4 ::real"); +if 2006 = size_of_term' 1 false(*true*) x t1 +then () else error "size_of_term' (L * q_0 * x \ 2) CHANGED)"; + +val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \ 3) :: real"); +if 3004 = size_of_term' 1 false(*true*) x t2 +then () else error "size_of_term' (- 1 * (q_0 * x \ 3)) CHANGED"; + + +\ ML \ +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; + val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")]; + val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")]; + val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")]; + + val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x"; + val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b"; + val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b"; + val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b"; + +if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then () +else error "termorder.sml diff.behav ord_make_polynomial_in #1"; + +if ord_make_polynomial_in false(*true*) thy substa (x1,x2) = true(*LESS *) then () +else error "termorder.sml diff.behav ord_make_polynomial_in #2"; + +if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then () +else error "termorder.sml diff.behav ord_make_polynomial_in #3"; + + val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; + val bb = (Thm.term_of o the o (TermC.parse thy)) "x \ 3"; + ord_make_polynomial_in false(*true*) thy substx (aa, bb); + true; (* => LESS *) + + val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; + val bb = (Thm.term_of o the o (TermC.parse thy)) "x \ 3"; + ord_make_polynomial_in false(*true*) thy substa (aa, bb); + false; (* => GREATER *) + +(* und nach dem Re-engineering der Termorders in den 'rulesets' + kannst Du die 'gr"osste' Variable frei w"ahlen: *) + val bdv= TermC.str2term "bdv ::real"; + val x = TermC.str2term "x ::real"; + val a = TermC.str2term "a ::real"; + val b = TermC.str2term "b ::real"; +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; +if UnparseC.term t' = "b + x + a" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #11"; + +val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2; + +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2; +if UnparseC.term t' = "a + b + x" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #13"; + + val ppp' = "-6 + -5*x + x \ 3 + - 1*x \ 2 + - 1*x \ 3 + - 14*x \ 2"; + val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp'; +val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; +if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \ 2" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #15"; + + val ttt' = "(3*x + 5)/18 ::real"; + val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt'; +val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; +if UnparseC.term uuu = "(5 + 3 * x) / 18" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #16a"; + +val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt; +if UnparseC.term uuu = "(5 + 3 * x) / 18" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #16b"; + +\ ML \ +"----------- lin.eq degree_0 -------------------------------------"; +"----------- lin.eq degree_0 -------------------------------------"; +"----------- lin.eq degree_0 -------------------------------------"; +"----- d0_false ------"; +val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d0_polyeq_equation"]); +(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ======== +TODO: change to "equality (x + - 1*x = (0::real))" + and search for an appropriate problem and method. + +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => () + | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []"; + +"----- d0_true ------"; +val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d0_polyeq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => () + | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList"; +============ inhibit exn WN110914 ============================================*) + +\ text \ (*=====calcul: rhs = (- 1) \ 2 *) +"----------- test thm's d2_pq_formulsxx[_neg]---------------------"; +"----------- test thm's d2_pq_formulsxx[_neg]---------------------"; +"----------- test thm's d2_pq_formulsxx[_neg]---------------------"; +"----- d2_pqformula1 ------!!!!"; +val fmz = ["equality (- 1/8 + (- 1/4)*z + z \ 2 = (0::real))", "solveFor z", "solutions L"]; +val (dI',pI',mI') = + ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +if p = ([], Res) andalso + f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then + case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \ 2 = (0::real)) CHANGED 1" +else error "(- 1/8 + (- 1/4)*z + z \ 2 = (0::real)) CHANGED 2"; + +\ text \ (*=====calcul: rhs = (- 1) \ 2 *) +"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; +"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; +"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; +"----- d2_pqformula1_neg ------"; +val fmz = ["equality (2 +(- 1)*x + x \ 2 = (0::real))", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*### or2list False + ([1],Res) False Or_to_List)*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*### or2list False + ([2],Res) [] Check_elementwise "Assumptions"*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val asm = Ctree.get_assumptions pt p; +if f2str f = "[]" andalso + UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \ 2 = 0) is_poly_in x\", " ^ + "\"lhs (2 + - 1 * x + x \ 2 = 0) has_degree_in x = 2\"]" then () +else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \ 2 = 0"; + +\ text \ (*=====calcul: rhs = (- 1) \ 2 *) +"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; +"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; +"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; +"----- d2_pqformula2 ------"; +val fmz = ["equality (- 2 +(- 1)*x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 2, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]"; + + +\ ML \ +"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; +"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; +"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; +"----- d2_pqformula3 ------"; +(*EP-9*) +val fmz = ["equality (- 2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 1, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]"; + + +\ ML \ +"----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; +"----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; +"----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; +"----- d2_pqformula3_neg ------"; +val fmz = ["equality (2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +"TODO 2 + x + x \ 2 = 0"; +"TODO 2 + x + x \ 2 = 0"; +"TODO 2 + x + x \ 2 = 0"; + +\ ML \ +"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; +"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; +"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; +"----- d2_pqformula4 ------"; +val fmz = ["equality (- 2 + x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 1, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \ 2 = 0 -> [x = 1, x = - 2]"; + +\ ML \ +"----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; +"----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; +"----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; +"----- d2_pqformula5 ------"; +val fmz = ["equality (1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]"; + +\ ML \ +"----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; +"----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; +"----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; +"----- d2_pqformula6 ------"; +val fmz = ["equality (1*x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]"; + +\ text \ (*=====calcul: rhs = (1::?'a) - (0::?'a) *) +"----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; +"----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; +"----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; +"----- d2_pqformula7 ------"; +(*EP- 10*) +val fmz = ["equality ( x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; + +\ text \ (*=====calcul: rhs = (1::?'b) - (0::?'b) *) +"----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; +"----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; +"----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; +"----- d2_pqformula8 ------"; +val fmz = ["equality (x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]"; + +\ ML \ +"----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; +"----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; +"----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; +"----- d2_pqformula9 ------"; +val fmz = ["equality (-4 + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 2, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]"; + + +\ ML \ +"----------- equality (4 + 1*x \ 2 = 0) -------------------------------------------------------"; +"----------- equality (4 + 1*x \ 2 = 0) -------------------------------------------------------"; +"----------- equality (4 + 1*x \ 2 = 0) -------------------------------------------------------"; +"----- d2_pqformula9_neg ------"; +val fmz = ["equality (4 + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_pq_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +"TODO 4 + 1*x \ 2 = 0"; +"TODO 4 + 1*x \ 2 = 0"; +"TODO 4 + 1*x \ 2 = 0"; + +\ text \ (*=====calcul: rhs = (- 1) \ 2 *) +"-------------------- test thm's d2_abc_formulsxx[_neg]-----"; +"-------------------- test thm's d2_abc_formulsxx[_neg]-----"; +"-------------------- test thm's d2_abc_formulsxx[_neg]-----"; +val fmz = ["equality (- 1 +(- 1)*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => () + | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]"; + +\ text \ (*=====calcul: rhs = (- 1) \ 2 *) +"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; +"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; +"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; +val fmz = ["equality (1 +(- 1)*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +"TODO 1 +(- 1)*x + 2*x \ 2 = 0"; +"TODO 1 +(- 1)*x + 2*x \ 2 = 0"; +"TODO 1 +(- 1)*x + 2*x \ 2 = 0"; + + +\ ML \ +"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; +"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; +"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; +(*EP- 11*) +val fmz = ["equality (- 1 + x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]"; + + +\ text \ (*=====calcul: rhs = (1::?'c) - (0::?'c) *) +"----------- equality (1 + x + 2*x \ 2 = 0) --------------------------------------------------"; +"----------- equality (1 + x + 2*x \ 2 = 0) --------------------------------------------------"; +"----------- equality (1 + x + 2*x \ 2 = 0) --------------------------------------------------"; +val fmz = ["equality (1 + x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +"TODO 1 + x + 2*x \ 2 = 0"; +"TODO 1 + x + 2*x \ 2 = 0"; +"TODO 1 + x + 2*x \ 2 = 0"; + + +val fmz = ["equality (- 2 + 1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 1, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]"; + +val fmz = ["equality ( 2 + 1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +"TODO 2 + 1*x + x \ 2 = 0"; +"TODO 2 + 1*x + x \ 2 = 0"; +"TODO 2 + 1*x + x \ 2 = 0"; + +(*EP- 12*) +val fmz = ["equality (- 2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 1, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]"; + +val fmz = ["equality ( 2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +"TODO 2 + x + x \ 2 = 0"; +"TODO 2 + x + x \ 2 = 0"; +"TODO 2 + x + x \ 2 = 0"; + +(*EP- 13*) +val fmz = ["equality (-8 + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 2, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]"; + +val fmz = ["equality ( 8+ 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +"TODO 8+ 2*x \ 2 = 0"; +"TODO 8+ 2*x \ 2 = 0"; +"TODO 8+ 2*x \ 2 = 0"; + +(*EP- 14*) +val fmz = ["equality (-4 + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 2, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]"; + + +val fmz = ["equality ( 4+ x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +"TODO 4+ x \ 2 = 0"; +"TODO 4+ x \ 2 = 0"; +"TODO 4+ x \ 2 = 0"; + +(*EP- 15*) +val fmz = ["equality (2*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; + +val fmz = ["equality (1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; + +(*EP- 16*) +val fmz = ["equality (x + 2 * x \ 2 = (0::real))", "solveFor (x::real)", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +(*+*)val Test_Out.FormKF "x + 2 * x \ 2 = 0" = f; +(*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \ 2 = 0", d2_polyeq_abcFormula_simplify*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => () + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]"; + +(*EP-//*) +val fmz = ["equality (x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], + ["PolyEq", "solve_d2_polyeq_abc_equation"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; + + +\ ML \ +"----------- (-8 - 2*x + x \ 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; +"----------- (-8 - 2*x + x \ 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; +"----------- (-8 - 2*x + x \ 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; +(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat +see --- val rls = calculate_RootRat > calculate_Rational --- +calculate_RootRat was a TODO with 2002, requires re-design. +see also --- (-8 - 2*x + x \ 2 = 0), by rewriting --- below +*) + val fmz = ["equality (-8 - 2*x + x \ 2 = 0)", (*Schalk 2, S.67 Nr.31.b*) + "solveFor x", "solutions L"]; + val (dI',pI',mI') = + ("PolyEq",["degree_2", "expanded", "univariate", "equation"], + ["PolyEq", "complete_square"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*Apply_Method ("PolyEq", "complete_square")*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"-8 - 2 * x + x \ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"-8 + (2 / 2 - x) \ 2 = (2 / 2) \ 2", nxt = Rewrite("square_explicit1"*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"(2 / 2 - x) \ 2 = (2 / 2) \ 2 - -8" nxt = Rewrite("root_plus_minus*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) | + 2 / 2 - x = - sqrt ((2 / 2) \ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) | + - 1*x = - (2 / 2) + - sqrt ((2 / 2) \ 2 - -8)"nxt = R_Inst("bdv_explt2"*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) | + - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))"nxt = bdv_explicit3*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) | + x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))" nxt = bdv_explicit3*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \ 2 - -8)) | + x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))"nxt = calculate_Rational + NOT IMPLEMENTED SINCE 2002 ------------------------------ \ \ \ \ \ \ *) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"x = - 2 | x = 4" nxt = Or_to_List*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"[x = - 2, x = 4]" nxt = Check_Postcond*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; +(* FIXXXME + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO + | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]"; +*) +if f2str f = + "[x = - 1 * - 1 + - 1 * sqrt (2 \ 2 / 2 \ 2 - - 8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - - 8))]" +(*"[x = - 1 * - 1 + - 1 * sqrt (1 \ 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \ 2 - -8))]"*) +then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]"; + + +"----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; +"----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; +"----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; +(*stopped due to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat +see --- val rls = calculate_RootRat > calculate_Rational ---*) +val thy = @{theory PolyEq}; +val ctxt = Proof_Context.init_global thy; +val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")]; +val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \ 2 = (0::real)"; + +val rls = complete_square; +val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t; +if UnparseC.term t = "- 8 + (2 / 2 - x) \ 2 = (2 / 2) \ 2" +then () else error "rls complete_square CHANGED"; + +val thm = @{thm square_explicit1}; +val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t; +if UnparseC.term t = "(2 / 2 - x) \ 2 = (2 / 2) \ 2 - - 8" +then () else error "thm square_explicit1 CHANGED"; + +val thm = @{thm root_plus_minus}; +val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t; +if UnparseC.term t = +"2 / 2 - x = sqrt ((2 / 2) \ 2 - - 8) \\n2 / 2 - x = - 1 * sqrt ((2 / 2) \ 2 - - 8)" +then () else error "thm root_plus_minus CHANGED"; + +(*the thm bdv_explicit2* here required to be constrained to ::real*) +val thm = @{thm bdv_explicit2}; +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; +if UnparseC.term t = +"2 / 2 - x = sqrt ((2 / 2) \ 2 - - 8) \\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - - 8)" +then () else error "thm bdv_explicit2 CHANGED"; + +val thm = @{thm bdv_explicit3}; +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; +if UnparseC.term t = +"2 / 2 - x = sqrt ((2 / 2) \ 2 - - 8) \\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - - 8))" +then () else error "thm bdv_explicit3 CHANGED"; + +val thm = @{thm bdv_explicit2}; +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; +if UnparseC.term t = +"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - - 8) \\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - - 8))" +then () else error "thm bdv_explicit2 CHANGED"; + +val rls = calculate_RootRat; +val SOME (t,asm) = rewrite_set_ thy true rls t; +if UnparseC.term t = + "- 1 * x = - 1 + sqrt (2 \ 2 / 2 \ 2 - - 8) \\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - - 8))" +(*"- 1 * x = - 1 + sqrt (2 \ 2 / 2 \ 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - -8))"..isabisac15*) +then () else error "(-8 - 2*x + x \ 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT"; +(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*) + + +"-------------------- (3 - 10*x + 3*x \ 2 = 0), ----------------------"; +"-------------------- (3 - 10*x + 3*x \ 2 = 0), ----------------------"; +"-------------------- (3 - 10*x + 3*x \ 2 = 0), ----------------------"; +"---- test the erls ----"; + val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \ 2 - 1"; + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1; + val t' = UnparseC.term t; + (*if t'= \<^const_name>\True\ then () + else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*) +(* *) + val fmz = ["equality (3 - 10*x + 3*x \ 2 = 0)", + "solveFor x", "solutions L"]; + val (dI',pI',mI') = + ("PolyEq",["degree_2", "expanded", "univariate", "equation"], + ["PolyEq", "complete_square"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*Apply_Method ("PolyEq", "complete_square")*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; + +"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; +"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; +"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; + val fmz = ["equality (- 16 + 4*x + 2*x \ 2 = 0)", + "solveFor x", "solutions L"]; + val (dI',pI',mI') = + ("PolyEq",["degree_2", "expanded", "univariate", "equation"], + ["PolyEq", "complete_square"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*Apply_Method ("PolyEq", "complete_square")*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(* FIXXXXME n1., + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO + | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]"; +*) + \ ML \ \ ML \ \