|
1 (* tests on rewrite orders |
|
2 |
|
3 use"../kbtest/termorder.sml"; |
|
4 use"kbtest/termorder.sml"; |
|
5 *) |
|
6 |
|
7 |
|
8 (*die ersten Tests*) |
|
9 val substa = [(e_term, (term_of o the o (parse thy)) "a")]; |
|
10 val substb = [(e_term, (term_of o the o (parse thy)) "b")]; |
|
11 val substx = [(e_term, (term_of o the o (parse thy)) "x")]; |
|
12 val x1 = (term_of o the o (parse thy)) "a + b + x"; |
|
13 val x2 = (term_of o the o (parse thy)) "a + x + b"; |
|
14 val x3 = (term_of o the o (parse thy)) "a + x + b"; |
|
15 val x4 = (term_of o the o (parse thy)) "x + a + b"; |
|
16 ord_make_polynomial_in true thy substx (x1,x2); |
|
17 true; (* => LESS *) |
|
18 ord_make_polynomial_in true thy substa (x1,x2); |
|
19 true; (* => LESS *) |
|
20 ord_make_polynomial_in true thy substb (x1,x2); |
|
21 false; (* => GREATER *) |
|
22 |
|
23 val aa = (term_of o the o (parse thy)) "-1 * a * x"; |
|
24 val bb = (term_of o the o (parse thy)) "x^^^3"; |
|
25 ord_make_polynomial_in true thy substx (aa, bb); |
|
26 true; (* => LESS *) |
|
27 |
|
28 val aa = (term_of o the o (parse thy)) "-1 * a * x"; |
|
29 val bb = (term_of o the o (parse thy)) "x^^^3"; |
|
30 ord_make_polynomial_in true thy substa (aa, bb); |
|
31 false; (* => GREATER *) |
|
32 |
|
33 (*und nach dem Re-engineering der Termorders in den 'rulesets' |
|
34 kannst Du die 'gr"osste' Variable frei w"ahlen: *) |
|
35 val bdv= (term_of o the o (parse thy)) "bdv"; |
|
36 val x = (term_of o the o (parse thy)) "x"; |
|
37 val a = (term_of o the o (parse thy)) "a"; |
|
38 val b = (term_of o the o (parse thy)) "b"; |
|
39 val Some (t',_) = |
|
40 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; |
|
41 term2str t'; |
|
42 "b + x + a"; |
|
43 val None = |
|
44 rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2; |
|
45 term2str t'; |
|
46 "a + x + b"; |
|
47 val Some (t',_) = |
|
48 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2; |
|
49 term2str t'; |
|
50 "a + b + x"; |
|
51 |
|
52 |
|
53 val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2"; |
|
54 val ppp = (term_of o the o (parse thy)) ppp'; |
|
55 val Some (t',_) = |
|
56 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; |
|
57 term2str t'; |
|
58 "(-6) + (-5 * x + (-15 * x ^^^ 2))"; |
|
59 val Some (t',_) = |
|
60 rewrite_set_inst "Isac.thy"false [("bdv","x")] "make_polynomial_in" ppp'; |
|
61 "(-6) + (-5 * x + (-15) * x ^^^ 2)"; |
|
62 |
|
63 |
|
64 val ttt' = "(3*x + 5)/18"; |
|
65 val ttt = (term_of o the o (parse thy)) ttt'; |
|
66 val Some (uuu,_) = |
|
67 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; |
|
68 term2str uuu; |
|
69 "(5 + 3 * x) / 18"; |
|
70 val Some (uuu,_) = |
|
71 rewrite_set_ thy false make_polynomial ttt; |
|
72 term2str uuu; |
|
73 "(5 + 3 * x) / 18"; |
|
74 |
|
75 |
|
76 |
|
77 |
|
78 (*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML |
|
79 |
|
80 (*Aufgabe zum Einstieg in die Arbeit...*) |
|
81 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0"; |
|
82 (*ein 'ruleset' aus Poly.ML wird angewandt...*) |
|
83 val Some (t,_) = rewrite_set_ thy poly_erls false make_polynomial t; |
|
84 term2str t; |
|
85 "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0"; |
|
86 val Some (t,_) = |
|
87 rewrite_set_inst_ thy poly_erls false [("bdv","a")] make_polynomial_in t; |
|
88 term2str t; |
|
89 "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0"; |
|
90 (* bei Verwendung von "size_of-term" nach MG :*) |
|
91 (*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *) |
|
92 |
|
93 (*wir holen 'a' wieder aus der Klammerung heraus...*) |
|
94 val Some (t,_) = rewrite_set_ thy poly_erls false discard_parentheses t; |
|
95 term2str t; |
|
96 "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0"; |
|
97 (* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *) |
|
98 |
|
99 val Some (t,_) = |
|
100 rewrite_set_inst_ thy poly_erls false [("bdv","a")] make_polynomial_in t; |
|
101 term2str t; |
|
102 "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; |
|
103 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben |
|
104 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*) |
|
105 |
|
106 (*das rewriting l"asst sich beobachten mit |
|
107 trace_rewrite:=true; |
|
108 *) |
|
109 |
|
110 |
|
111 |
|
112 "------15.11.02 --------------------------"; |
|
113 val t = (term_of o the o (parse thy)) "1 + a * x + b * x"; |
|
114 val bdv = (term_of o the o (parse thy)) "bdv"; |
|
115 val a = (term_of o the o (parse thy)) "a"; |
|
116 |
|
117 trace_rewrite:=true; |
|
118 (* Anwenden einer Regelmenge aus Termorder.ML: *) |
|
119 val Some (t,_) = |
|
120 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
|
121 term2str t; |
|
122 val Some (t,_) = |
|
123 rewrite_set_ thy false discard_parentheses t; |
|
124 term2str t; |
|
125 "1 + b * x + x * a"; |
|
126 |
|
127 val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2"; |
|
128 val Some (t,_) = |
|
129 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
|
130 term2str t; |
|
131 val Some (t,_) = |
|
132 rewrite_set_ thy false discard_parentheses t; |
|
133 term2str t; |
|
134 "1 + (x + b * x) * a + a ^^^ 2"; |
|
135 |
|
136 val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2"; |
|
137 val Some (t,_) = |
|
138 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
|
139 term2str t; |
|
140 val Some (t,_) = |
|
141 rewrite_set_ thy false discard_parentheses t; |
|
142 term2str t; |
|
143 "1 + b * a + (7 + x) * a ^^^ 2"; |
|
144 |
|
145 (* |
|
146 Atools.thy grundlegende Algebra |
|
147 Poly.thy Polynome |
|
148 Rational.thy Br"uche |
|
149 Root.thy Wurzeln |
|
150 RootRat.thy Wurzen + Br"uche |
|
151 Termorder.thy BITTE NUR HIERHER SCHREIBEN |
|
152 |
|
153 cd"knowledge"; |
|
154 remove_thy"Termorder"; |
|
155 use_thy"Isac"; |
|
156 |
|
157 get_thm Termorder.thy "bdv_n_collect"; |
|
158 get_thm Isac.thy "bdv_n_collect"; |
|
159 |
|
160 *) |
|
161 val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2"; |
|
162 val Some (t,_) = |
|
163 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
|
164 term2str t; |
|
165 val Some (t,_) = |
|
166 rewrite_set_ thy false discard_parentheses t; |
|
167 term2str t; |
|
168 "(7 + x) * a ^^^ 2"; |
|
169 |
|
170 val t = (term_of o the o (parse Termorder.thy)) "Pi"; |
|
171 |
|
172 val t = (term_of o the o (parseold thy)) "7"; |
|
173 |
|
174 ----------------------------------------------------------------------*) |