|
1 (* RL 10.02 |
|
2 use"../kbtest/rooteq.sml"; |
|
3 testexamples for RootEq, equations with fractions |
|
4 |
|
5 Compiler.Control.Print.printDepth:=10; (*4 default*) |
|
6 Compiler.Control.Print.printDepth:=5; (*4 default*) |
|
7 trace_rewrite:=true; |
|
8 *) |
|
9 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootequation_in x"; |
|
10 val Some(t_, _) = rewrite_set_ RootEq.thy false rooteq_prls t; |
|
11 val result = term2str t_; |
|
12 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
|
13 |
|
14 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootequation_in x"; |
|
15 val Some(t_, _) = rewrite_set_ RootEq.thy false rooteq_prls t; |
|
16 val result = term2str t_; |
|
17 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
|
18 |
|
19 val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootequation_in x"; |
|
20 val Some(t_, _) = rewrite_set_ RootEq.thy false rooteq_prls t; |
|
21 val result = term2str t_; |
|
22 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
|
23 |
|
24 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtequation_in x"; |
|
25 val Some(t_, _) = rewrite_set_ RootEq.thy false rooteq_prls t; |
|
26 val result = term2str t_; |
|
27 if result <> "True" then raise error "rooteq.sml: new behaviour:" else (); |
|
28 |
|
29 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtequation_in x"; |
|
30 val Some(t_, _) = rewrite_set_ RootEq.thy false rooteq_prls t; |
|
31 val result = term2str t_; |
|
32 if result <> "False" then raise error "rooteq.sml: new behaviour:" else (); |
|
33 |
|
34 |
|
35 val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] |
|
36 (get_pbt ["root","univariate","equation"]); |
|
37 case result of Matches' _ => () | _ => raise error "rooteq.sml: new behaviour:"; |
|
38 |
|
39 val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"] |
|
40 (get_pbt ["root","univariate","equation"]); |
|
41 case result of NoMatch' _ => () | _ => raise error "rooteq.sml: new behaviour:"; |
|
42 |
|
43 (*---------rooteq---- 23.8.02 ---------------------*) |
|
44 val fmz = ["equality (sqrt(x)=5)","solveFor x","solutions L"]; |
|
45 val fmz = ["equality (5*sqrt(3*x+1)=3*sqrt(5*x+25))","solveFor x","solutions L"]; |
|
46 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))","solveFor x","solutions L"]; |
|
47 (*0=0*) |
|
48 val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))","solveFor x","solutions L"]; |
|
49 (* [x = -2] *) |
|
50 |
|
51 (* refine fmz ["univariate","equation"]; |
|
52 Compiler.Control.Print.printDepth:=10; (*4 default*) |
|
53 Compiler.Control.Print.printDepth:=5; (*4 default*) |
|
54 trace_rewrite:=true; |
|
55 *) |
|
56 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],("RootEq.thy","no_met")); |
|
57 val p = e_pos'; |
|
58 val c = []; |
|
59 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
60 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
61 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
62 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
63 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
65 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
66 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
68 |
|
69 |
|
70 |