1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 23 12:33:10 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 23 14:24:06 2021 +0200
1.3 @@ -2,14 +2,14 @@
1.4 testexamples for PolyEq, poynomial equations and equational systems
1.5 Author: Richard Lang 2003
1.6 (c) due to copyright terms
1.7 -WN030609: some expls dont work due to unfinished handling of 'expanded terms';
1.8 - others marked with TODO have to be checked, too.
1.9 +
1.10 +Separation into polyeq-1.sml and polyeq-1a.sml due to
1.11 *)
1.12
1.13 "-----------------------------------------------------------------";
1.14 "table of contents -----------------------------------------------";
1.15 "-----------------------------------------------------------------";
1.16 -"------ polyeq- 1.sml ---------------------------------------------";
1.17 +"------ polyeq-1.sml ---------------------------------------------";
1.18 "----------- tests on predicates in problems ---------------------";
1.19 "----------- test matching problems ------------------------------";
1.20 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.21 @@ -22,6 +22,7 @@
1.22 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.23 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.24 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.25 +"------ polyeq- 2.sml ---------------------------------------------";
1.26 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.27 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.28 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.29 @@ -50,6 +51,7 @@
1.30 "----------- tests on predicates in problems ---------------------";
1.31 "----------- tests on predicates in problems ---------------------";
1.32 "----------- tests on predicates in problems ---------------------";
1.33 +val thy = @{theory};
1.34 Rewrite.trace_on:=false; (*true false*)
1.35
1.36 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
1.37 @@ -323,16 +325,16 @@
1.38 (** )end;( *local*)
1.39
1.40 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
1.41 -if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?";
1.42 +if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then () else error "still GREATER?";
1.43
1.44 val x = TermC.str2term "x ::real";
1.45
1.46 val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
1.47 -if 2006 = size_of_term' 1 true x t1
1.48 +if 2006 = size_of_term' 1 false(*true*) x t1
1.49 then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
1.50
1.51 val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
1.52 -if 3004 = size_of_term' 1 true x t2
1.53 +if 3004 = size_of_term' 1 false(*true*) x t2
1.54 then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
1.55
1.56
1.57 @@ -348,23 +350,23 @@
1.58 val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
1.59 val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
1.60
1.61 -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
1.62 +if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then ()
1.63 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
1.64
1.65 -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
1.66 +if ord_make_polynomial_in false(*true*) thy substa (x1,x2) = true(*LESS *) then ()
1.67 else error "termorder.sml diff.behav ord_make_polynomial_in #2";
1.68
1.69 -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
1.70 +if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then ()
1.71 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
1.72
1.73 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
1.74 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
1.75 - ord_make_polynomial_in true thy substx (aa, bb);
1.76 + ord_make_polynomial_in false(*true*) thy substx (aa, bb);
1.77 true; (* => LESS *)
1.78
1.79 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
1.80 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
1.81 - ord_make_polynomial_in true thy substa (aa, bb);
1.82 + ord_make_polynomial_in false(*true*) thy substa (aa, bb);
1.83 false; (* => GREATER *)
1.84
1.85 (* und nach dem Re-engineering der Termorders in den 'rulesets'
1.86 @@ -909,7 +911,7 @@
1.87 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
1.88
1.89 (*EP- 16*)
1.90 -val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.91 +val fmz = ["equality (x + 2 * x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];
1.92 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.93 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.94 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.95 @@ -917,7 +919,12 @@
1.96 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.97 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.98 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.99 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.100 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.101 +
1.102 +(*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f;
1.103 +(*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt
1.104 +
1.105 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)
1.106 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.107 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.108 case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
1.109 @@ -991,7 +998,7 @@
1.110 | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
1.111 *)
1.112 if f2str f =
1.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))]"
1.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))]"
1.115 (*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
1.116 then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
1.117
1.118 @@ -999,7 +1006,7 @@
1.119 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.120 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.121 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.122 -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1.123 +(*stopped due to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1.124 see --- val rls = calculate_RootRat > calculate_Rational ---*)
1.125 val thy = @{theory PolyEq};
1.126 val ctxt = Proof_Context.init_global thy;
1.127 @@ -1008,37 +1015,43 @@
1.128
1.129 val rls = complete_square;
1.130 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
1.131 -UnparseC.term t = "-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2";
1.132 +if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2"
1.133 +then () else error "rls complete_square CHANGED";
1.134
1.135 -val thm = ThmC.numerals_to_Free @{thm square_explicit1};
1.136 +val thm = @{thm square_explicit1};
1.137 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
1.138 -UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8";
1.139 +if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
1.140 +then () else error "thm square_explicit1 CHANGED";
1.141
1.142 -val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
1.143 +val thm = @{thm root_plus_minus};
1.144 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1.145 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.146 - "\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
1.147 +if UnparseC.term t =
1.148 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
1.149 +then () else error "thm root_plus_minus CHANGED";
1.150
1.151 (*the thm bdv_explicit2* here required to be constrained to ::real*)
1.152 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1.153 +val thm = @{thm bdv_explicit2};
1.154 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.155 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.156 - "\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
1.157 +if UnparseC.term t =
1.158 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
1.159 +then () else error "thm bdv_explicit2 CHANGED";
1.160
1.161 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
1.162 +val thm = @{thm bdv_explicit3};
1.163 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.164 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.165 - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
1.166 +if UnparseC.term t =
1.167 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
1.168 +then () else error "thm bdv_explicit3 CHANGED";
1.169
1.170 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1.171 +val thm = @{thm bdv_explicit2};
1.172 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.173 -UnparseC.term t = "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
1.174 - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
1.175 +if UnparseC.term t =
1.176 +"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
1.177 +then () else error "thm bdv_explicit2 CHANGED";
1.178
1.179 val rls = calculate_RootRat;
1.180 val SOME (t,asm) = rewrite_set_ thy true rls t;
1.181 if UnparseC.term t =
1.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))"
1.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))"
1.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*)
1.185 then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1.186 (*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)