2 use"../kbtest/rooteq.sml";
4 testexamples for RootEq, equations with fractions
6 Compiler.Control.Print.printDepth:=10; (*4 default*)
7 Compiler.Control.Print.printDepth:=5; (*4 default*)
10 "----------- rooteq.sml begin--------";
11 "--------------(1/sqrt(x)=5)---------------------------------------";
12 "--------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))----------------------";
13 "--------------(sqrt(x+1)=5)---------------------------------------";
14 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
15 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
16 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
18 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
19 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
20 val result = term2str t_;
21 if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
23 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
24 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25 val result = term2str t_;
26 if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
28 val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x";
29 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
30 val result = term2str t_;
31 if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
33 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x";
34 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
35 val result = term2str t_;
36 if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
38 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x";
39 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
40 val result = term2str t_;
41 if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
43 val t = (term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
44 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
45 val result = term2str t_;
46 if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
48 val t = (term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
49 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
50 val result = term2str t_;
51 if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
53 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
54 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
55 val result = term2str t_;
56 if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
58 val t = (term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
59 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
60 val result = term2str t_;
61 if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
63 val t = (term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
64 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
65 val result = term2str t_;
66 if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
68 val t = (term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
69 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
70 val result = term2str t_;
71 if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
73 val t = (term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
74 val Some(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
75 val result = term2str t_;
76 if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
80 val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
81 (get_pbt ["root","univariate","equation"]);
82 case result of Matches' _ => () | _ => raise error "rooteq.sml: new behaviour:";
84 val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
85 (get_pbt ["root","univariate","equation"]);
86 case result of NoMatch' _ => () | _ => raise error "rooteq.sml: new behaviour:";
88 (*---------rooteq---- 23.8.02 ---------------------*)
89 "---------(1/sqrt(x)=5)---------------------";
90 val fmz = ["equality (1/sqrt(x)=5)","solveFor x","solutions L"];
91 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
93 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
100 (*"1 / x = 25" -> Subproblem ("RootEq.thy", ["univariate", ...]) *)
101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
107 (*"1 = 25 * x" -> Subproblem ("RatEq.thy", ["univariate", ...])*)
108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
114 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -25 * x = 0")) then ()
115 else raise error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
116 (*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
128 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => ()
129 | _ => raise error "rooteq.sml: diff.behav. [x = 1 / 25]";
130 if asms2str (get_assumptions_ pt p) = "[(0 <= 1 / 25, [])]"
131 (*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..:
132 [(str2term"25 ~= 0",[])] *)
133 then writeln "should be True\n\
136 else raise error "rooteq.sml: diff.behav. with 25 ~= 0";
138 "---------(sqrt(x+1)=5)---------------------";
139 val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"];
140 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
143 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
144 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
145 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
146 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
152 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
154 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
159 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + x = 0")) then ()
160 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
161 (*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
163 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
166 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
167 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
168 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
169 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
170 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
171 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 24]")) => ()
172 | _ => raise error "rooteq.sml: diff.behav. [x = 24]";
174 "-------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))-----------------";
175 val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))","solveFor x","solutions L"];
176 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
178 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
179 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
180 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
181 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
182 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
183 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
184 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
185 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
186 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
187 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
188 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
190 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-184 + 46 * x = 0")) then ()
191 else raise error "rooteq.sml: diff.behav.poly in 4*sqrt(4*x+2)=3*sqrt(2*x+24)";
192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
194 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
195 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
196 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
197 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
199 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
200 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
201 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
202 | _ => raise error "rooteq.sml: diff.behav. [x = 4]";
203 if get_assumptions_ pt p = [(str2term"0 <= 12 * sqrt 2 * 4",[])]
204 then writeln "should be True\nshould be True\nshould be True\n\
205 \should be True\nshould be True\nshould be True\n"
206 else raise error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4";
208 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------";
209 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))","solveFor x","solutions L"];
210 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
212 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
213 (*val nxt = Model_Problem ["sq","root","univariate","equation"]) *)
214 val (p,_,f,nxt,_,pt) = me nxt p c pt;
215 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
216 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
217 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
218 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
219 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
220 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
221 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
222 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
223 val (p,_,f,nxt,_,pt) = me nxt p c pt;
224 (*val nxt = Model_Problem ["sq","root","univariate","equation"]) *)
225 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
226 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
227 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
228 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
229 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
230 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
231 val (p,_,f,nxt,_,pt) = me nxt p c pt;
232 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
233 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
234 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
235 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
236 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
237 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
238 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
239 val (p,_,f,nxt,_,pt) = me nxt p c pt;
240 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
241 else raise error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr..";
242 (*-> Subproblem ("PolyEq.thy", ["degree_0", ...])*)
243 val (p,_,f,nxt,_,pt) = me nxt p c pt;
244 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
245 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
246 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
247 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
248 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
249 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
250 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
251 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
252 val (p,_,f,nxt,_,pt) = me nxt p c pt;
253 val asm = get_assumptions_ pt p;
254 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso asm = []
255 then () else raise error "rooteq.sml: diff.behav. in UniversalList 1";
259 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------";
261 ["equality (13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
262 "solveFor x","solutions L"];
263 val (dI',pI',mI') = ("RootEq.thy",["sq","root","univariate","equation"],
264 ["RootEq","solve_sq_root_equation"]);
265 (*val p = e_pos'; val c = [];
266 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
267 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
268 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
269 val (p,_,f,nxt,_,pt) = me nxt p c pt;
270 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
271 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
272 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
273 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
274 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
275 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
276 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
277 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"])) *)
278 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
279 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
280 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
281 val (p,_,f,nxt,_,pt) = me nxt p c pt;
282 (*val p = ([6],Pbl)val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
283 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
284 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
285 (*val p = ([6,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
286 val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
287 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
288 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
289 val (p,_,f,nxt,_,pt) = me nxt p c pt;
290 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
291 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
292 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
293 (*val nxt = Specify_Method ["PolyEq","solve_d0_polyeq_equation"]) *)
294 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
295 val (p,_,f,nxt,_,pt) = me nxt p c pt;
296 (*val p = ([6,3,1],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"True"))
297 val nxt = ("Or_to_List",Or_to_List) : string * tac*)
298 val (p,_,f,nxt,_,pt) = me nxt p c pt;
299 (*val p = ([6,3,2],Res) val f = (~1,EdUndef,3,Nundef,"UniversalList"))
300 val nxt = Check_Postcond ["degree_0","polynomial","univariate","equation"])*)
301 val (p,_,f,nxt,_,pt) = me nxt p c pt;
302 (*val p = ([6,3],Res) val f =(~1,EdUndef,2,Nundef,"UniversalList"))
303 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
304 val (p,_,f,nxt,_,pt) = me nxt p c pt;
305 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "UniversalList")) then ()
306 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
307 (* val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;
310 (*same error as full expl #######*)
312 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- OKversion----";
313 val fmz = ["equality (sqrt(x) = 1)","solveFor x","solutions L"];
314 val (dI',pI',mI') = ("RootEq.thy",["sq","root","univariate","equation"],
315 ["RootEq","solve_sq_root_equation"]);
316 (*val p = e_pos'; val c = [];
317 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
318 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
319 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
320 val (p,_,f,nxt,_,pt) = me nxt p c pt;
321 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
322 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
323 val (p,_,f,nxt,_,pt) = me nxt p c pt;
324 (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq","solve_sq_root_equation"*)
325 val (p,_,f,nxt,_,pt) = me nxt p c pt;
326 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
327 val (p,_,f,nxt,_,pt) = me nxt p c pt;
328 (* val p = ([2],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = 1"))
329 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
330 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
331 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
332 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
333 val (p,_,f,nxt,_,pt) = me nxt p c pt;
334 (*val nxt = ("Specify_Method",Specify_Method ["PolyEq","normalize_poly"])*)
335 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
336 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
337 (*val p = ([3,2],Res)val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0"))
338 val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
339 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + x = 0")) then ()
340 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
341 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
342 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
343 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
344 val (p,_,f,nxt,_,pt) = me nxt p c pt;
345 (*val nxt = Specify_Method ["PolyEq","solve_d1_polyeq_equation"]) *)
346 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
347 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
348 (*val p = ([3,3,2],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"x = 1"))
349 val nxt = ("Or_to_List",Or_to_List) *)
350 val (p,_,f,nxt,_,pt) = me nxt p c pt;
351 (*val p = ([3,3,3],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 1]"))
352 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
353 val (p,_,f,nxt,_,pt) = me nxt p c pt;
354 (*val p = ([3,3,4],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 1]"))
355 val nxt = Check_Postcond ["degree_1","polynomial","univariate","equation"])*)
356 val (p,_,f,nxt,_,pt) = me nxt p c pt;
357 (*val p = ([3,3],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"[x = 1]"))
358 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
359 val (p,_,f,nxt,_,pt) = me nxt p c pt;
361 (*val p = ([3],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
362 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")
363 --------------------------------*)
364 val (p,_,f,nxt,_,pt) = me nxt p c pt;
365 (*val p = ([4],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
366 val nxt = Check_Postcond ["sq","root","univariate","equation"]) *)
367 val (p,_,f,nxt,_,pt) = me nxt p c pt;
368 if p = ([],Res) andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1]"))
369 then () else raise error "diff.behav. in rooteq.sml: sqrt(x) = 1";
372 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\
374 val fmz = ["equality (sqrt x = sqrt x)","solveFor x","solutions L"];
375 val (dI',pI',mI') = ("RootEq.thy",["sq","root","univariate","equation"],
376 ["RootEq","solve_sq_root_equation"]);
377 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
378 val (p,_,f,nxt,_,pt) = me nxt p c pt;
379 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
380 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
381 val (p,_,f,nxt,_,pt) = me nxt p c pt;
382 (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq","solve_sq_root_equation"*)
383 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
384 val (p,_,f,nxt,_,pt) = me nxt p c pt;
385 (*val p = ([1],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = x"))
386 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
387 val (p,_,f,nxt,_,pt) = me nxt p c pt;
388 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
389 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
390 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
391 (*val p = ([2],Pbl) val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
392 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
393 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
394 (*val p = ([2,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
395 val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
396 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
397 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
398 val (p,_,f,nxt,_,pt) = me nxt p c pt;
399 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
400 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
401 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
402 (*val p = ([2,3],Pbl)nxt=Specify_Method ["PolyEq","solve_d0_polyeq_equation"]*)
403 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
404 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
405 (*val p = ([2,3,2],Res) val f = (FormKF (~1,EdUndef,3,Nundef,"UniversalList"))
406 val nxt = Check_Postcond ["degree_0","polynomial","univariate","equation"])*)
407 val (p,_,f,nxt,_,pt) = me nxt p c pt;
408 (*val p = ([2,3],Res) val f = (FormKF (~1,EdUndef,2,Nundef,"UniversalList"))
409 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
410 val (p,_,f,nxt,_,pt) = me nxt p c pt;
411 (*val p = ([2],Res) val f = (FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
412 val nxt = Check_elementwise "Assumptions"*)
413 val (p,_,f,nxt,_,pt) = me nxt p c pt;
414 (*val p = ([3],Res) val f = (FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
415 val nxt = Check_Postcond ["sq","root","univariate","equation"]) *)
416 val (p,_,f,nxt,_,pt) = me nxt p c pt;
417 if p = ([],Res) andalso f = Form'(FormKF (~1,EdUndef,0,Nundef,"UniversalList"))
418 then () else raise error "new behav. in rooteq.sml: sqrt x = sqrt x";
421 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
422 val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))","solveFor x","solutions L"];
423 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
425 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
426 val (p,_,f,nxt,_,pt) = me nxt p c pt;
427 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
428 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
429 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
430 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
431 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
432 val (p,_,f,nxt,_,pt) = me nxt p c pt;
433 (* "6 + x = 60 + 13 * x + -6 * sqrt ((3 + x) * (33 + 4 * x))")) : mout
434 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
435 val (p,_,f,nxt,_,pt) = me nxt p c pt;
436 (*val nxt = Model_Problem ["sq","root","univariate","equation"]) *)
437 val (p,_,f,nxt,_,pt) = me nxt p c pt;
438 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
439 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
440 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
441 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
442 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
443 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
444 (*"2916 + x ^^^ 2 + 1296 * x + 143 * x ^^^ 2 = 3564 + 1620 * x + 144 * x ^^^ 2"))
445 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
446 val (p,_,f,nxt,_,pt) = me nxt p c pt;
447 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
448 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
449 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
450 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
451 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
452 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-648 + -324 * x = 0")) then ()
453 else raise error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt..";
454 (*-> Subproblem ("PolyEq.thy", ["degree_1", ...])*)
455 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
456 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
457 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
458 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
459 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
460 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
461 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
462 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
463 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
464 val (p,_,f,nxt,_,pt) = me nxt p c pt;
465 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2]")) => ()
466 | _ => raise error "rooteq.sml: diff.behav. [x = -2]";
468 "----------- rooteq.sml end--------";