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))-----------------";
17 "--------------------------------------------------------";
19 (*=== inhibit exn ?=============================================================
21 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
22 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
23 val result = term2str t_;
24 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
26 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
27 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
28 val result = term2str t_;
29 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
31 val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x";
32 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
33 val result = term2str t_;
34 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
36 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x";
37 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
38 val result = term2str t_;
39 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
41 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x";
42 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
43 val result = term2str t_;
44 if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
46 val t = (term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
47 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
48 val result = term2str t_;
49 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
51 val t = (term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
52 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
53 val result = term2str t_;
54 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
56 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
57 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
58 val result = term2str t_;
59 if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
61 val t = (term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
62 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
63 val result = term2str t_;
64 if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
66 val t = (term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
67 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
68 val result = term2str t_;
69 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
71 val t = (term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
72 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
73 val result = term2str t_;
74 if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
76 val t = (term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
77 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
78 val result = term2str t_;
79 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
83 val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
84 (get_pbt ["root'","univariate","equation"]);
85 case result of Matches' _ => () | _ => error "rooteq.sml: new behaviour:";
87 val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
88 (get_pbt ["root'","univariate","equation"]);
89 case result of NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:";
91 (*---------rooteq---- 23.8.02 ---------------------*)
92 "---------(1/sqrt(x)=5)---------------------";
93 val fmz = ["equality (1/sqrt(x)=5)","solveFor x","solutions L"];
94 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
96 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
97 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;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
103 (*"1 / x = 25" -> Subproblem ("RootEq", ["univariate", ...]) *)
104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
105 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;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 (*"1 = 25 * x" -> Subproblem ("RatEq", ["univariate", ...])*)
111 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
117 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -25 * x = 0")) then ()
118 else error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
119 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
121 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
131 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => ()
132 | _ => error "rooteq.sml: diff.behav. [x = 1 / 25]";
133 if terms2str (*WN1104changed*) (get_assumptions_ pt p) = "[0 <= 1 / 25]"
134 (*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..:
135 [(str2term"25 ~= 0",[])] *)
136 then writeln "should be True\n\
139 else error "rooteq.sml: diff.behav. with 25 ~= 0";
141 "---------(sqrt(x+1)=5)---------------------";
142 val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"];
143 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
146 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
147 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
148 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
149 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;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 (*-> Subproblem ("RootEq", ["univariate", ...])*)
156 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
160 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
161 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
162 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + x = 0")) then ()
163 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
164 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
165 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
172 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
173 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
174 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 24]")) => ()
175 | _ => error "rooteq.sml: diff.behav. [x = 24]";
177 "-------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))-----------------";
178 val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))","solveFor x","solutions L"];
179 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
181 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
191 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
193 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-184 + 46 * x = 0")) then ()
194 else error "rooteq.sml: diff.behav.poly in 4*sqrt(4*x+2)=3*sqrt(2*x+24)";
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
202 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
203 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
204 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
205 | _ => error "rooteq.sml: diff.behav. [x = 4]";
206 if get_assumptions_ pt p = [str2term"0 <= 12 * sqrt 2 * 4"]
207 then writeln "should be True\nshould be True\nshould be True\n\
208 \should be True\nshould be True\nshould be True\n"
209 else error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4";
211 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------";
212 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))","solveFor x","solutions L"];
213 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
215 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
216 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
217 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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
222 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
223 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
224 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
225 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
226 val (p,_,f,nxt,_,pt) = me nxt p c pt;
227 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
232 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
233 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
234 val (p,_,f,nxt,_,pt) = me nxt p c pt;
235 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
236 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
240 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
241 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
242 val (p,_,f,nxt,_,pt) = me nxt p c pt;
243 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
244 else error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr..";
245 (*-> Subproblem ("PolyEq", ["degree_0", ...])*)
246 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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
253 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
254 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
255 val (p,_,f,nxt,_,pt) = me nxt p c pt;
256 val asm = get_assumptions_ pt p;
257 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso asm = []
258 then () else error "rooteq.sml: diff.behav. in UniversalList 1";
262 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------";
264 ["equality (13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
265 "solveFor x","solutions L"];
266 val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
267 ["RootEq","solve_sq_root_equation"]);
268 (*val p = e_pos'; val c = [];
269 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
270 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
271 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
272 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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
277 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
278 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
279 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
280 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"])) *)
281 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
282 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
285 (*val p = ([6],Pbl)val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
286 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
287 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
288 (*val p = ([6,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
289 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
290 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
291 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
292 val (p,_,f,nxt,_,pt) = me nxt p c pt;
293 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
296 (*val nxt = Specify_Method ["PolyEq","solve_d0_polyeq_equation"]) *)
297 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
298 val (p,_,f,nxt,_,pt) = me nxt p c pt;
299 (*val p = ([6,3,1],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"HOL.True"))
300 val nxt = ("Or_to_List",Or_to_List) : string * tac*)
301 val (p,_,f,nxt,_,pt) = me nxt p c pt;
302 (*val p = ([6,3,2],Res) val f = (~1,EdUndef,3,Nundef,"UniversalList"))
303 val nxt = Check_Postcond ["degree_0","polynomial","univariate","equation"])*)
304 val (p,_,f,nxt,_,pt) = me nxt p c pt;
305 (*val p = ([6,3],Res) val f =(~1,EdUndef,2,Nundef,"UniversalList"))
306 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
307 val (p,_,f,nxt,_,pt) = me nxt p c pt;
308 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "UniversalList")) then ()
309 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
310 (* val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;
313 (*same error as full expl #######*)
315 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- OKversion----";
316 val fmz = ["equality (sqrt(x) = 1)","solveFor x","solutions L"];
317 val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
318 ["RootEq","solve_sq_root_equation"]);
319 (*val p = e_pos'; val c = [];
320 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
321 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
322 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
323 val (p,_,f,nxt,_,pt) = me nxt p c pt;
324 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
325 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
326 val (p,_,f,nxt,_,pt) = me nxt p c pt;
327 (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq","solve_sq_root_equation"*)
328 val (p,_,f,nxt,_,pt) = me nxt p c pt;
329 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
330 val (p,_,f,nxt,_,pt) = me nxt p c pt;
331 (* val p = ([2],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = 1"))
332 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
333 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
334 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
337 (*val nxt = ("Specify_Method",Specify_Method ["PolyEq","normalize_poly"])*)
338 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
339 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
340 (*val p = ([3,2],Res)val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0"))
341 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
342 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + x = 0")) then ()
343 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
344 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
345 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
348 (*val nxt = Specify_Method ["PolyEq","solve_d1_polyeq_equation"]) *)
349 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
350 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
351 (*val p = ([3,3,2],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"x = 1"))
352 val nxt = ("Or_to_List",Or_to_List) *)
353 val (p,_,f,nxt,_,pt) = me nxt p c pt;
354 (*val p = ([3,3,3],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 1]"))
355 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
356 val (p,_,f,nxt,_,pt) = me nxt p c pt;
357 (*val p = ([3,3,4],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 1]"))
358 val nxt = Check_Postcond ["degree_1","polynomial","univariate","equation"])*)
359 val (p,_,f,nxt,_,pt) = me nxt p c pt;
360 (*val p = ([3,3],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"[x = 1]"))
361 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
362 val (p,_,f,nxt,_,pt) = me nxt p c pt;
364 (*val p = ([3],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
365 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")
366 --------------------------------*)
367 val (p,_,f,nxt,_,pt) = me nxt p c pt;
368 (*val p = ([4],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
369 val nxt = Check_Postcond ["sq","root'","univariate","equation"]) *)
370 val (p,_,f,nxt,_,pt) = me nxt p c pt;
371 if p = ([],Res) andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1]"))
372 then () else error "diff.behav. in rooteq.sml: sqrt(x) = 1";
375 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\
377 val fmz = ["equality (sqrt x = sqrt x)","solveFor x","solutions L"];
378 val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
379 ["RootEq","solve_sq_root_equation"]);
380 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
381 val (p,_,f,nxt,_,pt) = me nxt p c pt;
382 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 = ([],Pbl)val nxt = Specify_Method ["RootEq","solve_sq_root_equation"*)
386 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
387 val (p,_,f,nxt,_,pt) = me nxt p c pt;
388 (*val p = ([1],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = x"))
389 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
390 val (p,_,f,nxt,_,pt) = me nxt p c pt;
391 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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],Pbl) val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
395 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
396 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
397 (*val p = ([2,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
398 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
399 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
400 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
401 val (p,_,f,nxt,_,pt) = me nxt p c pt;
402 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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],Pbl)nxt=Specify_Method ["PolyEq","solve_d0_polyeq_equation"]*)
406 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
407 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
408 (*val p = ([2,3,2],Res) val f = (FormKF (~1,EdUndef,3,Nundef,"UniversalList"))
409 val nxt = Check_Postcond ["degree_0","polynomial","univariate","equation"])*)
410 val (p,_,f,nxt,_,pt) = me nxt p c pt;
411 (*val p = ([2,3],Res) val f = (FormKF (~1,EdUndef,2,Nundef,"UniversalList"))
412 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
413 val (p,_,f,nxt,_,pt) = me nxt p c pt;
414 (*val p = ([2],Res) val f = (FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
415 val nxt = Check_elementwise "Assumptions"*)
416 val (p,_,f,nxt,_,pt) = me nxt p c pt;
417 (*val p = ([3],Res) val f = (FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
418 val nxt = Check_Postcond ["sq","root'","univariate","equation"]) *)
419 val (p,_,f,nxt,_,pt) = me nxt p c pt;
420 if p = ([],Res) andalso f = Form'(FormKF (~1,EdUndef,0,Nundef,"UniversalList"))
421 then () else error "new behav. in rooteq.sml: sqrt x = sqrt x";
424 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
425 val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))","solveFor x","solutions L"];
426 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
428 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
429 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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
433 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
434 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
435 val (p,_,f,nxt,_,pt) = me nxt p c pt;
436 (* "6 + x = 60 + 13 * x + -6 * sqrt ((3 + x) * (33 + 4 * x))")) : mout
437 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
438 val (p,_,f,nxt,_,pt) = me nxt p c pt;
439 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
440 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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
445 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
446 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
447 (*"2916 + x ^^^ 2 + 1296 * x + 143 * x ^^^ 2 = 3564 + 1620 * x + 144 * x ^^^ 2"))
448 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
449 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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
453 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
454 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
455 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-648 + -324 * x = 0")) then ()
456 else error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt..";
457 (*-> Subproblem ("PolyEq", ["degree_1", ...])*)
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
465 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
466 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
467 val (p,_,f,nxt,_,pt) = me nxt p c pt;
468 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2]")) => ()
469 | _ => error "rooteq.sml: diff.behav. [x = -2]";
471 "----------- rooteq.sml end--------";
474 ===== inhibit exn ?===========================================================*)