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*)
9 "----------- rooteq.sml begin--------";
10 "--------------(1/sqrt(x)=5)---------------------------------------";
11 "--------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))----------------------";
12 "--------------(sqrt(x+1)=5)---------------------------------------";
13 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
14 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
15 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
16 "---------------- root-eq + subpbl: solve_linear ----------";
17 "---------------- root-eq + subpbl: solve_plain_square ----";
18 "---------------- root-eq + subpbl: no_met: linear --------";
19 "---------------- root-eq + subpbl: no_met: square --------";
20 "---------------- no_met in rootpbl -> linear -------------";
21 "--------------------------------------------------------";
23 (*=== inhibit exn ?=============================================================
25 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
26 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
27 val result = UnparseC.term t_;
28 if result <> \<^const_name>\<open>True\<close> then error "rooteq.sml: new behaviour:" else ();
30 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
31 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
32 val result = UnparseC.term t_;
33 if result <> \<^const_name>\<open>True\<close> then error "rooteq.sml: new behaviour:" else ();
35 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x";
36 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
37 val result = UnparseC.term t_;
38 if result <> \<^const_name>\<open>True\<close> then error "rooteq.sml: new behaviour:" else ();
40 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x";
41 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
42 val result = UnparseC.term t_;
43 if result <> \<^const_name>\<open>True\<close> then error "rooteq.sml: new behaviour:" else ();
45 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x";
46 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
47 val result = UnparseC.term t_;
48 if result <> \<^const_name>\<open>False\<close> then error "rooteq.sml: new behaviour:" else ();
50 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
51 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
52 val result = UnparseC.term t_;
53 if result <> \<^const_name>\<open>True\<close> then error "rooteq.sml: new behaviour:" else ();
55 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
56 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
57 val result = UnparseC.term t_;
58 if result <> \<^const_name>\<open>True\<close> then error "rooteq.sml: new behaviour:" else ();
60 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
61 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
62 val result = UnparseC.term t_;
63 if result <> \<^const_name>\<open>False\<close> then error "rooteq.sml: new behaviour:" else ();
65 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
66 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
67 val result = UnparseC.term t_;
68 if result <> \<^const_name>\<open>False\<close> then error "rooteq.sml: new behaviour:" else ();
70 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
71 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
72 val result = UnparseC.term t_;
73 if result <> \<^const_name>\<open>True\<close> then error "rooteq.sml: new behaviour:" else ();
75 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(1 - (sqrt(2+x+3) \<up> 3)) is_normSqrtTerm_in x";
76 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
77 val result = UnparseC.term t_;
78 if result <> \<^const_name>\<open>False\<close> then error "rooteq.sml: new behaviour:" else ();
80 val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(1 + (sqrt(2+x+3) \<up> 3)) is_normSqrtTerm_in x";
81 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
82 val result = UnparseC.term t_;
83 if result <> \<^const_name>\<open>True\<close> then error "rooteq.sml: new behaviour:" else ();
87 val result = M_Match.match_pbl ["equality (sqrt(x)=1)", "solveFor x", "solutions L"]
88 (Problem.from_store ["rootX", "univariate", "equation"]);
89 case result of M_Match.Matches' _ => () | _ => error "rooteq.sml: new behaviour:";
91 val result = M_Match.match_pbl ["equality (sqrt(25)=1)", "solveFor x", "solutions L"]
92 (Problem.from_store ["rootX", "univariate", "equation"]);
93 case result of M_Match.NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:";
95 (*---------rooteq---- 23.8.02 ---------------------*)
96 "---------(1/sqrt(x)=5)---------------------";
97 val fmz = ["equality (1/sqrt(x)=5)", "solveFor x", "solutions L"];
98 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
100 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;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;
107 (*"1 / x = 25" -> Subproblem ("RootEq", ["univariate", ...]) *)
108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
109 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 (*"1 = 25 * x" -> Subproblem ("RatEq", ["univariate", ...])*)
115 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;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 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "1 + - 25 * x = 0")) then ()
122 else error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
123 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
125 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
135 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => ()
136 | _ => error "rooteq.sml: diff.behav. [x = 1 / 25]";
137 if UnparseC.terms (*WN1104changed*) (Ctree.get_assumptions pt p) = "[0 <= 1 / 25]"
138 (*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..:
139 [(TermC.parse_test @{context}"25 ~= 0",[])] *)
140 then writeln "should be True\n\
143 else error "rooteq.sml: diff.behav. with 25 ~= 0";
145 "---------(sqrt(x+1)=5)---------------------";
146 val fmz = ["equality (sqrt(x+1)=5)", "solveFor x", "solutions L"];
147 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
149 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
150 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
156 (*-> Subproblem ("RootEq", ["univariate", ...])*)
157 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
163 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 24 + x = 0")) then ()
164 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
165 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
166 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
175 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 24]")) => ()
176 | _ => error "rooteq.sml: diff.behav. [x = 24]";
178 "-------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))-----------------";
179 val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))", "solveFor x", "solutions L"];
180 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
182 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
194 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 184 + 46 * x = 0")) then ()
195 else error "rooteq.sml: diff.behav.poly in 4*sqrt(4*x+2)=3*sqrt(2*x+24)";
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
205 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
206 | _ => error "rooteq.sml: diff.behav. [x = 4]";
207 if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"0 <= 12 * sqrt 2 * 4"]
208 then writeln "should be True\nshould be True\nshould be True\n\
209 \should be True\nshould be True\nshould be True\n"
210 else error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4";
212 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------";
213 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))", "solveFor x", "solutions L"];
214 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
216 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
217 (*val nxt = Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
218 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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
225 (*"13 + 13 * x + - 2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
226 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
227 val (p,_,f,nxt,_,pt) = me nxt p c pt;
228 (*val nxt = Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
235 val (p,_,f,nxt,_,pt) = me nxt p c pt;
236 (*"144 + 288 * x + 144 * x \<up> 2 = 144 + x \<up> 2 + 288 * x + 143 * x \<up> 2"))
237 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
243 val (p,_,f,nxt,_,pt) = me nxt p c pt;
244 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
245 else error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr..";
246 (*-> Subproblem ("PolyEq", ["degree_0", ...])*)
247 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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
256 val (p,_,f,nxt,_,pt) = me nxt p c pt;
257 val asm = Ctree.get_assumptions pt p;
258 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso asm = []
259 then () else error "rooteq.sml: diff.behav. in UniversalList 1";
263 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------";
265 ["equality (13 + 13 * x + - 2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
266 "solveFor x", "solutions L"];
267 val (dI',pI',mI') = ("RootEq",["sq", "rootX", "univariate", "equation"],
268 ["RootEq", "solve_sq_root_equation"]);
269 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
270 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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
277 (*"144 + 288 * x + 144 * x \<up> 2 = 144 + x \<up> 2 + 288 * x + 143 * x \<up> 2"))
278 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"])) *)
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
282 val (p,_,f,nxt,_,pt) = me nxt p c pt;
283 (*val p = ([6],Pbl)val nxt = Specify_Method ["PolyEq", "normalise_poly"])*)
284 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
285 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
286 (*val p = ([6,2],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
287 val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
288 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
289 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
290 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 (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
294 (*val nxt = Specify_Method ["PolyEq", "solve_d0_polyeq_equation"]) *)
295 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
296 val (p,_,f,nxt,_,pt) = me nxt p c pt;
297 (*val p = ([6,3,1],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,3,Nundef,\<^const_name>\<open>True\<close>))
298 val nxt = ("Or_to_List",Or_to_List) : string * tac*)
299 val (p,_,f,nxt,_,pt) = me nxt p c pt;
300 (*val p = ([6,3,2],Res) val f = (~1,EdUndef,3,Nundef,"UniversalList"))
301 val nxt = Check_Postcond ["degree_0", "polynomial", "univariate", "equation"])*)
302 val (p,_,f,nxt,_,pt) = me nxt p c pt;
303 (*val p = ([6,3],Res) val f =(~1,EdUndef,2,Nundef,"UniversalList"))
304 val nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"])*)
305 val (p,_,f,nxt,_,pt) = me nxt p c pt;
306 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "UniversalList")) then ()
307 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
308 (* val Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, str)) = f;
311 (*same error as full expl #######*)
313 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- OKversion----";
314 val fmz = ["equality (sqrt(x) = 1)", "solveFor x", "solutions L"];
315 val (dI',pI',mI') = ("RootEq",["sq", "rootX", "univariate", "equation"],
316 ["RootEq", "solve_sq_root_equation"]);
317 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
318 val (p,_,f,nxt,_,pt) = me nxt p c pt;
319 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
320 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
321 val (p,_,f,nxt,_,pt) = me nxt p c pt;
322 (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq", "solve_sq_root_equation"*)
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;
326 (* val p = ([2],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"x = 1"))
327 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
328 val (p,_,f,nxt,_,pt) = me nxt p c pt;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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
331 val (p,_,f,nxt,_,pt) = me nxt p c pt;
332 (*val nxt = ("Specify_Method",Specify_Method ["PolyEq", "normalise_poly"])*)
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 = ([3,2],Res)val f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"- 1 + x = 0"))
336 val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
337 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 1 + x = 0")) then ()
338 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
339 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
340 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
343 (*val nxt = Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]) *)
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 = ([3,3,2],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,3,Nundef,"x = 1"))
347 val nxt = ("Or_to_List",Or_to_List) *)
348 val (p,_,f,nxt,_,pt) = me nxt p c pt;
349 (*val p = ([3,3,3],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,3,Nundef,"[x = 1]"))
350 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
351 val (p,_,f,nxt,_,pt) = me nxt p c pt;
352 (*val p = ([3,3,4],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,3,Nundef,"[x = 1]"))
353 val nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"])*)
354 val (p,_,f,nxt,_,pt) = me nxt p c pt;
355 (*val p = ([3,3],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"[x = 1]"))
356 val nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"])*)
357 val (p,_,f,nxt,_,pt) = me nxt p c pt;
359 (*val p = ([3],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
360 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")
361 --------------------------------*)
362 val (p,_,f,nxt,_,pt) = me nxt p c pt;
363 (*val p = ([4],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
364 val nxt = Check_Postcond ["sq", "rootX", "univariate", "equation"]) *)
365 val (p,_,f,nxt,_,pt) = me nxt p c pt;
366 if p = ([],Res) andalso f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1]"))
367 then () else error "diff.behav. in rooteq.sml: sqrt(x) = 1";
370 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\
372 val fmz = ["equality (sqrt x = sqrt x)", "solveFor x", "solutions L"];
373 val (dI',pI',mI') = ("RootEq",["sq", "rootX", "univariate", "equation"],
374 ["RootEq", "solve_sq_root_equation"]);
375 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
376 val (p,_,f,nxt,_,pt) = me nxt p c pt;
377 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
378 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
379 val (p,_,f,nxt,_,pt) = me nxt p c pt;
380 (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq", "solve_sq_root_equation"*)
381 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
382 val (p,_,f,nxt,_,pt) = me nxt p c pt;
383 (*val p = ([1],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"x = x"))
384 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
385 val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;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 = ([2],Pbl) val nxt = Specify_Method ["PolyEq", "normalise_poly"])*)
390 val (p,_,f,nxt,_,pt) = me nxt p c pt;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 = ([2,2],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
393 val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
394 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
395 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
396 val (p,_,f,nxt,_,pt) = me nxt p c pt;
397 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
398 val (p,_,f,nxt,_,pt) = me nxt p c pt;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 = ([2,3],Pbl)nxt=Specify_Method ["PolyEq", "solve_d0_polyeq_equation"]*)
401 val (p,_,f,nxt,_,pt) = me nxt p c pt;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 = ([2,3,2],Res) val f = (Test_Out.FormKF (~1,EdUndef,3,Nundef,"UniversalList"))
404 val nxt = Check_Postcond ["degree_0", "polynomial", "univariate", "equation"])*)
405 val (p,_,f,nxt,_,pt) = me nxt p c pt;
406 (*val p = ([2,3],Res) val f = (Test_Out.FormKF (~1,EdUndef,2,Nundef,"UniversalList"))
407 val nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"])*)
408 val (p,_,f,nxt,_,pt) = me nxt p c pt;
409 (*val p = ([2],Res) val f = (Test_Out.FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
410 val nxt = Check_elementwise "Assumptions"*)
411 val (p,_,f,nxt,_,pt) = me nxt p c pt;
412 (*val p = ([3],Res) val f = (Test_Out.FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
413 val nxt = Check_Postcond ["sq", "rootX", "univariate", "equation"]) *)
414 val (p,_,f,nxt,_,pt) = me nxt p c pt;
415 if p = ([],Res) andalso f = Form'(Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList"))
416 then () else error "new behav. in rooteq.sml: sqrt x = sqrt x";
419 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
420 val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))", "solveFor x", "solutions L"];
421 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
423 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
424 val (p,_,f,nxt,_,pt) = me nxt p c pt;
425 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
426 val (p,_,f,nxt,_,pt) = me nxt p c pt;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;
431 (* "6 + x = 60 + 13 * x + -6 * sqrt ((3 + x) * (33 + 4 * x))")) : mout
432 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
433 val (p,_,f,nxt,_,pt) = me nxt p c pt;
434 (*val nxt = Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
435 val (p,_,f,nxt,_,pt) = me nxt p c pt;
436 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
437 val (p,_,f,nxt,_,pt) = me nxt p c pt;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 (*"2916 + x \<up> 2 + 1296 * x + 143 * x \<up> 2 = 3564 + 1620 * x + 144 * x \<up> 2"))
443 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
444 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 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 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "-648 + -324 * x = 0")) then ()
451 else error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt..";
452 (*-> Subproblem ("PolyEq", ["degree_1", ...])*)
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 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;
463 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2]")) => ()
464 | _ => error "rooteq.sml: diff.behav. [x = - 2]";
466 "----------- rooteq.sml end--------";
469 ===== inhibit exn ?===========================================================*)
471 (*===== copied here from OLDTESTS in case there is a Program ===vvv=============================
474 "---------------- root-eq + subpbl: solve_linear ----------";
475 "---------------- root-eq + subpbl: solve_linear ----------";
476 "---------------- root-eq + subpbl: solve_linear ----------";
477 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
478 "solveFor x", "solutions L"];
480 ("Test",["sqroot-test", "univariate", "equation", "test"],
481 ["Test", "square_equation1"]);
482 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
483 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
484 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
485 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
486 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
487 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
488 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
489 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
490 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
491 (*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"
492 square_equation_left*)
493 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
494 (*"9 + 4 * x = (sqrt x + sqrt (5 + x)) \<up> 2"
496 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
497 (*"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x \<up> 2 + 5 * x))"
499 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
500 (*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x \<up> 2 + 5 * x)"
502 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
503 (*"sqrt (x \<up> 2 + 5 * x) = (5 + 2 * x + - 1 * (9 + 4 * x)) / (- 1 * 2)"
505 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
506 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
507 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
508 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
509 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
510 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
511 (*"x \<up> 2 + 5 * x + - 1 * (4 + (x \<up> 2 + 4 * x)) = 0"*)
512 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
514 val nxt =("Subproblem",Subproblem ("Test",["LINEAR", "univariate"...*)
515 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
516 (*val nxt =("Model_Problem",Model_Problem ["LINEAR", "univariate"...*)
517 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
518 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
520 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
521 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
522 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
523 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
524 (*("Specify_Problem",Specify_Problem ["LINEAR", "univariate", "equation"])*)
525 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
526 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
527 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
528 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
529 (*"x = 0 + - 1 * -4", nxt Test_simplify*)
530 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
531 (*"x = 4", nxt Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
532 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
533 (*"[x = 4]", nxt Check_elementwise "Assumptions"*)
534 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
535 (*"[]", nxt Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
536 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
537 val Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,res)) = f;
538 if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
539 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_linear";
543 "---------------- root-eq + subpbl: solve_plain_square ----";
544 "---------------- root-eq + subpbl: solve_plain_square ----";
545 "---------------- root-eq + subpbl: solve_plain_square ----";
546 val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
547 "solveFor x", "solutions L"];
549 ("Test",["sqroot-test", "univariate", "equation", "test"],
550 ["Test", "square_equation2"]);
551 val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "square_equation2"];
552 (writeln o UnparseC.term) sc;
554 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
555 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
556 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
557 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
558 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
559 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
560 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
561 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
562 (*val nxt = ("Apply_Method",Apply_Method ("Test", "square_equation1"))*)
563 val (p,_,f,nxt,_,pt) =
566 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
567 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
568 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
569 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
570 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
571 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
572 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
573 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
574 (*"9 + - 1 * x \<up> 2 = 0"
575 Subproblem ("Test",["plain_square", "univariate", "equation"]))*)
576 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
577 (*Model_Problem ["plain_square", "univariate", "equation"]*)
578 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
579 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
580 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
581 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
582 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
583 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
584 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
585 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
586 (*Apply_Method ("Test", "solve_plain_square")*)
587 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
588 (*"9 + - 1 * x \<up> 2 = 0", nxt Rewrite_Set "isolate_bdv"*)
589 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
590 (*"x \<up> 2 = (0 + - 1 * 9) / - 1", nxt Rewrite_Set "Test_simplify"*)
591 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
592 (*"x \<up> 2 = 9", nxt Rewrite ("square_equality"*)
593 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
594 (*"x = sqrt 9 | x = - 1 * sqrt 9", nxt Rewrite_Set "tval_rls"*)
595 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
596 (*"x = -3 | x = 3", nxt Or_to_List*)
597 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
599 nxt Check_Postcond ["plain_square", "univariate", "equation", "test"]*)
600 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
604 (*"[x = -3, x = 3]", nxt Check_elementwise "Assumptions"*)
605 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
606 (*"[]", nxt Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
607 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
608 val Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,res)) = f;
609 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
610 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square";
613 writeln (pr_ctree pr_short pt);
617 val Prog s = (#scr o MethodC.from_store ctxt) ["Test", "square_equation"];
623 "---------------- root-eq + subpbl: no_met: linear ----";
624 "---------------- root-eq + subpbl: no_met: linear ----";
625 "---------------- root-eq + subpbl: no_met: linear ----";
626 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
627 "solveFor x", "solutions L"];
629 ("Test",["squareroot", "univariate", "equation", "test"],
630 ["Test", "square_equation"]);
631 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
632 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
633 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
634 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
635 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
636 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
637 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
638 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
639 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
640 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
641 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
642 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
643 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
644 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
645 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
646 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
647 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
648 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
649 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
650 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
651 (*"-4 + x = 0", nxt Subproblem ("Test",["univariate", "equation"]))*)
652 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
653 (*val nxt =("Model_Problem",Model_Problem ["LINEAR", "univar...*)
654 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
655 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
656 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
657 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
658 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
659 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
660 (*val nxt = ("Specify_Problem",Specify_Problem ["LINEAR", "univariate", "equ*)
661 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
662 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
663 (*Apply_Method ("Test", "norm_univar_equation")*)
664 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
665 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
666 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
667 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
668 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
669 if p = ([13],Res) then ()
670 else error ("subp-rooteq.sml: new.behav. in \
671 \root-eq + subpbl: solve_linear, p ="^(pos'2str p));
672 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
673 val Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,res)) = f;
674 if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
675 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square";
680 "---------------- root-eq + subpbl: no_met: square ----";
681 "---------------- root-eq + subpbl: no_met: square ----";
682 "---------------- root-eq + subpbl: no_met: square ----";
683 val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
684 "solveFor x", "solutions L"];
686 ("Test",["squareroot", "univariate", "equation", "test"],
687 ["Test", "square_equation"]);
688 val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "square_equation"];
689 (writeln o UnparseC.term) sc;
691 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
692 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
693 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
694 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
695 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
696 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
697 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
698 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
699 (*val nxt = ("Apply_Method",Apply_Method ("Test", "square_equation1"))*)
700 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
701 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
702 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
703 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
704 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
705 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
706 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
707 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
708 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
709 (*Subproblem ("Test",["univariate", "equation"]))*)
710 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
711 (*Model_Problem ["plain_square", "univariate", "equation"]*)
712 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
713 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
714 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
715 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
716 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
717 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
718 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
719 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
720 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
721 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
722 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
723 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
724 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
725 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
726 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
727 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
728 (*val nxt = ("Check_Postcond",Check_Postcond ["squareroot", "univariate", "equ*)
729 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
730 val Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,res)) = f;
731 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
732 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: no_met: square";
736 "---------------- no_met in rootpbl -> linear --------------";
737 "---------------- no_met in rootpbl -> linear --------------";
738 "---------------- no_met in rootpbl -> linear --------------";
739 val fmz = ["equality (1+2*x+3=4*x- 6)",
740 "solveFor x", "solutions L"];
742 ("Test",["univariate", "equation", "test"],
744 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
745 (*val nxt = ("Model_Problem",Model_Problem ["normalise", "univariate", "equati*)
746 val (p,_,f,nxt,_,pt) = me nxt p c pt;
747 val (p,_,f,nxt,_,pt) = me nxt p c pt;
748 val (p,_,f,nxt,_,pt) = me nxt p c pt;
749 val (p,_,f,nxt,_,pt) = me nxt p c pt;
750 val (p,_,f,nxt,_,pt) = me nxt p c pt;
751 val (p,_,f,nxt,_,pt) = me nxt p c pt;
752 val (p,_,f,nxt,_,pt) = me nxt p c pt;
753 (*val nxt = ("Apply_Method",Apply_Method ("Test", "norm_univar_equation"*)
754 val (p,_,f,nxt,_,pt) = me nxt p c pt;
755 val (p,_,f,nxt,_,pt) = me nxt p c pt;
756 val (p,_,f,nxt,_,pt) = me nxt p c pt;
757 (*val nxt = ("Subproblem",Subproblem ("Test",["univariate", "equation"])*)
758 val (p,_,f,nxt,_,pt) = me nxt p c pt;
759 (*val nxt = ("Model_Problem",Model_Problem ["LINEAR", "univariate", "equation"]*)
760 val (p,_,f,nxt,_,pt) = me nxt p c pt;
761 val (p,_,f,nxt,_,pt) = me nxt p c pt;
762 val (p,_,f,nxt,_,pt) = me nxt p c pt;
763 val (p,_,f,nxt,_,pt) = me nxt p c pt;
764 val (p,_,f,nxt,_,pt) = me nxt p c pt;
765 val (p,_,f,nxt,_,pt) = me nxt p c pt;
766 val (p,_,f,nxt,_,pt) = me nxt p c pt;
767 (*val nxt = ("Apply_Method",Apply_Method ("Test", "solve_linear"))*)
768 val (p,_,f,nxt,_,pt) = me nxt p c pt;
769 val (p,_,f,nxt,_,pt) = me nxt p c pt;
770 val (p,_,f,nxt,_,pt) = me nxt p c pt;
771 (*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR", "univariate", "equatio*)
772 val (p,_,f,nxt,_,pt) = me nxt p c pt;
773 (*val nxt = ("Check_Postcond",Check_Postcond ["normalise", "univariate", "equa*)
774 val (p,_,Form' (Test_Out.FormKF (_,_,_,_,f)),nxt,_,_) =
776 if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then ()
777 else error "subp-rooteq.sml: new.behav. in no_met in rootpbl -> linear ---";
780 Refine.refine fmz ["univariate", "equation", "test"];
781 M_Match.match_pbl fmz (Problem.from_store ["polynomial", "univariate", "equation", "test"]);
783 ===== copied here from OLDTESTS in case there is a Program === \<up> =============================*)