12 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------"; |
12 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------"; |
13 |
13 |
14 val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x"; |
14 val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x"; |
15 val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t; |
15 val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t; |
16 val result = term2str t_; |
16 val result = term2str t_; |
17 if result <> "True" then raise error "rateq.sml: new behaviour 1:" else (); |
17 if result <> "True" then error "rateq.sml: new behaviour 1:" else (); |
18 |
18 |
19 val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in x"; |
19 val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in x"; |
20 val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t; |
20 val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t; |
21 val result = term2str t_; |
21 val result = term2str t_; |
22 if result <> "False" then raise error "rateq.sml: new behaviour 2:" else (); |
22 if result <> "False" then error "rateq.sml: new behaviour 2:" else (); |
23 |
23 |
24 val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x"; |
24 val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x"; |
25 val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t; |
25 val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t; |
26 val result = term2str t_; |
26 val result = term2str t_; |
27 if result <> "False" then raise error "rateq.sml: new behaviour 3:" else (); |
27 if result <> "False" then error "rateq.sml: new behaviour 3:" else (); |
28 |
28 |
29 val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x"; |
29 val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x"; |
30 val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t; |
30 val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t; |
31 val result = term2str t_; |
31 val result = term2str t_; |
32 if result <> "True" then raise error "rateq.sml: new behaviour 4:" else (); |
32 if result <> "True" then error "rateq.sml: new behaviour 4:" else (); |
33 |
33 |
34 val result = match_pbl ["equality (x=1)","solveFor x","solutions L"] |
34 val result = match_pbl ["equality (x=1)","solveFor x","solutions L"] |
35 (get_pbt ["rational","univariate","equation"]); |
35 (get_pbt ["rational","univariate","equation"]); |
36 case result of NoMatch' _ => () | _ => raise error "rateq.sml: new behaviour: 5"; |
36 case result of NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5"; |
37 |
37 |
38 val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"] |
38 val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"] |
39 (get_pbt ["rational","univariate","equation"]); |
39 (get_pbt ["rational","univariate","equation"]); |
40 case result of Matches' _ => () | _ => raise error "rateq.sml: new behaviour: 6"; |
40 case result of Matches' _ => () | _ => error "rateq.sml: new behaviour: 6"; |
41 |
41 |
42 |
42 |
43 (*---------rateq---- 23.8.02 ---------------------*) |
43 (*---------rateq---- 23.8.02 ---------------------*) |
44 "---------(1/x=5) ---------------------"; |
44 "---------(1/x=5) ---------------------"; |
45 val fmz = ["equality (1/x=5)","solveFor x","solutions L"]; |
45 val fmz = ["equality (1/x=5)","solveFor x","solutions L"]; |
88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
90 (* "x = 1 / 5" *) |
90 (* "x = 1 / 5" *) |
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
92 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = 1 / 5])" then () |
92 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = 1 / 5])" then () |
93 else raise error "rateq.sml: new behaviour: [x = 1 / 5]"; |
93 else error "rateq.sml: new behaviour: [x = 1 / 5]"; |
94 |
94 |
95 |
95 |
96 |
96 |
97 (*---------((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------*) |
97 (*---------((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------*) |
98 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------"; |
98 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------"; |
138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
141 (* "x = -2, x = 10" *) |
141 (* "x = -2, x = 10" *) |
142 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then() |
142 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then() |
143 else raise error "rateq.sml: new behaviour: [x = -2, x = 10]"; |
143 else error "rateq.sml: new behaviour: [x = -2, x = 10]"; |
144 |
144 |
145 "----------- rateq.sml end--------"; |
145 "----------- rateq.sml end--------"; |