walther@59627
|
1 |
(* Title: Knowledge/polyeq-1.sml
|
walther@59627
|
2 |
testexamples for PolyEq, poynomial equations and equational systems
|
walther@59627
|
3 |
Author: Richard Lang 2003
|
walther@59627
|
4 |
(c) due to copyright terms
|
walther@59627
|
5 |
WN030609: some expls dont work due to unfinished handling of 'expanded terms';
|
walther@59627
|
6 |
others marked with TODO have to be checked, too.
|
walther@59627
|
7 |
*)
|
walther@59627
|
8 |
|
walther@59627
|
9 |
"-----------------------------------------------------------------";
|
walther@59627
|
10 |
"table of contents -----------------------------------------------";
|
walther@59627
|
11 |
"-----------------------------------------------------------------";
|
walther@59627
|
12 |
"------ polyeq-1.sml ---------------------------------------------";
|
walther@59627
|
13 |
"----------- tests on predicates in problems ---------------------";
|
walther@59627
|
14 |
"----------- test matching problems ------------------------------";
|
walther@59627
|
15 |
"----------- lin.eq degree_0 -------------------------------------";
|
walther@59627
|
16 |
"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
|
walther@59627
|
17 |
"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
|
walther@59627
|
18 |
"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
|
walther@59627
|
19 |
"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
|
walther@59627
|
20 |
"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
21 |
"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
|
walther@59627
|
22 |
"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
23 |
"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
24 |
"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
|
walther@59627
|
25 |
"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
|
walther@59627
|
26 |
"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
|
walther@59627
|
27 |
"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
|
walther@59627
|
28 |
"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
|
walther@59627
|
29 |
"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
|
walther@59627
|
30 |
"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
|
walther@59627
|
31 |
"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
walther@59627
|
32 |
"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
|
walther@59627
|
33 |
"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
|
walther@59627
|
34 |
"-----------------------------------------------------------------";
|
walther@59627
|
35 |
"------ polyeq-2.sml ---------------------------------------------";
|
walther@59627
|
36 |
"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
|
walther@59627
|
37 |
"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
|
walther@59627
|
38 |
"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
|
walther@59627
|
39 |
"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
|
walther@59627
|
40 |
"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
|
walther@59627
|
41 |
"----------- rls make_polynomial_in ------------------------------";
|
walther@59627
|
42 |
"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
|
walther@59627
|
43 |
"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
|
walther@59627
|
44 |
"-----------------------------------------------------------------";
|
walther@59627
|
45 |
"-----------------------------------------------------------------";
|
walther@59627
|
46 |
|
walther@59627
|
47 |
"----------- tests on predicates in problems ---------------------";
|
walther@59627
|
48 |
"----------- tests on predicates in problems ---------------------";
|
walther@59627
|
49 |
"----------- tests on predicates in problems ---------------------";
|
walther@59627
|
50 |
(* trace_rewrite:=true;
|
walther@59627
|
51 |
trace_rewrite:=false;
|
walther@59627
|
52 |
*)
|
walther@59627
|
53 |
val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
|
walther@59627
|
54 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
|
walther@59627
|
55 |
if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
|
walther@59627
|
56 |
else error "polyeq.sml: diff.behav. in lhs";
|
walther@59627
|
57 |
|
walther@59627
|
58 |
val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
|
walther@59627
|
59 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
|
walther@59627
|
60 |
if (term2str t) = "True" then ()
|
walther@59627
|
61 |
else error "polyeq.sml: diff.behav. 1 in is_expended_in";
|
walther@59627
|
62 |
|
walther@59627
|
63 |
val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
|
walther@59627
|
64 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
|
walther@59627
|
65 |
if (term2str t) = "False" then ()
|
walther@59627
|
66 |
else error "polyeq.sml: diff.behav. 2 in is_poly_in";
|
walther@59627
|
67 |
|
walther@59627
|
68 |
val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
|
walther@59627
|
69 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
|
walther@59627
|
70 |
if (term2str t) = "True" then ()
|
walther@59627
|
71 |
else error "polyeq.sml: diff.behav. 3 in is_poly_in";
|
walther@59627
|
72 |
|
walther@59627
|
73 |
val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
|
walther@59627
|
74 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
|
walther@59627
|
75 |
if (term2str t) = "True" then ()
|
walther@59627
|
76 |
else error "polyeq.sml: diff.behav. 4 in is_expended_in";
|
walther@59627
|
77 |
|
walther@59627
|
78 |
|
walther@59627
|
79 |
val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
|
walther@59627
|
80 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
|
walther@59627
|
81 |
if (term2str t) = "True" then ()
|
walther@59627
|
82 |
else error "polyeq.sml: diff.behav. 5 in is_expended_in";
|
walther@59627
|
83 |
|
walther@59627
|
84 |
val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
|
walther@59627
|
85 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
|
walther@59627
|
86 |
if (term2str t) = "True" then ()
|
walther@59627
|
87 |
else error "polyeq.sml: diff.behav. in has_degree_in_in";
|
walther@59627
|
88 |
|
walther@59627
|
89 |
val t3 = (Thm.term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
|
walther@59627
|
90 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
|
walther@59627
|
91 |
if (term2str t) = "False" then ()
|
walther@59627
|
92 |
else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
|
walther@59627
|
93 |
|
walther@59627
|
94 |
val t4 = (Thm.term_of o the o (parse thy))
|
walther@59627
|
95 |
"((-8 - 2*x + x^^^2) has_degree_in x) = 1";
|
walther@59627
|
96 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
|
walther@59627
|
97 |
if (term2str t) = "False" then ()
|
walther@59627
|
98 |
else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
|
walther@59627
|
99 |
|
walther@59627
|
100 |
val t5 = (Thm.term_of o the o (parse thy))
|
walther@59627
|
101 |
"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
|
walther@59627
|
102 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
|
walther@59627
|
103 |
if (term2str t) = "True" then ()
|
walther@59627
|
104 |
else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
|
walther@59627
|
105 |
|
walther@59627
|
106 |
"----------- test matching problems --------------------------0---";
|
walther@59627
|
107 |
"----------- test matching problems --------------------------0---";
|
walther@59627
|
108 |
"----------- test matching problems --------------------------0---";
|
walther@59627
|
109 |
val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
110 |
if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
|
walther@59627
|
111 |
Matches' {Find = [Correct "solutions L"],
|
walther@59627
|
112 |
With = [],
|
walther@59627
|
113 |
Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
|
walther@59627
|
114 |
Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
|
walther@59627
|
115 |
Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
|
walther@59627
|
116 |
Relate = []}
|
walther@59627
|
117 |
then () else error "match_pbl [expanded,univariate,equation]";
|
walther@59627
|
118 |
|
walther@59627
|
119 |
if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
|
walther@59627
|
120 |
Matches' {Find = [Correct "solutions L"],
|
walther@59627
|
121 |
With = [],
|
walther@59627
|
122 |
Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
|
walther@59627
|
123 |
Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
|
walther@59627
|
124 |
Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
|
walther@59627
|
125 |
then () else error "match_pbl [degree_2,expanded,univariate,equation]";
|
walther@59627
|
126 |
|
walther@59627
|
127 |
"----------- lin.eq degree_0 -------------------------------------";
|
walther@59627
|
128 |
"----------- lin.eq degree_0 -------------------------------------";
|
walther@59627
|
129 |
"----------- lin.eq degree_0 -------------------------------------";
|
walther@59627
|
130 |
"----- d0_false ------";
|
walther@59627
|
131 |
val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
|
walther@59627
|
132 |
val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
|
walther@59627
|
133 |
["PolyEq","solve_d0_polyeq_equation"]);
|
walther@59627
|
134 |
(*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
|
walther@59627
|
135 |
TODO: change to "equality (x + -1*x = (0::real))"
|
walther@59627
|
136 |
and search for an appropriate problem and method.
|
walther@59627
|
137 |
|
walther@59627
|
138 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
139 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
140 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
141 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
142 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
143 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
144 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
145 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
|
walther@59627
|
146 |
| _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
|
walther@59627
|
147 |
|
walther@59627
|
148 |
"----- d0_true ------";
|
walther@59627
|
149 |
val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
|
walther@59627
|
150 |
val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
|
walther@59627
|
151 |
["PolyEq","solve_d0_polyeq_equation"]);
|
walther@59627
|
152 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
153 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
154 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
155 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
156 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
157 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
158 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
159 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
|
walther@59627
|
160 |
| _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
|
walther@59627
|
161 |
============ inhibit exn WN110914 ============================================*)
|
walther@59627
|
162 |
|
walther@59627
|
163 |
"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
|
walther@59627
|
164 |
"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
|
walther@59627
|
165 |
"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
|
walther@59627
|
166 |
"----- d2_pqformula1 ------!!!!";
|
walther@59627
|
167 |
val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
|
walther@59627
|
168 |
val (dI',pI',mI') =
|
walther@59627
|
169 |
("Isac_Knowledge", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
|
walther@59627
|
170 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
171 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
172 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
173 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
174 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
175 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
176 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
177 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
|
walther@59627
|
178 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
179 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
180 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
181 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
182 |
|
walther@59627
|
183 |
(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
|
walther@59627
|
184 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
|
walther@59749
|
185 |
"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
|
walther@59627
|
186 |
"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
|
walther@59755
|
187 |
val Appl m = applicable_in p pt tac;
|
walther@59627
|
188 |
val Check_elementwise' (trm1, str, (trm2, trms)) = m;
|
walther@59627
|
189 |
term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
|
walther@59627
|
190 |
str = "Assumptions";
|
walther@59627
|
191 |
term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
|
walther@59627
|
192 |
terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
|
walther@59627
|
193 |
" (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
|
walther@59627
|
194 |
"\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
|
walther@59627
|
195 |
"has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
|
walther@59627
|
196 |
"\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^
|
walther@59627
|
197 |
"\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]";
|
walther@59627
|
198 |
(*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
|
walther@59755
|
199 |
(*if*) Tactic.for_specify' m; (*false*)
|
walther@59627
|
200 |
(*loc_solve_ (mI,m) ptp;
|
walther@59712
|
201 |
WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
|
walther@59749
|
202 |
"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
|
walther@59627
|
203 |
(*solve m (pt, pos);
|
walther@59712
|
204 |
WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
|
walther@59751
|
205 |
"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
|
walther@59627
|
206 |
e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
|
walther@59627
|
207 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@59627
|
208 |
val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
|
walther@59627
|
209 |
val d = e_rls;
|
walther@59627
|
210 |
(*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
|
walther@59712
|
211 |
WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
|
walther@59679
|
212 |
"~~~~~ fun locate_input_tactic, args:"; val () = ();
|
walther@59679
|
213 |
(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
|
walther@59627
|
214 |
l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
|
walther@59712
|
215 |
(*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
|
walther@59718
|
216 |
... Accept_Tac1 ... is correct*)
|
walther@59691
|
217 |
"~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
|
walther@59627
|
218 |
((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
|
walther@59627
|
219 |
1 < length l (*true*);
|
walther@59627
|
220 |
val up = drop_last l;
|
walther@59627
|
221 |
term2str (go up sc);
|
walther@59627
|
222 |
(go up sc);
|
walther@59712
|
223 |
(*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
|
walther@59627
|
224 |
... ???? ... is correct*)
|
walther@59691
|
225 |
"~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss),
|
walther@59627
|
226 |
(Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc));
|
walther@59627
|
227 |
val l = drop_last l; (*comes from e, goes to Abs*)
|
walther@59627
|
228 |
val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
|
walther@59627
|
229 |
val i = mk_Free (i, T);
|
walther@59697
|
230 |
val E = Env.update E (i, v);
|
walther@59627
|
231 |
(*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
|
walther@59627
|
232 |
val [(tac_, mout, ctree, pos', xxx)] = ss;
|
walther@59627
|
233 |
val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
|
walther@59718
|
234 |
(*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),ORundef) ((E, l@[R,D], a,v,S,b),ss) body
|
walther@59718
|
235 |
... Accept_Tac1 ... is correct*)
|
walther@59691
|
236 |
"~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
|
walther@59718
|
237 |
((((y,s),d),ORundef), ((E, l@[R,D], a,v,S,b),ss), body);
|
walther@59721
|
238 |
val (Program.Tac stac, a') = interpret_leaf "locate" thy' sr (E, (a, v)) t
|
walther@59627
|
239 |
val ctxt = get_ctxt pt (p,p_)
|
walther@59627
|
240 |
val p' = lev_on p : pos;
|
walther@59627
|
241 |
(* WAS val NotAss = associate pt d (m, stac)
|
walther@59627
|
242 |
... Ass ... is correct*)
|
walther@59627
|
243 |
"~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
|
walther@59627
|
244 |
(Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
|
walther@59627
|
245 |
term2str consts;
|
walther@59627
|
246 |
term2str consts';
|
walther@59627
|
247 |
if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
|
walther@59627
|
248 |
(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
|
walther@59679
|
249 |
( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
|
walther@59627
|
250 |
|
walther@59627
|
251 |
"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
|
walther@59627
|
252 |
"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
|
walther@59627
|
253 |
"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
|
walther@59627
|
254 |
"----- d2_pqformula1_neg ------";
|
walther@59627
|
255 |
val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
|
walther@59627
|
256 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
257 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
258 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
259 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
260 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
261 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
262 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
263 |
(*### or2list False
|
walther@59627
|
264 |
([1],Res) False Or_to_List)*)
|
walther@59627
|
265 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
266 |
(*### or2list False
|
walther@59627
|
267 |
([2],Res) [] Check_elementwise "Assumptions"*)
|
walther@59627
|
268 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
269 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
270 |
val asm = get_assumptions_ pt p;
|
walther@59627
|
271 |
if f2str f = "[]" andalso
|
walther@59627
|
272 |
terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
|
walther@59627
|
273 |
"\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
|
walther@59627
|
274 |
else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
|
walther@59627
|
275 |
|
walther@59627
|
276 |
"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
|
walther@59627
|
277 |
"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
|
walther@59627
|
278 |
"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
|
walther@59627
|
279 |
"----- d2_pqformula2 ------";
|
walther@59627
|
280 |
val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
281 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
282 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
283 |
(*val p = e_pos';
|
walther@59627
|
284 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
walther@59627
|
285 |
val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
|
walther@59627
|
286 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
287 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
288 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
289 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
290 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
291 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
292 |
|
walther@59627
|
293 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
294 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
295 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
296 |
case f of FormKF "[x = 2, x = -1]" => ()
|
walther@59627
|
297 |
| _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
|
walther@59627
|
298 |
|
walther@59627
|
299 |
|
walther@59627
|
300 |
"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
|
walther@59627
|
301 |
"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
|
walther@59627
|
302 |
"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
|
walther@59627
|
303 |
"----- d2_pqformula3 ------";
|
walther@59627
|
304 |
(*EP-9*)
|
walther@59627
|
305 |
val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
306 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
307 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
308 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
309 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
310 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
311 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
312 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
313 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
314 |
|
walther@59627
|
315 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
316 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
317 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
318 |
case f of FormKF "[x = 1, x = -2]" => ()
|
walther@59627
|
319 |
| _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
|
walther@59627
|
320 |
|
walther@59627
|
321 |
|
walther@59627
|
322 |
"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
323 |
"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
324 |
"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
325 |
"----- d2_pqformula3_neg ------";
|
walther@59627
|
326 |
val fmz = ["equality (2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
327 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
328 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
329 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
330 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
331 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
332 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
333 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
334 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
335 |
|
walther@59627
|
336 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
337 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
338 |
"TODO 2 + x + x^^^2 = 0";
|
walther@59627
|
339 |
"TODO 2 + x + x^^^2 = 0";
|
walther@59627
|
340 |
"TODO 2 + x + x^^^2 = 0";
|
walther@59627
|
341 |
|
walther@59627
|
342 |
"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
|
walther@59627
|
343 |
"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
|
walther@59627
|
344 |
"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
|
walther@59627
|
345 |
"----- d2_pqformula4 ------";
|
walther@59627
|
346 |
val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
347 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
348 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
349 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
350 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
351 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
352 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
353 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
354 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
355 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
356 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
357 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
358 |
case f of FormKF "[x = 1, x = -2]" => ()
|
walther@59627
|
359 |
| _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
|
walther@59627
|
360 |
|
walther@59627
|
361 |
"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
362 |
"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
363 |
"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
364 |
"----- d2_pqformula5 ------";
|
walther@59627
|
365 |
val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
366 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
367 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
368 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
369 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
370 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
371 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
372 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
373 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
374 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
375 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
376 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
377 |
case f of FormKF "[x = 0, x = -1]" => ()
|
walther@59627
|
378 |
| _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
|
walther@59627
|
379 |
|
walther@59627
|
380 |
"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
381 |
"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
382 |
"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
|
walther@59627
|
383 |
"----- d2_pqformula6 ------";
|
walther@59627
|
384 |
val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
385 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
386 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
387 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
388 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
389 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
390 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
391 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
392 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
393 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
394 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
395 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
396 |
case f of FormKF "[x = 0, x = -1]" => ()
|
walther@59627
|
397 |
| _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
|
walther@59627
|
398 |
|
walther@59627
|
399 |
"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
|
walther@59627
|
400 |
"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
|
walther@59627
|
401 |
"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
|
walther@59627
|
402 |
"----- d2_pqformula7 ------";
|
walther@59627
|
403 |
(*EP-10*)
|
walther@59627
|
404 |
val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
405 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
406 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
407 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
408 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
409 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
410 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
411 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
412 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
413 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
414 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
415 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
416 |
case f of FormKF "[x = 0, x = -1]" => ()
|
walther@59627
|
417 |
| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
|
walther@59627
|
418 |
|
walther@59627
|
419 |
"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
|
walther@59627
|
420 |
"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
|
walther@59627
|
421 |
"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
|
walther@59627
|
422 |
"----- d2_pqformula8 ------";
|
walther@59627
|
423 |
val fmz = ["equality (x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
424 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
425 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
426 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
427 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
428 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
429 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
430 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
431 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
432 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
433 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
434 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
435 |
case f of FormKF "[x = 0, x = -1]" => ()
|
walther@59627
|
436 |
| _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
|
walther@59627
|
437 |
|
walther@59627
|
438 |
"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
|
walther@59627
|
439 |
"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
|
walther@59627
|
440 |
"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
|
walther@59627
|
441 |
"----- d2_pqformula9 ------";
|
walther@59627
|
442 |
val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
443 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
444 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
445 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
446 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
447 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
448 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
449 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
450 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
451 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
452 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
453 |
case f of FormKF "[x = 2, x = -2]" => ()
|
walther@59627
|
454 |
| _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
|
walther@59627
|
455 |
|
walther@59627
|
456 |
|
walther@59627
|
457 |
"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
|
walther@59627
|
458 |
"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
|
walther@59627
|
459 |
"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
|
walther@59627
|
460 |
"----- d2_pqformula9_neg ------";
|
walther@59627
|
461 |
val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
462 |
val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
463 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
464 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
465 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
466 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
467 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
468 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
469 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
470 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
471 |
"TODO 4 + 1*x^^^2 = 0";
|
walther@59627
|
472 |
"TODO 4 + 1*x^^^2 = 0";
|
walther@59627
|
473 |
"TODO 4 + 1*x^^^2 = 0";
|
walther@59627
|
474 |
|
walther@59627
|
475 |
"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
|
walther@59627
|
476 |
"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
|
walther@59627
|
477 |
"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
|
walther@59627
|
478 |
val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
479 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
480 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
481 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
482 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
483 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
484 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
485 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
486 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
487 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
488 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
489 |
case f of FormKF "[x = 1, x = -1 / 2]" => ()
|
walther@59627
|
490 |
| _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
|
walther@59627
|
491 |
|
walther@59627
|
492 |
"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
|
walther@59627
|
493 |
"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
|
walther@59627
|
494 |
"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
|
walther@59627
|
495 |
val fmz = ["equality (1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
496 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
497 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
498 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
499 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
500 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
501 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
502 |
|
walther@59627
|
503 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
504 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
505 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
506 |
"TODO 1 +(-1)*x + 2*x^^^2 = 0";
|
walther@59627
|
507 |
"TODO 1 +(-1)*x + 2*x^^^2 = 0";
|
walther@59627
|
508 |
"TODO 1 +(-1)*x + 2*x^^^2 = 0";
|
walther@59627
|
509 |
|
walther@59627
|
510 |
|
walther@59627
|
511 |
"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
|
walther@59627
|
512 |
"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
|
walther@59627
|
513 |
"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
|
walther@59627
|
514 |
(*EP-11*)
|
walther@59627
|
515 |
val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
516 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
517 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
518 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
519 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
520 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
521 |
|
walther@59627
|
522 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
523 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
524 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
525 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
526 |
|
walther@59627
|
527 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
528 |
case f of FormKF "[x = 1 / 2, x = -1]" => ()
|
walther@59627
|
529 |
| _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
|
walther@59627
|
530 |
|
walther@59627
|
531 |
|
walther@59627
|
532 |
"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
|
walther@59627
|
533 |
"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
|
walther@59627
|
534 |
"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
|
walther@59627
|
535 |
val fmz = ["equality (1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
536 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
537 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
538 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
539 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
540 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
541 |
|
walther@59627
|
542 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
543 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
544 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
545 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
546 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
547 |
"TODO 1 + x + 2*x^^^2 = 0";
|
walther@59627
|
548 |
"TODO 1 + x + 2*x^^^2 = 0";
|
walther@59627
|
549 |
"TODO 1 + x + 2*x^^^2 = 0";
|
walther@59627
|
550 |
|
walther@59627
|
551 |
|
walther@59627
|
552 |
val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
553 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
554 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
555 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
556 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
557 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
558 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
559 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
560 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
561 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
562 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
563 |
case f of FormKF "[x = 1, x = -2]" => ()
|
walther@59627
|
564 |
| _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
|
walther@59627
|
565 |
|
walther@59627
|
566 |
val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
567 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
568 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
569 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
570 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
571 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
572 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
573 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
574 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
575 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
576 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
577 |
"TODO 2 + 1*x + x^^^2 = 0";
|
walther@59627
|
578 |
"TODO 2 + 1*x + x^^^2 = 0";
|
walther@59627
|
579 |
"TODO 2 + 1*x + x^^^2 = 0";
|
walther@59627
|
580 |
|
walther@59627
|
581 |
(*EP-12*)
|
walther@59627
|
582 |
val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
583 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
584 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
585 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
586 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
587 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
588 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
589 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
590 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
591 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
592 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
593 |
case f of FormKF "[x = 1, x = -2]" => ()
|
walther@59627
|
594 |
| _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
|
walther@59627
|
595 |
|
walther@59627
|
596 |
val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
597 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
598 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
599 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
600 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
601 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
602 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
603 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
604 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
605 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
606 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
607 |
"TODO 2 + x + x^^^2 = 0";
|
walther@59627
|
608 |
"TODO 2 + x + x^^^2 = 0";
|
walther@59627
|
609 |
"TODO 2 + x + x^^^2 = 0";
|
walther@59627
|
610 |
|
walther@59627
|
611 |
(*EP-13*)
|
walther@59627
|
612 |
val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
613 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
614 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
615 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
616 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
617 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
618 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
619 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
620 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
621 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
622 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
623 |
case f of FormKF "[x = 2, x = -2]" => ()
|
walther@59627
|
624 |
| _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
|
walther@59627
|
625 |
|
walther@59627
|
626 |
val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
627 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
628 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
629 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
630 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
631 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
632 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
633 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
634 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
635 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
636 |
"TODO 8+ 2*x^^^2 = 0";
|
walther@59627
|
637 |
"TODO 8+ 2*x^^^2 = 0";
|
walther@59627
|
638 |
"TODO 8+ 2*x^^^2 = 0";
|
walther@59627
|
639 |
|
walther@59627
|
640 |
(*EP-14*)
|
walther@59627
|
641 |
val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
642 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
643 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
644 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
645 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
646 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
647 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
648 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
649 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
650 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
651 |
case f of FormKF "[x = 2, x = -2]" => ()
|
walther@59627
|
652 |
| _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
|
walther@59627
|
653 |
|
walther@59627
|
654 |
|
walther@59627
|
655 |
val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
656 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
657 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
658 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
659 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
660 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
661 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
662 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
663 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
664 |
"TODO 4+ x^^^2 = 0";
|
walther@59627
|
665 |
"TODO 4+ x^^^2 = 0";
|
walther@59627
|
666 |
"TODO 4+ x^^^2 = 0";
|
walther@59627
|
667 |
|
walther@59627
|
668 |
(*EP-15*)
|
walther@59627
|
669 |
val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
670 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
671 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
672 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
673 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
674 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
675 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
676 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
677 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
678 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
679 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
680 |
case f of FormKF "[x = 0, x = -1]" => ()
|
walther@59627
|
681 |
| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
|
walther@59627
|
682 |
|
walther@59627
|
683 |
val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
684 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
685 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
686 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
687 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
688 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
689 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
690 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
691 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
692 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
693 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
694 |
case f of FormKF "[x = 0, x = -1]" => ()
|
walther@59627
|
695 |
| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
|
walther@59627
|
696 |
|
walther@59627
|
697 |
(*EP-16*)
|
walther@59627
|
698 |
val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
699 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
700 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
701 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
702 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
703 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
704 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
705 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
706 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
707 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
708 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
709 |
case f of FormKF "[x = 0, x = -1 / 2]" => ()
|
walther@59627
|
710 |
| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
|
walther@59627
|
711 |
|
walther@59627
|
712 |
(*EP-//*)
|
walther@59627
|
713 |
val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
|
walther@59627
|
714 |
val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
|
walther@59627
|
715 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
716 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
717 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
718 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
719 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
720 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
721 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
722 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
723 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
724 |
case f of FormKF "[x = 0, x = -1]" => ()
|
walther@59627
|
725 |
| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
|
walther@59627
|
726 |
|
walther@59627
|
727 |
|
walther@59627
|
728 |
"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
walther@59627
|
729 |
"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
walther@59627
|
730 |
"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
walther@59627
|
731 |
(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
|
walther@59627
|
732 |
see --- val rls = calculate_RootRat > calculate_Rational ---
|
walther@59627
|
733 |
calculate_RootRat was a TODO with 2002, requires re-design.
|
walther@59627
|
734 |
see also --- (-8 - 2*x + x^^^2 = 0), by rewriting --- below
|
walther@59627
|
735 |
*)
|
walther@59627
|
736 |
val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
|
walther@59627
|
737 |
"solveFor x","solutions L"];
|
walther@59627
|
738 |
val (dI',pI',mI') =
|
walther@59627
|
739 |
("PolyEq",["degree_2","expanded","univariate","equation"],
|
walther@59627
|
740 |
["PolyEq","complete_square"]);
|
walther@59627
|
741 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
742 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
743 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
744 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
745 |
|
walther@59627
|
746 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
747 |
(*Apply_Method ("PolyEq","complete_square")*)
|
walther@59627
|
748 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
749 |
(*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
|
walther@59627
|
750 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
751 |
(*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
|
walther@59627
|
752 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
753 |
(*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
|
walther@59627
|
754 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
755 |
(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
|
walther@59627
|
756 |
2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
|
walther@59627
|
757 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
758 |
(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
|
walther@59627
|
759 |
-1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
|
walther@59627
|
760 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
761 |
(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
|
walther@59627
|
762 |
-1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
|
walther@59627
|
763 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
764 |
(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
|
walther@59627
|
765 |
x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
|
walther@59627
|
766 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
767 |
(*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
|
walther@59627
|
768 |
x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Rational
|
walther@59627
|
769 |
NOT IMPLEMENTED SINCE 2002 ------------------------------^^^^^^^^^^^^^^^^^^*)
|
walther@59627
|
770 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
771 |
(*"x = -2 | x = 4" nxt = Or_to_List*)
|
walther@59627
|
772 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
773 |
(*"[x = -2, x = 4]" nxt = Check_Postcond*)
|
walther@59627
|
774 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
|
walther@59627
|
775 |
(* FIXXXME
|
walther@59627
|
776 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
|
walther@59627
|
777 |
| _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
|
walther@59627
|
778 |
*)
|
walther@59627
|
779 |
if f2str f =
|
walther@59627
|
780 |
"[x = -1 * -1 + -1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))]"
|
walther@59627
|
781 |
(*"[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]"*)
|
walther@59627
|
782 |
then () else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
|
walther@59627
|
783 |
|
walther@59627
|
784 |
|
walther@59627
|
785 |
"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
|
walther@59627
|
786 |
"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
|
walther@59627
|
787 |
"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
|
walther@59627
|
788 |
(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
|
walther@59627
|
789 |
see --- val rls = calculate_RootRat > calculate_Rational ---*)
|
walther@59627
|
790 |
val thy = @{theory PolyEq};
|
walther@59627
|
791 |
val ctxt = Proof_Context.init_global thy;
|
walther@59627
|
792 |
val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
|
walther@59627
|
793 |
val t = (the o (parseNEW ctxt)) "-8 - 2*x + x^^^2 = (0::real)";
|
walther@59627
|
794 |
|
walther@59627
|
795 |
val rls = complete_square;
|
walther@59627
|
796 |
val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
|
walther@59627
|
797 |
term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
|
walther@59627
|
798 |
|
walther@59627
|
799 |
val thm = num_str @{thm square_explicit1};
|
walther@59627
|
800 |
val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t;
|
walther@59627
|
801 |
term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
|
walther@59627
|
802 |
|
walther@59627
|
803 |
val thm = num_str @{thm root_plus_minus};
|
walther@59627
|
804 |
val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
|
walther@59627
|
805 |
term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
|
walther@59627
|
806 |
"\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
|
walther@59627
|
807 |
|
walther@59627
|
808 |
(*the thm bdv_explicit2* here required to be constrained to ::real*)
|
walther@59627
|
809 |
val thm = num_str @{thm bdv_explicit2};
|
walther@59627
|
810 |
val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
|
walther@59627
|
811 |
term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
|
walther@59627
|
812 |
"\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
|
walther@59627
|
813 |
|
walther@59627
|
814 |
val thm = num_str @{thm bdv_explicit3};
|
walther@59627
|
815 |
val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
|
walther@59627
|
816 |
term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
|
walther@59627
|
817 |
"\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
|
walther@59627
|
818 |
|
walther@59627
|
819 |
val thm = num_str @{thm bdv_explicit2};
|
walther@59627
|
820 |
val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
|
walther@59627
|
821 |
term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
|
walther@59627
|
822 |
"\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
|
walther@59627
|
823 |
|
walther@59627
|
824 |
val rls = calculate_RootRat;
|
walther@59627
|
825 |
val SOME (t,asm) = rewrite_set_ thy true rls t;
|
walther@59627
|
826 |
if term2str t =
|
walther@59627
|
827 |
"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \<or>\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
|
walther@59627
|
828 |
(*"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"..isabisac15*)
|
walther@59627
|
829 |
then () else error "(-8 - 2*x + x^^^2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
|
walther@59627
|
830 |
(*SHOULD BE: term2str = "x = -2 | x = 4;*)
|
walther@59627
|
831 |
|
walther@59627
|
832 |
|
walther@59627
|
833 |
"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
|
walther@59627
|
834 |
"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
|
walther@59627
|
835 |
"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
|
walther@59627
|
836 |
"---- test the erls ----";
|
walther@59627
|
837 |
val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
|
walther@59627
|
838 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
|
walther@59627
|
839 |
val t' = term2str t;
|
walther@59627
|
840 |
(*if t'= "HOL.True" then ()
|
walther@59627
|
841 |
else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
|
walther@59627
|
842 |
(* *)
|
walther@59627
|
843 |
val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
|
walther@59627
|
844 |
"solveFor x","solutions L"];
|
walther@59627
|
845 |
val (dI',pI',mI') =
|
walther@59627
|
846 |
("PolyEq",["degree_2","expanded","univariate","equation"],
|
walther@59627
|
847 |
["PolyEq","complete_square"]);
|
walther@59627
|
848 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
849 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
850 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
851 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
852 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
853 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
854 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
855 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
856 |
(*Apply_Method ("PolyEq","complete_square")*)
|
walther@59627
|
857 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
|
walther@59627
|
858 |
|
walther@59627
|
859 |
"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
|
walther@59627
|
860 |
"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
|
walther@59627
|
861 |
"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
|
walther@59627
|
862 |
val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
|
walther@59627
|
863 |
"solveFor x","solutions L"];
|
walther@59627
|
864 |
val (dI',pI',mI') =
|
walther@59627
|
865 |
("PolyEq",["degree_2","expanded","univariate","equation"],
|
walther@59627
|
866 |
["PolyEq","complete_square"]);
|
walther@59627
|
867 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
868 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
869 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
870 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
871 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
872 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
873 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
874 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
875 |
(*Apply_Method ("PolyEq","complete_square")*)
|
walther@59627
|
876 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
877 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
878 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
879 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
880 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
881 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
882 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
883 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
884 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
885 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
886 |
(* FIXXXXME n1.,
|
walther@59627
|
887 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
|
walther@59627
|
888 |
| _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
|
walther@59627
|
889 |
*)
|
walther@59627
|
890 |
|