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 |
"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
|
walther@59627
|
13 |
"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
|
walther@59627
|
14 |
"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
|
walther@59627
|
15 |
"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
|
walther@59627
|
16 |
"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
|
walther@59627
|
17 |
"----------- rls make_polynomial_in ------------------------------";
|
walther@59627
|
18 |
"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
|
walther@59627
|
19 |
"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
|
walther@59627
|
20 |
"-----------------------------------------------------------------";
|
walther@59627
|
21 |
"-----------------------------------------------------------------";
|
walther@59627
|
22 |
|
walther@59627
|
23 |
|
walther@59627
|
24 |
"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
|
walther@59627
|
25 |
"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
|
walther@59627
|
26 |
"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
|
walther@59627
|
27 |
val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
|
walther@59627
|
28 |
"solveFor x","solutions L"];
|
walther@59627
|
29 |
val (dI',pI',mI') =
|
walther@59627
|
30 |
("PolyEq",["degree_2","expanded","univariate","equation"],
|
walther@59627
|
31 |
["PolyEq","complete_square"]);
|
walther@59627
|
32 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
33 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
34 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
35 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
36 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
37 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
38 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
39 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
40 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
41 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
42 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
43 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
44 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
45 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
46 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
47 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
48 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
49 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
50 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
|
walther@59627
|
51 |
(*WN.2.5.03 TODO FIXME Matthias ?
|
walther@59627
|
52 |
case f of
|
walther@59627
|
53 |
Form'
|
walther@59959
|
54 |
(Test_Out.FormKF
|
walther@59627
|
55 |
(~1,EdUndef,0,Nundef,
|
walther@59627
|
56 |
"[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)]"))
|
walther@59627
|
57 |
=> ()
|
walther@59627
|
58 |
| _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
|
walther@59627
|
59 |
this will be simplified [x = a, x = b] to by Factor.ML*)
|
walther@59627
|
60 |
|
walther@59627
|
61 |
|
walther@59627
|
62 |
"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
|
walther@59627
|
63 |
"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
|
walther@59627
|
64 |
"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
|
walther@59627
|
65 |
val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
|
walther@59627
|
66 |
"solveFor x","solutions L"];
|
walther@59627
|
67 |
val (dI',pI',mI') =
|
walther@59627
|
68 |
("PolyEq",["degree_2","expanded","univariate","equation"],
|
walther@59627
|
69 |
["PolyEq","complete_square"]);
|
walther@59627
|
70 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
71 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
72 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
73 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
74 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
75 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
76 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
77 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
78 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
79 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
80 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
81 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
82 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
83 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
|
walther@59627
|
84 |
(*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
|
walther@59959
|
85 |
case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
|
walther@59627
|
86 |
| _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
|
walther@59627
|
87 |
*)
|
walther@59627
|
88 |
|
walther@59627
|
89 |
"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
|
walther@59627
|
90 |
"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
|
walther@59627
|
91 |
"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
|
walther@59627
|
92 |
val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
|
walther@59627
|
93 |
"solveFor x","solutions L"];
|
walther@59627
|
94 |
val (dI',pI',mI') =
|
walther@59627
|
95 |
("PolyEq",["degree_2","expanded","univariate","equation"],
|
walther@59627
|
96 |
["PolyEq","complete_square"]);
|
walther@59627
|
97 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
98 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
99 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
100 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
101 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
102 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
103 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
104 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
105 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
106 |
(*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
|
walther@59959
|
107 |
case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
|
walther@59627
|
108 |
| _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
|
walther@59627
|
109 |
*)
|
walther@59627
|
110 |
if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
|
walther@59627
|
111 |
else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
|
walther@59627
|
112 |
|
walther@59627
|
113 |
|
walther@59627
|
114 |
"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
|
walther@59627
|
115 |
"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
|
walther@59627
|
116 |
"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
|
walther@59627
|
117 |
(*EP-17 Schalk_I_p86_n5*)
|
walther@59627
|
118 |
val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
|
walther@59968
|
119 |
(* Refine.refine fmz ["univariate","equation"];
|
walther@59627
|
120 |
*)
|
walther@59627
|
121 |
val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
|
walther@59627
|
122 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
123 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
124 |
(* val nxt =
|
walther@59627
|
125 |
("Model_Problem",
|
walther@59627
|
126 |
Model_Problem ["normalise","polynomial","univariate","equation"])
|
walther@59627
|
127 |
: string * tac*)
|
walther@59627
|
128 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
129 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
130 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
131 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
132 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
133 |
(* val nxt =
|
walther@59627
|
134 |
("Subproblem",
|
walther@59627
|
135 |
Subproblem ("PolyEq",["polynomial","univariate","equation"]))
|
walther@59627
|
136 |
: string * tac *)
|
walther@59627
|
137 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
138 |
(*val nxt =
|
walther@59627
|
139 |
("Model_Problem",
|
walther@59627
|
140 |
Model_Problem ["degree_1","polynomial","univariate","equation"])
|
walther@59627
|
141 |
: string * tac *)
|
walther@59627
|
142 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
143 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
144 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
145 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
146 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
147 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
148 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59959
|
149 |
case f of Test_Out.FormKF "[x = 2]" => ()
|
walther@59627
|
150 |
| _ => error "polyeq.sml: diff.behav. in [x = 2]";
|
walther@59627
|
151 |
|
walther@59627
|
152 |
|
walther@59627
|
153 |
"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
|
walther@59627
|
154 |
"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
|
walther@59627
|
155 |
"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
|
walther@59627
|
156 |
(*is in rlang.sml, too*)
|
walther@59627
|
157 |
val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
|
walther@59627
|
158 |
"solveFor x","solutions L"];
|
walther@59627
|
159 |
val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
|
walther@59627
|
160 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
161 |
(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
|
walther@59627
|
162 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
163 |
(* val nxt =
|
walther@59627
|
164 |
("Model_Problem",
|
walther@59627
|
165 |
Model_Problem ["normalise","polynomial","univariate","equation"])
|
walther@59627
|
166 |
: string * tac *)
|
walther@59627
|
167 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
168 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
169 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
170 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
171 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
172 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
173 |
(* val nxt =
|
walther@59627
|
174 |
("Subproblem",
|
walther@59627
|
175 |
Subproblem ("PolyEq",["polynomial","univariate","equation"]))
|
walther@59627
|
176 |
: string * tac*)
|
walther@59627
|
177 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
178 |
(*val nxt =
|
walther@59627
|
179 |
("Model_Problem",
|
walther@59627
|
180 |
Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
|
walther@59627
|
181 |
: string * tac*)
|
walther@59627
|
182 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
183 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
184 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
185 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
186 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
187 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
188 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59959
|
189 |
case f of Test_Out.FormKF "[x = 2 / 15, x = 1]" => ()
|
walther@59627
|
190 |
| _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
|
walther@59627
|
191 |
|
walther@59627
|
192 |
|
walther@59627
|
193 |
" -4 + x^^^2 =0 ";
|
walther@59627
|
194 |
" -4 + x^^^2 =0 ";
|
walther@59627
|
195 |
" -4 + x^^^2 =0 ";
|
walther@59627
|
196 |
val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
|
walther@59627
|
197 |
(* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
|
walther@59627
|
198 |
(*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
|
walther@59627
|
199 |
val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
|
walther@59627
|
200 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
201 |
|
walther@59627
|
202 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
203 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
204 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
205 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
206 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
207 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59627
|
208 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59959
|
209 |
case f of Test_Out.FormKF "[x = 2, x = -2]" => ()
|
walther@59627
|
210 |
| _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
|
walther@59627
|
211 |
|
walther@59627
|
212 |
"----------- rls make_polynomial_in ------------------------------";
|
walther@59627
|
213 |
"----------- rls make_polynomial_in ------------------------------";
|
walther@59627
|
214 |
"----------- rls make_polynomial_in ------------------------------";
|
walther@59627
|
215 |
(*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
|
walther@59627
|
216 |
(*WN.19.3.03 ---v-*)
|
walther@59627
|
217 |
(*3(b)*)val (bdv,v) = (str2term "''bdv''", str2term "R1");
|
walther@59627
|
218 |
val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
|
walther@59627
|
219 |
val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
|
walther@59868
|
220 |
if UnparseC.term t' = "-1 * R * R2 + R2 * R1 + -1 * R * R1 = 0" then ()
|
walther@59627
|
221 |
else error "make_polynomial_in (-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0)";
|
walther@59627
|
222 |
"-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
|
walther@59627
|
223 |
(*WN.19.3.03 ---^-*)
|
walther@59627
|
224 |
|
walther@59627
|
225 |
(*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
|
walther@59627
|
226 |
val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
|
walther@59627
|
227 |
val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
|
walther@59868
|
228 |
if UnparseC.term t' = "y ^^^ 2 + -2 * x * p = 0" then ()
|
walther@59627
|
229 |
else error "make_polynomial_in (y ^^^ 2 + -2 * (x * p) = 0)";
|
walther@59627
|
230 |
|
walther@59627
|
231 |
(*3(d)*)val (bdv,v) = (str2term "''bdv''", str2term "x2");
|
walther@59627
|
232 |
val t = str2term
|
walther@59627
|
233 |
"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";
|
walther@59627
|
234 |
val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
|
walther@59868
|
235 |
if UnparseC.term t' =
|
walther@59627
|
236 |
"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) +\n-1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n-1 * y3 * (1 / 2) * x2 =\n0"
|
walther@59627
|
237 |
then ()
|
walther@59627
|
238 |
else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
|
walther@59627
|
239 |
"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";
|
walther@59627
|
240 |
|
walther@59627
|
241 |
val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
|
walther@59868
|
242 |
if UnparseC.term t' =
|
walther@59627
|
243 |
"A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + -1 * x1 * y2 / 2 + -1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n-1 * y3 * x2 / 2 =\n0"
|
walther@59627
|
244 |
then ()
|
walther@59627
|
245 |
else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
|
walther@59627
|
246 |
"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";
|
walther@59627
|
247 |
|
walther@59627
|
248 |
(*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
|
walther@59627
|
249 |
val t = str2term
|
walther@59627
|
250 |
"A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
|
walther@59627
|
251 |
val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
|
walther@59627
|
252 |
(* the invisible parentheses are as expected *)
|
walther@59627
|
253 |
|
walther@59627
|
254 |
val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
|
walther@59901
|
255 |
Rewrite.trace_on:=(*true*)false;
|
walther@59627
|
256 |
rewrite_set_ thy false expand_binoms t;
|
walther@59901
|
257 |
Rewrite.trace_on:=false;
|
walther@59627
|
258 |
|
walther@59627
|
259 |
|
walther@59627
|
260 |
"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
|
walther@59627
|
261 |
"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
|
walther@59627
|
262 |
"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
|
walther@59627
|
263 |
reset_states ();
|
walther@59627
|
264 |
CalcTree
|
walther@59627
|
265 |
[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
|
walther@59627
|
266 |
("PolyEq",["univariate","equation"],["no_met"]))];
|
walther@59627
|
267 |
Iterator 1;
|
walther@59627
|
268 |
moveActiveRoot 1;
|
walther@59627
|
269 |
|
walther@59627
|
270 |
autoCalculate 1 CompleteCalc;
|
walther@59627
|
271 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
walther@59627
|
272 |
interSteps 1 ([1],Res)
|
walther@59627
|
273 |
(*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);
|
walther@59627
|
274 |
|
walther@59627
|
275 |
|
walther@59627
|
276 |
"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
|
walther@59627
|
277 |
"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
|
walther@59627
|
278 |
"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
|
walther@59627
|
279 |
val t = str2term "-6 * x + 5 * x ^^^ 2 = (0::real)";
|
walther@59627
|
280 |
val subst = [(str2term "(bdv::real)", str2term "(x::real)")];
|
walther@59627
|
281 |
val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
|
walther@59627
|
282 |
(* steps in rls d2_polyeq_bdv_only_simplify:*)
|
walther@59627
|
283 |
|
walther@59627
|
284 |
(*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
|
walther@59868
|
285 |
t |> UnparseC.term; t |> atomty;
|
walther@59871
|
286 |
val thm = ThmC.numerals_to_Free @{thm d2_prescind1};
|
walther@59868
|
287 |
thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
|
walther@59868
|
288 |
val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
|
walther@59627
|
289 |
|
walther@59627
|
290 |
(*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1",""))
|
walther@59627
|
291 |
--> x = 0 | -6 + 5 * x = 0*)
|
walther@59868
|
292 |
t' |> UnparseC.term; t' |> atomty;
|
walther@59871
|
293 |
val thm = ThmC.numerals_to_Free @{thm d2_reduce_equation1};
|
walther@59868
|
294 |
thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
|
walther@59868
|
295 |
val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
|
walther@59627
|
296 |
(* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
|
walther@59627
|
297 |
instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
|
walther@59627
|
298 |
*)
|
walther@59868
|
299 |
if UnparseC.term t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
|
walther@59627
|
300 |
else error "rls d2_polyeq_bdv_only_simplify broken";
|