1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Aug 23 12:33:10 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Aug 23 14:24:06 2021 +0200
1.3 @@ -650,7 +650,7 @@
1.4 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.5 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.6 rules = [
1.7 - (*\<^rule_thm>\<open>divide_1\<close>, "?x / 1 = ?x" unnecessary.for normalform*)
1.8 + \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
1.9 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
1.10 \<^rule_thm>\<open>minus_zero\<close>, (*"- 0 = 0"*)
1.11 (*\<^rule_thm>\<open>real_mult_minus1\<close>, "-1 * z = - z"*)
1.12 @@ -711,7 +711,7 @@
1.13 erls = Atools_erls, srls = Rule_Set.Empty,
1.14 calc = [], errpatts = [],
1.15 rules = [
1.16 - Rule.Rls_ norm_Rational_min,
1.17 + Rule.Rls_ norm_Rational_min,
1.18 Rule.Rls_ discard_parentheses],
1.19 scr = Rule.Empty_Prog});
1.20
2.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 23 12:33:10 2021 +0200
2.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 23 14:24:06 2021 +0200
2.3 @@ -2,14 +2,14 @@
2.4 testexamples for PolyEq, poynomial equations and equational systems
2.5 Author: Richard Lang 2003
2.6 (c) due to copyright terms
2.7 -WN030609: some expls dont work due to unfinished handling of 'expanded terms';
2.8 - others marked with TODO have to be checked, too.
2.9 +
2.10 +Separation into polyeq-1.sml and polyeq-1a.sml due to
2.11 *)
2.12
2.13 "-----------------------------------------------------------------";
2.14 "table of contents -----------------------------------------------";
2.15 "-----------------------------------------------------------------";
2.16 -"------ polyeq- 1.sml ---------------------------------------------";
2.17 +"------ polyeq-1.sml ---------------------------------------------";
2.18 "----------- tests on predicates in problems ---------------------";
2.19 "----------- test matching problems ------------------------------";
2.20 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
2.21 @@ -22,6 +22,7 @@
2.22 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
2.23 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
2.24 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
2.25 +"------ polyeq- 2.sml ---------------------------------------------";
2.26 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
2.27 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
2.28 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
2.29 @@ -50,6 +51,7 @@
2.30 "----------- tests on predicates in problems ---------------------";
2.31 "----------- tests on predicates in problems ---------------------";
2.32 "----------- tests on predicates in problems ---------------------";
2.33 +val thy = @{theory};
2.34 Rewrite.trace_on:=false; (*true false*)
2.35
2.36 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
2.37 @@ -323,16 +325,16 @@
2.38 (** )end;( *local*)
2.39
2.40 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
2.41 -if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?";
2.42 +if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then () else error "still GREATER?";
2.43
2.44 val x = TermC.str2term "x ::real";
2.45
2.46 val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
2.47 -if 2006 = size_of_term' 1 true x t1
2.48 +if 2006 = size_of_term' 1 false(*true*) x t1
2.49 then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
2.50
2.51 val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
2.52 -if 3004 = size_of_term' 1 true x t2
2.53 +if 3004 = size_of_term' 1 false(*true*) x t2
2.54 then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
2.55
2.56
2.57 @@ -348,23 +350,23 @@
2.58 val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
2.59 val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
2.60
2.61 -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
2.62 +if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then ()
2.63 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
2.64
2.65 -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
2.66 +if ord_make_polynomial_in false(*true*) thy substa (x1,x2) = true(*LESS *) then ()
2.67 else error "termorder.sml diff.behav ord_make_polynomial_in #2";
2.68
2.69 -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
2.70 +if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then ()
2.71 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
2.72
2.73 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
2.74 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
2.75 - ord_make_polynomial_in true thy substx (aa, bb);
2.76 + ord_make_polynomial_in false(*true*) thy substx (aa, bb);
2.77 true; (* => LESS *)
2.78
2.79 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
2.80 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
2.81 - ord_make_polynomial_in true thy substa (aa, bb);
2.82 + ord_make_polynomial_in false(*true*) thy substa (aa, bb);
2.83 false; (* => GREATER *)
2.84
2.85 (* und nach dem Re-engineering der Termorders in den 'rulesets'
2.86 @@ -909,7 +911,7 @@
2.87 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
2.88
2.89 (*EP- 16*)
2.90 -val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.91 +val fmz = ["equality (x + 2 * x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];
2.92 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.93 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.94 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.95 @@ -917,7 +919,12 @@
2.96 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.97 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.98 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.99 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.100 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.101 +
2.102 +(*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f;
2.103 +(*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt
2.104 +
2.105 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)
2.106 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.107 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.108 case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
2.109 @@ -991,7 +998,7 @@
2.110 | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
2.111 *)
2.112 if f2str f =
2.113 -"[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))]"
2.114 + "[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))]"
2.115 (*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
2.116 then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
2.117
2.118 @@ -999,7 +1006,7 @@
2.119 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
2.120 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
2.121 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
2.122 -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
2.123 +(*stopped due to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
2.124 see --- val rls = calculate_RootRat > calculate_Rational ---*)
2.125 val thy = @{theory PolyEq};
2.126 val ctxt = Proof_Context.init_global thy;
2.127 @@ -1008,37 +1015,43 @@
2.128
2.129 val rls = complete_square;
2.130 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
2.131 -UnparseC.term t = "-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2";
2.132 +if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2"
2.133 +then () else error "rls complete_square CHANGED";
2.134
2.135 -val thm = ThmC.numerals_to_Free @{thm square_explicit1};
2.136 +val thm = @{thm square_explicit1};
2.137 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
2.138 -UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8";
2.139 +if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
2.140 +then () else error "thm square_explicit1 CHANGED";
2.141
2.142 -val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
2.143 +val thm = @{thm root_plus_minus};
2.144 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
2.145 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
2.146 - "\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
2.147 +if UnparseC.term t =
2.148 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
2.149 +then () else error "thm root_plus_minus CHANGED";
2.150
2.151 (*the thm bdv_explicit2* here required to be constrained to ::real*)
2.152 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
2.153 +val thm = @{thm bdv_explicit2};
2.154 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
2.155 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
2.156 - "\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
2.157 +if UnparseC.term t =
2.158 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
2.159 +then () else error "thm bdv_explicit2 CHANGED";
2.160
2.161 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
2.162 +val thm = @{thm bdv_explicit3};
2.163 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
2.164 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
2.165 - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
2.166 +if UnparseC.term t =
2.167 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
2.168 +then () else error "thm bdv_explicit3 CHANGED";
2.169
2.170 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
2.171 +val thm = @{thm bdv_explicit2};
2.172 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
2.173 -UnparseC.term t = "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
2.174 - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
2.175 +if UnparseC.term t =
2.176 +"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
2.177 +then () else error "thm bdv_explicit2 CHANGED";
2.178
2.179 val rls = calculate_RootRat;
2.180 val SOME (t,asm) = rewrite_set_ thy true rls t;
2.181 if UnparseC.term t =
2.182 - "- 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))"
2.183 + "- 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))"
2.184 (*"- 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*)
2.185 then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
2.186 (*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
3.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Mon Aug 23 12:33:10 2021 +0200
3.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Mon Aug 23 14:24:06 2021 +0200
3.3 @@ -107,7 +107,7 @@
3.4 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
3.5 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
3.6 *)
3.7 -if f2str f = "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]" then ()
3.8 +if f2str f = "[x = sqrt (0 - - 49), x = - 1 * sqrt (0 - - 49)]" then ()
3.9 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
3.10
3.11
3.12 @@ -212,6 +212,7 @@
3.13 "----------- rls make_polynomial_in ------------------------------";
3.14 "----------- rls make_polynomial_in ------------------------------";
3.15 "----------- rls make_polynomial_in ------------------------------";
3.16 +val thy = @{theory};
3.17 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
3.18 (*WN.19.3.03 ---v-*)
3.19 (*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");
3.20 @@ -283,18 +284,18 @@
3.21
3.22 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
3.23 t |> UnparseC.term; t |> TermC.atomty;
3.24 -val thm = ThmC.numerals_to_Free @{thm d2_prescind1};
3.25 +val thm = @{thm d2_prescind1};
3.26 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
3.27 val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
3.28
3.29 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", ""))
3.30 --> x = 0 | -6 + 5 * x = 0*)
3.31 t' |> UnparseC.term; t' |> TermC.atomty;
3.32 -val thm = ThmC.numerals_to_Free @{thm d2_reduce_equation1};
3.33 +val thm = @{thm d2_reduce_equation1};
3.34 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
3.35 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
3.36 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
3.37 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
3.38 *)
3.39 -if UnparseC.term t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
3.40 +if UnparseC.term t'' = "x = 0 \<or> - 6 + 5 * x = 0" then ()
3.41 else error "rls d2_polyeq_bdv_only_simplify broken";
4.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Aug 23 12:33:10 2021 +0200
4.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon Aug 23 14:24:06 2021 +0200
4.3 @@ -484,18 +484,11 @@
4.4 (*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2"
4.5 *)
4.6
4.7 +val NONE = adhoc_thm @{theory} eval_ t;
4.8 +"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
4.9 val NONE =
4.10 - adhoc_thm @{theory} eval_ t;
4.11 -"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
4.12 -val SOME ("#divide_e~1_2", t') =
4.13 (*case*) get_pair thy op_ eval_fn t (*of*);
4.14
4.15 -(*+*)UnparseC.term t = "- 1 / 2";
4.16 -(*+*)UnparseC.term t' = "- 1 / 2 = - 1 / 2"; "HOL.Trueprop";
4.17 -
4.18 -if t = (TermC.rhs o HOLogic.dest_Trueprop) t'
4.19 -then () else error "fun adhoc_thm + fun eval_cancel CHANGED";
4.20 -
4.21
4.22 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
4.23 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
5.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Aug 23 12:33:10 2021 +0200
5.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Aug 23 14:24:06 2021 +0200
5.3 @@ -293,8 +293,8 @@
5.4 ML_file "Knowledge/rootrat.sml"
5.5 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
5.6 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
5.7 -(*ML_file "Knowledge/polyeq-1.sml" TOODOO.1 error inherited from root.sml*)
5.8 -(*ML_file "Knowledge/polyeq-2.sml" TOODOO.1 Test_Isac_Short*)
5.9 + ML_file "Knowledge/polyeq-1.sml"
5.10 +(*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*)
5.11 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
5.12 ML_file "Knowledge/calculus.sml"
5.13 ML_file "Knowledge/trig.sml"
6.1 --- a/test/Tools/isac/Test_Some.thy Mon Aug 23 12:33:10 2021 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 23 14:24:06 2021 +0200
6.3 @@ -107,19 +107,7 @@
6.4 section \<open>===================================================================================\<close>
6.5 ML \<open>
6.6 \<close> ML \<open>
6.7 -\<close> ML \<open>
6.8 -\<close> ML \<open>
6.9 -\<close>
6.10 -
6.11 -ML \<open>
6.12 -val thy = @{theory}; Rewrite.trace_on := false; (**)
6.13 -\<close>
6.14 -(* ML_file "Knowledge/polyeq-1.sml" TOODOO.1 error inherited from root.sml*)
6.15 -section \<open>======== check test/../polyeq-1.sml ===============================================\<close>
6.16 -ML \<open>
6.17 -val thy = @{theory};
6.18 -\<close> ML \<open>
6.19 -(* Title: Knowledge/polyeq-1.sml
6.20 +(* Title: Knowledge/polyeq- 1.sml
6.21 testexamples for PolyEq, poynomial equations and equational systems
6.22 Author: Richard Lang 2003
6.23 (c) due to copyright terms
6.24 @@ -130,33 +118,6 @@
6.25 "-----------------------------------------------------------------";
6.26 "table of contents -----------------------------------------------";
6.27 "-----------------------------------------------------------------";
6.28 -"------ polyeq- 1.sml ---------------------------------------------";
6.29 -"----------- tests on predicates in problems ---------------------";
6.30 -"----------- test matching problems ------------------------------";
6.31 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
6.32 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
6.33 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
6.34 -"----------- lin.eq degree_0 -------------------------------------";
6.35 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
6.36 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
6.37 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
6.38 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
6.39 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
6.40 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
6.41 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
6.42 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
6.43 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
6.44 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
6.45 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
6.46 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
6.47 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
6.48 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
6.49 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
6.50 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
6.51 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
6.52 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
6.53 -"-----------------------------------------------------------------";
6.54 -"------ polyeq- 2.sml ---------------------------------------------";
6.55 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
6.56 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
6.57 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
6.58 @@ -168,1529 +129,292 @@
6.59 "-----------------------------------------------------------------";
6.60 "-----------------------------------------------------------------";
6.61
6.62 -"----------- tests on predicates in problems ---------------------";
6.63 -"----------- tests on predicates in problems ---------------------";
6.64 -"----------- tests on predicates in problems ---------------------";
6.65 -val thy = @{theory};
6.66 -Rewrite.trace_on:=false; (*true false*)
6.67
6.68 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
6.69 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
6.70 - if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
6.71 - else error "polyeq.sml: diff.behav. in lhs";
6.72 -
6.73 - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
6.74 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
6.75 - if (UnparseC.term t) = "True" then ()
6.76 - else error "polyeq.sml: diff.behav. 1 in is_expended_in";
6.77 -
6.78 - val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
6.79 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
6.80 - if (UnparseC.term t) = "False" then ()
6.81 - else error "polyeq.sml: diff.behav. 2 in is_poly_in";
6.82 -
6.83 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
6.84 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
6.85 - if (UnparseC.term t) = "True" then ()
6.86 - else error "polyeq.sml: diff.behav. 3 in is_poly_in";
6.87 -
6.88 - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
6.89 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
6.90 - if (UnparseC.term t) = "True" then ()
6.91 - else error "polyeq.sml: diff.behav. 4 in is_expended_in";
6.92 -
6.93 - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
6.94 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
6.95 - if (UnparseC.term t) = "True" then ()
6.96 - else error "polyeq.sml: diff.behav. 5 in is_expended_in";
6.97 -
6.98 - val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
6.99 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
6.100 - if (UnparseC.term t) = "True" then ()
6.101 - else error "polyeq.sml: diff.behav. in has_degree_in_in";
6.102 -
6.103 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
6.104 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
6.105 - if (UnparseC.term t) = "False" then ()
6.106 - else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
6.107 -
6.108 - val t4 = (Thm.term_of o the o (TermC.parse thy))
6.109 - "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
6.110 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
6.111 - if (UnparseC.term t) = "False" then ()
6.112 - else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
6.113 -
6.114 -val t5 = (Thm.term_of o the o (TermC.parse thy))
6.115 - "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
6.116 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
6.117 - if (UnparseC.term t) = "True" then ()
6.118 - else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
6.119 -
6.120 -\<close> ML \<open>
6.121 -"----------- test matching problems --------------------------0---";
6.122 -"----------- test matching problems --------------------------0---";
6.123 -"----------- test matching problems --------------------------0---";
6.124 -val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.125 -if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
6.126 - M_Match.Matches' {Find = [Correct "solutions L"],
6.127 - With = [],
6.128 - Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
6.129 - Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
6.130 - Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
6.131 - Relate = []}
6.132 -then () else error "M_Match.match_pbl [expanded,univariate,equation]";
6.133 -
6.134 -if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
6.135 - M_Match.Matches' {Find = [Correct "solutions L"],
6.136 - With = [],
6.137 - Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
6.138 - Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
6.139 - Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
6.140 -then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
6.141 -
6.142 -
6.143 -\<close> ML \<open>
6.144 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
6.145 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
6.146 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
6.147 -(*##################################################################################
6.148 ------------ 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
6.149 -
6.150 - (*Aufgabe zum Einstieg in die Arbeit...*)
6.151 - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
6.152 - (*ein 'ruleset' aus Poly.ML wird angewandt...*)
6.153 - val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
6.154 - UnparseC.term t;
6.155 - "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
6.156 - val SOME (t,_) =
6.157 - rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
6.158 - UnparseC.term t;
6.159 - "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
6.160 -(* bei Verwendung von "size_of-term" nach MG :*)
6.161 -(*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
6.162 -
6.163 - (*wir holen 'a' wieder aus der Klammerung heraus...*)
6.164 - val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
6.165 - UnparseC.term t;
6.166 - "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
6.167 -(* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
6.168 -
6.169 - val SOME (t,_) =
6.170 - rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
6.171 - UnparseC.term t;
6.172 - "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
6.173 - (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
6.174 - "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
6.175 -
6.176 - (*das rewriting l"asst sich beobachten mit
6.177 -Rewrite.trace_on := false; (*true false*)
6.178 - *)
6.179 -
6.180 -"------ 15.11.02 --------------------------";
6.181 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
6.182 - val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
6.183 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
6.184 -
6.185 -Rewrite.trace_on := false; (*true false*)
6.186 - (* Anwenden einer Regelmenge aus Termorder.ML: *)
6.187 - val SOME (t,_) =
6.188 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
6.189 - UnparseC.term t;
6.190 - val SOME (t,_) =
6.191 - rewrite_set_ thy false discard_parentheses t;
6.192 - UnparseC.term t;
6.193 -"1 + b * x + x * a";
6.194 -
6.195 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
6.196 - val SOME (t,_) =
6.197 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
6.198 - UnparseC.term t;
6.199 - val SOME (t,_) =
6.200 - rewrite_set_ thy false discard_parentheses t;
6.201 - UnparseC.term t;
6.202 -"1 + (x + b * x) * a + a \<up> 2";
6.203 -
6.204 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
6.205 - val SOME (t,_) =
6.206 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
6.207 - UnparseC.term t;
6.208 - val SOME (t,_) =
6.209 - rewrite_set_ thy false discard_parentheses t;
6.210 - UnparseC.term t;
6.211 -"1 + b * a + (7 + x) * a \<up> 2";
6.212 -
6.213 -(* MG2003
6.214 - Prog_Expr.thy grundlegende Algebra
6.215 - Poly.thy Polynome
6.216 - Rational.thy Br"uche
6.217 - Root.thy Wurzeln
6.218 - RootRat.thy Wurzen + Br"uche
6.219 - Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
6.220 -
6.221 - get_thm Termorder.thy "bdv_n_collect";
6.222 - get_thm (theory "Isac_Knowledge") "bdv_n_collect";
6.223 -*)
6.224 - val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
6.225 - val SOME (t,_) =
6.226 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
6.227 - UnparseC.term t;
6.228 - val SOME (t,_) =
6.229 - rewrite_set_ thy false discard_parentheses t;
6.230 - UnparseC.term t;
6.231 -"(7 + x) * a \<up> 2";
6.232 -
6.233 - val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
6.234 -
6.235 - val t = (Thm.term_of o the o (parseold thy)) "7";
6.236 -##################################################################################*)
6.237 -
6.238 -
6.239 -\<close> ML \<open>
6.240 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
6.241 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
6.242 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
6.243 -(* termorder hacked by MG, adapted later by WN *)
6.244 -(** )local ( *. for make_polynomial_in .*)
6.245 -
6.246 -open Term; (* for type order = EQUAL | LESS | GREATER *)
6.247 -
6.248 -fun pr_ord EQUAL = "EQUAL"
6.249 - | pr_ord LESS = "LESS"
6.250 - | pr_ord GREATER = "GREATER";
6.251 -
6.252 -fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
6.253 - | dest_hd' x (t as Free (a, T)) =
6.254 - if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
6.255 - else (((a, 0), T), 1)
6.256 - | dest_hd' _ (Var v) = (v, 2)
6.257 - | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
6.258 - | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
6.259 - | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
6.260 -
6.261 -fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
6.262 - Free (var, _) $ Free (pot, _)) =
6.263 - (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
6.264 - case x of (*WN*)
6.265 - (Free (xstr, _)) =>
6.266 - if xstr = var
6.267 - then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
6.268 - 1000 * (the (TermC.int_opt_of_string pot)))
6.269 - else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
6.270 - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
6.271 - | size_of_term' i pr x (t as Abs (_, _, body)) =
6.272 - (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
6.273 - 1 + size_of_term' (i + 1) pr x body)
6.274 - | size_of_term' i pr x (f $ t) =
6.275 - let
6.276 - val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
6.277 - val s1 = size_of_term' (i + 1) pr x f
6.278 - val s2 = size_of_term' (i + 1) pr x t
6.279 - val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
6.280 - in (s1 + s2) end
6.281 - | size_of_term' i pr x t =
6.282 - (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
6.283 - case t of
6.284 - Free (subst, _) =>
6.285 - (case x of
6.286 - Free (xstr, _) =>
6.287 - if xstr = subst
6.288 - then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
6.289 - else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
6.290 - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
6.291 - | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
6.292 -
6.293 -fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
6.294 - let
6.295 - val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
6.296 - val ord =
6.297 - case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
6.298 - val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
6.299 - in ord end
6.300 - | term_ord' i pr x _ (t, u) =
6.301 - let
6.302 - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
6.303 - val ord =
6.304 - case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
6.305 - EQUAL =>
6.306 - let val (f, ts) = strip_comb t and (g, us) = strip_comb u
6.307 - in
6.308 - (case hd_ord (i + 1) pr x (f, g) of
6.309 - EQUAL => (terms_ord x (i + 1) pr) (ts, us)
6.310 - | ord => ord)
6.311 - end
6.312 - | ord => ord
6.313 - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
6.314 - in ord end
6.315 -and hd_ord i pr x (f, g) = (* ~ term.ML *)
6.316 - let
6.317 - val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
6.318 - val ord = prod_ord
6.319 - (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
6.320 - (dest_hd' x f, dest_hd' x g)
6.321 - val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
6.322 - in ord end
6.323 -and terms_ord x i pr (ts, us) =
6.324 - let
6.325 - val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
6.326 - val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
6.327 - val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
6.328 - in ord end
6.329 -
6.330 -(** )in( *local*)
6.331 -
6.332 -fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
6.333 - ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
6.334 - case subst of
6.335 - (_, x) :: _ =>
6.336 - term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
6.337 - | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
6.338 -
6.339 -(** )end;( *local*)
6.340 -
6.341 -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
6.342 -if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?";
6.343 -
6.344 -val x = TermC.str2term "x ::real";
6.345 -
6.346 -val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
6.347 -if 2006 = size_of_term' 1 true x t1
6.348 -then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
6.349 -
6.350 -val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
6.351 -if 3004 = size_of_term' 1 true x t2
6.352 -then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
6.353 -
6.354 -
6.355 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
6.356 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
6.357 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
6.358 - val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
6.359 - val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
6.360 - val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
6.361 -
6.362 - val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
6.363 - val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
6.364 - val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
6.365 - val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
6.366 -
6.367 -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
6.368 -else error "termorder.sml diff.behav ord_make_polynomial_in #1";
6.369 -
6.370 -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
6.371 -else error "termorder.sml diff.behav ord_make_polynomial_in #2";
6.372 -
6.373 -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
6.374 -else error "termorder.sml diff.behav ord_make_polynomial_in #3";
6.375 -
6.376 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
6.377 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
6.378 - ord_make_polynomial_in true thy substx (aa, bb);
6.379 - true; (* => LESS *)
6.380 -
6.381 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
6.382 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
6.383 - ord_make_polynomial_in true thy substa (aa, bb);
6.384 - false; (* => GREATER *)
6.385 -
6.386 -(* und nach dem Re-engineering der Termorders in den 'rulesets'
6.387 - kannst Du die 'gr"osste' Variable frei w"ahlen: *)
6.388 - val bdv= TermC.str2term "bdv ::real";
6.389 - val x = TermC.str2term "x ::real";
6.390 - val a = TermC.str2term "a ::real";
6.391 - val b = TermC.str2term "b ::real";
6.392 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
6.393 -if UnparseC.term t' = "b + x + a" then ()
6.394 -else error "termorder.sml diff.behav ord_make_polynomial_in #11";
6.395 -
6.396 -val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
6.397 -
6.398 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
6.399 -if UnparseC.term t' = "a + b + x" then ()
6.400 -else error "termorder.sml diff.behav ord_make_polynomial_in #13";
6.401 -
6.402 - val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
6.403 - val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
6.404 -val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
6.405 -if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
6.406 -else error "termorder.sml diff.behav ord_make_polynomial_in #15";
6.407 -
6.408 - val ttt' = "(3*x + 5)/18 ::real";
6.409 - val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
6.410 -val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
6.411 -if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
6.412 -else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
6.413 -
6.414 -val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
6.415 -if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
6.416 -else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
6.417 -
6.418 -"----------- lin.eq degree_0 -------------------------------------";
6.419 -"----------- lin.eq degree_0 -------------------------------------";
6.420 -"----------- lin.eq degree_0 -------------------------------------";
6.421 -"----- d0_false ------";
6.422 -val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
6.423 -val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
6.424 - ["PolyEq", "solve_d0_polyeq_equation"]);
6.425 -(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
6.426 -TODO: change to "equality (x + - 1*x = (0::real))"
6.427 - and search for an appropriate problem and method.
6.428 -
6.429 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.430 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.431 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.432 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.433 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.434 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.435 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.436 -case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
6.437 - | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
6.438 -
6.439 -"----- d0_true ------";
6.440 -val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
6.441 -val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
6.442 - ["PolyEq", "solve_d0_polyeq_equation"]);
6.443 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.444 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.445 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.446 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.447 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.448 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.449 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.450 -case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
6.451 - | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
6.452 -============ inhibit exn WN110914 ============================================*)
6.453 -
6.454 -\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
6.455 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
6.456 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
6.457 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
6.458 -"----- d2_pqformula1 ------!!!!";
6.459 -val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
6.460 -val (dI',pI',mI') =
6.461 - ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
6.462 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.463 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.464 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.465 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.466 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.467 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.468 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.469 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
6.470 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.471 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.472 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.473 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.474 -
6.475 -(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
6.476 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
6.477 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.478 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.479 -
6.480 -if p = ([], Res) andalso
6.481 - f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
6.482 - case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
6.483 -else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
6.484 -
6.485 -\<close> ML \<open>
6.486 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
6.487 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
6.488 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
6.489 -"----- d2_pqformula1_neg ------";
6.490 -val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
6.491 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.492 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.493 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.494 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.495 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.496 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.497 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.498 -(*### or2list False
6.499 - ([1],Res) False Or_to_List)*)
6.500 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.501 -(*### or2list False
6.502 - ([2],Res) [] Check_elementwise "Assumptions"*)
6.503 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.504 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.505 -val asm = Ctree.get_assumptions pt p;
6.506 -if f2str f = "[]" andalso
6.507 - UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
6.508 - "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
6.509 -else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
6.510 -
6.511 -\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
6.512 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
6.513 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
6.514 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
6.515 -"----- d2_pqformula2 ------";
6.516 -val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.517 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
6.518 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.519 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.520 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.521 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.522 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.523 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.524 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.525 -
6.526 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.527 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.528 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.529 -case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
6.530 - | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
6.531 -
6.532 -
6.533 -\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
6.534 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
6.535 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
6.536 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
6.537 -"----- d2_pqformula3 ------";
6.538 -(*EP-9*)
6.539 -val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.540 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
6.541 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.542 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.543 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.544 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.545 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.546 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.547 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.548 -
6.549 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.550 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.551 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.552 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
6.553 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
6.554 -
6.555 -
6.556 -\<close> ML \<open>
6.557 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
6.558 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
6.559 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
6.560 -"----- d2_pqformula3_neg ------";
6.561 -val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.562 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
6.563 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.564 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.565 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.566 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.567 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.568 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.569 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.570 -
6.571 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.572 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.573 -"TODO 2 + x + x \<up> 2 = 0";
6.574 -"TODO 2 + x + x \<up> 2 = 0";
6.575 -"TODO 2 + x + x \<up> 2 = 0";
6.576 -
6.577 -\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
6.578 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
6.579 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
6.580 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
6.581 -"----- d2_pqformula4 ------";
6.582 -val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.583 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
6.584 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.585 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.586 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.587 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.588 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.589 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.590 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.591 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.592 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.593 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.594 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
6.595 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
6.596 -
6.597 -\<close> ML \<open>
6.598 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
6.599 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
6.600 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
6.601 -"----- d2_pqformula5 ------";
6.602 -val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.603 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
6.604 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.605 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.606 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.607 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.608 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.609 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.610 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.611 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.612 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.613 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.614 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.615 - | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
6.616 -
6.617 -\<close> ML \<open>
6.618 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
6.619 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
6.620 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
6.621 -"----- d2_pqformula6 ------";
6.622 -val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.623 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
6.624 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.625 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.626 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.627 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.628 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.629 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.630 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.631 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.632 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.633 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.634 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.635 - | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
6.636 -
6.637 -\<close> ML \<open>
6.638 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
6.639 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
6.640 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
6.641 -"----- d2_pqformula7 ------";
6.642 -(*EP- 10*)
6.643 -val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.644 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
6.645 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.646 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.647 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.648 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.649 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.650 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.651 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.652 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.653 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.654 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.655 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.656 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
6.657 -
6.658 -\<close> ML \<open>
6.659 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
6.660 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
6.661 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
6.662 -"----- d2_pqformula8 ------";
6.663 -val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.664 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
6.665 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.666 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.667 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.668 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.669 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.670 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.671 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.672 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.673 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.674 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.675 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.676 - | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
6.677 -
6.678 -\<close> ML \<open>
6.679 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
6.680 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
6.681 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
6.682 -"----- d2_pqformula9 ------";
6.683 -val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.684 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
6.685 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.686 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.687 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.688 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.689 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.690 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.691 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.692 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.693 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.694 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
6.695 - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
6.696 -
6.697 -
6.698 -\<close> ML \<open>
6.699 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
6.700 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
6.701 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
6.702 -"----- d2_pqformula9_neg ------";
6.703 -val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.704 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
6.705 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
6.706 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.707 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.708 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.709 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.710 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.711 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.712 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.713 -"TODO 4 + 1*x \<up> 2 = 0";
6.714 -"TODO 4 + 1*x \<up> 2 = 0";
6.715 -"TODO 4 + 1*x \<up> 2 = 0";
6.716 -
6.717 -\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
6.718 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
6.719 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
6.720 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
6.721 -val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.722 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.723 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.724 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.725 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.726 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.727 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.728 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.729 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.730 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.731 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.732 -case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
6.733 - | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
6.734 -
6.735 -\<close> ML \<open>
6.736 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
6.737 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
6.738 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
6.739 -val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.740 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.741 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.742 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.743 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.744 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.745 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.746 -
6.747 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.748 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.749 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.750 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
6.751 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
6.752 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
6.753 -
6.754 -
6.755 -\<close> ML \<open>
6.756 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
6.757 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
6.758 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
6.759 -(*EP- 11*)
6.760 -val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.761 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.762 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.763 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.764 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.765 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.766 -
6.767 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.768 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.769 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.770 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.771 -
6.772 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.773 -case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
6.774 - | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
6.775 -
6.776 -
6.777 -\<close> ML \<open>
6.778 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
6.779 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
6.780 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
6.781 -val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.782 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.783 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.784 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.785 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.786 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.787 -
6.788 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.789 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.790 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.791 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.792 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.793 -"TODO 1 + x + 2*x \<up> 2 = 0";
6.794 -"TODO 1 + x + 2*x \<up> 2 = 0";
6.795 -"TODO 1 + x + 2*x \<up> 2 = 0";
6.796 -
6.797 -
6.798 -val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.799 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.800 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.801 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.802 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.803 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.804 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.805 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.806 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.807 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.808 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.809 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
6.810 - | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
6.811 -
6.812 -val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.813 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.814 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.815 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.816 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.817 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.818 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.819 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.820 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.821 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.822 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.823 -"TODO 2 + 1*x + x \<up> 2 = 0";
6.824 -"TODO 2 + 1*x + x \<up> 2 = 0";
6.825 -"TODO 2 + 1*x + x \<up> 2 = 0";
6.826 -
6.827 -\<close> ML \<open>
6.828 -(*EP- 12*)
6.829 -val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.830 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.831 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.832 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.833 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.834 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.835 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.836 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.837 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.838 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.839 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.840 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
6.841 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
6.842 -
6.843 -val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.844 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.845 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.846 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.847 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.848 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.849 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.850 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.851 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.852 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.853 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.854 -"TODO 2 + x + x \<up> 2 = 0";
6.855 -"TODO 2 + x + x \<up> 2 = 0";
6.856 -"TODO 2 + x + x \<up> 2 = 0";
6.857 -
6.858 -\<close> ML \<open>
6.859 -(*EP- 13*)
6.860 -val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.861 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.862 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.863 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.864 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.865 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.866 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.867 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.868 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.869 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.870 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.871 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
6.872 - | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
6.873 -
6.874 -val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.875 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.876 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.877 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.878 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.879 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.880 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.881 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.882 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.883 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.884 -"TODO 8+ 2*x \<up> 2 = 0";
6.885 -"TODO 8+ 2*x \<up> 2 = 0";
6.886 -"TODO 8+ 2*x \<up> 2 = 0";
6.887 -
6.888 -\<close> ML \<open>
6.889 -(*EP- 14*)
6.890 -val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.891 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.892 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.893 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.894 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.895 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.896 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.897 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.898 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.899 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.900 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
6.901 - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
6.902 -
6.903 -
6.904 -\<close> ML \<open>
6.905 -val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.906 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.907 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.908 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.909 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.910 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.911 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.912 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.913 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.914 -"TODO 4+ x \<up> 2 = 0";
6.915 -"TODO 4+ x \<up> 2 = 0";
6.916 -"TODO 4+ x \<up> 2 = 0";
6.917 -
6.918 -\<close> ML \<open>
6.919 -(*EP- 15*)
6.920 -val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.921 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.922 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.923 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.924 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.925 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.926 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.927 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.928 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.929 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.930 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.931 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.932 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
6.933 -
6.934 -\<close> ML \<open>
6.935 -val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.936 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.937 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.938 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.939 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.940 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.941 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.942 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.943 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.944 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.945 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.946 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.947 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
6.948 -
6.949 -\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
6.950 -\<close> ML \<open>
6.951 -(*EP- 16*)
6.952 -val fmz = ["equality (x + 2 * x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];
6.953 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.954 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.955 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.956 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.957 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.958 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.959 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.960 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.961 -\<close> ML \<open>
6.962 -(*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f;
6.963 -(*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt
6.964 -\<close> ML \<open>
6.965 -Rewrite.trace_on := false; (*false true*)
6.966 -\<close> text \<open> (* *)
6.967 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)
6.968 -\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
6.969 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
6.970 -\<close> ML \<open>
6.971 - val (pt, p) =
6.972 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
6.973 - case Step.by_tactic tac (pt, p) of
6.974 - ("ok", (_, _, ptp)) => ptp
6.975 - | ("unsafe-ok", (_, _, ptp)) => ptp
6.976 - | ("not-applicable",_) => (pt, p)
6.977 - | ("end-of-calculation", (_, _, ptp)) => ptp
6.978 - | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
6.979 - | _ => raise ERROR "me: uncovered case Step.by_tactic"
6.980 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.981 - (*case*)
6.982 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
6.983 -\<close> ML \<open>
6.984 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
6.985 -\<close> ML \<open>
6.986 - (*if*) Pos.on_calc_end ip (*else*);
6.987 -\<close> ML \<open>
6.988 - val (_, probl_id, _) = Calc.references (pt, p);
6.989 -\<close> ML \<open>
6.990 -val _ =
6.991 - (*case*) tacis (*of*);
6.992 -\<close> ML \<open>
6.993 - (*if*) probl_id = Problem.id_empty (*else*);
6.994 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.995 - switch_specify_solve p_ (pt, ip);
6.996 -\<close> ML \<open>
6.997 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.998 -\<close> ML \<open>
6.999 - (*if*) Pos.on_specification ([], state_pos) (*else*);
6.1000 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1001 - LI.do_next (pt, input_pos)
6.1002 -\<close> ML \<open>
6.1003 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
6.1004 -\<close> ML \<open>
6.1005 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
6.1006 -\<close> ML \<open>
6.1007 - val thy' = get_obj g_domID pt (par_pblobj pt p);
6.1008 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
6.1009 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1010 - (*case*)
6.1011 - LI.find_next_step sc (pt, pos) ist ctxt (*of*);
6.1012 -\<close> ML \<open>
6.1013 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) =
6.1014 - (sc, (pt, pos), ist, ctxt);
6.1015 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1016 - (*case*)
6.1017 - LI.scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist)
6.1018 -\<close> ML \<open>
6.1019 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) =
6.1020 - ((prog, (ptp, ctxt)), (Pstate ist));
6.1021 -\<close> ML \<open>
6.1022 - (*if*) path = [] (*else*);
6.1023 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1024 - go_scan_up (prog, cc) (trans_scan_up ist)
6.1025 -\<close> ML \<open>
6.1026 -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
6.1027 - ((prog, cc), (trans_scan_up ist));
6.1028 -\<close> ML \<open>
6.1029 - (*if*) path = [R] (*else*);
6.1030 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1031 - scan_up pcc (ist |> path_up) (go_up path sc)
6.1032 -\<close> ML \<open>
6.1033 -"~~~~~ and scan_up , args:"; val (pcc, ist,(Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ _ )) =
6.1034 - (pcc, (ist |> path_up), (go_up path sc));
6.1035 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
6.1036 - go_scan_up pcc ist
6.1037 -\<close> ML \<open>
6.1038 -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
6.1039 - (pcc, ist);
6.1040 -\<close> ML \<open>
6.1041 - (*if*) path = [R] (*else*);
6.1042 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1043 - scan_up pcc (ist |> path_up) (go_up path sc)
6.1044 -\<close> ML \<open>
6.1045 -"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _)) =
6.1046 - (pcc, (ist |> path_up), (go_up path sc));
6.1047 -\<close> ML \<open>
6.1048 - val e2 = check_Seq_up ist sc;
6.1049 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1050 - (*case*)
6.1051 - scan_dn cc (ist |> path_up_down [R]) e2 (*of*);
6.1052 -\<close> ML \<open>
6.1053 -"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2)) =
6.1054 - (cc, (ist |> path_up_down [R]), e2);
6.1055 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1056 - (*case*)
6.1057 - scan_dn cc (ist |> path_down [L, R]) e1 (*of*);
6.1058 -\<close> ML \<open>
6.1059 -"~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e)) =
6.1060 - (cc, (ist |> path_down [L, R]), e1);
6.1061 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1062 - (*case*)
6.1063 - scan_dn cc (ist |> path_down [R]) e (*of*);
6.1064 -\<close> ML \<open>
6.1065 -"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) =
6.1066 - (cc, (ist |> path_down [R]), e);
6.1067 -\<close> ML \<open>
6.1068 - (*if*) Tactical.contained_in t (*else*);
6.1069 -\<close> ML \<open>
6.1070 -val (Program.Tac prog_tac, form_arg) = (*case*)
6.1071 - LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
6.1072 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1073 - check_tac cc ist (prog_tac, form_arg)
6.1074 -\<close> ML \<open>
6.1075 -"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) =
6.1076 - (cc, ist, (prog_tac, form_arg));
6.1077 -\<close> ML \<open>
6.1078 - val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
6.1079 -\<close> ML \<open>
6.1080 -val _ = (*case*) m (*of*);
6.1081 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1082 - (*case*)
6.1083 -Solve_Step.check m (pt, p) (*of*);
6.1084 -\<close> ML \<open>
6.1085 -"~~~~~ fun check , args:"; val ((Tactic.Rewrite_Set rls), (cs as (pt, (p, _)))) =
6.1086 - (m, (pt, p));
6.1087 -\<close> ML \<open>
6.1088 - val pp = Ctree.par_pblobj pt p;
6.1089 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
6.1090 - val f = Calc.current_formula cs;
6.1091 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1092 - (*case*)
6.1093 - Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f (*of*);
6.1094 -\<close> ML \<open>
6.1095 -"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) =
6.1096 - ((ThyC.get_theory thy'), false, (assoc_rls rls), f);
6.1097 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1098 - rewrite__set_ thy 1 bool [] rls term;
6.1099 -\<close> ML \<open>
6.1100 -"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
6.1101 - (thy, 1, bool, [], rls, term);
6.1102 -\<close> ML \<open>
6.1103 -\<close> ML \<open> (* \<longrightarrow> src/../rewrite.sml *)
6.1104 -(*//-------------------------------- cp fromewrite.sml-----------------------------------------\\*)
6.1105 -\<close> ML \<open>
6.1106 -fun msg call thy op_ thmC t =
6.1107 - call ^ ": \n" ^
6.1108 - "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
6.1109 - "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
6.1110 -\<close> ML \<open>
6.1111 - (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
6.1112 - datatype switch = Appl | Noap;
6.1113 - fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
6.1114 - | rew_once ruls asm ct Appl [] =
6.1115 - (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
6.1116 - | Rule_Set.Sequence _ => (ct, asm)
6.1117 - | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
6.1118 - | rew_once ruls asm ct apno (rul :: thms) =
6.1119 - case rul of
6.1120 - Rule.Thm (thmid, thm) =>
6.1121 - (trace_in1 i "try thm" thmid;
6.1122 - case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1123 - ((#erls o Rule_Set.rep) rls) put_asm thm ct of
6.1124 - NONE => rew_once ruls asm ct apno thms
6.1125 - | SOME (ct', asm') =>
6.1126 - (trace_in2 i "rewrites to" thy ct';
6.1127 - rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
6.1128 - (* once again try the same rule, e.g. associativity against "()"*)
6.1129 - | Rule.Eval (cc as (op_, _)) =>
6.1130 - let val _ = trace_in1 i "try calc" op_;
6.1131 - in case Eval.adhoc_thm thy cc ct of
6.1132 - NONE => rew_once ruls asm ct apno thms
6.1133 - | SOME (_, thm') =>
6.1134 - let
6.1135 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1136 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
6.1137 - val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" thy op_ thm' ct)
6.1138 - val _ = trace_in3 i "calc. to" thy pairopt;
6.1139 - in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
6.1140 - end
6.1141 - | Rule.Cal1 (cc as (op_, _)) =>
6.1142 - let val _ = trace_in1 i "try cal1" op_;
6.1143 - in case Eval.adhoc_thm1_ thy cc ct of
6.1144 - NONE => (ct, asm)
6.1145 - | SOME (_, thm') =>
6.1146 - let
6.1147 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1148 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
6.1149 - val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
6.1150 - ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
6.1151 - val _ = trace_in3 i "cal1. to" thy pairopt;
6.1152 - in the pairopt end
6.1153 - end
6.1154 - | Rule.Rls_ rls' =>
6.1155 - (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
6.1156 - SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
6.1157 - | NONE => rew_once ruls asm ct apno thms)
6.1158 - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
6.1159 -(*\\------------------------------- cp from rewrite.sml---------------------------------------//*)
6.1160 -\<close> ML \<open>
6.1161 - val ruls = (#rules o Rule_Set.rep) rls;
6.1162 -\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1163 -Rewrite.trace_on := false; (*false rew_once-3-isa.txt true*)
6.1164 - val (ct', asm') =
6.1165 - rew_once ruls [] ct Noap ruls;
6.1166 -\<close> ML \<open>
6.1167 -(*+*)UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)";
6.1168 -\<close> ML \<open>
6.1169 -(*+*)rls;(*val it =
6.1170 - Repeat
6.1171 - {calc =
6.1172 - [("PLUS", ("Groups.plus_class.plus", fn)), ("MINUS", ("Groups.minus_class.minus", fn)), ("TIMES", ("Groups.times_class.times", fn)),
6.1173 - ("DIVIDE", ("Rings.divide_class.divide", fn)), ("SQRT", ("NthRoot.sqrt", fn)), ("POWER", ("Transcendental.powr", fn))],
6.1174 - ======^^^^^^======
6.1175 - erls = ------------------------------ id = "calc_rat_erls" ------------------------------------------------------vvvvvvvvvvvvvvvvvvvv
6.1176 - Repeat
6.1177 - {calc = [("DIVIDE", ("Rings.divide_class.divide", fn))], erls =
6.1178 - ======^^^^^^======
6.1179 - Repeat
6.1180 - {calc = [("matches", ("Prog_Expr.matches", fn)), ("equal", ("HOL.eq", fn)), ("is_num", ("Prog_Expr.is_num", fn))], erls = Empty, errpatts = [], id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", fn),
6.1181 - rules = [Eval ("Prog_Expr.matches", fn), Eval ("HOL.eq", fn), Eval ("Prog_Expr.is_num", fn), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True")], scr = Empty_Prog, srls = Empty},
6.1182 - errpatts = [], id = "PolyEq_erls", <<<------------------------------------- "PolyEq_erls"
6.1183 - preconds = [], rew_ord = ("dummy_ord", fn), rules =
6.1184 - [Thm ("real_assoc_1", "?a + (?b + ?c) = ?a + ?b + ?c"), Eval ("Transcendental.powr", fn), Eval ("Groups.times_class.times", fn), Eval ("Groups.minus_class.minus", fn), Eval ("Groups.plus_class.plus", fn),
6.1185 - Thm ("real_unari_minus", "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.occurs_in", fn), Eval ("Prog_Expr.is_num", fn), Eval ("Prog_Expr.ident", fn),
6.1186 - Eval ("Orderings.ord_class.less_eq", fn), Eval ("Orderings.ord_class.less", fn), Thm ("radd_left_cancel_le", "(?k + ?m \<le> ?k + ?n) = (?m \<le> ?n)"), Thm ("order_refl", "?x \<le> ?x"), Thm ("refl", "?t = ?t"),
6.1187 - Thm ("or_false", "(?a \<or> False) = ?a"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("and_false", "(?a \<and> False) = False"), Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("not_false", "(\<not> False) = True"),
6.1188 - Thm ("not_true", "(\<not> True) = False"), Thm ("mult_cross2", "?d \<noteq> 0 \<Longrightarrow> (?a = ?c / ?d) = (?a * ?d = ?c)"), Thm ("mult_cross1", "?b \<noteq> 0 \<Longrightarrow> (?a / ?b = ?c) = (?a = ?b * ?c)"),
6.1189 - Thm ("mult_cross", "?b \<noteq> 0 \<Longrightarrow> ?d \<noteq> 0 \<Longrightarrow> (?a / ?b = ?c / ?d) = (?a * ?d = ?b * ?c)"), Thm ("rat_power", "(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"), Thm ("divide_divide_eq_left", "?a / ?b / ?c = ?a / (?b * ?c)"),
6.1190 - Thm ("real_divide_divide1", "?y \<noteq> 0 \<Longrightarrow> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"), Thm ("times_divide_eq_left", "?b / ?c * ?a = ?b * ?a / ?c"),
6.1191 - Thm ("times_divide_eq_right", "?a * (?b / ?c) = ?a * ?b / ?c"), Thm ("rat_mult", "?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"),
6.1192 - Thm ("rat_add3", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?a + ?b / ?c = (?a * ?c + ?b) / ?c"), Thm ("rat_add2", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"),
6.1193 - Thm ("rat_add1", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?a / ?c + ?b / ?c = (?a + ?b) / ?c"),
6.1194 - Thm ("rat_add", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?d is_num \<Longrightarrow> ?a / ?c + ?b / ?d = (?a * ?d + ?b * ?c) / (?c * ?d)"), Thm ("sym_minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
6.1195 - Eval ("Rings.divide_class.divide", fn), Eval ("HOL.eq", fn), Thm ("plus_leq", "(0 \<le> ?a + ?b) = (- 1 * ?b \<le> ?a)"), Thm ("minus_leq", "(0 \<le> ?a - ?b) = (?b \<le> ?a)"),
6.1196 - ======^^^^^^======
6.1197 - Thm ("rat_leq1", "0 \<noteq> ?b \<Longrightarrow> 0 \<noteq> ?d \<Longrightarrow> (?a / ?b \<le> ?c / ?d) = (?a * ?d \<le> ?b * ?c)"), Thm ("rat_leq2", "0 \<noteq> ?d \<Longrightarrow> (?a \<le> ?c / ?d) = (?a * ?d \<le> ?c)"),
6.1198 - Thm ("rat_leq3", "0 \<noteq> ?b \<Longrightarrow> (?a / ?b \<le> ?c) = (?a \<le> ?b * ?c)")],
6.1199 - scr = Empty_Prog, srls = Empty},
6.1200 - errpatts = [], id = "polyeq_simplify", <<<------------------------------- "polyeq_simplify"
6.1201 - preconds = [], rew_ord = ("termlessI", fn), rules =
6.1202 - [Thm ("real_assoc_1", "?a + (?b + ?c) = ?a + ?b + ?c"), Thm ("real_assoc_2", "?a * (?b * ?c) = ?a * ?b * ?c"), Thm ("real_diff_minus", "?a - ?b = ?a + - 1 * ?b"),
6.1203 - Thm ("real_unari_minus", "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"), Thm ("realpow_multI", "(?r * ?s) \<up> ?n = ?r \<up> ?n * ?s \<up> ?n"), Eval ("Groups.plus_class.plus", fn), Eval ("Groups.minus_class.minus", fn),
6.1204 - Eval ("Groups.times_class.times", fn), Eval ("Rings.divide_class.divide", fn), Eval ("NthRoot.sqrt", fn), Eval ("Transcendental.powr", fn),
6.1205 - ======^^^^^^======
6.1206 - Rls_
6.1207 - (
6.1208 - Repeat
6.1209 - {calc = [], erls =
6.1210 - Repeat ---------vvvvvvvvvvvvvvvvvvvvvvvvv------------------
6.1211 - {calc = [], erls = Empty, errpatts = [], id = "erls_in_reduce_012", preconds = [], rew_ord = ("dummy_ord", fn), rules =
6.1212 - [Eval ("Prog_Expr.is_num", fn), Thm ("not_false", "(\<not> False) = True"), Thm ("not_true", "(\<not> True) = False")], scr = Empty_Prog, srls = Empty},
6.1213 - errpatts = [], id = "reduce_012", <<<---------------------------------- "reduce_012"
6.1214 - preconds = [], rew_ord = ("dummy_ord", fn), rules =
6.1215 - [Thm ("mult_1_left", "1 * ?a = ?a"), Thm ("real_minus_mult_left", "\<not> (?a is_num) \<Longrightarrow> - ?a * ?b = - (?a * ?b)"), Thm ("mult_zero_left", "0 * ?a = 0"), Thm ("add_0_left", "0 + ?a = ?a"),
6.1216 - Thm ("add_0_right", "?a + 0 = ?a"), Thm ("right_minus", "?a + - ?a = 0"), Thm ("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1"), Thm ("real_mult_2_assoc", "?z1.0 + (?z1.0 + ?k) = 2 * ?z1.0 + ?k")],
6.1217 - scr = Empty_Prog, srls = Empty}
6.1218 - )],
6.1219 - scr = Empty_Prog, srls = Empty}: id =
6.1220 - Rule_Def.rule_set*)
6.1221 -\<close> ML \<open>
6.1222 -"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms)) =
6.1223 - (ruls, [], ct, Noap, ruls);
6.1224 -\<close> ML \<open>
6.1225 -val Rule.Thm (thmid, thm) =
6.1226 - (*case*) rul (*of*);
6.1227 -\<close> ML \<open>
6.1228 -val NONE = (*case*) rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1229 - ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*);
6.1230 -\<close> ML \<open>
6.1231 -(* GOON: find a way to find out, why test -- fun adhoc_thm + fun eval_cancel -- gives
6.1232 - Eval.adhoc_thm \<longrightarrow> NONE and above we have ERROR
6.1233 -(*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
6.1234 -
6.1235 - *)
6.1236 -\<close> ML \<open>
6.1237 -\<close> ML \<open>
6.1238 -\<close> ML \<open>
6.1239 -\<close> ML \<open>
6.1240 -\<close> ML \<open>
6.1241 -\<close> ML \<open>
6.1242 -\<close> ML \<open>
6.1243 -\<close> ML \<open>
6.1244 -\<close> ML \<open>
6.1245 -\<close> ML \<open>
6.1246 -\<close> ML \<open>
6.1247 -\<close> ML \<open>
6.1248 -\<close> ML \<open>
6.1249 -\<close> ML \<open>
6.1250 -\<close> ML \<open>
6.1251 -\<close> ML \<open>
6.1252 -\<close> ML \<open>
6.1253 -\<close> ML \<open>
6.1254 -\<close> ML \<open>
6.1255 -\<close> ML \<open>
6.1256 -\<close> ML \<open>
6.1257 -\<close> ML \<open>
6.1258 -\<close> ML \<open>
6.1259 -\<close> ML \<open>
6.1260 -\<close> ML \<open>
6.1261 -\<close> ML \<open>
6.1262 -\<close> ML \<open>
6.1263 -(*/------------------------------- fun rew_once ITERATED BY HAND -----------------------------\*)
6.1264 -\<close> ML \<open>
6.1265 -UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)";
6.1266 -\<close> ML \<open>
6.1267 -val thm = Rule.thm (nth 1 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*)
6.1268 -\<close> ML \<open>
6.1269 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1270 - ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*);
6.1271 -\<close> ML \<open>
6.1272 -val thm = Rule.thm (nth 2 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"
6.1273 - ATTENTION "real_assoc_1" == "real_assoc_2"*)
6.1274 -\<close> ML \<open>
6.1275 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1276 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
6.1277 -\<close> ML \<open>
6.1278 -val thm = Rule.thm (nth 3 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*)
6.1279 -\<close> ML \<open>
6.1280 -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1281 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
6.1282 -\<close> ML \<open>
6.1283 -UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 - 0)) / (2 * 2)"
6.1284 -\<close> ML \<open>
6.1285 -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1286 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
6.1287 -\<close> ML \<open>
6.1288 -UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)"
6.1289 -\<close> ML \<open>
6.1290 -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1291 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
6.1292 -\<close> ML \<open>
6.1293 -UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)"
6.1294 -\<close> ML \<open>
6.1295 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1296 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
6.1297 -\<close> ML \<open>
6.1298 -val thm = Rule.thm (nth 4 ruls); (* = "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"*)
6.1299 -\<close> ML \<open>
6.1300 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1301 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
6.1302 -\<close> ML \<open>
6.1303 -val thm = Rule.thm (nth 5 ruls); (* = "(?r * ?s) \<up> ?n = ?r \<up> ?n * ?s \<up> ?n"*)
6.1304 -\<close> ML \<open>
6.1305 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1306 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
6.1307 -\<close> ML \<open> (* \<longrightarrow> Rule.*)
6.1308 -\<close> ML \<open>
6.1309 -val (cc as (op_, _)) = Rule.eval (nth 6 ruls); (* = "Groups.plus_class.plus"*)
6.1310 -\<close> ML \<open>
6.1311 -val NONE = Eval.adhoc_thm thy cc ct
6.1312 -\<close> ML \<open>
6.1313 -val (cc as (op_, _)) = Rule.eval (nth 7 ruls); (* = "Groups.minus_class.minus"*)
6.1314 -\<close> ML \<open>
6.1315 -val NONE = Eval.adhoc_thm thy cc ct
6.1316 -\<close> ML \<open>
6.1317 -val (cc as (op_, _)) = Rule.eval (nth 8 ruls); (* = "Groups.times_class.times"*)
6.1318 -\<close> ML \<open>
6.1319 -val SOME (_, thm') = Eval.adhoc_thm thy cc ct
6.1320 -\<close> ML \<open>
6.1321 -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1322 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
6.1323 -\<close> ML \<open>
6.1324 - "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)";
6.1325 -UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)"
6.1326 -\<close> ML \<open>
6.1327 -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1328 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
6.1329 -\<close> ML \<open>
6.1330 -UnparseC.term ct = "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)"
6.1331 -\<close> ML \<open>
6.1332 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
6.1333 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
6.1334 -\<close> ML \<open>
6.1335 -val (cc as (op_, _)) = Rule.eval (nth 9 ruls); (* = "Rings.divide_class.divide"*)
6.1336 -\<close> ML \<open>
6.1337 -val NONE = Eval.adhoc_thm thy cc ct
6.1338 -\<close> ML \<open>
6.1339 -val (cc as (op_, _)) = Rule.eval (nth 10 ruls); (* = "NthRoot.sqrt"*)
6.1340 -\<close> ML \<open>
6.1341 -val NONE = Eval.adhoc_thm thy cc ct
6.1342 -\<close> ML \<open>
6.1343 -val (cc as (op_, _)) = Rule.eval (nth 11 ruls); (* = "Transcendental.powr"*)
6.1344 -\<close> ML \<open>
6.1345 -val NONE = Eval.adhoc_thm thy cc ct
6.1346 -\<close> ML \<open>
6.1347 -val rls' = Rule.rls (nth 12 ruls); (* = "reduce_012"*)
6.1348 -\<close> ML \<open>
6.1349 -val SOME (ct, []) = rewrite__set_ thy (i + 1) put_asm bdv rls' ct
6.1350 -\<close> ML \<open>
6.1351 - "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)";
6.1352 -UnparseC.term ct = "x = (- 1 + sqrt 1) / (2 * 2) \<or> x = (- 1 + - 1 * sqrt 1) / (2 * 2)"
6.1353 -\<close> ML \<open>
6.1354 -length ruls = 12;
6.1355 -(*========== now are further iterations to come, and there is the strange error ===============*)
6.1356 -\<close> ML \<open>
6.1357 -\<close> ML \<open>
6.1358 -\<close> ML \<open>
6.1359 -\<close> ML \<open>
6.1360 -\<close> ML \<open>
6.1361 -\<close> ML \<open>
6.1362 -\<close> ML \<open>
6.1363 -\<close> ML \<open>
6.1364 -\<close> ML \<open>
6.1365 -\<close> ML \<open>
6.1366 -\<close> ML \<open>
6.1367 -\<close> ML \<open>
6.1368 -\<close> ML \<open>
6.1369 -\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
6.1370 -\<close> text \<open>
6.1371 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1372 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1373 -case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
6.1374 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
6.1375 -
6.1376 -\<close> ML \<open>
6.1377 -(*EP-//*)
6.1378 -val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.1379 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.1380 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.1381 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.1382 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1383 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1384 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1385 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1386 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1387 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1388 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1389 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.1390 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
6.1391 -
6.1392 -
6.1393 -\<close> ML \<open>
6.1394 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
6.1395 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
6.1396 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
6.1397 -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
6.1398 -see --- val rls = calculate_RootRat > calculate_Rational ---
6.1399 -calculate_RootRat was a TODO with 2002, requires re-design.
6.1400 -see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
6.1401 -*)
6.1402 - val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
6.1403 +"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
6.1404 +"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
6.1405 +"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
6.1406 + val fmz = ["equality (a*b - (a+b)*x + x \<up> 2 = 0)",
6.1407 "solveFor x", "solutions L"];
6.1408 val (dI',pI',mI') =
6.1409 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
6.1410 ["PolyEq", "complete_square"]);
6.1411 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.1412 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1413 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1414 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1415 -
6.1416 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1417 -(*Apply_Method ("PolyEq", "complete_square")*)
6.1418 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1419 -(*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
6.1420 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1421 -(*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
6.1422 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1423 -(*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
6.1424 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1425 -(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
6.1426 - 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
6.1427 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1428 -(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
6.1429 - - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
6.1430 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1431 -(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
6.1432 - - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
6.1433 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1434 -(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
6.1435 - x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
6.1436 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1437 -(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
6.1438 - x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
6.1439 - NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
6.1440 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1441 -(*"x = - 2 | x = 4" nxt = Or_to_List*)
6.1442 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1443 -(*"[x = - 2, x = 4]" nxt = Check_Postcond*)
6.1444 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1445 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1446 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1447 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1448 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1449 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1450 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
6.1451 -(* FIXXXME
6.1452 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
6.1453 - | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
6.1454 -*)
6.1455 -if f2str f =
6.1456 - "[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))]"
6.1457 -(*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
6.1458 -then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
6.1459 +(*WN.2.5.03 TODO FIXME Matthias ?
6.1460 + case f of
6.1461 + Form'
6.1462 + (Test_Out.FormKF
6.1463 + (~1,EdUndef,0,Nundef,
6.1464 + "[x = (a + b) / 2 + - 1 * sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b)]"))
6.1465 + => ()
6.1466 + | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x \<up> 2 = 0";
6.1467 + this will be simplified [x = a, x = b] to by Factor.ML*)
6.1468
6.1469
6.1470 \<close> ML \<open>
6.1471 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
6.1472 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
6.1473 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
6.1474 -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
6.1475 -see --- val rls = calculate_RootRat > calculate_Rational ---*)
6.1476 -val thy = @{theory PolyEq};
6.1477 -val ctxt = Proof_Context.init_global thy;
6.1478 -val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
6.1479 -val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
6.1480 -
6.1481 -\<close> ML \<open>
6.1482 -val rls = complete_square;
6.1483 -val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
6.1484 -\<close> ML \<open>
6.1485 -if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2"
6.1486 -then () else error "rls complete_square CHANGED";
6.1487 -
6.1488 -\<close> ML \<open>
6.1489 -val thm = @{thm square_explicit1};
6.1490 -val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
6.1491 -\<close> ML \<open>
6.1492 -if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
6.1493 -then () else error "thm square_explicit1 CHANGED";
6.1494 -
6.1495 -\<close> ML \<open>
6.1496 -val thm = @{thm root_plus_minus};
6.1497 -val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
6.1498 -\<close> ML \<open>
6.1499 -if UnparseC.term t =
6.1500 -"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
6.1501 -then () else error "thm root_plus_minus CHANGED";
6.1502 -
6.1503 -\<close> ML \<open>
6.1504 -(*the thm bdv_explicit2* here required to be constrained to ::real*)
6.1505 -val thm = @{thm bdv_explicit2};
6.1506 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
6.1507 -\<close> ML \<open>
6.1508 -if UnparseC.term t =
6.1509 -"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
6.1510 -then () else error "thm bdv_explicit2 CHANGED";
6.1511 -
6.1512 -\<close> ML \<open>
6.1513 -val thm = @{thm bdv_explicit3};
6.1514 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
6.1515 -\<close> ML \<open>
6.1516 -if UnparseC.term t =
6.1517 -"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
6.1518 -then () else error "thm bdv_explicit3 CHANGED";
6.1519 -
6.1520 -\<close> ML \<open>
6.1521 -val thm = @{thm bdv_explicit2};
6.1522 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
6.1523 -\<close> ML \<open>
6.1524 -if UnparseC.term t =
6.1525 -"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
6.1526 -then () else error "thm bdv_explicit2 CHANGED";
6.1527 -
6.1528 -\<close> ML \<open>
6.1529 -val rls = calculate_RootRat;
6.1530 -val SOME (t,asm) = rewrite_set_ thy true rls t;
6.1531 -\<close> ML \<open>
6.1532 -if UnparseC.term t =
6.1533 - "- 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))"
6.1534 -(*"- 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*)
6.1535 -then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
6.1536 -(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
6.1537 -
6.1538 -
6.1539 -\<close> ML \<open>
6.1540 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
6.1541 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
6.1542 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
6.1543 -"---- test the erls ----";
6.1544 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
6.1545 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
6.1546 - val t' = UnparseC.term t;
6.1547 - (*if t'= \<^const_name>\<open>True\<close> then ()
6.1548 - else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
6.1549 -(* *)
6.1550 - val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
6.1551 +"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
6.1552 +"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
6.1553 +"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
6.1554 + val fmz = ["equality (-64 + x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
6.1555 "solveFor x", "solutions L"];
6.1556 val (dI',pI',mI') =
6.1557 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
6.1558 ["PolyEq", "complete_square"]);
6.1559 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.1560 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1561 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1562 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1563 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1564 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1565 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1566 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1567 - (*Apply_Method ("PolyEq", "complete_square")*)
6.1568 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
6.1569 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1570 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1571 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1572 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1573 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1574 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1575 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1576 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1577 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1578 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1579 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1580 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
6.1581 +(*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = - 1 * sqrt (0 - -64)]"
6.1582 + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
6.1583 + | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
6.1584 +*)
6.1585
6.1586 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
6.1587 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
6.1588 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
6.1589 - val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
6.1590 +\<close> ML \<open>
6.1591 +"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
6.1592 +"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
6.1593 +"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
6.1594 +val fmz = ["equality (- 147 + 3*x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
6.1595 "solveFor x", "solutions L"];
6.1596 - val (dI',pI',mI') =
6.1597 +val (dI',pI',mI') =
6.1598 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
6.1599 ["PolyEq", "complete_square"]);
6.1600 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.1601 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1602 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1603 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1604 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1605 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1606 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1607 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1608 - (*Apply_Method ("PolyEq", "complete_square")*)
6.1609 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1610 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1611 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1612 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1613 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1614 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1615 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1616 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1617 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1618 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1619 -(* FIXXXXME n1.,
6.1620 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
6.1621 - | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
6.1622 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1623 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1624 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1625 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1626 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1627 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1628 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1629 +(*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]"
6.1630 + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
6.1631 + | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
6.1632 *)
6.1633 +if f2str f = "[x = sqrt (0 - - 49), x = - 1 * sqrt (0 - - 49)]" then ()
6.1634 +else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
6.1635 +
6.1636
6.1637 \<close> ML \<open>
6.1638 -\<close>
6.1639 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
6.1640 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
6.1641 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
6.1642 +(*EP- 17 Schalk_I_p86_n5*)
6.1643 +val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"];
6.1644 +(* Refine.refine fmz ["univariate", "equation"];
6.1645 +*)
6.1646 +val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
6.1647 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.1648 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1649 +(* val nxt =
6.1650 + ("Model_Problem",
6.1651 + Model_Problem ["normalise", "polynomial", "univariate", "equation"])
6.1652 + : string * tac*)
6.1653 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1654 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1655 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1656 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1657 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1658 +(* val nxt =
6.1659 + ("Subproblem",
6.1660 + Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))
6.1661 + : string * tac *)
6.1662 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1663 +(*val nxt =
6.1664 + ("Model_Problem",
6.1665 + Model_Problem ["degree_1", "polynomial", "univariate", "equation"])
6.1666 + : string * tac *)
6.1667 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1668 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1669 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1670 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1671 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1672 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1673 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1674 +case f of Test_Out.FormKF "[x = 2]" => ()
6.1675 + | _ => error "polyeq.sml: diff.behav. in [x = 2]";
6.1676
6.1677 -section \<open>===================================================================================\<close>
6.1678 -ML \<open>
6.1679 +
6.1680 \<close> ML \<open>
6.1681 +"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
6.1682 +"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
6.1683 +"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
6.1684 +(*is in rlang.sml, too*)
6.1685 +val fmz = ["equality ((x+1)*(x+2) - (3*x - 2) \<up> 2=(2*x - 1) \<up> 2+(3*x - 1)*(x+1))",
6.1686 + "solveFor x", "solutions L"];
6.1687 +val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
6.1688 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.1689 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate", "equation"])*)
6.1690 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1691 +(* val nxt =
6.1692 + ("Model_Problem",
6.1693 + Model_Problem ["normalise", "polynomial", "univariate", "equation"])
6.1694 + : string * tac *)
6.1695 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1696 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1697 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1698 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1699 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1700 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1701 +(* val nxt =
6.1702 + ("Subproblem",
6.1703 + Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))
6.1704 + : string * tac*)
6.1705 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1706 +(*val nxt =
6.1707 + ("Model_Problem",
6.1708 + Model_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])
6.1709 + : string * tac*)
6.1710 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1711 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1712 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1713 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1714 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1715 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1716 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1717 +case f of Test_Out.FormKF "[x = 2 / 15, x = 1]" => ()
6.1718 + | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
6.1719 +
6.1720 +
6.1721 +" -4 + x \<up> 2 =0 ";
6.1722 +" -4 + x \<up> 2 =0 ";
6.1723 +" -4 + x \<up> 2 =0 ";
6.1724 +val fmz = ["equality ( -4 + x \<up> 2 =0)", "solveFor x", "solutions L"];
6.1725 +(* val fmz = ["equality (1 + x \<up> 2 =0)", "solveFor x", "solutions L"];*)
6.1726 +(*val fmz = ["equality (0 =0)", "solveFor x", "solutions L"];*)
6.1727 +val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
6.1728 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.1729 +
6.1730 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1731 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1732 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1733 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1734 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1735 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1736 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.1737 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
6.1738 + | _ => error "polyeq.sml: diff.behav. in [x = 2, x = - 2]";
6.1739 +
6.1740 +\<close> ML \<open>
6.1741 +"----------- rls make_polynomial_in ------------------------------";
6.1742 +"----------- rls make_polynomial_in ------------------------------";
6.1743 +"----------- rls make_polynomial_in ------------------------------";
6.1744 +val thy = @{theory};
6.1745 +(*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
6.1746 +(*WN.19.3.03 ---v-*)
6.1747 +(*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");
6.1748 +val t = TermC.str2term "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
6.1749 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
6.1750 +if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then ()
6.1751 +else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)";
6.1752 +"- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0";
6.1753 +(*WN.19.3.03 ---^-*)
6.1754 +
6.1755 +(*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p");
6.1756 +val t = TermC.str2term "y \<up> 2 + - 2 * (x * p) = 0";
6.1757 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
6.1758 +if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then ()
6.1759 +else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)";
6.1760 +
6.1761 +(*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2");
6.1762 +val t = TermC.str2term
6.1763 +"A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1 * (x1 * (y2 * (1 / 2))) + - 1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + - 1 * (y3 * (1 / 2 * x2)) = 0";
6.1764 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
6.1765 +if UnparseC.term t' =
6.1766 +"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) +\n- 1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n- 1 * y3 * (1 / 2) * x2 =\n0"
6.1767 +then ()
6.1768 +else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
6.1769 +"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";
6.1770 +
6.1771 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
6.1772 +if UnparseC.term t' =
6.1773 +"A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + - 1 * x1 * y2 / 2 + - 1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n- 1 * y3 * x2 / 2 =\n0"
6.1774 +then ()
6.1775 +else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
6.1776 +"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) + - 1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - 1 * y3 * (1 / 2)) * x2 = 0";
6.1777 +
6.1778 +(*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a");
6.1779 +val t = TermC.str2term
6.1780 +"A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0";
6.1781 +val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
6.1782 +(* the invisible parentheses are as expected *)
6.1783 +
6.1784 +val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";
6.1785 +Rewrite.trace_on:= false; (*true false*)
6.1786 +rewrite_set_ thy false expand_binoms t;
6.1787 +Rewrite.trace_on:=false; (*true false*)
6.1788 +
6.1789 +
6.1790 +\<close> ML \<open>
6.1791 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
6.1792 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
6.1793 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
6.1794 +reset_states ();
6.1795 +CalcTree
6.1796 +[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"],
6.1797 + ("PolyEq",["univariate", "equation"],["no_met"]))];
6.1798 +Iterator 1;
6.1799 +moveActiveRoot 1;
6.1800 +
6.1801 +autoCalculate 1 CompleteCalc;
6.1802 +val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.1803 +interSteps 1 ([1],Res)
6.1804 +(*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);
6.1805 +
6.1806 +
6.1807 +\<close> ML \<open>
6.1808 +"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
6.1809 +"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
6.1810 +"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
6.1811 +val t = TermC.str2term "-6 * x + 5 * x \<up> 2 = (0::real)";
6.1812 +val subst = [(TermC.str2term "(bdv::real)", TermC.str2term "(x::real)")];
6.1813 +val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
6.1814 +(* steps in rls d2_polyeq_bdv_only_simplify:*)
6.1815 +
6.1816 +(*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
6.1817 +t |> UnparseC.term; t |> TermC.atomty;
6.1818 +val thm = @{thm d2_prescind1};
6.1819 +thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
6.1820 +val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
6.1821 +
6.1822 +(*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", ""))
6.1823 + --> x = 0 | -6 + 5 * x = 0*)
6.1824 +t' |> UnparseC.term; t' |> TermC.atomty;
6.1825 +val thm = @{thm d2_reduce_equation1};
6.1826 +thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
6.1827 +val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
6.1828 +(* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
6.1829 + instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
6.1830 +*)
6.1831 +if UnparseC.term t'' = "x = 0 \<or> - 6 + 5 * x = 0" then ()
6.1832 +else error "rls d2_polyeq_bdv_only_simplify broken";
6.1833 \<close> ML \<open>
6.1834 \<close> ML \<open>
6.1835 \<close>