neuper@37906
|
1 |
(* testexamples for PolyEq, poynomial equations and equational systems
|
neuper@37906
|
2 |
author: Richard Lang
|
neuper@37906
|
3 |
2003
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
use"../smltest/IsacKnowledge/polyeq.sml";
|
neuper@37906
|
7 |
use"polyeq.sml";
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
WN030609: some expls dont work due to unfinished handling of 'expanded terms';
|
neuper@37906
|
10 |
others marked with TODO have to be checked, too.
|
neuper@37906
|
11 |
*)
|
neuper@37906
|
12 |
|
neuper@37906
|
13 |
"-----------------------------------------------------------------";
|
neuper@37906
|
14 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
15 |
(*WN060608 some ----- are not in this table*)
|
neuper@37906
|
16 |
"-----------------------------------------------------------------";
|
neuper@37906
|
17 |
"----------- tests on predicates in problems ---------------------";
|
neuper@37906
|
18 |
"----------- test matching problems --------------------------0---";
|
neuper@37906
|
19 |
"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
neuper@37906
|
20 |
"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
|
neuper@37906
|
21 |
"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
|
neuper@37906
|
22 |
"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
|
neuper@37906
|
23 |
"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
|
neuper@37906
|
24 |
"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
|
neuper@37906
|
25 |
"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
|
neuper@37906
|
26 |
"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
|
neuper@37906
|
27 |
"-----------------------------------------------------------------";
|
neuper@37906
|
28 |
"-----------------------------------------------------------------";
|
neuper@37906
|
29 |
"-----------------------------------------------------------------";
|
neuper@37906
|
30 |
|
neuper@37906
|
31 |
val c = [];
|
neuper@37906
|
32 |
|
neuper@37906
|
33 |
"----------- tests on predicates in problems ---------------------";
|
neuper@37906
|
34 |
"----------- tests on predicates in problems ---------------------";
|
neuper@37906
|
35 |
"----------- tests on predicates in problems ---------------------";
|
neuper@37906
|
36 |
(*
|
neuper@37906
|
37 |
Compiler.Control.Print.printDepth:=5; (*4 default*)
|
neuper@37906
|
38 |
trace_rewrite:=true;
|
neuper@37906
|
39 |
trace_rewrite:=false;
|
neuper@37906
|
40 |
*)
|
neuper@37906
|
41 |
val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
|
neuper@37906
|
42 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t1;
|
neuper@37906
|
43 |
if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
|
neuper@37906
|
44 |
else raise error "polyeq.sml: diff.behav. in lhs";
|
neuper@37906
|
45 |
|
neuper@37906
|
46 |
|
neuper@37906
|
47 |
val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
|
neuper@37906
|
48 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2;
|
neuper@37906
|
49 |
if (term2str t) = "True" then ()
|
neuper@37906
|
50 |
else raise error "polyeq.sml: diff.behav. 1 in is_expended_in";
|
neuper@37906
|
51 |
|
neuper@37906
|
52 |
val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
|
neuper@37906
|
53 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0;
|
neuper@37906
|
54 |
if (term2str t) = "False" then ()
|
neuper@37906
|
55 |
else raise error "polyeq.sml: diff.behav. 2 in is_poly_in";
|
neuper@37906
|
56 |
|
neuper@37906
|
57 |
|
neuper@37906
|
58 |
val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
|
neuper@37906
|
59 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
|
neuper@37906
|
60 |
if (term2str t) = "True" then ()
|
neuper@37906
|
61 |
else raise error "polyeq.sml: diff.behav. 3 in is_poly_in";
|
neuper@37906
|
62 |
|
neuper@37906
|
63 |
|
neuper@37906
|
64 |
val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
|
neuper@37906
|
65 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
|
neuper@37906
|
66 |
if (term2str t) = "True" then ()
|
neuper@37906
|
67 |
else raise error "polyeq.sml: diff.behav. 4 in is_expended_in";
|
neuper@37906
|
68 |
|
neuper@37906
|
69 |
|
neuper@37906
|
70 |
val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
|
neuper@37906
|
71 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6;
|
neuper@37906
|
72 |
if (term2str t) = "True" then ()
|
neuper@37906
|
73 |
else raise error "polyeq.sml: diff.behav. 5 in is_expended_in";
|
neuper@37906
|
74 |
|
neuper@37906
|
75 |
val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
|
neuper@37906
|
76 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
|
neuper@37906
|
77 |
if (term2str t) = "True" then ()
|
neuper@37906
|
78 |
else raise error "polyeq.sml: diff.behav. in has_degree_in_in";
|
neuper@37906
|
79 |
|
neuper@37906
|
80 |
|
neuper@37906
|
81 |
val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
|
neuper@37906
|
82 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
|
neuper@37906
|
83 |
if (term2str t) = "False" then ()
|
neuper@37906
|
84 |
else raise error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
|
neuper@37906
|
85 |
|
neuper@37906
|
86 |
val t4 = (term_of o the o (parse thy))
|
neuper@37906
|
87 |
"((-8 - 2*x + x^^^2) has_degree_in x) = 1";
|
neuper@37906
|
88 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
|
neuper@37906
|
89 |
if (term2str t) = "False" then ()
|
neuper@37906
|
90 |
else raise error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
|
neuper@37906
|
91 |
|
neuper@37906
|
92 |
|
neuper@37906
|
93 |
val t5 = (term_of o the o (parse thy))
|
neuper@37906
|
94 |
"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
|
neuper@37906
|
95 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5;
|
neuper@37906
|
96 |
if (term2str t) = "True" then ()
|
neuper@37906
|
97 |
else raise error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
|
neuper@37906
|
98 |
|
neuper@37906
|
99 |
|
neuper@37906
|
100 |
"----------- test matching problems --------------------------0---";
|
neuper@37906
|
101 |
"----------- test matching problems --------------------------0---";
|
neuper@37906
|
102 |
"----------- test matching problems --------------------------0---";
|
neuper@37906
|
103 |
val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
104 |
val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
|
neuper@37906
|
105 |
get_pbt ["expanded","univariate","equation"];
|
neuper@37906
|
106 |
|
neuper@37906
|
107 |
match_pbl fmz (get_pbt ["expanded","univariate","equation"]);
|
neuper@37906
|
108 |
(*Matches'
|
neuper@37906
|
109 |
{Find=[Correct "solutions L"],
|
neuper@37906
|
110 |
Given=[Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)",
|
neuper@37906
|
111 |
Correct "solveFor x"],Relate=[],
|
neuper@37906
|
112 |
Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
|
neuper@37906
|
113 |
Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],With=[]}
|
neuper@37906
|
114 |
*)
|
neuper@37906
|
115 |
match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]);
|
neuper@37906
|
116 |
(*Matches'
|
neuper@37906
|
117 |
{Find=[Correct "solutions L"],
|
neuper@37906
|
118 |
Given=[Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)",
|
neuper@37906
|
119 |
Correct "solveFor x"],Relate=[],
|
neuper@37906
|
120 |
Where=[Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x =!= 2"],
|
neuper@37906
|
121 |
With=[]}*)
|
neuper@37906
|
122 |
|
neuper@37906
|
123 |
"-------------------- test thm's degree_0 --------------------------------------";
|
neuper@37906
|
124 |
"-------------------- test thm's degree_0 --------------------------------------";
|
neuper@37906
|
125 |
"----- d0_false ------";
|
neuper@37906
|
126 |
(*EP*)
|
neuper@37906
|
127 |
val fmz = ["equality ( 1 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
128 |
val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"],
|
neuper@37906
|
129 |
["PolyEq","solve_d0_polyeq_equation"]);
|
neuper@37906
|
130 |
(*val p = e_pos';
|
neuper@37906
|
131 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
132 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
133 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
134 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
135 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
136 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
137 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
138 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
139 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
140 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
|
neuper@37906
|
141 |
| _ => raise error "polyeq.sml: diff.behav. in 1 = 0 -> []";
|
neuper@37906
|
142 |
|
neuper@37906
|
143 |
"----- d0_true ------";
|
neuper@37906
|
144 |
(*EP-7*)
|
neuper@37906
|
145 |
val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
146 |
val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"],
|
neuper@37906
|
147 |
["PolyEq","solve_d0_polyeq_equation"]);
|
neuper@37906
|
148 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
149 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
150 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
151 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
152 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
153 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
154 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
155 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
156 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
157 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
158 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
|
neuper@37906
|
159 |
| _ => raise error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
|
neuper@37906
|
160 |
|
neuper@37906
|
161 |
"-------------------- test thm's degree_2 ------------------------------------------";
|
neuper@37906
|
162 |
"-------------------- test thm's degree_2 ------------------------------------------";
|
neuper@37906
|
163 |
|
neuper@37906
|
164 |
"-------------------- test thm's d2_pq_formulsxx[_neg]-----";
|
neuper@37906
|
165 |
"-------------------- test thm's d2_pq_formulsxx[_neg]-----";
|
neuper@37906
|
166 |
"-------------------- test thm's d2_pq_formulsxx[_neg]-----";
|
neuper@37906
|
167 |
|
neuper@37906
|
168 |
"----- d2_pqformula1 ------!!!!";
|
neuper@37906
|
169 |
val fmz = ["equality (-2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
170 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
171 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
172 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
173 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
174 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
175 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
176 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
177 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
178 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
179 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
180 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
181 |
(*### or2list _ | _
|
neuper@37906
|
182 |
([3],Res) "x = 2 | x = -1" Or_to_List*)
|
neuper@37906
|
183 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
184 |
(*### or2list _ | _
|
neuper@37906
|
185 |
### applicable_in Check_elementwise: --> ([x = 2, x = -1], [])
|
neuper@37906
|
186 |
([4],Res) "[x = 2, x = -1]" Check_elementwise "Assumptions"*)
|
neuper@37906
|
187 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
188 |
(*### applicable_in Check_elementwise: --> ([x = 2, x = -1], [])
|
neuper@37906
|
189 |
([5],Res) "[x = 2, x = -1]" Check_Postcond*)
|
neuper@37906
|
190 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
191 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
|
neuper@37906
|
192 |
| _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
|
neuper@37906
|
193 |
|
neuper@37906
|
194 |
"----- d2_pqformula1_neg ------";
|
neuper@37906
|
195 |
(*EP-8*)
|
neuper@37906
|
196 |
val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
197 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
198 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
199 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
200 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
201 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
202 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
203 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
204 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
205 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
206 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
207 |
(*### or2list False
|
neuper@37906
|
208 |
([1],Res) False Or_to_List)*)
|
neuper@37906
|
209 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
210 |
(*### or2list False
|
neuper@37906
|
211 |
([2],Res) [] Check_elementwise "Assumptions"*)
|
neuper@37906
|
212 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
213 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
214 |
val asm = get_assumptions_ pt p;
|
neuper@37906
|
215 |
if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
|
neuper@37906
|
216 |
else raise error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
|
neuper@37906
|
217 |
|
neuper@37906
|
218 |
"----- d2_pqformula2 ------";
|
neuper@37906
|
219 |
val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
220 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
221 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
222 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
223 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
224 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
225 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
226 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
227 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
228 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
229 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
230 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
231 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
232 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
233 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
234 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
|
neuper@37906
|
235 |
| _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
|
neuper@37906
|
236 |
|
neuper@37906
|
237 |
|
neuper@37906
|
238 |
"----- d2_pqformula2_neg ------";
|
neuper@37906
|
239 |
val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
240 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
241 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
242 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
243 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
244 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
245 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
246 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
247 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
248 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
249 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
250 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
251 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
252 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
253 |
"TODO 2 +(-1)*x + 1*x^^^2 = 0";
|
neuper@37906
|
254 |
"TODO 2 +(-1)*x + 1*x^^^2 = 0";
|
neuper@37906
|
255 |
"TODO 2 +(-1)*x + 1*x^^^2 = 0";
|
neuper@37906
|
256 |
|
neuper@37906
|
257 |
|
neuper@37906
|
258 |
"----- d2_pqformula3 ------";
|
neuper@37906
|
259 |
(*EP-9*)
|
neuper@37906
|
260 |
val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
261 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
262 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
263 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
264 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
265 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
266 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
267 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
268 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
269 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
270 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
271 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
272 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
273 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
274 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
275 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
|
neuper@37906
|
276 |
| _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
|
neuper@37906
|
277 |
|
neuper@37906
|
278 |
"----- d2_pqformula3_neg ------";
|
neuper@37906
|
279 |
val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
280 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
281 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
282 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
283 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
284 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
285 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
286 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
287 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
288 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
289 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
290 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
291 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
292 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
293 |
"TODO 2 + x + x^^^2 = 0";
|
neuper@37906
|
294 |
"TODO 2 + x + x^^^2 = 0";
|
neuper@37906
|
295 |
"TODO 2 + x + x^^^2 = 0";
|
neuper@37906
|
296 |
|
neuper@37906
|
297 |
|
neuper@37906
|
298 |
"----- d2_pqformula4 ------";
|
neuper@37906
|
299 |
val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
300 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
301 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
302 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
303 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
304 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
305 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
306 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
307 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
308 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
309 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
310 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
311 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
312 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
313 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
314 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
|
neuper@37906
|
315 |
| _ => raise error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
|
neuper@37906
|
316 |
|
neuper@37906
|
317 |
"----- d2_pqformula4_neg ------";
|
neuper@37906
|
318 |
val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
319 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
320 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
321 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
322 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
323 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
324 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
325 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
326 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
327 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
328 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
329 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
330 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
331 |
"TODO 2 + x + 1*x^^^2 = 0";
|
neuper@37906
|
332 |
"TODO 2 + x + 1*x^^^2 = 0";
|
neuper@37906
|
333 |
"TODO 2 + x + 1*x^^^2 = 0";
|
neuper@37906
|
334 |
|
neuper@37906
|
335 |
"----- d2_pqformula5 ------";
|
neuper@37906
|
336 |
val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
337 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
338 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
339 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
340 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
341 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
342 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
343 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
344 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
345 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
346 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
347 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
348 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
349 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
350 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
351 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
|
neuper@37906
|
352 |
| _ => raise error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
|
neuper@37906
|
353 |
|
neuper@37906
|
354 |
"----- d2_pqformula6 ------";
|
neuper@37906
|
355 |
val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
356 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
357 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
358 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
359 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
360 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
361 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
362 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
363 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
364 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
365 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
366 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
367 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
368 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
369 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
370 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
|
neuper@37906
|
371 |
| _ => raise error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
|
neuper@37906
|
372 |
|
neuper@37906
|
373 |
"----- d2_pqformula7 ------";
|
neuper@37906
|
374 |
(*EP-10*)
|
neuper@37906
|
375 |
val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
376 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
377 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
378 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
379 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
380 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
381 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
382 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
383 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
384 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
385 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
386 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
387 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
388 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
389 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
390 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
|
neuper@37906
|
391 |
| _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
|
neuper@37906
|
392 |
|
neuper@37906
|
393 |
"----- d2_pqformula8 ------";
|
neuper@37906
|
394 |
val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
395 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
396 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
397 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
398 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
399 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
400 |
|
neuper@37906
|
401 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
402 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
403 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
404 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
405 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
406 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
407 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
408 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
409 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
410 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
|
neuper@37906
|
411 |
| _ => raise error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
|
neuper@37906
|
412 |
|
neuper@37906
|
413 |
"----- d2_pqformula9 ------";
|
neuper@37906
|
414 |
val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
415 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
416 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
417 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
418 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
419 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
420 |
|
neuper@37906
|
421 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
422 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
423 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
424 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
425 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
426 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
427 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
428 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
429 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
|
neuper@37906
|
430 |
| _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
|
neuper@37906
|
431 |
|
neuper@37906
|
432 |
|
neuper@37906
|
433 |
"----- d2_pqformula10_neg ------";
|
neuper@37906
|
434 |
val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
435 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
436 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
437 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
438 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
439 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
440 |
|
neuper@37906
|
441 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
442 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
443 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
444 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
445 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
446 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
447 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
448 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
449 |
"TODO 4 + x^^^2 = 0";
|
neuper@37906
|
450 |
"TODO 4 + x^^^2 = 0";
|
neuper@37906
|
451 |
"TODO 4 + x^^^2 = 0";
|
neuper@37906
|
452 |
|
neuper@37906
|
453 |
"----- d2_pqformula10 ------";
|
neuper@37906
|
454 |
val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
455 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
456 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
457 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
458 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
459 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
460 |
|
neuper@37906
|
461 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
462 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
463 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
464 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
465 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
466 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
467 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
468 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
469 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
|
neuper@37906
|
470 |
| _ => raise error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
|
neuper@37906
|
471 |
|
neuper@37906
|
472 |
"----- d2_pqformula9_neg ------";
|
neuper@37906
|
473 |
val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
474 |
val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
475 |
["PolyEq","solve_d2_polyeq_pq_equation"]);
|
neuper@37906
|
476 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
477 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
478 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
479 |
|
neuper@37906
|
480 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
481 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
482 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
483 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
484 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
485 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
486 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
487 |
"TODO 4 + 1*x^^^2 = 0";
|
neuper@37906
|
488 |
"TODO 4 + 1*x^^^2 = 0";
|
neuper@37906
|
489 |
"TODO 4 + 1*x^^^2 = 0";
|
neuper@37906
|
490 |
|
neuper@37906
|
491 |
"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
|
neuper@37906
|
492 |
"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
|
neuper@37906
|
493 |
"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
|
neuper@37906
|
494 |
|
neuper@37906
|
495 |
val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
496 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
497 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
498 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
499 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
500 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
501 |
|
neuper@37906
|
502 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
503 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
504 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
505 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
506 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
507 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
508 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
509 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
510 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
|
neuper@37906
|
511 |
| _ => raise error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
|
neuper@37906
|
512 |
|
neuper@37906
|
513 |
val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
514 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
515 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
516 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
517 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
518 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
519 |
|
neuper@37906
|
520 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
521 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
522 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
523 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
524 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
525 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
526 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
527 |
"TODO 1 +(-1)*x + 2*x^^^2 = 0";
|
neuper@37906
|
528 |
"TODO 1 +(-1)*x + 2*x^^^2 = 0";
|
neuper@37906
|
529 |
"TODO 1 +(-1)*x + 2*x^^^2 = 0";
|
neuper@37906
|
530 |
|
neuper@37906
|
531 |
(*EP-11*)
|
neuper@37906
|
532 |
val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
533 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
534 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
535 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
536 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
537 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
538 |
|
neuper@37906
|
539 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
540 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
541 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
542 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
543 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
544 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
545 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
546 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
547 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
|
neuper@37906
|
548 |
| _ => raise error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
|
neuper@37906
|
549 |
|
neuper@37906
|
550 |
val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
551 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
552 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
553 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
554 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
555 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
556 |
|
neuper@37906
|
557 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
558 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
559 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
560 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
561 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
562 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
563 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
564 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
565 |
"TODO 1 + x + 2*x^^^2 = 0";
|
neuper@37906
|
566 |
"TODO 1 + x + 2*x^^^2 = 0";
|
neuper@37906
|
567 |
"TODO 1 + x + 2*x^^^2 = 0";
|
neuper@37906
|
568 |
|
neuper@37906
|
569 |
val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
570 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
571 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
572 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
573 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
574 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
575 |
|
neuper@37906
|
576 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
577 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
578 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
579 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
580 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
581 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
582 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
583 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
584 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
|
neuper@37906
|
585 |
| _ => raise error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
|
neuper@37906
|
586 |
|
neuper@37906
|
587 |
val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
588 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
589 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
590 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
591 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
592 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
593 |
|
neuper@37906
|
594 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
595 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
596 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
597 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
598 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
599 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
600 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
601 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
602 |
"TODO 2 + 1*x + x^^^2 = 0";
|
neuper@37906
|
603 |
"TODO 2 + 1*x + x^^^2 = 0";
|
neuper@37906
|
604 |
"TODO 2 + 1*x + x^^^2 = 0";
|
neuper@37906
|
605 |
|
neuper@37906
|
606 |
(*EP-12*)
|
neuper@37906
|
607 |
val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
608 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
609 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
610 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
611 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
612 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
613 |
|
neuper@37906
|
614 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
615 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
616 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
617 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
618 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
619 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
620 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
621 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
622 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
|
neuper@37906
|
623 |
| _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
|
neuper@37906
|
624 |
|
neuper@37906
|
625 |
val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
626 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
627 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
628 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
629 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
630 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
631 |
|
neuper@37906
|
632 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
633 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
634 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
635 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
636 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
637 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
638 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
639 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
640 |
"TODO 2 + x + x^^^2 = 0";
|
neuper@37906
|
641 |
"TODO 2 + x + x^^^2 = 0";
|
neuper@37906
|
642 |
"TODO 2 + x + x^^^2 = 0";
|
neuper@37906
|
643 |
|
neuper@37906
|
644 |
(*EP-13*)
|
neuper@37906
|
645 |
val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
646 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
647 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
648 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
649 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
650 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
651 |
|
neuper@37906
|
652 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
653 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
654 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
655 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
656 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
657 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
658 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
659 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
660 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
|
neuper@37906
|
661 |
| _ => raise error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
|
neuper@37906
|
662 |
|
neuper@37906
|
663 |
val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
664 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
665 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
666 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
667 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
668 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
669 |
|
neuper@37906
|
670 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
671 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
672 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
673 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
674 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
675 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
676 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
677 |
"TODO 8+ 2*x^^^2 = 0";
|
neuper@37906
|
678 |
"TODO 8+ 2*x^^^2 = 0";
|
neuper@37906
|
679 |
"TODO 8+ 2*x^^^2 = 0";
|
neuper@37906
|
680 |
|
neuper@37906
|
681 |
(*EP-14*)
|
neuper@37906
|
682 |
val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
683 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
684 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
685 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
686 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
687 |
|
neuper@37906
|
688 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
689 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
690 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
691 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
692 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
693 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
694 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
695 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
696 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
|
neuper@37906
|
697 |
| _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
|
neuper@37906
|
698 |
|
neuper@37906
|
699 |
|
neuper@37906
|
700 |
val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
701 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
702 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
703 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
704 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
705 |
|
neuper@37906
|
706 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
707 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
708 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
709 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
710 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
711 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
712 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
713 |
"TODO 4+ x^^^2 = 0";
|
neuper@37906
|
714 |
"TODO 4+ x^^^2 = 0";
|
neuper@37906
|
715 |
"TODO 4+ x^^^2 = 0";
|
neuper@37906
|
716 |
|
neuper@37906
|
717 |
(*EP-15*)
|
neuper@37906
|
718 |
val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
719 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
720 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
721 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
722 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
723 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
724 |
|
neuper@37906
|
725 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
726 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
727 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
728 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
729 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
730 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
731 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
732 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
733 |
case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
|
neuper@37906
|
734 |
| _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
|
neuper@37906
|
735 |
|
neuper@37906
|
736 |
val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
737 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
738 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
739 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
740 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
741 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
742 |
|
neuper@37906
|
743 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
744 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
745 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
746 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
747 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
748 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
749 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
750 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
751 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
|
neuper@37906
|
752 |
| _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
|
neuper@37906
|
753 |
|
neuper@37906
|
754 |
(*EP-16*)
|
neuper@37906
|
755 |
val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
756 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
757 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
758 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
759 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
760 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
761 |
|
neuper@37906
|
762 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
763 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
764 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
765 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
766 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
767 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
768 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
769 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
770 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
|
neuper@37906
|
771 |
| _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
|
neuper@37906
|
772 |
|
neuper@37906
|
773 |
(*EP-//*)
|
neuper@37906
|
774 |
val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
|
neuper@37906
|
775 |
val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@37906
|
776 |
["PolyEq","solve_d2_polyeq_abc_equation"]);
|
neuper@37906
|
777 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
778 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
779 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
780 |
|
neuper@37906
|
781 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
782 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
783 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
784 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
785 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
786 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
787 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
788 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
789 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
|
neuper@37906
|
790 |
| _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
|
neuper@37906
|
791 |
|
neuper@37906
|
792 |
"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
neuper@37906
|
793 |
"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
neuper@37906
|
794 |
"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
neuper@37906
|
795 |
val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
|
neuper@37906
|
796 |
"solveFor x","solutions L"];
|
neuper@37906
|
797 |
val (dI',pI',mI') =
|
neuper@37906
|
798 |
("PolyEq.thy",["degree_2","expanded","univariate","equation"],
|
neuper@37906
|
799 |
["PolyEq","complete_square"]);
|
neuper@37906
|
800 |
(* val p = e_pos'; val c = [];
|
neuper@37906
|
801 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
802 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
803 |
|
neuper@37906
|
804 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
805 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
806 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
807 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
808 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
809 |
(*Apply_Method ("PolyEq.thy","complete_square")*)
|
neuper@37906
|
810 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
811 |
(*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
|
neuper@37906
|
812 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
813 |
(*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
|
neuper@37906
|
814 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
815 |
(*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
|
neuper@37906
|
816 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
817 |
(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
|
neuper@37906
|
818 |
2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
|
neuper@37906
|
819 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
820 |
(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
|
neuper@37906
|
821 |
-1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
|
neuper@37906
|
822 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
823 |
(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
|
neuper@37906
|
824 |
-1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
|
neuper@37906
|
825 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
826 |
(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
|
neuper@37906
|
827 |
x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
|
neuper@37906
|
828 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
829 |
(*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
|
neuper@37906
|
830 |
x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
|
neuper@37906
|
831 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
832 |
(*"x = -2 | x = 4" nxt = Or_to_List*)
|
neuper@37906
|
833 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
834 |
(*"[x = -2, x = 4]" nxt = Check_Postcond*)
|
neuper@37906
|
835 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
neuper@37906
|
836 |
(* FIXXXME
|
neuper@37906
|
837 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
|
neuper@37906
|
838 |
| _ => raise error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
|
neuper@37906
|
839 |
*)
|
neuper@37906
|
840 |
if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
|
neuper@37906
|
841 |
else raise error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
|
neuper@37906
|
842 |
|
neuper@37906
|
843 |
|
neuper@37906
|
844 |
"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
|
neuper@37906
|
845 |
"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
|
neuper@37906
|
846 |
"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
|
neuper@37906
|
847 |
"---- test the erls ----";
|
neuper@37906
|
848 |
val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
|
neuper@37906
|
849 |
val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
|
neuper@37906
|
850 |
val t' = term2str t;
|
neuper@37906
|
851 |
(*if t'= "True" then ()
|
neuper@37906
|
852 |
else raise error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
|
neuper@37906
|
853 |
(* *)
|
neuper@37906
|
854 |
val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
|
neuper@37906
|
855 |
"solveFor x","solutions L"];
|
neuper@37906
|
856 |
val (dI',pI',mI') =
|
neuper@37906
|
857 |
("PolyEq.thy",["degree_2","expanded","univariate","equation"],
|
neuper@37906
|
858 |
["PolyEq","complete_square"]);
|
neuper@37906
|
859 |
(* val p = e_pos'; val c = [];
|
neuper@37906
|
860 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
861 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
862 |
|
neuper@37906
|
863 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
864 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
865 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
866 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
867 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
868 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
869 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
870 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
871 |
(*Apply_Method ("PolyEq.thy","complete_square")*)
|
neuper@37906
|
872 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
neuper@37906
|
873 |
|
neuper@37906
|
874 |
"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
|
neuper@37906
|
875 |
"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
|
neuper@37906
|
876 |
"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
|
neuper@37906
|
877 |
val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
|
neuper@37906
|
878 |
"solveFor x","solutions L"];
|
neuper@37906
|
879 |
val (dI',pI',mI') =
|
neuper@37906
|
880 |
("PolyEq.thy",["degree_2","expanded","univariate","equation"],
|
neuper@37906
|
881 |
["PolyEq","complete_square"]);
|
neuper@37906
|
882 |
(* val p = e_pos'; val c = [];
|
neuper@37906
|
883 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
884 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
885 |
|
neuper@37906
|
886 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
887 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
888 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
889 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
890 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
891 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
892 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
893 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
894 |
(*Apply_Method ("PolyEq.thy","complete_square")*)
|
neuper@37906
|
895 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
896 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
897 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
898 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
899 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
900 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
901 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
902 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
903 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
904 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
905 |
(* FIXXXXME n1.,
|
neuper@37906
|
906 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
|
neuper@37906
|
907 |
| _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
|
neuper@37906
|
908 |
*)
|
neuper@37906
|
909 |
|
neuper@37906
|
910 |
"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
|
neuper@37906
|
911 |
"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
|
neuper@37906
|
912 |
"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
|
neuper@37906
|
913 |
val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
|
neuper@37906
|
914 |
"solveFor x","solutions L"];
|
neuper@37906
|
915 |
val (dI',pI',mI') =
|
neuper@37906
|
916 |
("PolyEq.thy",["degree_2","expanded","univariate","equation"],
|
neuper@37906
|
917 |
["PolyEq","complete_square"]);
|
neuper@37906
|
918 |
(* val p = e_pos'; val c = [];
|
neuper@37906
|
919 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
920 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
921 |
|
neuper@37906
|
922 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
923 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
924 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
925 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
926 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
927 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
928 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
929 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
930 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
931 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
932 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
933 |
|
neuper@37906
|
934 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
935 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
936 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
937 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
938 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
939 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
940 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
941 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
neuper@37906
|
942 |
(*WN.2.5.03 TODO FIXME Matthias ?
|
neuper@37906
|
943 |
case f of
|
neuper@37906
|
944 |
Form'
|
neuper@37906
|
945 |
(FormKF
|
neuper@37906
|
946 |
(~1,EdUndef,0,Nundef,
|
neuper@37906
|
947 |
"[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)]"))
|
neuper@37906
|
948 |
=> ()
|
neuper@37906
|
949 |
| _ => raise error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
|
neuper@37906
|
950 |
this will be simplified [x = a, x = b] to by Factor.ML*)
|
neuper@37906
|
951 |
|
neuper@37906
|
952 |
|
neuper@37906
|
953 |
"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
|
neuper@37906
|
954 |
"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
|
neuper@37906
|
955 |
"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
|
neuper@37906
|
956 |
val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
|
neuper@37906
|
957 |
"solveFor x","solutions L"];
|
neuper@37906
|
958 |
val (dI',pI',mI') =
|
neuper@37906
|
959 |
("PolyEq.thy",["degree_2","expanded","univariate","equation"],
|
neuper@37906
|
960 |
["PolyEq","complete_square"]);
|
neuper@37906
|
961 |
(* val p = e_pos'; val c = [];
|
neuper@37906
|
962 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
963 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
964 |
|
neuper@37906
|
965 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
966 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
967 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
968 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
969 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
970 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
971 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
972 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
973 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
974 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
975 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
976 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
977 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
978 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
neuper@37906
|
979 |
(*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
|
neuper@37906
|
980 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
|
neuper@37906
|
981 |
| _ => raise error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
|
neuper@37906
|
982 |
*)
|
neuper@37906
|
983 |
|
neuper@37906
|
984 |
"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
|
neuper@37906
|
985 |
"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
|
neuper@37906
|
986 |
"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
|
neuper@37906
|
987 |
val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
|
neuper@37906
|
988 |
"solveFor x","solutions L"];
|
neuper@37906
|
989 |
val (dI',pI',mI') =
|
neuper@37906
|
990 |
("PolyEq.thy",["degree_2","expanded","univariate","equation"],
|
neuper@37906
|
991 |
["PolyEq","complete_square"]);
|
neuper@37906
|
992 |
(* val p = e_pos'; val c = [];
|
neuper@37906
|
993 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
994 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
995 |
|
neuper@37906
|
996 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
997 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
998 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
999 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
1000 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
1001 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
1002 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
1003 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
1004 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
1005 |
(*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
|
neuper@37906
|
1006 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
|
neuper@37906
|
1007 |
| _ => raise error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
|
neuper@37906
|
1008 |
*)
|
neuper@37906
|
1009 |
if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
|
neuper@37906
|
1010 |
else raise error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
|
neuper@37906
|
1011 |
|
neuper@37906
|
1012 |
|
neuper@37906
|
1013 |
"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
|
neuper@37906
|
1014 |
"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
|
neuper@37906
|
1015 |
"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
|
neuper@37906
|
1016 |
(*EP-17 Schalk_I_p86_n5*)
|
neuper@37906
|
1017 |
val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
|
neuper@37906
|
1018 |
(* refine fmz ["univariate","equation"];
|
neuper@37906
|
1019 |
*)
|
neuper@37906
|
1020 |
val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
|
neuper@37906
|
1021 |
(*val p = e_pos';
|
neuper@37906
|
1022 |
val c = [];
|
neuper@37906
|
1023 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
1024 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
1025 |
|
neuper@37906
|
1026 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
1027 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1028 |
(* val nxt =
|
neuper@37906
|
1029 |
("Model_Problem",
|
neuper@37906
|
1030 |
Model_Problem ["normalize","polynomial","univariate","equation"])
|
neuper@37906
|
1031 |
: string * tac*)
|
neuper@37906
|
1032 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1033 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1034 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1035 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1036 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1037 |
(* val nxt =
|
neuper@37906
|
1038 |
("Subproblem",
|
neuper@37906
|
1039 |
Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
|
neuper@37906
|
1040 |
: string * tac *)
|
neuper@37906
|
1041 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1042 |
(*val nxt =
|
neuper@37906
|
1043 |
("Model_Problem",
|
neuper@37906
|
1044 |
Model_Problem ["degree_1","polynomial","univariate","equation"])
|
neuper@37906
|
1045 |
: string * tac *)
|
neuper@37906
|
1046 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1047 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1048 |
|
neuper@37906
|
1049 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1050 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1051 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1052 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1053 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1054 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
|
neuper@37906
|
1055 |
| _ => raise error "polyeq.sml: diff.behav. in [x = 2]";
|
neuper@37906
|
1056 |
|
neuper@37906
|
1057 |
|
neuper@37906
|
1058 |
"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
|
neuper@37906
|
1059 |
"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
|
neuper@37906
|
1060 |
"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
|
neuper@37906
|
1061 |
(*is in rlang.sml, too*)
|
neuper@37906
|
1062 |
val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
|
neuper@37906
|
1063 |
"solveFor x","solutions L"];
|
neuper@37906
|
1064 |
val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
|
neuper@37906
|
1065 |
|
neuper@37906
|
1066 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
1067 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
1068 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
1069 |
|
neuper@37906
|
1070 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
1071 |
(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
|
neuper@37906
|
1072 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1073 |
(* val nxt =
|
neuper@37906
|
1074 |
("Model_Problem",
|
neuper@37906
|
1075 |
Model_Problem ["normalize","polynomial","univariate","equation"])
|
neuper@37906
|
1076 |
: string * tac *)
|
neuper@37906
|
1077 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1078 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1079 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1080 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1081 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1082 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1083 |
(* val nxt =
|
neuper@37906
|
1084 |
("Subproblem",
|
neuper@37906
|
1085 |
Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
|
neuper@37906
|
1086 |
: string * tac*)
|
neuper@37906
|
1087 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1088 |
(*val nxt =
|
neuper@37906
|
1089 |
("Model_Problem",
|
neuper@37906
|
1090 |
Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
|
neuper@37906
|
1091 |
: string * tac*)
|
neuper@37906
|
1092 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1093 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1094 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1095 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1096 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1097 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1098 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1099 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
|
neuper@37906
|
1100 |
| _ => raise error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
|
neuper@37906
|
1101 |
|
neuper@37906
|
1102 |
|
neuper@37906
|
1103 |
" -4 + x^^^2 =0 ";
|
neuper@37906
|
1104 |
" -4 + x^^^2 =0 ";
|
neuper@37906
|
1105 |
" -4 + x^^^2 =0 ";
|
neuper@37906
|
1106 |
val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
|
neuper@37906
|
1107 |
(* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
|
neuper@37906
|
1108 |
(*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
|
neuper@37906
|
1109 |
val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
|
neuper@37906
|
1110 |
(*val p = e_pos';
|
neuper@37906
|
1111 |
val c = [];
|
neuper@37906
|
1112 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
1113 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
1114 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
1115 |
|
neuper@37906
|
1116 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1117 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1118 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1119 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1120 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1121 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1122 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
1123 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
|
neuper@37906
|
1124 |
| _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
|
neuper@37906
|
1125 |
|
neuper@37906
|
1126 |
"----------------- polyeq.sml end ------------------";
|
neuper@37906
|
1127 |
|
neuper@37906
|
1128 |
(*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
|
neuper@37906
|
1129 |
(*WN.19.3.03 ---v-*)
|
neuper@37906
|
1130 |
(*3(b)*)val (bdv,v) = (str2term "bdv", str2term "R1");
|
neuper@37906
|
1131 |
val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
|
neuper@37906
|
1132 |
val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
|
neuper@37906
|
1133 |
term2str t';
|
neuper@37906
|
1134 |
"-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
|
neuper@37906
|
1135 |
(*WN.19.3.03 ---^-*)
|
neuper@37906
|
1136 |
|
neuper@37906
|
1137 |
(*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
|
neuper@37906
|
1138 |
val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
|
neuper@37906
|
1139 |
val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
|
neuper@37906
|
1140 |
term2str t';
|
neuper@37906
|
1141 |
"y ^^^ 2 + -2 * x * p = 0";
|
neuper@37906
|
1142 |
|
neuper@37906
|
1143 |
(*3(d)*)val (bdv,v) = (str2term "bdv", str2term "x2");
|
neuper@37906
|
1144 |
val t = str2term
|
neuper@37906
|
1145 |
"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";
|
neuper@37906
|
1146 |
val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
|
neuper@37906
|
1147 |
term2str t';
|
neuper@37906
|
1148 |
"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";
|
neuper@37906
|
1149 |
val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
|
neuper@37906
|
1150 |
term2str t';
|
neuper@37906
|
1151 |
"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";
|
neuper@37906
|
1152 |
|
neuper@37906
|
1153 |
(*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
|
neuper@37906
|
1154 |
val t = str2term
|
neuper@37906
|
1155 |
"A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
|
neuper@37906
|
1156 |
val None = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
|
neuper@37906
|
1157 |
(*die _unsichtbare_ Klammern sind genau wie gew"unscht*)
|
neuper@37906
|
1158 |
|
neuper@37906
|
1159 |
|
neuper@37906
|
1160 |
val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
|
neuper@37906
|
1161 |
trace_rewrite:=true;
|
neuper@37906
|
1162 |
rewrite_set_ thy false expand_binoms t;
|
neuper@37906
|
1163 |
trace_rewrite:=false;
|
neuper@37906
|
1164 |
|
neuper@37906
|
1165 |
|
neuper@37906
|
1166 |
"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
|
neuper@37906
|
1167 |
"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
|
neuper@37906
|
1168 |
"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
|
neuper@37906
|
1169 |
states:=[];
|
neuper@37906
|
1170 |
CalcTree
|
neuper@37906
|
1171 |
[(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
|
neuper@37906
|
1172 |
("PolyEq.thy",["univariate","equation"],["no_met"]))];
|
neuper@37906
|
1173 |
Iterator 1;
|
neuper@37906
|
1174 |
moveActiveRoot 1;
|
neuper@37906
|
1175 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
1176 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
1177 |
|
neuper@37906
|
1178 |
interSteps 1 ([1],Res) (*no Rewrite_Set...*);
|