16 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------"; |
16 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------"; |
17 |
17 |
18 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x"; |
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; |
19 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
20 val result = term2str t_; |
20 val result = term2str t_; |
21 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
21 if result <> "True" then error "rooteq.sml: new behaviour:" else (); |
22 |
22 |
23 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x"; |
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; |
24 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
25 val result = term2str t_; |
25 val result = term2str t_; |
26 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
26 if result <> "True" then error "rooteq.sml: new behaviour:" else (); |
27 |
27 |
28 val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x"; |
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; |
29 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
30 val result = term2str t_; |
30 val result = term2str t_; |
31 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
31 if result <> "True" then error "rooteq.sml: new behaviour:" else (); |
32 |
32 |
33 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x"; |
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; |
34 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
35 val result = term2str t_; |
35 val result = term2str t_; |
36 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
36 if result <> "True" then error "rooteq.sml: new behaviour:" else (); |
37 |
37 |
38 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x"; |
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; |
39 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
40 val result = term2str t_; |
40 val result = term2str t_; |
41 if result <> "False" then raise error "rooteq.sml: new behaviour:" else (); |
41 if result <> "False" then error "rooteq.sml: new behaviour:" else (); |
42 |
42 |
43 val t = (term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x"; |
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; |
44 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
45 val result = term2str t_; |
45 val result = term2str t_; |
46 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
46 if result <> "True" then error "rooteq.sml: new behaviour:" else (); |
47 |
47 |
48 val t = (term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x"; |
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; |
49 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
50 val result = term2str t_; |
50 val result = term2str t_; |
51 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
51 if result <> "True" then error "rooteq.sml: new behaviour:" else (); |
52 |
52 |
53 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x"; |
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; |
54 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
55 val result = term2str t_; |
55 val result = term2str t_; |
56 if result <> "False" then raise error "rooteq.sml: new behaviour:" else (); |
56 if result <> "False" then error "rooteq.sml: new behaviour:" else (); |
57 |
57 |
58 val t = (term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u"; |
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; |
59 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
60 val result = term2str t_; |
60 val result = term2str t_; |
61 if result <> "False" then raise error "rooteq.sml: new behaviour:" else (); |
61 if result <> "False" then error "rooteq.sml: new behaviour:" else (); |
62 |
62 |
63 val t = (term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x"; |
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; |
64 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
65 val result = term2str t_; |
65 val result = term2str t_; |
66 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
66 if result <> "True" then error "rooteq.sml: new behaviour:" else (); |
67 |
67 |
68 val t = (term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x"; |
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; |
69 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
70 val result = term2str t_; |
70 val result = term2str t_; |
71 if result <> "False" then raise error "rooteq.sml: new behaviour:" else (); |
71 if result <> "False" then error "rooteq.sml: new behaviour:" else (); |
72 |
72 |
73 val t = (term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x"; |
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; |
74 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; |
75 val result = term2str t_; |
75 val result = term2str t_; |
76 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
76 if result <> "True" then error "rooteq.sml: new behaviour:" else (); |
77 |
77 |
78 |
78 |
79 |
79 |
80 val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] |
80 val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] |
81 (get_pbt ["root'","univariate","equation"]); |
81 (get_pbt ["root'","univariate","equation"]); |
82 case result of Matches' _ => () | _ => raise error "rooteq.sml: new behaviour:"; |
82 case result of Matches' _ => () | _ => error "rooteq.sml: new behaviour:"; |
83 |
83 |
84 val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"] |
84 val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"] |
85 (get_pbt ["root'","univariate","equation"]); |
85 (get_pbt ["root'","univariate","equation"]); |
86 case result of NoMatch' _ => () | _ => raise error "rooteq.sml: new behaviour:"; |
86 case result of NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:"; |
87 |
87 |
88 (*---------rooteq---- 23.8.02 ---------------------*) |
88 (*---------rooteq---- 23.8.02 ---------------------*) |
89 "---------(1/sqrt(x)=5)---------------------"; |
89 "---------(1/sqrt(x)=5)---------------------"; |
90 val fmz = ["equality (1/sqrt(x)=5)","solveFor x","solutions L"]; |
90 val fmz = ["equality (1/sqrt(x)=5)","solveFor x","solutions L"]; |
91 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); |
91 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); |
110 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; |
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; |
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; |
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 () |
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)"; |
115 else error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)"; |
116 (*-> Subproblem ("PolyEq", ["polynomial", ...])*) |
116 (*-> Subproblem ("PolyEq", ["polynomial", ...])*) |
117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
118 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; |
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; |
120 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; |
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; |
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; |
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; |
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]")) => () |
128 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => () |
129 | _ => raise error "rooteq.sml: diff.behav. [x = 1 / 25]"; |
129 | _ => error "rooteq.sml: diff.behav. [x = 1 / 25]"; |
130 if asms2str (get_assumptions_ pt p) = "[(0 <= 1 / 25, [])]" |
130 if asms2str (get_assumptions_ pt p) = "[(0 <= 1 / 25, [])]" |
131 (*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..: |
131 (*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..: |
132 [(str2term"25 ~= 0",[])] *) |
132 [(str2term"25 ~= 0",[])] *) |
133 then writeln "should be True\n\ |
133 then writeln "should be True\n\ |
134 \should be True\n\ |
134 \should be True\n\ |
135 \should be True\n" |
135 \should be True\n" |
136 else raise error "rooteq.sml: diff.behav. with 25 ~= 0"; |
136 else error "rooteq.sml: diff.behav. with 25 ~= 0"; |
137 |
137 |
138 "---------(sqrt(x+1)=5)---------------------"; |
138 "---------(sqrt(x+1)=5)---------------------"; |
139 val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"]; |
139 val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"]; |
140 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); |
140 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); |
141 (*val p = e_pos'; |
141 (*val p = e_pos'; |
155 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; |
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; |
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; |
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 () |
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"; |
160 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5"; |
161 (*-> Subproblem ("PolyEq", ["polynomial", ...])*) |
161 (*-> Subproblem ("PolyEq", ["polynomial", ...])*) |
162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
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; |
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; |
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; |
165 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; |
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; |
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; |
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; |
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]")) => () |
171 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 24]")) => () |
172 | _ => raise error "rooteq.sml: diff.behav. [x = 24]"; |
172 | _ => error "rooteq.sml: diff.behav. [x = 24]"; |
173 |
173 |
174 "-------------(4*sqrt(4*x+2)=3*sqrt(2*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"]; |
175 val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))","solveFor x","solutions L"]; |
176 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); |
176 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); |
177 |
177 |
186 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; |
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; |
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; |
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 () |
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)"; |
191 else 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; |
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; |
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; |
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; |
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; |
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; |
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; |
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; |
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; |
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]")) => () |
201 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => () |
202 | _ => raise error "rooteq.sml: diff.behav. [x = 4]"; |
202 | _ => error "rooteq.sml: diff.behav. [x = 4]"; |
203 if get_assumptions_ pt p = [(str2term"0 <= 12 * sqrt 2 * 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\ |
204 then writeln "should be True\nshould be True\nshould be True\n\ |
205 \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"; |
206 else error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4"; |
207 |
207 |
208 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------"; |
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"]; |
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",["univariate","equation"],["no_met"]); |
210 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); |
211 |
211 |
236 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; |
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; |
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; |
239 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
240 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then () |
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.."; |
241 else error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr.."; |
242 (*-> Subproblem ("PolyEq", ["degree_0", ...])*) |
242 (*-> Subproblem ("PolyEq", ["degree_0", ...])*) |
243 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
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; |
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; |
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; |
246 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; |
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; |
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; |
252 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
253 val asm = get_assumptions_ pt p; |
253 val asm = get_assumptions_ pt p; |
254 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso asm = [] |
254 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso asm = [] |
255 then () else raise error "rooteq.sml: diff.behav. in UniversalList 1"; |
255 then () else error "rooteq.sml: diff.behav. in UniversalList 1"; |
256 |
256 |
257 |
257 |
258 |
258 |
259 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------"; |
259 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------"; |
260 val fmz = |
260 val fmz = |
283 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;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")) |
285 (*val p = ([6,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0")) |
286 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) |
286 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) |
287 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then () |
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.."; |
288 else 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; |
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; |
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; |
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; |
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"]) *) |
293 (*val nxt = Specify_Method ["PolyEq","solve_d0_polyeq_equation"]) *) |
301 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
301 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
302 (*val p = ([6,3],Res) val f =(~1,EdUndef,2,Nundef,"UniversalList")) |
302 (*val p = ([6,3],Res) val f =(~1,EdUndef,2,Nundef,"UniversalList")) |
303 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*) |
303 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*) |
304 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
304 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
305 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "UniversalList")) then () |
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.."; |
306 else 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; |
307 (* val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f; |
308 *) |
308 *) |
309 |
309 |
310 (*same error as full expl #######*) |
310 (*same error as full expl #######*) |
311 |
311 |
335 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;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")) |
337 (*val p = ([3,2],Res)val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0")) |
338 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) |
338 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) |
339 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + x = 0")) then () |
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.."; |
340 else 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; |
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; |
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; |
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; |
344 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
345 (*val nxt = Specify_Method ["PolyEq","solve_d1_polyeq_equation"]) *) |
345 (*val nxt = Specify_Method ["PolyEq","solve_d1_polyeq_equation"]) *) |
364 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
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]")) |
365 (*val p = ([4],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 1]")) |
366 val nxt = Check_Postcond ["sq","root'","univariate","equation"]) *) |
366 val nxt = Check_Postcond ["sq","root'","univariate","equation"]) *) |
367 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
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]")) |
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"; |
369 then () else error "diff.behav. in rooteq.sml: sqrt(x) = 1"; |
370 |
370 |
371 |
371 |
372 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\ |
372 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\ |
373 \ with same error"; |
373 \ with same error"; |
374 val fmz = ["equality (sqrt x = sqrt x)","solveFor x","solutions L"]; |
374 val fmz = ["equality (sqrt x = sqrt x)","solveFor x","solutions L"]; |
392 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; |
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")) |
394 (*val p = ([2,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0")) |
395 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) |
395 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) |
396 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then () |
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.."; |
397 else 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; |
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; |
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; |
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; |
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"]*) |
402 (*val p = ([2,3],Pbl)nxt=Specify_Method ["PolyEq","solve_d0_polyeq_equation"]*) |
413 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
413 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
414 (*val p = ([3],Res) val f = (FormKF (~1,EdUndef,1,Nundef,"UniversalList")) |
414 (*val p = ([3],Res) val f = (FormKF (~1,EdUndef,1,Nundef,"UniversalList")) |
415 val nxt = Check_Postcond ["sq","root'","univariate","equation"]) *) |
415 val nxt = Check_Postcond ["sq","root'","univariate","equation"]) *) |
416 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
416 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
417 if p = ([],Res) andalso f = Form'(FormKF (~1,EdUndef,0,Nundef,"UniversalList")) |
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"; |
418 then () else error "new behav. in rooteq.sml: sqrt x = sqrt x"; |
419 |
419 |
420 |
420 |
421 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------"; |
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"]; |
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",["univariate","equation"],["no_met"]); |
423 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); |
448 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; |
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; |
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; |
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 () |
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.."; |
453 else error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt.."; |
454 (*-> Subproblem ("PolyEq", ["degree_1", ...])*) |
454 (*-> Subproblem ("PolyEq", ["degree_1", ...])*) |
455 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; |
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; |
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; |
458 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; |
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; |
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; |
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; |
464 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
465 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2]")) => () |
465 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2]")) => () |
466 | _ => raise error "rooteq.sml: diff.behav. [x = -2]"; |
466 | _ => error "rooteq.sml: diff.behav. [x = -2]"; |
467 |
467 |
468 "----------- rooteq.sml end--------"; |
468 "----------- rooteq.sml end--------"; |
469 |
469 |
470 |
470 |