|
agriesma@334
|
1 |
(* RL 09.02
|
|
agriesma@334
|
2 |
testexamples for RatEq, equations with fractions
|
|
agriesma@334
|
3 |
|
|
agriesma@334
|
4 |
Compiler.Control.Print.printDepth:=10; (*4 default*)
|
|
agriesma@334
|
5 |
Compiler.Control.Print.printDepth:=5; (*4 default*)
|
|
agriesma@334
|
6 |
trace_rewrite:=true;
|
|
agriesma@334
|
7 |
*)
|
|
agriesma@334
|
8 |
"----------- rateq.sml begin--------";
|
|
agriesma@334
|
9 |
"---------(1/x=5) ---------------------";
|
|
agriesma@334
|
10 |
"--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
|
|
agriesma@334
|
11 |
|
|
agriesma@334
|
12 |
val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x";
|
|
agriesma@334
|
13 |
val Some(t_, _) = rewrite_set_ RatEq.thy false rateq_prls t;
|
|
agriesma@334
|
14 |
val result = term2str t_;
|
|
agriesma@334
|
15 |
if result <> "True" then raise error "rateq.sml: new behaviour:" else ();
|
|
agriesma@334
|
16 |
|
|
agriesma@334
|
17 |
val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in x";
|
|
agriesma@334
|
18 |
val Some(t_, _) = rewrite_set_ RatEq.thy false rateq_prls t;
|
|
agriesma@334
|
19 |
val result = term2str t_;
|
|
agriesma@334
|
20 |
if result <> "False" then raise error "rateq.sml: new behaviour:" else ();
|
|
agriesma@334
|
21 |
|
|
agriesma@334
|
22 |
val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x";
|
|
agriesma@334
|
23 |
val Some(t_,_) = rewrite_set_ RatEq.thy false rateq_prls t;
|
|
agriesma@334
|
24 |
val result = term2str t_;
|
|
agriesma@334
|
25 |
if result <> "False" then raise error "rateq.sml: new behaviour:" else ();
|
|
agriesma@334
|
26 |
|
|
agriesma@334
|
27 |
val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
|
|
agriesma@334
|
28 |
val Some(t_,_) = rewrite_set_ RatEq.thy false rateq_prls t;
|
|
agriesma@334
|
29 |
val result = term2str t_;
|
|
agriesma@334
|
30 |
if result <> "True" then raise error "rateq.sml: new behaviour:" else ();
|
|
agriesma@334
|
31 |
|
|
agriesma@334
|
32 |
val result = match_pbl ["equality (x=1)","solveFor x","solutions L"]
|
|
agriesma@334
|
33 |
(get_pbt ["rational","univariate","equation"]);
|
|
agriesma@334
|
34 |
case result of NoMatch' _ => () | _ => raise error "rateq.sml: new behaviour:";
|
|
agriesma@334
|
35 |
|
|
agriesma@334
|
36 |
val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
|
|
agriesma@334
|
37 |
(get_pbt ["rational","univariate","equation"]);
|
|
agriesma@334
|
38 |
case result of Matches' _ => () | _ => raise error "rateq.sml: new behaviour:";
|
|
agriesma@334
|
39 |
|
|
agriesma@334
|
40 |
|
|
agriesma@334
|
41 |
(*---------rateq---- 23.8.02 ---------------------*)
|
|
agriesma@334
|
42 |
"---------(1/x=5) ---------------------";
|
|
agriesma@334
|
43 |
val fmz = ["equality (1/x=5)","solveFor x","solutions L"];
|
|
agriesma@334
|
44 |
(* refine fmz ["univariate","equation"];
|
|
agriesma@334
|
45 |
*)
|
|
agriesma@334
|
46 |
|
|
agriesma@334
|
47 |
val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
|
|
agriesma@334
|
48 |
val p = e_pos';
|
|
agriesma@334
|
49 |
val c = [];
|
|
agriesma@334
|
50 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
|
agriesma@334
|
51 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
|
|
agriesma@334
|
52 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
53 |
(* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
|
|
agriesma@334
|
54 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
55 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
56 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
57 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
58 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
59 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
60 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
61 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
62 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
63 |
(* val nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"]))*)
|
|
agriesma@334
|
64 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
65 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
66 |
(*val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
|
|
agriesma@334
|
67 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
68 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
69 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
70 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
71 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
72 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
73 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
74 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
75 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
76 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
77 |
(* val nxt = ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
|
|
agriesma@334
|
78 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
79 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
80 |
(* ("Model_Problem", Model_Problem ["degree_1","polynomial","univariate","equation"])*)
|
|
agriesma@334
|
81 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
82 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
83 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
84 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
85 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
86 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
87 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
88 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
89 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
90 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
91 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
92 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
93 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
94 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
95 |
(* "x = 1 / 5" *)
|
|
agriesma@334
|
96 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
97 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
98 |
if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = 1 / 5])" then ()
|
|
agriesma@334
|
99 |
else raise error "rateq.sml: new behaviour:";
|
|
agriesma@334
|
100 |
|
|
agriesma@334
|
101 |
(*---------((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------*)
|
|
agriesma@334
|
102 |
"--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
|
|
agriesma@334
|
103 |
val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/5)","solveFor x","solutions L"];
|
|
agriesma@334
|
104 |
(* val fmz = ["equality (3+x= 9*x^^^4+((1+2*x)/x^^^2)^^^2 + 6*(x^^^2*((1+2*x)/x^^^2)))",
|
|
agriesma@334
|
105 |
"solveFor x","solutions L"];*)
|
|
agriesma@334
|
106 |
|
|
agriesma@334
|
107 |
(* refine fmz ["univariate","equation"];
|
|
agriesma@334
|
108 |
*)
|
|
agriesma@334
|
109 |
|
|
agriesma@334
|
110 |
val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
|
|
agriesma@334
|
111 |
val p = e_pos';
|
|
agriesma@334
|
112 |
val c = [];
|
|
agriesma@334
|
113 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
|
agriesma@334
|
114 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
|
|
agriesma@334
|
115 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
116 |
(* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
|
|
agriesma@334
|
117 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
118 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
119 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
120 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
121 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
122 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
123 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
124 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
125 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
126 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
127 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
128 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
129 |
(* nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"]))*)
|
|
agriesma@334
|
130 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
131 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
132 |
(* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
|
|
agriesma@334
|
133 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
134 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
135 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
136 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
137 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
138 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
139 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
140 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
141 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
142 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
143 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
144 |
(* ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])) *)
|
|
agriesma@334
|
145 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
146 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
147 |
(* nxt = ("Model_Problem", Model_Problem
|
|
agriesma@334
|
148 |
["abcFormula","degree_2","polynomial","univariate","equation"])*)
|
|
agriesma@334
|
149 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
150 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
151 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
152 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
153 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
154 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
155 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
156 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
157 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
158 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
159 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
160 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
161 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
162 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
163 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
164 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
165 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
agriesma@334
|
166 |
(* "x = -2, x = 10" *)
|
|
agriesma@334
|
167 |
if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then ()
|
|
agriesma@334
|
168 |
else raise error "rateq.sml: new behaviour:";
|
|
agriesma@334
|
169 |
|
|
agriesma@334
|
170 |
"----------- rateq.sml end--------";
|