1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/IsacKnowledge/polyeq.sml Thu Aug 12 11:02:32 2010 +0200
1.3 @@ -0,0 +1,1178 @@
1.4 +(* testexamples for PolyEq, poynomial equations and equational systems
1.5 + author: Richard Lang
1.6 + 2003
1.7 + (c) due to copyright terms
1.8 +
1.9 +use"../smltest/IsacKnowledge/polyeq.sml";
1.10 +use"polyeq.sml";
1.11 +
1.12 +WN030609: some expls dont work due to unfinished handling of 'expanded terms';
1.13 + others marked with TODO have to be checked, too.
1.14 +*)
1.15 +
1.16 +"-----------------------------------------------------------------";
1.17 +"table of contents -----------------------------------------------";
1.18 +(*WN060608 some ----- are not in this table*)
1.19 +"-----------------------------------------------------------------";
1.20 +"----------- tests on predicates in problems ---------------------";
1.21 +"----------- test matching problems --------------------------0---";
1.22 +"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.23 +"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.24 +"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.25 +"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.26 +"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.27 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.28 +"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.29 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.30 +"-----------------------------------------------------------------";
1.31 +"-----------------------------------------------------------------";
1.32 +"-----------------------------------------------------------------";
1.33 +
1.34 +val c = [];
1.35 +
1.36 +"----------- tests on predicates in problems ---------------------";
1.37 +"----------- tests on predicates in problems ---------------------";
1.38 +"----------- tests on predicates in problems ---------------------";
1.39 +(*
1.40 + Compiler.Control.Print.printDepth:=5; (*4 default*)
1.41 + trace_rewrite:=true;
1.42 + trace_rewrite:=false;
1.43 +*)
1.44 + val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
1.45 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t1;
1.46 + if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
1.47 + else raise error "polyeq.sml: diff.behav. in lhs";
1.48 +
1.49 +
1.50 + val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
1.51 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2;
1.52 + if (term2str t) = "True" then ()
1.53 + else raise error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.54 +
1.55 + val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
1.56 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0;
1.57 + if (term2str t) = "False" then ()
1.58 + else raise error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.59 +
1.60 +
1.61 + val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
1.62 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.63 + if (term2str t) = "True" then ()
1.64 + else raise error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.65 +
1.66 +
1.67 + val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
1.68 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
1.69 + if (term2str t) = "True" then ()
1.70 + else raise error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.71 +
1.72 +
1.73 + val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
1.74 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6;
1.75 + if (term2str t) = "True" then ()
1.76 + else raise error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.77 +
1.78 + val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.79 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.80 + if (term2str t) = "True" then ()
1.81 + else raise error "polyeq.sml: diff.behav. in has_degree_in_in";
1.82 +
1.83 +
1.84 + val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
1.85 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.86 + if (term2str t) = "False" then ()
1.87 + else raise error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.88 +
1.89 + val t4 = (term_of o the o (parse thy))
1.90 + "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
1.91 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
1.92 + if (term2str t) = "False" then ()
1.93 + else raise error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.94 +
1.95 +
1.96 + val t5 = (term_of o the o (parse thy))
1.97 + "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.98 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5;
1.99 + if (term2str t) = "True" then ()
1.100 + else raise error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
1.101 +
1.102 +
1.103 +"----------- test matching problems --------------------------0---";
1.104 +"----------- test matching problems --------------------------0---";
1.105 +"----------- test matching problems --------------------------0---";
1.106 + val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.107 + val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
1.108 + get_pbt ["expanded","univariate","equation"];
1.109 +
1.110 + match_pbl fmz (get_pbt ["expanded","univariate","equation"]);
1.111 + (*Matches'
1.112 + {Find=[Correct "solutions L"],
1.113 + Given=[Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)",
1.114 + Correct "solveFor x"],Relate=[],
1.115 + Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
1.116 + Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],With=[]}
1.117 + *)
1.118 + match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]);
1.119 + (*Matches'
1.120 + {Find=[Correct "solutions L"],
1.121 + Given=[Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)",
1.122 + Correct "solveFor x"],Relate=[],
1.123 + Where=[Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x =!= 2"],
1.124 + With=[]}*)
1.125 +
1.126 +"-------------------- test thm's degree_0 --------------------------------------";
1.127 +"-------------------- test thm's degree_0 --------------------------------------";
1.128 +"----- d0_false ------";
1.129 +(*EP*)
1.130 +val fmz = ["equality ( 1 = 0)", "solveFor x","solutions L"];
1.131 +val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"],
1.132 + ["PolyEq","solve_d0_polyeq_equation"]);
1.133 +(*val p = e_pos';
1.134 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.135 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.136 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.137 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.138 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.139 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.140 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.141 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.142 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.143 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
1.144 + | _ => raise error "polyeq.sml: diff.behav. in 1 = 0 -> []";
1.145 +
1.146 +"----- d0_true ------";
1.147 +(*EP-7*)
1.148 +val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"];
1.149 +val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"],
1.150 + ["PolyEq","solve_d0_polyeq_equation"]);
1.151 +(*val p = e_pos'; val c = [];
1.152 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.153 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.154 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.155 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.156 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.157 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.158 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.159 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.160 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.161 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
1.162 + | _ => raise error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
1.163 +
1.164 +"-------------------- test thm's degree_2 ------------------------------------------";
1.165 +"-------------------- test thm's degree_2 ------------------------------------------";
1.166 +
1.167 +"-------------------- test thm's d2_pq_formulsxx[_neg]-----";
1.168 +"-------------------- test thm's d2_pq_formulsxx[_neg]-----";
1.169 +"-------------------- test thm's d2_pq_formulsxx[_neg]-----";
1.170 +
1.171 +"----- d2_pqformula1 ------!!!!";
1.172 +val fmz = ["equality (-2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.173 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.174 +(*val p = e_pos'; val c = [];
1.175 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.176 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.177 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.178 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.179 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.180 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.181 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.182 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.183 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.184 +(*### or2list _ | _
1.185 + ([3],Res) "x = 2 | x = -1" Or_to_List*)
1.186 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.187 +(*### or2list _ | _
1.188 + ### applicable_in Check_elementwise: --> ([x = 2, x = -1], [])
1.189 + ([4],Res) "[x = 2, x = -1]" Check_elementwise "Assumptions"*)
1.190 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.191 +(*### applicable_in Check_elementwise: --> ([x = 2, x = -1], [])
1.192 + ([5],Res) "[x = 2, x = -1]" Check_Postcond*)
1.193 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.194 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
1.195 + | _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
1.196 +
1.197 +"----- d2_pqformula1_neg ------";
1.198 +(*EP-8*)
1.199 +val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.200 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.201 +(*val p = e_pos'; val c = [];
1.202 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.203 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.204 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.205 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.206 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.207 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.208 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.209 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.210 +(*### or2list False
1.211 + ([1],Res) False Or_to_List)*)
1.212 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.213 +(*### or2list False
1.214 + ([2],Res) [] Check_elementwise "Assumptions"*)
1.215 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.216 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.217 +val asm = get_assumptions_ pt p;
1.218 +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
1.219 +else raise error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
1.220 +
1.221 +"----- d2_pqformula2 ------";
1.222 +val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.223 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.224 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.225 +(*val p = e_pos'; val c = [];
1.226 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.227 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.228 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.229 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.230 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.231 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.232 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.233 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.234 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.235 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.236 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.237 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
1.238 + | _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
1.239 +
1.240 +
1.241 +"----- d2_pqformula2_neg ------";
1.242 +val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.243 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.244 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.245 +(*val p = e_pos'; val c = [];
1.246 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.247 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.248 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.249 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.250 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.251 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.252 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.253 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.254 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.255 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.256 +"TODO 2 +(-1)*x + 1*x^^^2 = 0";
1.257 +"TODO 2 +(-1)*x + 1*x^^^2 = 0";
1.258 +"TODO 2 +(-1)*x + 1*x^^^2 = 0";
1.259 +
1.260 +
1.261 +"----- d2_pqformula3 ------";
1.262 +(*EP-9*)
1.263 +val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.264 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.265 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.266 +(*val p = e_pos'; val c = [];
1.267 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.268 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.269 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.270 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.271 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.272 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.273 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.274 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.275 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.276 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.277 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.278 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
1.279 + | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
1.280 +
1.281 +"----- d2_pqformula3_neg ------";
1.282 +val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.283 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.284 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.285 +(*val p = e_pos'; val c = [];
1.286 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.287 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.288 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.289 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.290 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.291 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.292 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.293 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.294 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.295 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.296 +"TODO 2 + x + x^^^2 = 0";
1.297 +"TODO 2 + x + x^^^2 = 0";
1.298 +"TODO 2 + x + x^^^2 = 0";
1.299 +
1.300 +
1.301 +"----- d2_pqformula4 ------";
1.302 +val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.303 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.304 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.305 +(*val p = e_pos'; val c = [];
1.306 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.307 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.308 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.309 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.310 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.311 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.312 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.313 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.314 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.315 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.316 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.317 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
1.318 + | _ => raise error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
1.319 +
1.320 +"----- d2_pqformula4_neg ------";
1.321 +val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.322 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.323 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.324 +(*val p = e_pos'; val c = [];
1.325 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.326 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.327 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.328 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.329 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.330 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.331 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.332 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.333 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.334 +"TODO 2 + x + 1*x^^^2 = 0";
1.335 +"TODO 2 + x + 1*x^^^2 = 0";
1.336 +"TODO 2 + x + 1*x^^^2 = 0";
1.337 +
1.338 +"----- d2_pqformula5 ------";
1.339 +val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.340 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.341 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.342 +(*val p = e_pos'; val c = [];
1.343 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.344 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.345 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.346 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.347 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.348 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.349 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.350 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.351 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.352 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.353 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.354 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.355 + | _ => raise error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
1.356 +
1.357 +"----- d2_pqformula6 ------";
1.358 +val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.359 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.360 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.361 +(*val p = e_pos'; val c = [];
1.362 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.363 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.364 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.365 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.366 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.367 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.368 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.369 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.370 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.371 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.372 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.373 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.374 + | _ => raise error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.375 +
1.376 +"----- d2_pqformula7 ------";
1.377 +(*EP-10*)
1.378 +val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
1.379 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.380 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.381 +(*val p = e_pos'; val c = [];
1.382 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.383 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.384 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.385 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.386 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.387 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.388 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.389 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.390 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.391 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.392 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.393 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.394 + | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.395 +
1.396 +"----- d2_pqformula8 ------";
1.397 +val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.398 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.399 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.400 +(*val p = e_pos'; val c = [];
1.401 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.402 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.403 +
1.404 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.405 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.406 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.407 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.408 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.409 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.410 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.411 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.412 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.413 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.414 + | _ => raise error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.415 +
1.416 +"----- d2_pqformula9 ------";
1.417 +val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.418 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.419 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.420 +(*val p = e_pos'; val c = [];
1.421 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.422 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.423 +
1.424 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.425 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.426 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.427 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.428 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.429 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.430 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.431 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.432 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.433 + | _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.434 +
1.435 +
1.436 +"----- d2_pqformula10_neg ------";
1.437 +val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.438 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.439 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.440 +(*val p = e_pos'; val c = [];
1.441 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.442 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.443 +
1.444 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.445 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.446 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.447 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.448 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.449 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.450 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.451 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.452 +"TODO 4 + x^^^2 = 0";
1.453 +"TODO 4 + x^^^2 = 0";
1.454 +"TODO 4 + x^^^2 = 0";
1.455 +
1.456 +"----- d2_pqformula10 ------";
1.457 +val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.458 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.459 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.460 +(*val p = e_pos'; val c = [];
1.461 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.462 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.463 +
1.464 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.465 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.466 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.467 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.468 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.469 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.470 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.471 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.472 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.473 + | _ => raise error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
1.474 +
1.475 +"----- d2_pqformula9_neg ------";
1.476 +val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.477 +val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.478 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.479 +(*val p = e_pos'; val c = [];
1.480 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.481 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.482 +
1.483 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.484 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.485 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.486 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.487 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.488 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.489 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.490 +"TODO 4 + 1*x^^^2 = 0";
1.491 +"TODO 4 + 1*x^^^2 = 0";
1.492 +"TODO 4 + 1*x^^^2 = 0";
1.493 +
1.494 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.495 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.496 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.497 +
1.498 +val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.499 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.500 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.501 +(*val p = e_pos'; val c = [];
1.502 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.503 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.504 +
1.505 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.506 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.507 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.508 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.509 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.510 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.511 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.512 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.513 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
1.514 + | _ => raise error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
1.515 +
1.516 +val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.517 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.518 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.519 +(*val p = e_pos'; val c = [];
1.520 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.521 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.522 +
1.523 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.524 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.525 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.526 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.527 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.528 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.529 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.530 +"TODO 1 +(-1)*x + 2*x^^^2 = 0";
1.531 +"TODO 1 +(-1)*x + 2*x^^^2 = 0";
1.532 +"TODO 1 +(-1)*x + 2*x^^^2 = 0";
1.533 +
1.534 +(*EP-11*)
1.535 +val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.536 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.537 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.538 +(*val p = e_pos'; val c = [];
1.539 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.540 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.541 +
1.542 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.543 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.544 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.545 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.546 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.547 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.548 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.549 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.550 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
1.551 + | _ => raise error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
1.552 +
1.553 +val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.554 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.555 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.556 +(*val p = e_pos'; val c = [];
1.557 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.558 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.559 +
1.560 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.561 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.562 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.563 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.564 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.565 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.566 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.567 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.568 +"TODO 1 + x + 2*x^^^2 = 0";
1.569 +"TODO 1 + x + 2*x^^^2 = 0";
1.570 +"TODO 1 + x + 2*x^^^2 = 0";
1.571 +
1.572 +val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.573 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.574 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.575 +(*val p = e_pos'; val c = [];
1.576 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.577 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.578 +
1.579 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.580 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.581 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.582 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.583 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.584 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.585 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.586 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.587 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
1.588 + | _ => raise error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
1.589 +
1.590 +val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.591 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.592 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.593 +(*val p = e_pos'; val c = [];
1.594 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.595 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.596 +
1.597 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.598 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.599 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.600 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.601 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.602 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.603 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.604 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.605 +"TODO 2 + 1*x + x^^^2 = 0";
1.606 +"TODO 2 + 1*x + x^^^2 = 0";
1.607 +"TODO 2 + 1*x + x^^^2 = 0";
1.608 +
1.609 +(*EP-12*)
1.610 +val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.611 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.612 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.613 +(*val p = e_pos'; val c = [];
1.614 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.615 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.616 +
1.617 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.618 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.619 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.620 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.621 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.622 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.623 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.624 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.625 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
1.626 + | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
1.627 +
1.628 +val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.629 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.630 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.631 +(*val p = e_pos'; val c = [];
1.632 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.633 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.634 +
1.635 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.636 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.637 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.638 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.639 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.640 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.641 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.642 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.643 +"TODO 2 + x + x^^^2 = 0";
1.644 +"TODO 2 + x + x^^^2 = 0";
1.645 +"TODO 2 + x + x^^^2 = 0";
1.646 +
1.647 +(*EP-13*)
1.648 +val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.649 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.650 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.651 +(*val p = e_pos'; val c = [];
1.652 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.653 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.654 +
1.655 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.656 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.657 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.658 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.659 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.660 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.661 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.662 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.663 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.664 + | _ => raise error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
1.665 +
1.666 +val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.667 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.668 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.669 +(*val p = e_pos'; val c = [];
1.670 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.671 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.672 +
1.673 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.674 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.675 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.676 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.677 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.678 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.679 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.680 +"TODO 8+ 2*x^^^2 = 0";
1.681 +"TODO 8+ 2*x^^^2 = 0";
1.682 +"TODO 8+ 2*x^^^2 = 0";
1.683 +
1.684 +(*EP-14*)
1.685 +val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.686 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.687 +(*val p = e_pos'; val c = [];
1.688 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.689 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.690 +
1.691 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.692 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.693 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.694 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.695 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.696 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.697 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.698 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.699 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.700 + | _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.701 +
1.702 +
1.703 +val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
1.704 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.705 +(*val p = e_pos'; val c = [];
1.706 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.707 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.708 +
1.709 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.710 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.711 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.712 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.713 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.714 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.715 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.716 +"TODO 4+ x^^^2 = 0";
1.717 +"TODO 4+ x^^^2 = 0";
1.718 +"TODO 4+ x^^^2 = 0";
1.719 +
1.720 +(*EP-15*)
1.721 +val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.722 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.723 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.724 +(*val p = e_pos'; val c = [];
1.725 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.726 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.727 +
1.728 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.729 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.730 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.731 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.732 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.733 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.734 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.735 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.736 +case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
1.737 + | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.738 +
1.739 +val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.740 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.741 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.742 +(*val p = e_pos'; val c = [];
1.743 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.744 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.745 +
1.746 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.747 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.748 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.749 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.750 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.751 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.752 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.753 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.754 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.755 + | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.756 +
1.757 +(*EP-16*)
1.758 +val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.759 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.760 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.761 +(*val p = e_pos'; val c = [];
1.762 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.763 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.764 +
1.765 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.766 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.767 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.768 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.769 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.770 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.771 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.772 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.773 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
1.774 + | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
1.775 +
1.776 +(*EP-//*)
1.777 +val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
1.778 +val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.779 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.780 +(*val p = e_pos'; val c = [];
1.781 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.782 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.783 +
1.784 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.785 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.786 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.787 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.788 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.789 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.790 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.791 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.792 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.793 + | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.794 +
1.795 +"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.796 +"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.797 +"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.798 + val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
1.799 + "solveFor x","solutions L"];
1.800 + val (dI',pI',mI') =
1.801 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.802 + ["PolyEq","complete_square"]);
1.803 +(* val p = e_pos'; val c = [];
1.804 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.805 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.806 +
1.807 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.808 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.809 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.810 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.811 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.812 + (*Apply_Method ("PolyEq.thy","complete_square")*)
1.813 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.814 + (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
1.815 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.816 + (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
1.817 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.818 + (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
1.819 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.820 + (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
1.821 + 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
1.822 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.823 + (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
1.824 + -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
1.825 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.826 + (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
1.827 + -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
1.828 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.829 + (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
1.830 + x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
1.831 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.832 + (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
1.833 + x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
1.834 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.835 + (*"x = -2 | x = 4" nxt = Or_to_List*)
1.836 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.837 + (*"[x = -2, x = 4]" nxt = Check_Postcond*)
1.838 + val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.839 +(* FIXXXME
1.840 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
1.841 + | _ => raise error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
1.842 +*)
1.843 +if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
1.844 +else raise error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
1.845 +
1.846 +
1.847 +"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.848 +"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.849 +"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.850 +"---- test the erls ----";
1.851 + val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
1.852 + val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
1.853 + val t' = term2str t;
1.854 + (*if t'= "True" then ()
1.855 + else raise error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1.856 +(* *)
1.857 + val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
1.858 + "solveFor x","solutions L"];
1.859 + val (dI',pI',mI') =
1.860 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.861 + ["PolyEq","complete_square"]);
1.862 +(* val p = e_pos'; val c = [];
1.863 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.864 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.865 +
1.866 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.867 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.868 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.869 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.870 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.871 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.872 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.873 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.874 + (*Apply_Method ("PolyEq.thy","complete_square")*)
1.875 + val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.876 +
1.877 +"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.878 +"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.879 +"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.880 + val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
1.881 + "solveFor x","solutions L"];
1.882 + val (dI',pI',mI') =
1.883 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.884 + ["PolyEq","complete_square"]);
1.885 +(* val p = e_pos'; val c = [];
1.886 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.887 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.888 +
1.889 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.890 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.891 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.892 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.893 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.894 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.895 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.896 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.897 + (*Apply_Method ("PolyEq.thy","complete_square")*)
1.898 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.899 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.900 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.901 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.902 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.903 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.904 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.905 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.906 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.907 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.908 +(* FIXXXXME n1.,
1.909 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
1.910 + | _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
1.911 +*)
1.912 +
1.913 +"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.914 +"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.915 +"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.916 + val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
1.917 + "solveFor x","solutions L"];
1.918 + val (dI',pI',mI') =
1.919 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.920 + ["PolyEq","complete_square"]);
1.921 +(* val p = e_pos'; val c = [];
1.922 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.923 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.924 +
1.925 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.926 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.927 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.928 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.929 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.930 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.931 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.932 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.933 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.934 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.935 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.936 +
1.937 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.938 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.939 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.940 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.941 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.942 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.943 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.944 + val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.945 +(*WN.2.5.03 TODO FIXME Matthias ?
1.946 + case f of
1.947 + Form'
1.948 + (FormKF
1.949 + (~1,EdUndef,0,Nundef,
1.950 + "[x = (a + b) / 2 + -1 * sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b)]"))
1.951 + => ()
1.952 + | _ => raise error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
1.953 + this will be simplified [x = a, x = b] to by Factor.ML*)
1.954 +
1.955 +
1.956 +"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.957 +"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.958 +"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.959 + val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
1.960 + "solveFor x","solutions L"];
1.961 + val (dI',pI',mI') =
1.962 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.963 + ["PolyEq","complete_square"]);
1.964 +(* val p = e_pos'; val c = [];
1.965 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.966 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.967 +
1.968 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.969 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.970 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.971 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.972 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.973 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.974 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.975 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.976 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.977 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.978 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.979 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.980 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.981 + val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.982 +(*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
1.983 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
1.984 + | _ => raise error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
1.985 +*)
1.986 +
1.987 +"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.988 +"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.989 +"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.990 + val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1.991 + "solveFor x","solutions L"];
1.992 + val (dI',pI',mI') =
1.993 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.994 + ["PolyEq","complete_square"]);
1.995 +(* val p = e_pos'; val c = [];
1.996 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.997 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.998 +
1.999 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.1000 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1001 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1002 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1003 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1004 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1005 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1006 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1007 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1008 +(*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
1.1009 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
1.1010 + | _ => raise error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
1.1011 +*)
1.1012 +if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
1.1013 +else raise error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
1.1014 +
1.1015 +
1.1016 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.1017 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.1018 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.1019 +(*EP-17 Schalk_I_p86_n5*)
1.1020 +val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
1.1021 +(* refine fmz ["univariate","equation"];
1.1022 +*)
1.1023 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.1024 +(*val p = e_pos';
1.1025 +val c = [];
1.1026 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.1027 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.1028 +
1.1029 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.1030 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1031 +(* val nxt =
1.1032 + ("Model_Problem",
1.1033 + Model_Problem ["normalize","polynomial","univariate","equation"])
1.1034 + : string * tac*)
1.1035 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1036 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1037 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1038 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1039 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1040 +(* val nxt =
1.1041 + ("Subproblem",
1.1042 + Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
1.1043 + : string * tac *)
1.1044 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1045 +(*val nxt =
1.1046 + ("Model_Problem",
1.1047 + Model_Problem ["degree_1","polynomial","univariate","equation"])
1.1048 + : string * tac *)
1.1049 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1050 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1051 +
1.1052 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1053 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1054 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1055 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1056 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1057 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
1.1058 + | _ => raise error "polyeq.sml: diff.behav. in [x = 2]";
1.1059 +
1.1060 +
1.1061 +"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.1062 +"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.1063 +"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.1064 +(*is in rlang.sml, too*)
1.1065 +val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
1.1066 + "solveFor x","solutions L"];
1.1067 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.1068 +
1.1069 +(*val p = e_pos'; val c = [];
1.1070 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.1071 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.1072 +
1.1073 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.1074 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1.1075 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1076 +(* val nxt =
1.1077 + ("Model_Problem",
1.1078 + Model_Problem ["normalize","polynomial","univariate","equation"])
1.1079 + : string * tac *)
1.1080 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1081 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1082 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1083 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1084 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1085 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1086 +(* val nxt =
1.1087 + ("Subproblem",
1.1088 + Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
1.1089 + : string * tac*)
1.1090 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1091 +(*val nxt =
1.1092 + ("Model_Problem",
1.1093 + Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
1.1094 + : string * tac*)
1.1095 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1096 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1097 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1098 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1099 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1100 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1101 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1102 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
1.1103 + | _ => raise error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
1.1104 +
1.1105 +
1.1106 +" -4 + x^^^2 =0 ";
1.1107 +" -4 + x^^^2 =0 ";
1.1108 +" -4 + x^^^2 =0 ";
1.1109 +val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
1.1110 +(* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
1.1111 +(*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
1.1112 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.1113 +(*val p = e_pos';
1.1114 +val c = [];
1.1115 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.1116 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.1117 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.1118 +
1.1119 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1120 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1121 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1122 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1123 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1124 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1125 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1126 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.1127 + | _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
1.1128 +
1.1129 +"----------------- polyeq.sml end ------------------";
1.1130 +
1.1131 +(*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
1.1132 +(*WN.19.3.03 ---v-*)
1.1133 +(*3(b)*)val (bdv,v) = (str2term "bdv", str2term "R1");
1.1134 +val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
1.1135 +val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.1136 +term2str t';
1.1137 +"-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
1.1138 +(*WN.19.3.03 ---^-*)
1.1139 +
1.1140 +(*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
1.1141 +val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
1.1142 +val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.1143 +term2str t';
1.1144 +"y ^^^ 2 + -2 * x * p = 0";
1.1145 +
1.1146 +(*3(d)*)val (bdv,v) = (str2term "bdv", str2term "x2");
1.1147 +val t = str2term
1.1148 +"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";
1.1149 +val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.1150 +term2str t';
1.1151 +"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";
1.1152 +val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
1.1153 +term2str t';
1.1154 +"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";
1.1155 +
1.1156 +(*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
1.1157 +val t = str2term
1.1158 +"A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
1.1159 +val None = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.1160 +(*die _unsichtbare_ Klammern sind genau wie gew"unscht*)
1.1161 +
1.1162 +
1.1163 +val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
1.1164 +trace_rewrite:=true;
1.1165 +rewrite_set_ thy false expand_binoms t;
1.1166 +trace_rewrite:=false;
1.1167 +
1.1168 +
1.1169 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.1170 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.1171 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.1172 +states:=[];
1.1173 +CalcTree
1.1174 +[(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
1.1175 + ("PolyEq.thy",["univariate","equation"],["no_met"]))];
1.1176 +Iterator 1;
1.1177 +moveActiveRoot 1;
1.1178 +autoCalculate 1 CompleteCalc;
1.1179 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.1180 +
1.1181 +interSteps 1 ([1],Res) (*no Rewrite_Set...*);