1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Mon Sep 27 13:17:52 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Mon Sep 27 20:24:24 2021 +0200
1.3 @@ -56,10 +56,11 @@
1.4 apply (simp_all add: realpow_def even_real_def odd_real_def inv_real_eq)
1.5 by (simp add: powr_minus_divide)
1.6
1.7 - ML_file termC.sml
1.8 - ML_file substitution.sml
1.9 - ML_file contextC.sml
1.10 - ML_file environment.sml
1.11 +ML_file termC.sml
1.12 +ML_file substitution.sml
1.13 +ML_file contextC.sml
1.14 +ML_file environment.sml
1.15 +
1.16
1.17 ML \<open>
1.18 \<close> ML \<open>
2.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Sep 27 13:17:52 2021 +0200
2.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Sep 27 20:24:24 2021 +0200
2.3 @@ -207,22 +207,22 @@
2.4 d2_abcformula6_neg:
2.5 "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv \<up> 2=0) = False" and
2.6 d2_abcformula7:
2.7 - "[|0<=b \<up> 2 - 0|] ==> ( b*bdv+a*bdv \<up> 2=0) =
2.8 + " ( b*bdv+a*bdv \<up> 2=0) =
2.9 ((bdv=( -b + sqrt(b \<up> 2 - 0))/(2*a))
2.10 | (bdv=( -b - sqrt(b \<up> 2 - 0))/(2*a)))" and
2.11 (* d2_abcformula7_neg not need b^2 never less zero in R *)
2.12 d2_abcformula8:
2.13 - "[|0<=b \<up> 2 - 0|] ==> ( b*bdv+ bdv \<up> 2=0) =
2.14 + " ( b*bdv+ bdv \<up> 2=0) =
2.15 ((bdv=( -b + sqrt(b \<up> 2 - 0))/(2*1))
2.16 | (bdv=( -b - sqrt(b \<up> 2 - 0))/(2*1)))" and
2.17 (* d2_abcformula8_neg not need b^2 never less zero in R *)
2.18 d2_abcformula9:
2.19 - "[|0<=1 - 0|] ==> ( bdv+a*bdv \<up> 2=0) =
2.20 + " ( bdv+a*bdv \<up> 2=0) =
2.21 ((bdv=( -1 + sqrt(1 - 0))/(2*a))
2.22 | (bdv=( -1 - sqrt(1 - 0))/(2*a)))" and
2.23 (* d2_abcformula9_neg not need, because 1<0 ==> False*)
2.24 d2_abcformula10:
2.25 - "[|0<=1 - 0|] ==> ( bdv+ bdv \<up> 2=0) =
2.26 + " ( bdv+ bdv \<up> 2=0) =
2.27 ((bdv=( -1 + sqrt(1 - 0))/(2*1))
2.28 | (bdv=( -1 - sqrt(1 - 0))/(2*1)))" and
2.29 (* d2_abcformula10_neg not need, because 1<0 ==> False*)
3.1 --- a/src/Tools/isac/ProgLang/Calculate.thy Mon Sep 27 13:17:52 2021 +0200
3.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy Mon Sep 27 20:24:24 2021 +0200
3.3 @@ -38,62 +38,6 @@
3.4 val rhs = Thm.term_of (Thm.rhs_of eq);
3.5 in rhs end;
3.6
3.7 -\<close> ML \<open> (* \<longrightarrow> test/../base-definitions.sml NEW FILE *)
3.8 -"----------- note on new realpow ------- -------------------------------------------------------";
3.9 -"----------- note on new realpow ------- -------------------------------------------------------";
3.10 -"----------- note on new realpow ------- -------------------------------------------------------";
3.11 -
3.12 -(* this and other numeral calculations have been accomplished by Simplifier.rewrite so far *)
3.13 -
3.14 -val t = calcul @{theory} @{term "4 * - 1 * 4 ::real"};
3.15 -if UnparseC.term_in_ctxt @{context} t = "- 16"
3.16 -then () else error "calcul 4 * - 1 * 4 \<longrightarrow> - 16";
3.17 -
3.18 -(*
3.19 - guess: simp_ctxt is not sufficient for simplifying the conditions in the definition -- RIGHT.
3.20 - note: missing cases, defined in lemma realpow_uminus_simps, go via [simp] into simp_ctxt.
3.21 -*)
3.22 -val t = calcul @{theory} @{term "4 \<up> 2 ::real"};
3.23 -if UnparseC.term_in_ctxt @{context} t = "16"
3.24 -then () else error "calcul 4 \<up> 2 \<longrightarrow> 16";
3.25 -
3.26 -val t = calcul @{theory} @{term "(- 1) \<up> 2"};
3.27 -if UnparseC.term_in_ctxt @{context} t = "1"
3.28 -then () else error "calcul (- 1) \<up> 2 \<longrightarrow> 1";
3.29 -
3.30 -val t = calcul @{theory} @{term "3 \<up> (- 2)"};
3.31 -if UnparseC.term_in_ctxt @{context} t = "1 / 9"
3.32 -then () else error "calcul 3 \<up> (- 2) \<longrightarrow> 1 / 9";
3.33 -
3.34 -\<close> ML \<open>
3.35 -val t = calcul @{theory} @{term "3 \<up> - 1"};
3.36 -if UnparseC.term_in_ctxt @{context} t = "1 / 3"
3.37 -then () else error "calcul 3 \<up> - 1 \<longrightarrow> 1 / 3";
3.38 -\<close> ML \<open>
3.39 -
3.40 -(* note on example "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" *)
3.41 -(*
3.42 - fun calcul should simplify both sides of the inequality.
3.43 - Afterwards the inequality - 64 \<le> 8 should evaluate to True.
3.44 -
3.45 - But we get the error:
3.46 - rew_once:
3.47 - Eval.get_pair for "BaseDefinitions.realpow" \<longrightarrow> SOME (_, "4 \<up> 2 = 4 \<up> 2")
3.48 - but rewrite__ on "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" \<longrightarrow> NONE
3.49 -
3.50 - The error occurs while rewriting and expecting \<longrightarrow> SOME (_, "4 \<up> 2 = 16");
3.51 - the rewriter takes the rhs 4 \<up> 2, the same as the lhs,
3.52 - and assumes to be able to simplify, but we have lhs = rhs \<longrightarrow> NONE,
3.53 - which is recognised by the rewriter as an error.
3.54 -
3.55 - Eval.get_pair ensures, that only pairs of numerals are passed to fun calcul,
3.56 - such that single-stepping is realised, although Simplifier.rewrite could do all at once.
3.57 -
3.58 - \<le> is a binary operator, too, but has another signature as algebraic operations.
3.59 - So \<le> is handled separately and not by fun calcul.
3.60 -*)
3.61 -\<close> ML \<open>
3.62 -
3.63 fun eval_binop (_: string) (_: string) t thy =
3.64 (case t of
3.65 (opp as Const (c1, T)) $ (Const (c2, _) $ v $ t1) $ t2 => (* binary \<circ> (v \<circ> n1) \<circ> n2 *)
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/test/Tools/isac/BaseDefinitions/base-definitions.sml Mon Sep 27 20:24:24 2021 +0200
4.3 @@ -0,0 +1,64 @@
4.4 +(* Title: "Interpret/lucas-interpreter.sml"
4.5 + Author: Walther Neuper
4.6 + (c) due to copyright terms
4.7 +*)
4.8 +
4.9 +"-----------------------------------------------------------------------------------------------";
4.10 +"table of contents -----------------------------------------------------------------------------";
4.11 +"-----------------------------------------------------------------------------------------------";
4.12 +"----------- note on new realpow ------- -------------------------------------------------------";
4.13 +"-----------------------------------------------------------------------------------------------";
4.14 +"-----------------------------------------------------------------------------------------------";
4.15 +"-----------------------------------------------------------------------------------------------";
4.16 +
4.17 +"----------- note on new realpow ------- -------------------------------------------------------";
4.18 +"----------- note on new realpow ------- -------------------------------------------------------";
4.19 +"----------- note on new realpow ------- -------------------------------------------------------";
4.20 +
4.21 +(* these and other numeral calculations have been accomplished by Simplifier.rewrite so far *)
4.22 +
4.23 +val t = calcul @{theory} @{term "4 * - 1 * 4 ::real"};
4.24 +if UnparseC.term_in_ctxt @{context} t = "- 16"
4.25 +then () else error "calcul 4 * - 1 * 4 \<longrightarrow> - 16";
4.26 +
4.27 +(*
4.28 + guess: simp_ctxt is not sufficient for simplifying the conditions in the definition -- RIGHT.
4.29 + note: missing cases, defined in lemma realpow_uminus_simps, go via [simp] into simp_ctxt.
4.30 +*)
4.31 +val t = calcul @{theory} @{term "4 \<up> 2 ::real"};
4.32 +if UnparseC.term_in_ctxt @{context} t = "16"
4.33 +then () else error "calcul 4 \<up> 2 \<longrightarrow> 16";
4.34 +
4.35 +val t = calcul @{theory} @{term "(- 1) \<up> 2"};
4.36 +if UnparseC.term_in_ctxt @{context} t = "1"
4.37 +then () else error "calcul (- 1) \<up> 2 \<longrightarrow> 1";
4.38 +
4.39 +val t = calcul @{theory} @{term "3 \<up> (- 2)"};
4.40 +if UnparseC.term_in_ctxt @{context} t = "1 / 9"
4.41 +then () else error "calcul 3 \<up> (- 2) \<longrightarrow> 1 / 9";
4.42 +
4.43 +val t = calcul @{theory} @{term "3 \<up> - 1"};
4.44 +if UnparseC.term_in_ctxt @{context} t = "1 / 3"
4.45 +then () else error "calcul 3 \<up> - 1 \<longrightarrow> 1 / 3";
4.46 +
4.47 +(* note on example "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" *)
4.48 +(*
4.49 + fun calcul should simplify both sides of the inequality.
4.50 + Afterwards the inequality - 64 \<le> 8 should evaluate to True.
4.51 +
4.52 + But we get the error:
4.53 + rew_once:
4.54 + Eval.get_pair for "BaseDefinitions.realpow" \<longrightarrow> SOME (_, "4 \<up> 2 = 4 \<up> 2")
4.55 + but rewrite__ on "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" \<longrightarrow> NONE
4.56 +
4.57 + The error occurs while rewriting and expecting \<longrightarrow> SOME (_, "4 \<up> 2 = 16");
4.58 + the rewriter takes the rhs 4 \<up> 2, the same as the lhs,
4.59 + and assumes to be able to simplify, but we have lhs = rhs \<longrightarrow> NONE,
4.60 + which is recognised by the rewriter as an error.
4.61 +
4.62 + Eval.get_pair ensures, that only pairs of numerals are passed to fun calcul,
4.63 + such that single-stepping is realised, although Simplifier.rewrite could do all at once.
4.64 +
4.65 + \<le> is a binary operator, too, but has another signature as algebraic operations.
4.66 + So \<le> is handled separately and not by fun calcul.
4.67 +*)
5.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Mon Sep 27 13:17:52 2021 +0200
5.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Mon Sep 27 20:24:24 2021 +0200
5.3 @@ -32,7 +32,9 @@
5.4
5.5 val ((pt, p),_) = get_calc 1;
5.6 if p = ([], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term) =
5.7 - "[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 * EI + - 24 * L * c_3 * EI + 12 * L \<up> 2 * c_2 +\n 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n (- 24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
5.8 + "[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
5.9 +(*"[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 * EI + - 24 * L * c_3 * EI + 12 * L \<up> 2 * c_2 +\n 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n (- 24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
5.10 + ^^^ BEFORE fun calcul IS EVALUATEDO BY Simplifier.rewrite *)
5.11 then () else error "auto method [Biegelinien,setzeRandbedingungenEin] changed";
5.12
5.13
5.14 @@ -56,7 +58,7 @@
5.15
5.16 "--- before 1.subpbl [Equation, fromFunction]";
5.17 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.18 -case nxt of (_, Apply_Method ["Biegelinien", "setzeRandbedingungenEin"])=>()
5.19 +case nxt of Apply_Method ["Biegelinien", "setzeRandbedingungenEin"] => ()
5.20 | _ => error "biegelinie.sml: met setzeRandbed*Ein aa";
5.21 "----- Randbedingung y 0 = 0 in SUBpbl with met [Equation, fromFunction]";
5.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.23 @@ -72,18 +74,19 @@
5.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.25 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.26 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.27 -case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
5.28 +case nxt of Apply_Method["Equation", "fromFunction"] => ()
5.29 | _ => error "biegelinie.sml met2 ff";
5.30 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.31 "y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";
5.32 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.33 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.34 -case nxt of (_, Check_Postcond ["makeFunctionTo", "equation"]) => ()
5.35 +case nxt of Check_Postcond ["makeFunctionTo", "equation"] => ()
5.36 | _ => error "biegelinie.sml met2 gg";
5.37
5.38 +(*========== inhibit exn WN210927 exception size SINCE BEFORE fun calcul WITH Simplifier.rewrite
5.39 "--- before 2.subpbl [Equation, fromFunction]";
5.40 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (- 1 * EI)" ;
5.41 -case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
5.42 +case nxt of Subproblem (_, ["makeFunctionTo", "equation"]) => ()
5.43 | _ => error "biegelinie.sml met2 hh";
5.44 "--- after 1st arrival at 2.subpbl [Equation, fromFunction]";
5.45
5.46 @@ -96,28 +99,35 @@
5.47 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.48 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.49 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.50 -case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
5.51 +case nxt of Apply_Method["Equation", "fromFunction"] => ()
5.52 | _ => error "biegelinie.sml met2 ii";
5.53 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";
5.54 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "y L =\nc_4 + c_3 * L +\n1 / (- 1 * EI) *\n(c_2 / 2 * L \<up> 2 + c / 6 * L \<up> 3 + - 1 * q_0 / 24 * L \<up> 4)";
5.55 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + c_3 * L +\n1 / (- 1 * EI) *\n(c_2 / 2 * L \<up> 2 + c / 6 * L \<up> 3 + - 1 * q_0 / 24 * L \<up> 4)";
5.56 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + L * c_3 +\n(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI)" ;
5.57 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + L * c_3 +\n(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI)";
5.58 -case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
5.59 +case nxt of Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]) => ()
5.60 | _ => error "biegelinie.sml met2 jj";
5.61 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.62 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.63 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.64 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.65 -case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
5.66 +case nxt of Apply_Method ["Equation", "fromFunction"] => ()
5.67 | _ => error "biegelinie.sml met2 kk";
5.68
5.69 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"(*true*);
5.70 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * 0 + - 1 * q_0 / 2 * 0 \<up> 2";
5.71 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.72 +if f2str f = "0 = - 1 * c_4 / - 1"
5.73 + (*"M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2" BEFORE fun calcul WITH Simplifier.rewrite*)
5.74 +then () else error "Method fromFunction CHANGED 1";
5.75 +
5.76 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.77 +val Test_Out.PpcKF (Test_Out.Problem [], {Find = [], Given = [], Relate = [],
5.78 + Where = [], With = []}) = f;
5.79 +( *========== inhibit exn WN210927 BEFORE fun calcul WITH Simplifier.rewrite ========
5.80 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
5.81 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
5.82 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.83 -(*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
5.84 +( *========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
5.85
5.86 case nxt of (_, Subproblem (_, ["makeFunctionTo", "equation"])) => ()
5.87 | _ => error "biegelinie.sml met2 ll";
6.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Sep 27 13:17:52 2021 +0200
6.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Sep 27 20:24:24 2021 +0200
6.3 @@ -175,6 +175,7 @@
6.4 section \<open>test ML Code of isac\<close>
6.5 subsection \<open>basic code first\<close>
6.6 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
6.7 + ML_file "BaseDefinitions/base-definitions.sml"
6.8 ML_file "BaseDefinitions/libraryC.sml"
6.9 ML_file "BaseDefinitions/rule-def.sml"
6.10 ML_file "BaseDefinitions/eval-def.sml"
6.11 @@ -293,18 +294,6 @@
6.12 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
6.13 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
6.14 ML_file "Knowledge/polyeq-1.sml"
6.15 -ML \<open>
6.16 -\<close> ML \<open>
6.17 -\<close> ML \<open>
6.18 -\<close> ML \<open>
6.19 -\<close> ML \<open>
6.20 -\<close> ML \<open>
6.21 -\<close> ML \<open>
6.22 -\<close> ML \<open>
6.23 -\<close> ML \<open>
6.24 -\<close> ML \<open>
6.25 -\<close> ML \<open>
6.26 -\<close>
6.27 (*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*)
6.28 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
6.29 ML_file "Knowledge/calculus.sml"
7.1 --- a/test/Tools/isac/Test_Some.thy Mon Sep 27 13:17:52 2021 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Mon Sep 27 20:24:24 2021 +0200
7.3 @@ -104,1207 +104,13 @@
7.4 \<close> ML \<open>
7.5 \<close>
7.6
7.7 -section \<open>====== comment simplification of numerals =========================================\<close>
7.8 +section \<open>===================================================================================\<close>
7.9 ML \<open>
7.10 -\<close> ML \<open> (* \<longrightarrow> test/../base-definitions.sml NEW FILE *)
7.11 -"----------- note on new realpow ------- -------------------------------------------------------";
7.12 -"----------- note on new realpow ------- -------------------------------------------------------";
7.13 -"----------- note on new realpow ------- -------------------------------------------------------";
7.14 -
7.15 -(* this and other numeral calculations have been accomplished by Simplifier.rewrite so far *)
7.16 -
7.17 -val t = calcul @{theory} @{term "4 * - 1 * 4 ::real"};
7.18 -if UnparseC.term_in_ctxt @{context} t = "- 16"
7.19 -then () else error "calcul 4 * - 1 * 4 \<longrightarrow> - 16";
7.20 \<close> ML \<open>
7.21 -
7.22 -(* guess: simp_ctxt is not sufficient for simplifying the conditions in the definition *)
7.23 -(*
7.24 - if-then-else \<and> < \<ge> even_real odd_real are possible reasons for insufficiency.
7.25 -*)
7.26 -val t = calcul @{theory} @{term "4 \<up> 2 ::real"};
7.27 -if UnparseC.term_in_ctxt @{context} t = "16"
7.28 -then () else error "calcul 4 \<up> 2 \<longrightarrow> 16";
7.29 \<close> ML \<open>
7.30 -val t = calcul @{theory} @{term "(- 1) \<up> 2"};
7.31 -if UnparseC.term_in_ctxt @{context} t = "1"
7.32 -then () else error "calcul (- 1) \<up> 2 \<longrightarrow> 1";
7.33 -
7.34 -(* note on example "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" *)
7.35 -(*
7.36 - fun calcul should simplify both sides of the inequality.
7.37 - Afterwards the inequality - 64 \<le> 8 should evaluate to True.
7.38 -
7.39 - But we get the error:
7.40 - rew_once:
7.41 - Eval.get_pair for "BaseDefinitions.realpow" \<longrightarrow> SOME (_, "4 \<up> 2 = 4 \<up> 2")
7.42 - but rewrite__ on "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" \<longrightarrow> NONE
7.43 -
7.44 - The error occurs while rewriting and expecting \<longrightarrow> SOME (_, "4 \<up> 2 = 16");
7.45 - the rewriter takes the rhs 4 \<up> 2, the same as the lhs,
7.46 - and assumes to be able to simplify, but we have lhs = rhs \<longrightarrow> NONE,
7.47 - which is recognised by the rewriter as an error.
7.48 -
7.49 - Eval.get_pair ensures, that only pairs of numerals are passed to fun calcul,
7.50 - such that single-stepping is realised, although Simplifier.rewrite could do all at once.
7.51 -
7.52 - \<le> is a binary operator, too, but has another signature as algebraic operations.
7.53 - So \<le> is handled separately and not by fun calcul.
7.54 -*)
7.55 \<close> ML \<open>
7.56 \<close>
7.57
7.58 -section \<open>====== check Knowledge/polyeq-1.sml ===============================================\<close>
7.59 -ML \<open>
7.60 -\<close> ML \<open>
7.61 -(* Title: Knowledge/polyeq-1.sml
7.62 - testexamples for PolyEq, poynomial equations and equational systems
7.63 - Author: Richard Lang 2003
7.64 - (c) due to copyright terms
7.65 -
7.66 -Separation into polyeq-1.sml and polyeq-1a.sml due to
7.67 -*)
7.68 -
7.69 -"-----------------------------------------------------------------";
7.70 -"table of contents -----------------------------------------------";
7.71 -"-----------------------------------------------------------------";
7.72 -"------ polyeq-1.sml ---------------------------------------------";
7.73 -"----------- tests on predicates in problems ---------------------";
7.74 -"----------- test matching problems ------------------------------";
7.75 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
7.76 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
7.77 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
7.78 -"----------- lin.eq degree_0 -------------------------------------";
7.79 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
7.80 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
7.81 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
7.82 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
7.83 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
7.84 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
7.85 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
7.86 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
7.87 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
7.88 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
7.89 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
7.90 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
7.91 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
7.92 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
7.93 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
7.94 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.95 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
7.96 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
7.97 -"-----------------------------------------------------------------";
7.98 -"------ polyeq-2.sml ---------------------------------------------";
7.99 -"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
7.100 -"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
7.101 -"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
7.102 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
7.103 -"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
7.104 -"----------- rls make_polynomial_in ------------------------------";
7.105 -"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
7.106 -"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
7.107 -"-----------------------------------------------------------------";
7.108 -"-----------------------------------------------------------------";
7.109 -
7.110 -\<close> ML \<open>
7.111 -Rewrite.trace_on := false (*false true*);
7.112 -"----------- tests on predicates in problems ---------------------";
7.113 -"----------- tests on predicates in problems ---------------------";
7.114 -"----------- tests on predicates in problems ---------------------";
7.115 -val thy = @{theory};
7.116 -Rewrite.trace_on:=false; (*true false*)
7.117 -
7.118 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
7.119 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
7.120 - if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
7.121 - else error "polyeq.sml: diff.behav. in lhs";
7.122 -
7.123 -\<close> ML \<open>
7.124 - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
7.125 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
7.126 - if (UnparseC.term t) = "True" then ()
7.127 - else error "polyeq.sml: diff.behav. 1 in is_expended_in";
7.128 -
7.129 - val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
7.130 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
7.131 - if (UnparseC.term t) = "False" then ()
7.132 - else error "polyeq.sml: diff.behav. 2 in is_poly_in";
7.133 -
7.134 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
7.135 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
7.136 - if (UnparseC.term t) = "True" then ()
7.137 - else error "polyeq.sml: diff.behav. 3 in is_poly_in";
7.138 -
7.139 - 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.140 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
7.141 - if (UnparseC.term t) = "True" then ()
7.142 - else error "polyeq.sml: diff.behav. 4 in is_expended_in";
7.143 -
7.144 - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
7.145 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
7.146 - if (UnparseC.term t) = "True" then ()
7.147 - else error "polyeq.sml: diff.behav. 5 in is_expended_in";
7.148 -
7.149 - val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
7.150 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
7.151 - if (UnparseC.term t) = "True" then ()
7.152 - else error "polyeq.sml: diff.behav. in has_degree_in_in";
7.153 -
7.154 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
7.155 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
7.156 - if (UnparseC.term t) = "False" then ()
7.157 - else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
7.158 -
7.159 - val t4 = (Thm.term_of o the o (TermC.parse thy))
7.160 - "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
7.161 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
7.162 - if (UnparseC.term t) = "False" then ()
7.163 - else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
7.164 -
7.165 -val t5 = (Thm.term_of o the o (TermC.parse thy))
7.166 - "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
7.167 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
7.168 - if (UnparseC.term t) = "True" then ()
7.169 - else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
7.170 -
7.171 -\<close> ML \<open>
7.172 -"----------- test matching problems --------------------------0---";
7.173 -"----------- test matching problems --------------------------0---";
7.174 -"----------- test matching problems --------------------------0---";
7.175 -val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.176 -if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
7.177 - M_Match.Matches' {Find = [Correct "solutions L"],
7.178 - With = [],
7.179 - Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
7.180 - Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
7.181 - Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
7.182 - Relate = []}
7.183 -then () else error "M_Match.match_pbl [expanded,univariate,equation]";
7.184 -
7.185 -if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
7.186 - M_Match.Matches' {Find = [Correct "solutions L"],
7.187 - With = [],
7.188 - Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
7.189 - Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
7.190 - Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
7.191 -then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
7.192 -
7.193 -
7.194 -\<close> ML \<open>
7.195 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
7.196 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
7.197 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
7.198 -(*##################################################################################
7.199 ------------ 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
7.200 -
7.201 - (*Aufgabe zum Einstieg in die Arbeit...*)
7.202 - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
7.203 - (*ein 'ruleset' aus Poly.ML wird angewandt...*)
7.204 - val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
7.205 - UnparseC.term t;
7.206 - "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
7.207 - val SOME (t,_) =
7.208 - rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
7.209 - UnparseC.term t;
7.210 - "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
7.211 -(* bei Verwendung von "size_of-term" nach MG :*)
7.212 -(*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
7.213 -
7.214 - (*wir holen 'a' wieder aus der Klammerung heraus...*)
7.215 - val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
7.216 - UnparseC.term t;
7.217 - "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
7.218 -(* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
7.219 -
7.220 - val SOME (t,_) =
7.221 - rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
7.222 - UnparseC.term t;
7.223 - "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
7.224 - (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
7.225 - "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
7.226 -
7.227 - (*das rewriting l"asst sich beobachten mit
7.228 -Rewrite.trace_on := false; (*true false*)
7.229 - *)
7.230 -
7.231 -"------ 15.11.02 --------------------------";
7.232 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
7.233 - val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
7.234 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
7.235 -
7.236 -Rewrite.trace_on := false; (*true false*)
7.237 - (* Anwenden einer Regelmenge aus Termorder.ML: *)
7.238 - val SOME (t,_) =
7.239 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
7.240 - UnparseC.term t;
7.241 - val SOME (t,_) =
7.242 - rewrite_set_ thy false discard_parentheses t;
7.243 - UnparseC.term t;
7.244 -"1 + b * x + x * a";
7.245 -
7.246 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
7.247 - val SOME (t,_) =
7.248 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
7.249 - UnparseC.term t;
7.250 - val SOME (t,_) =
7.251 - rewrite_set_ thy false discard_parentheses t;
7.252 - UnparseC.term t;
7.253 -"1 + (x + b * x) * a + a \<up> 2";
7.254 -
7.255 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
7.256 - val SOME (t,_) =
7.257 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
7.258 - UnparseC.term t;
7.259 - val SOME (t,_) =
7.260 - rewrite_set_ thy false discard_parentheses t;
7.261 - UnparseC.term t;
7.262 -"1 + b * a + (7 + x) * a \<up> 2";
7.263 -
7.264 -(* MG2003
7.265 - Prog_Expr.thy grundlegende Algebra
7.266 - Poly.thy Polynome
7.267 - Rational.thy Br"uche
7.268 - Root.thy Wurzeln
7.269 - RootRat.thy Wurzen + Br"uche
7.270 - Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
7.271 -
7.272 - get_thm Termorder.thy "bdv_n_collect";
7.273 - get_thm (theory "Isac_Knowledge") "bdv_n_collect";
7.274 -*)
7.275 - val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
7.276 - val SOME (t,_) =
7.277 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
7.278 - UnparseC.term t;
7.279 - val SOME (t,_) =
7.280 - rewrite_set_ thy false discard_parentheses t;
7.281 - UnparseC.term t;
7.282 -"(7 + x) * a \<up> 2";
7.283 -
7.284 - val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
7.285 -
7.286 - val t = (Thm.term_of o the o (parseold thy)) "7";
7.287 -##################################################################################*)
7.288 -
7.289 -
7.290 -\<close> ML \<open>
7.291 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
7.292 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
7.293 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
7.294 -(* termorder hacked by MG, adapted later by WN *)
7.295 -(** )local ( *. for make_polynomial_in .*)
7.296 -
7.297 -open Term; (* for type order = EQUAL | LESS | GREATER *)
7.298 -
7.299 -fun pr_ord EQUAL = "EQUAL"
7.300 - | pr_ord LESS = "LESS"
7.301 - | pr_ord GREATER = "GREATER";
7.302 -
7.303 -fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
7.304 - | dest_hd' x (t as Free (a, T)) =
7.305 - if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
7.306 - else (((a, 0), T), 1)
7.307 - | dest_hd' _ (Var v) = (v, 2)
7.308 - | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
7.309 - | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
7.310 - | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
7.311 -
7.312 -fun size_of_term' i pr x (t as Const (\<^const_name>\<open>realpow\<close>, _) $
7.313 - Free (var, _) $ Free (pot, _)) =
7.314 - (if pr then tracing (idt "#" i ^ "size_of_term' realpow: " ^ UnparseC.term t) else ();
7.315 - case x of (*WN*)
7.316 - (Free (xstr, _)) =>
7.317 - if xstr = var
7.318 - then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
7.319 - 1000 * (the (TermC.int_opt_of_string pot)))
7.320 - else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
7.321 - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
7.322 - | size_of_term' i pr x (t as Abs (_, _, body)) =
7.323 - (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
7.324 - 1 + size_of_term' (i + 1) pr x body)
7.325 - | size_of_term' i pr x (f $ t) =
7.326 - let
7.327 - val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
7.328 - val s1 = size_of_term' (i + 1) pr x f
7.329 - val s2 = size_of_term' (i + 1) pr x t
7.330 - 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.331 - in (s1 + s2) end
7.332 - | size_of_term' i pr x t =
7.333 - (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
7.334 - case t of
7.335 - Free (subst, _) =>
7.336 - (case x of
7.337 - Free (xstr, _) =>
7.338 - if xstr = subst
7.339 - then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
7.340 - else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
7.341 - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
7.342 - | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
7.343 -
7.344 -fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
7.345 - let
7.346 - val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
7.347 - val ord =
7.348 - case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
7.349 - val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
7.350 - in ord end
7.351 - | term_ord' i pr x _ (t, u) =
7.352 - let
7.353 - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
7.354 - val ord =
7.355 - case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
7.356 - EQUAL =>
7.357 - let val (f, ts) = strip_comb t and (g, us) = strip_comb u
7.358 - in
7.359 - (case hd_ord (i + 1) pr x (f, g) of
7.360 - EQUAL => (terms_ord x (i + 1) pr) (ts, us)
7.361 - | ord => ord)
7.362 - end
7.363 - | ord => ord
7.364 - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
7.365 - in ord end
7.366 -and hd_ord i pr x (f, g) = (* ~ term.ML *)
7.367 - let
7.368 - val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
7.369 - val ord = prod_ord
7.370 - (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
7.371 - (dest_hd' x f, dest_hd' x g)
7.372 - val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
7.373 - in ord end
7.374 -and terms_ord x i pr (ts, us) =
7.375 - let
7.376 - val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
7.377 - val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
7.378 - val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
7.379 - in ord end
7.380 -
7.381 -(** )in( *local*)
7.382 -
7.383 -fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
7.384 - ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
7.385 - case subst of
7.386 - (_, x) :: _ =>
7.387 - term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
7.388 - | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
7.389 -
7.390 -(** )end;( *local*)
7.391 -
7.392 -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
7.393 -if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then () else error "still GREATER?";
7.394 -
7.395 -val x = TermC.str2term "x ::real";
7.396 -
7.397 -val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
7.398 -if 2006 = size_of_term' 1 false(*true*) x t1
7.399 -then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
7.400 -
7.401 -val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
7.402 -if 3004 = size_of_term' 1 false(*true*) x t2
7.403 -then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
7.404 -
7.405 -
7.406 -\<close> ML \<open>
7.407 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
7.408 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
7.409 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
7.410 - val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
7.411 - val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
7.412 - val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
7.413 -
7.414 - val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
7.415 - val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
7.416 - val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
7.417 - val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
7.418 -
7.419 -if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then ()
7.420 -else error "termorder.sml diff.behav ord_make_polynomial_in #1";
7.421 -
7.422 -if ord_make_polynomial_in false(*true*) thy substa (x1,x2) = true(*LESS *) then ()
7.423 -else error "termorder.sml diff.behav ord_make_polynomial_in #2";
7.424 -
7.425 -if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then ()
7.426 -else error "termorder.sml diff.behav ord_make_polynomial_in #3";
7.427 -
7.428 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
7.429 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
7.430 - ord_make_polynomial_in false(*true*) thy substx (aa, bb);
7.431 - true; (* => LESS *)
7.432 -
7.433 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
7.434 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
7.435 - ord_make_polynomial_in false(*true*) thy substa (aa, bb);
7.436 - false; (* => GREATER *)
7.437 -
7.438 -(* und nach dem Re-engineering der Termorders in den 'rulesets'
7.439 - kannst Du die 'gr"osste' Variable frei w"ahlen: *)
7.440 - val bdv= TermC.str2term "bdv ::real";
7.441 - val x = TermC.str2term "x ::real";
7.442 - val a = TermC.str2term "a ::real";
7.443 - val b = TermC.str2term "b ::real";
7.444 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
7.445 -if UnparseC.term t' = "b + x + a" then ()
7.446 -else error "termorder.sml diff.behav ord_make_polynomial_in #11";
7.447 -
7.448 -val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
7.449 -
7.450 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
7.451 -if UnparseC.term t' = "a + b + x" then ()
7.452 -else error "termorder.sml diff.behav ord_make_polynomial_in #13";
7.453 -
7.454 - val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
7.455 - val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
7.456 -val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
7.457 -if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
7.458 -else error "termorder.sml diff.behav ord_make_polynomial_in #15";
7.459 -
7.460 - val ttt' = "(3*x + 5)/18 ::real";
7.461 - val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
7.462 -val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
7.463 -if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
7.464 -else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
7.465 -
7.466 -val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
7.467 -if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
7.468 -else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
7.469 -
7.470 -\<close> ML \<open>
7.471 -"----------- lin.eq degree_0 -------------------------------------";
7.472 -"----------- lin.eq degree_0 -------------------------------------";
7.473 -"----------- lin.eq degree_0 -------------------------------------";
7.474 -"----- d0_false ------";
7.475 -val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
7.476 -val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
7.477 - ["PolyEq", "solve_d0_polyeq_equation"]);
7.478 -(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
7.479 -TODO: change to "equality (x + - 1*x = (0::real))"
7.480 - and search for an appropriate problem and method.
7.481 -
7.482 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.483 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.484 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.485 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.486 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.487 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.488 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.489 -case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
7.490 - | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
7.491 -
7.492 -"----- d0_true ------";
7.493 -val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
7.494 -val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
7.495 - ["PolyEq", "solve_d0_polyeq_equation"]);
7.496 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.497 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.498 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.499 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.500 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.501 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.502 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.503 -case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
7.504 - | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
7.505 -============ inhibit exn WN110914 ============================================*)
7.506 -
7.507 -\<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)
7.508 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
7.509 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
7.510 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
7.511 -"----- d2_pqformula1 ------!!!!";
7.512 -val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
7.513 -val (dI',pI',mI') =
7.514 - ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
7.515 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.516 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.517 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.518 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.519 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.520 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.521 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.522 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
7.523 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.524 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.525 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.526 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.527 -
7.528 -(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
7.529 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
7.530 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.531 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.532 -
7.533 -if p = ([], Res) andalso
7.534 - f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
7.535 - case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
7.536 -else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
7.537 -
7.538 -\<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)
7.539 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
7.540 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
7.541 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
7.542 -"----- d2_pqformula1_neg ------";
7.543 -val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
7.544 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.545 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.546 -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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.549 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.550 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.551 -(*### or2list False
7.552 - ([1],Res) False Or_to_List)*)
7.553 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.554 -(*### or2list False
7.555 - ([2],Res) [] Check_elementwise "Assumptions"*)
7.556 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.557 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.558 -val asm = Ctree.get_assumptions pt p;
7.559 -if f2str f = "[]" andalso
7.560 - UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
7.561 - "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
7.562 -else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
7.563 -
7.564 -\<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)
7.565 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
7.566 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
7.567 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
7.568 -"----- d2_pqformula2 ------";
7.569 -val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.570 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.571 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.572 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.573 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.574 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.575 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.576 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.577 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.578 -
7.579 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.580 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.581 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.582 -case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
7.583 - | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
7.584 -
7.585 -
7.586 -\<close> ML \<open>
7.587 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
7.588 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
7.589 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
7.590 -"----- d2_pqformula3 ------";
7.591 -(*EP-9*)
7.592 -val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.593 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.594 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.595 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.596 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.597 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.598 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.599 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.600 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.601 -
7.602 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.603 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.604 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.605 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
7.606 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
7.607 -
7.608 -
7.609 -\<close> ML \<open>
7.610 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
7.611 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
7.612 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
7.613 -"----- d2_pqformula3_neg ------";
7.614 -val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.615 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.616 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.617 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.618 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.619 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.620 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.621 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.622 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.623 -
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;
7.626 -"TODO 2 + x + x \<up> 2 = 0";
7.627 -"TODO 2 + x + x \<up> 2 = 0";
7.628 -"TODO 2 + x + x \<up> 2 = 0";
7.629 -
7.630 -\<close> ML \<open>
7.631 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
7.632 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
7.633 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
7.634 -"----- d2_pqformula4 ------";
7.635 -val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.636 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.637 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.638 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.639 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.640 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.641 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.642 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.643 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.644 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
7.647 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
7.648 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
7.649 -
7.650 -\<close> ML \<open>
7.651 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
7.652 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
7.653 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
7.654 -"----- d2_pqformula5 ------";
7.655 -val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.656 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.657 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.658 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.659 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.660 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.661 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.662 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.663 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.664 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
7.667 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.668 - | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
7.669 -
7.670 -\<close> ML \<open>
7.671 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
7.672 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
7.673 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
7.674 -"----- d2_pqformula6 ------";
7.675 -val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.676 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.677 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.678 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.679 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.680 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.681 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.682 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.683 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.684 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
7.687 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.688 - | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
7.689 -
7.690 -\<close> ML \<open> (*=====calcul: rhs = (1::?'a) - (0::?'a) *)
7.691 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
7.692 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
7.693 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
7.694 -"----- d2_pqformula7 ------";
7.695 -(*EP- 10*)
7.696 -val fmz = ["equality ( x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
7.697 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.698 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.699 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.700 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.701 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.702 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.703 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.704 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.705 -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;
7.709 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.710 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
7.711 -
7.712 -
7.713 -\<close> ML \<open> (*=====calcul: rhs = (1::?'b) - (0::?'b) *)
7.714 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
7.715 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
7.716 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
7.717 -"----- d2_pqformula8 ------";
7.718 -val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.719 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.720 - ["PolyEq", "solve_d2_polyeq_pq_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 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.730 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.731 - | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
7.732 -
7.733 -\<close> ML \<open>
7.734 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
7.735 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
7.736 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
7.737 -"----- d2_pqformula9 ------";
7.738 -val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.739 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.740 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.741 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.742 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.743 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.748 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.749 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
7.750 - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
7.751 -
7.752 -
7.753 -\<close> ML \<open>
7.754 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
7.755 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
7.756 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
7.757 -"----- d2_pqformula9_neg ------";
7.758 -val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.759 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
7.760 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
7.761 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.762 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.763 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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;
7.768 -"TODO 4 + 1*x \<up> 2 = 0";
7.769 -"TODO 4 + 1*x \<up> 2 = 0";
7.770 -"TODO 4 + 1*x \<up> 2 = 0";
7.771 -
7.772 -\<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)
7.773 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
7.774 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
7.775 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
7.776 -val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.777 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.778 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.779 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.780 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.781 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.782 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 -case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
7.788 - | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
7.789 -
7.790 -\<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)
7.791 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
7.792 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
7.793 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
7.794 -val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.795 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.796 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.797 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.798 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.799 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 -
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 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
7.806 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
7.807 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
7.808 -
7.809 -
7.810 -\<close> ML \<open>
7.811 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
7.812 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
7.813 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
7.814 -(*EP- 11*)
7.815 -val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.816 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.817 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.818 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.819 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.820 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.821 -
7.822 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.823 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.824 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.825 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.826 -
7.827 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.828 -case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
7.829 - | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
7.830 -
7.831 -
7.832 -\<close> text \<open> (*=====calcul: rhs = (1::?'c) - (0::?'c) *)
7.833 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
7.834 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
7.835 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
7.836 -val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.837 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.838 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.839 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.840 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.841 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.842 -
7.843 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
7.848 -"TODO 1 + x + 2*x \<up> 2 = 0";
7.849 -"TODO 1 + x + 2*x \<up> 2 = 0";
7.850 -"TODO 1 + x + 2*x \<up> 2 = 0";
7.851 -
7.852 -
7.853 -val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.854 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.855 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.856 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.857 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.858 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.859 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
7.865 - | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
7.866 -
7.867 -val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.868 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.869 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.870 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.871 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.872 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.873 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
7.878 -"TODO 2 + 1*x + x \<up> 2 = 0";
7.879 -"TODO 2 + 1*x + x \<up> 2 = 0";
7.880 -"TODO 2 + 1*x + x \<up> 2 = 0";
7.881 -
7.882 -(*EP- 12*)
7.883 -val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.884 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.885 - ["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 = 1, x = - 2]" => ()
7.895 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
7.896 -
7.897 -val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.898 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.899 - ["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 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.908 -"TODO 2 + x + x \<up> 2 = 0";
7.909 -"TODO 2 + x + x \<up> 2 = 0";
7.910 -"TODO 2 + x + x \<up> 2 = 0";
7.911 -
7.912 -(*EP- 13*)
7.913 -val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.914 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.915 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.916 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.917 -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 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.924 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
7.925 - | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
7.926 -
7.927 -val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.928 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.929 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.930 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.931 -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 -"TODO 8+ 2*x \<up> 2 = 0";
7.938 -"TODO 8+ 2*x \<up> 2 = 0";
7.939 -"TODO 8+ 2*x \<up> 2 = 0";
7.940 -
7.941 -(*EP- 14*)
7.942 -val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.943 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.950 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.951 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.952 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
7.953 - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
7.954 -
7.955 -
7.956 -val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.957 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.958 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.959 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.960 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.961 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.962 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.963 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.964 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.965 -"TODO 4+ x \<up> 2 = 0";
7.966 -"TODO 4+ x \<up> 2 = 0";
7.967 -"TODO 4+ x \<up> 2 = 0";
7.968 -
7.969 -(*EP- 15*)
7.970 -val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.971 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.972 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.973 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.974 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.975 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.976 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.977 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.978 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.979 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.980 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.981 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.982 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
7.983 -
7.984 -val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.985 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.986 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.987 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.988 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.989 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.990 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.991 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.995 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.996 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
7.997 -
7.998 -(*EP- 16*)
7.999 -val fmz = ["equality (x + 2 * x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];
7.1000 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.1001 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.1002 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.1003 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1004 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1005 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1006 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1007 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1008 -
7.1009 -(*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f;
7.1010 -(*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt
7.1011 -
7.1012 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)
7.1013 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1014 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1015 -case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
7.1016 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
7.1017 -
7.1018 -(*EP-//*)
7.1019 -val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
7.1020 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
7.1021 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
7.1022 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.1023 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1024 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1025 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1026 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1027 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1028 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1029 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1030 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
7.1031 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
7.1032 -
7.1033 -
7.1034 -\<close> ML \<open>
7.1035 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.1036 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.1037 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.1038 -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
7.1039 -see --- val rls = calculate_RootRat > calculate_Rational ---
7.1040 -calculate_RootRat was a TODO with 2002, requires re-design.
7.1041 -see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
7.1042 -*)
7.1043 - val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
7.1044 - "solveFor x", "solutions L"];
7.1045 - val (dI',pI',mI') =
7.1046 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
7.1047 - ["PolyEq", "complete_square"]);
7.1048 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.1049 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1050 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1051 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1052 -
7.1053 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1054 -(*Apply_Method ("PolyEq", "complete_square")*)
7.1055 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1056 -(*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
7.1057 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1058 -(*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
7.1059 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1060 -(*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
7.1061 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1062 -(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
7.1063 - 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
7.1064 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1065 -(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
7.1066 - - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
7.1067 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1068 -(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
7.1069 - - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
7.1070 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1071 -(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
7.1072 - x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
7.1073 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1074 -(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
7.1075 - x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
7.1076 - NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
7.1077 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1078 -(*"x = - 2 | x = 4" nxt = Or_to_List*)
7.1079 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1080 -(*"[x = - 2, x = 4]" nxt = Check_Postcond*)
7.1081 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
7.1082 -(* FIXXXME
7.1083 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
7.1084 - | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
7.1085 -*)
7.1086 -if f2str f =
7.1087 - "[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.1088 -(*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
7.1089 -then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
7.1090 -
7.1091 -
7.1092 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
7.1093 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
7.1094 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
7.1095 -(*stopped due to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
7.1096 -see --- val rls = calculate_RootRat > calculate_Rational ---*)
7.1097 -val thy = @{theory PolyEq};
7.1098 -val ctxt = Proof_Context.init_global thy;
7.1099 -val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
7.1100 -val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
7.1101 -
7.1102 -val rls = complete_square;
7.1103 -val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
7.1104 -if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2"
7.1105 -then () else error "rls complete_square CHANGED";
7.1106 -
7.1107 -val thm = @{thm square_explicit1};
7.1108 -val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
7.1109 -if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
7.1110 -then () else error "thm square_explicit1 CHANGED";
7.1111 -
7.1112 -val thm = @{thm root_plus_minus};
7.1113 -val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
7.1114 -if UnparseC.term t =
7.1115 -"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
7.1116 -then () else error "thm root_plus_minus CHANGED";
7.1117 -
7.1118 -(*the thm bdv_explicit2* here required to be constrained to ::real*)
7.1119 -val thm = @{thm bdv_explicit2};
7.1120 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
7.1121 -if UnparseC.term t =
7.1122 -"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
7.1123 -then () else error "thm bdv_explicit2 CHANGED";
7.1124 -
7.1125 -val thm = @{thm bdv_explicit3};
7.1126 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
7.1127 -if UnparseC.term t =
7.1128 -"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
7.1129 -then () else error "thm bdv_explicit3 CHANGED";
7.1130 -
7.1131 -val thm = @{thm bdv_explicit2};
7.1132 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
7.1133 -if UnparseC.term t =
7.1134 -"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
7.1135 -then () else error "thm bdv_explicit2 CHANGED";
7.1136 -
7.1137 -val rls = calculate_RootRat;
7.1138 -val SOME (t,asm) = rewrite_set_ thy true rls t;
7.1139 -if UnparseC.term t =
7.1140 - "- 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.1141 -(*"- 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.1142 -then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
7.1143 -(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
7.1144 -
7.1145 -
7.1146 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
7.1147 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
7.1148 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
7.1149 -"---- test the erls ----";
7.1150 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
7.1151 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
7.1152 - val t' = UnparseC.term t;
7.1153 - (*if t'= \<^const_name>\<open>True\<close> then ()
7.1154 - else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
7.1155 -(* *)
7.1156 - val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
7.1157 - "solveFor x", "solutions L"];
7.1158 - val (dI',pI',mI') =
7.1159 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
7.1160 - ["PolyEq", "complete_square"]);
7.1161 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.1162 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1163 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1164 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1165 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1166 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1167 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1168 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1169 - (*Apply_Method ("PolyEq", "complete_square")*)
7.1170 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
7.1171 -
7.1172 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
7.1173 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
7.1174 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
7.1175 - val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
7.1176 - "solveFor x", "solutions L"];
7.1177 - val (dI',pI',mI') =
7.1178 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
7.1179 - ["PolyEq", "complete_square"]);
7.1180 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.1181 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1182 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1183 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1184 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1185 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1186 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1187 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1188 - (*Apply_Method ("PolyEq", "complete_square")*)
7.1189 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1190 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1191 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1192 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1193 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1194 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1195 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1196 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1197 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1198 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.1199 -(* FIXXXXME n1.,
7.1200 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
7.1201 - | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
7.1202 -*)
7.1203 -
7.1204 -\<close> ML \<open>
7.1205 -\<close> ML \<open>
7.1206 -\<close>
7.1207 -
7.1208 -
7.1209 section \<open>===================================================================================\<close>
7.1210 ML \<open>
7.1211 \<close> ML \<open>