neuper@37954
|
1 |
(* some tests are based on specficially simple scripts etc.
|
neuper@37954
|
2 |
Author: Walther Neuper 2003
|
neuper@37954
|
3 |
(c) due to copyright terms
|
neuper@37954
|
4 |
*)
|
neuper@37906
|
5 |
|
neuper@38007
|
6 |
theory Test imports Atools Poly Rational Root Diff begin
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
consts
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
(*"cancel":: [real, real] => real (infixl "'/'/'/" 70) ...divide 2002*)
|
neuper@37906
|
11 |
|
neuper@37906
|
12 |
Expand'_binomtest
|
neuper@37954
|
13 |
:: "['y,
|
neuper@37954
|
14 |
'y] => 'y"
|
neuper@37954
|
15 |
("((Script Expand'_binomtest (_ =))//
|
neuper@37954
|
16 |
(_))" 9)
|
neuper@37906
|
17 |
|
neuper@37906
|
18 |
Solve'_univar'_err
|
neuper@37954
|
19 |
:: "[bool,real,bool,
|
neuper@37954
|
20 |
bool list] => bool list"
|
neuper@37954
|
21 |
("((Script Solve'_univar'_err (_ _ _ =))//
|
neuper@37954
|
22 |
(_))" 9)
|
neuper@37906
|
23 |
|
neuper@37906
|
24 |
Solve'_linear
|
neuper@37954
|
25 |
:: "[bool,real,
|
neuper@37954
|
26 |
bool list] => bool list"
|
neuper@37954
|
27 |
("((Script Solve'_linear (_ _ =))//
|
neuper@37954
|
28 |
(_))" 9)
|
neuper@37906
|
29 |
|
neuper@37906
|
30 |
(*17.9.02 aus SqRoot.thy------------------------------vvv---*)
|
neuper@37906
|
31 |
|
neuper@42008
|
32 |
"is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10)
|
neuper@42008
|
33 |
"contains'_root" :: "'a => bool" ("contains'_root _" 10)
|
neuper@42008
|
34 |
|
neuper@42008
|
35 |
"precond'_rootmet" :: "'a => bool" ("precond'_rootmet _" 10)
|
neuper@42008
|
36 |
"precond'_rootpbl" :: "'a => bool" ("precond'_rootpbl _" 10)
|
neuper@42008
|
37 |
"precond'_submet" :: "'a => bool" ("precond'_submet _" 10)
|
neuper@42008
|
38 |
"precond'_subpbl" :: "'a => bool" ("precond'_subpbl _" 10)
|
neuper@37906
|
39 |
|
neuper@37906
|
40 |
Solve'_root'_equation
|
neuper@37954
|
41 |
:: "[bool,real,
|
neuper@37954
|
42 |
bool list] => bool list"
|
neuper@37954
|
43 |
("((Script Solve'_root'_equation (_ _ =))//
|
neuper@37954
|
44 |
(_))" 9)
|
neuper@37906
|
45 |
|
neuper@37906
|
46 |
Solve'_plain'_square
|
neuper@37954
|
47 |
:: "[bool,real,
|
neuper@37954
|
48 |
bool list] => bool list"
|
neuper@37954
|
49 |
("((Script Solve'_plain'_square (_ _ =))//
|
neuper@37954
|
50 |
(_))" 9)
|
neuper@37906
|
51 |
|
neuper@37906
|
52 |
Norm'_univar'_equation
|
neuper@37954
|
53 |
:: "[bool,real,
|
neuper@37954
|
54 |
bool] => bool"
|
neuper@37954
|
55 |
("((Script Norm'_univar'_equation (_ _ =))//
|
neuper@37954
|
56 |
(_))" 9)
|
neuper@37906
|
57 |
|
neuper@37906
|
58 |
STest'_simplify
|
neuper@37954
|
59 |
:: "['z,
|
neuper@37954
|
60 |
'z] => 'z"
|
neuper@37954
|
61 |
("((Script STest'_simplify (_ =))//
|
neuper@37954
|
62 |
(_))" 9)
|
neuper@37906
|
63 |
|
neuper@37906
|
64 |
(*17.9.02 aus SqRoot.thy------------------------------^^^---*)
|
neuper@37906
|
65 |
|
t@42211
|
66 |
axioms(*axiomatization where*) (*TODO: prove as theorems*)
|
neuper@37906
|
67 |
|
t@42211
|
68 |
radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" (*and*)
|
t@42211
|
69 |
rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" (*and*)
|
t@42211
|
70 |
rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" (*and*)
|
t@42211
|
71 |
rdistr_div_right: "((k::real) + l) / n = k / n + l / n" (*and*)
|
neuper@37983
|
72 |
rcollect_right:
|
t@42211
|
73 |
"[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" (*and*)
|
neuper@37983
|
74 |
rcollect_one_left:
|
t@42211
|
75 |
"m is_const ==> (n::real) + m * n = (1 + m) * n" (*and*)
|
neuper@37983
|
76 |
rcollect_one_left_assoc:
|
t@42211
|
77 |
"m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" (*and*)
|
neuper@37983
|
78 |
rcollect_one_left_assoc_p:
|
t@42211
|
79 |
"m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" (*and*)
|
neuper@37906
|
80 |
|
t@42211
|
81 |
rtwo_of_the_same: "a + a = 2 * a" (*and*)
|
t@42211
|
82 |
rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" (*and*)
|
t@42211
|
83 |
rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" (*and*)
|
neuper@37906
|
84 |
|
t@42211
|
85 |
rcancel_den: "not(a=0) ==> a * (b / a) = b" (*and*)
|
t@42211
|
86 |
rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" (*and*)
|
t@42211
|
87 |
rshift_nominator: "(a::real) * b / c = a / c * b" (*and*)
|
neuper@37906
|
88 |
|
t@42211
|
89 |
exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" (*and*)
|
t@42211
|
90 |
rsqare: "(a::real) * a = a ^^^ 2" (*and*)
|
t@42211
|
91 |
power_1: "(a::real) ^^^ 1 = a" (*and*)
|
t@42211
|
92 |
rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" (*and*)
|
neuper@37906
|
93 |
|
t@42211
|
94 |
rmult_1: "1 * k = (k::real)" (*and*)
|
t@42211
|
95 |
rmult_1_right: "k * 1 = (k::real)" (*and*)
|
t@42211
|
96 |
rmult_0: "0 * k = (0::real)" (*and*)
|
t@42211
|
97 |
rmult_0_right: "k * 0 = (0::real)" (*and*)
|
t@42211
|
98 |
radd_0: "0 + k = (k::real)" (*and*)
|
t@42211
|
99 |
radd_0_right: "k + 0 = (k::real)" (*and*)
|
neuper@37906
|
100 |
|
neuper@37983
|
101 |
radd_real_const_eq:
|
t@42211
|
102 |
"[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" (*and*)
|
neuper@37983
|
103 |
radd_real_const:
|
neuper@37906
|
104 |
"[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
|
t@42211
|
105 |
(*and*)
|
neuper@37906
|
106 |
(*for AC-operators*)
|
t@42211
|
107 |
radd_commute: "(m::real) + (n::real) = n + m" (*and*)
|
t@42211
|
108 |
radd_left_commute: "(x::real) + (y + z) = y + (x + z)" (*and*)
|
t@42211
|
109 |
radd_assoc: "(m::real) + n + k = m + (n + k)" (*and*)
|
t@42211
|
110 |
rmult_commute: "(m::real) * n = n * m" (*and*)
|
t@42211
|
111 |
rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" (*and*)
|
t@42211
|
112 |
rmult_assoc: "(m::real) * n * k = m * (n * k)" (*and*)
|
neuper@37906
|
113 |
|
neuper@37906
|
114 |
(*for equations: 'bdv' is a meta-constant*)
|
t@42211
|
115 |
risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" (*and*)
|
t@42211
|
116 |
risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" (*and*)
|
t@42211
|
117 |
risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" (*and*)
|
neuper@37906
|
118 |
|
neuper@37983
|
119 |
rnorm_equation_add:
|
t@42211
|
120 |
"~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" (*and*)
|
neuper@37906
|
121 |
|
neuper@37906
|
122 |
(*17.9.02 aus SqRoot.thy------------------------------vvv---*)
|
t@42211
|
123 |
root_ge0: "0 <= a ==> 0 <= sqrt a" (*and*)
|
neuper@37906
|
124 |
(*should be dropped with better simplification in eval_rls ...*)
|
neuper@37983
|
125 |
root_add_ge0:
|
t@42211
|
126 |
"[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" (*and*)
|
neuper@37983
|
127 |
root_ge0_1:
|
t@42211
|
128 |
"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" (*and*)
|
neuper@37983
|
129 |
root_ge0_2:
|
t@42211
|
130 |
"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" (*and*)
|
neuper@37906
|
131 |
|
neuper@37906
|
132 |
|
t@42211
|
133 |
rroot_square_inv: "(sqrt a)^^^ 2 = a" (*and*)
|
t@42211
|
134 |
rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" (*and*)
|
t@42211
|
135 |
rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" (*and*)
|
t@42211
|
136 |
rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" (*and*)
|
neuper@37906
|
137 |
|
neuper@37906
|
138 |
|
neuper@37906
|
139 |
(*for root-equations*)
|
neuper@37983
|
140 |
square_equation_left:
|
t@42211
|
141 |
"[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" (*and*)
|
neuper@37983
|
142 |
square_equation_right:
|
t@42211
|
143 |
"[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" (*and*)
|
neuper@37906
|
144 |
(*causes frequently non-termination:*)
|
neuper@37983
|
145 |
square_equation:
|
t@42211
|
146 |
"[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" (*and*)
|
neuper@37906
|
147 |
|
t@42211
|
148 |
risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" (*and*)
|
t@42211
|
149 |
risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" (*and*)
|
t@42211
|
150 |
risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" (*and*)
|
neuper@37906
|
151 |
|
neuper@37906
|
152 |
(*for polynomial equations of degree 2; linear case in RatArith*)
|
t@42211
|
153 |
mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" (*and*)
|
t@42211
|
154 |
constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" (*and*)
|
t@42211
|
155 |
constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" (*and*)
|
neuper@37906
|
156 |
|
neuper@37983
|
157 |
square_equality:
|
t@42211
|
158 |
"0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" (*and*)
|
neuper@37983
|
159 |
square_equality_0:
|
t@42211
|
160 |
"(x^^^2 = 0) = (x = 0)" (*and*)
|
neuper@37906
|
161 |
|
neuper@37906
|
162 |
(*isolate root on the LEFT hand side of the equation
|
neuper@37906
|
163 |
otherwise shuffling from left to right would not terminate*)
|
neuper@37906
|
164 |
|
neuper@37983
|
165 |
rroot_to_lhs:
|
t@42211
|
166 |
"is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" (*and*)
|
neuper@37983
|
167 |
rroot_to_lhs_mult:
|
t@42211
|
168 |
"is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" (*and*)
|
neuper@37983
|
169 |
rroot_to_lhs_add_mult:
|
neuper@37906
|
170 |
"is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
|
neuper@37906
|
171 |
(*17.9.02 aus SqRoot.thy------------------------------^^^---*)
|
neuper@37906
|
172 |
|
neuper@37954
|
173 |
ML {*
|
neuper@37972
|
174 |
val thy = @{theory};
|
neuper@37972
|
175 |
|
neuper@37954
|
176 |
(** evaluation of numerals and predicates **)
|
neuper@37954
|
177 |
|
neuper@42008
|
178 |
(*does a term contain a root ? WN110518 seems incorrect, compare contains_root*)
|
neuper@52070
|
179 |
fun eval_root_free (thmid:string) _ (t as (Const (op0, t0) $ arg)) thy =
|
neuper@37954
|
180 |
if strip_thy op0 <> "is'_root'_free"
|
neuper@52070
|
181 |
then error ("eval_root_free: wrong " ^ op0)
|
neuper@37954
|
182 |
else if const_in (strip_thy op0) arg
|
neuper@52070
|
183 |
then SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
|
neuper@52070
|
184 |
Trueprop $ (mk_equality (t, @{term False})))
|
neuper@52070
|
185 |
else SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
|
neuper@52070
|
186 |
Trueprop $ (mk_equality (t, @{term True})))
|
neuper@38053
|
187 |
| eval_root_free _ _ _ _ = NONE;
|
neuper@37954
|
188 |
|
neuper@37954
|
189 |
(*does a term contain a root ?*)
|
neuper@37954
|
190 |
fun eval_contains_root (thmid:string) _
|
neuper@37954
|
191 |
(t as (Const("Test.contains'_root",t0) $ arg)) thy =
|
neuper@38053
|
192 |
if member op = (ids_of arg) "sqrt"
|
neuper@52070
|
193 |
then SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
|
neuper@52070
|
194 |
Trueprop $ (mk_equality (t, @{term True})))
|
neuper@52070
|
195 |
else SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
|
neuper@52070
|
196 |
Trueprop $ (mk_equality (t, @{term False})))
|
neuper@38053
|
197 |
| eval_contains_root _ _ _ _ = NONE;
|
neuper@42008
|
198 |
|
neuper@42008
|
199 |
(*dummy precondition for root-met of x+1=2*)
|
neuper@42008
|
200 |
fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy =
|
neuper@52070
|
201 |
SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
|
neuper@52070
|
202 |
Trueprop $ (mk_equality (t, @{term True})))
|
neuper@52070
|
203 |
| eval_precond_rootmet _ _ _ _ = NONE;
|
neuper@42008
|
204 |
|
neuper@42008
|
205 |
(*dummy precondition for root-pbl of x+1=2*)
|
neuper@42008
|
206 |
fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy =
|
neuper@52070
|
207 |
SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
|
neuper@52070
|
208 |
Trueprop $ (mk_equality (t, @{term True})))
|
neuper@52070
|
209 |
| eval_precond_rootpbl _ _ _ _ = NONE;
|
neuper@42008
|
210 |
|
neuper@37954
|
211 |
calclist':= overwritel (!calclist',
|
neuper@37954
|
212 |
[("is_root_free", ("Test.is'_root'_free",
|
neuper@37981
|
213 |
eval_root_free"#is_root_free_e")),
|
neuper@37954
|
214 |
("contains_root", ("Test.contains'_root",
|
neuper@42008
|
215 |
eval_contains_root"#contains_root_")),
|
neuper@42008
|
216 |
("Test.precond'_rootmet", ("Test.precond'_rootmet",
|
neuper@42008
|
217 |
eval_precond_rootmet"#Test.precond_rootmet_")),
|
neuper@42008
|
218 |
("Test.precond'_rootpbl", ("Test.precond'_rootpbl",
|
neuper@42024
|
219 |
eval_precond_rootpbl"#Test.precond_rootpbl_"))
|
neuper@37954
|
220 |
]);
|
neuper@37954
|
221 |
|
neuper@37954
|
222 |
(** term order **)
|
neuper@38001
|
223 |
fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
|
neuper@38001
|
224 |
*}
|
neuper@38001
|
225 |
ML {*
|
neuper@38001
|
226 |
(** rule sets **)
|
neuper@37954
|
227 |
|
neuper@37954
|
228 |
val testerls =
|
neuper@37954
|
229 |
Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
|
neuper@37954
|
230 |
erls = e_rls, srls = Erls,
|
neuper@42451
|
231 |
calc = [], errpatts = [],
|
neuper@37969
|
232 |
rules = [Thm ("refl",num_str @{thm refl}),
|
neuper@48764
|
233 |
Thm ("order_refl",num_str @{thm order_refl}),
|
neuper@37969
|
234 |
Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
|
neuper@37969
|
235 |
Thm ("not_true",num_str @{thm not_true}),
|
neuper@37969
|
236 |
Thm ("not_false",num_str @{thm not_false}),
|
neuper@37969
|
237 |
Thm ("and_true",num_str @{thm and_true}),
|
neuper@37969
|
238 |
Thm ("and_false",num_str @{thm and_false}),
|
neuper@37969
|
239 |
Thm ("or_true",num_str @{thm or_true}),
|
neuper@37969
|
240 |
Thm ("or_false",num_str @{thm or_false}),
|
neuper@37969
|
241 |
Thm ("and_commute",num_str @{thm and_commute}),
|
neuper@37969
|
242 |
Thm ("or_commute",num_str @{thm or_commute}),
|
neuper@37954
|
243 |
|
neuper@37954
|
244 |
Calc ("Atools.is'_const",eval_const "#is_const_"),
|
neuper@37954
|
245 |
Calc ("Tools.matches",eval_matches ""),
|
neuper@37954
|
246 |
|
neuper@38014
|
247 |
Calc ("Groups.plus_class.plus",eval_binop "#add_"),
|
neuper@38034
|
248 |
Calc ("Groups.times_class.times",eval_binop "#mult_"),
|
neuper@37954
|
249 |
Calc ("Atools.pow" ,eval_binop "#power_"),
|
neuper@37954
|
250 |
|
neuper@38045
|
251 |
Calc ("Orderings.ord_class.less",eval_equ "#less_"),
|
neuper@38045
|
252 |
Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
|
neuper@37954
|
253 |
|
neuper@37954
|
254 |
Calc ("Atools.ident",eval_ident "#ident_")],
|
neuper@48763
|
255 |
scr = Prog ((term_of o the o (parse thy)) "empty_script")
|
neuper@37954
|
256 |
}:rls;
|
neuper@38001
|
257 |
*}
|
neuper@38001
|
258 |
ML {*
|
neuper@37954
|
259 |
(*.for evaluation of conditions in rewrite rules.*)
|
neuper@37954
|
260 |
(*FIXXXXXXME 10.8.02: handle like _simplify*)
|
neuper@37954
|
261 |
val tval_rls =
|
neuper@37954
|
262 |
Rls{id = "tval_rls", preconds = [],
|
neuper@40836
|
263 |
rew_ord = ("sqrt_right",sqrt_right false (Thy_Info.get_theory "Pure")),
|
neuper@37954
|
264 |
erls=testerls,srls = e_rls,
|
neuper@42451
|
265 |
calc=[], errpatts = [],
|
neuper@37969
|
266 |
rules = [Thm ("refl",num_str @{thm refl}),
|
neuper@48764
|
267 |
Thm ("order_refl",num_str @{thm order_refl}),
|
neuper@37969
|
268 |
Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
|
neuper@37969
|
269 |
Thm ("not_true",num_str @{thm not_true}),
|
neuper@37969
|
270 |
Thm ("not_false",num_str @{thm not_false}),
|
neuper@37969
|
271 |
Thm ("and_true",num_str @{thm and_true}),
|
neuper@37969
|
272 |
Thm ("and_false",num_str @{thm and_false}),
|
neuper@37969
|
273 |
Thm ("or_true",num_str @{thm or_true}),
|
neuper@37969
|
274 |
Thm ("or_false",num_str @{thm or_false}),
|
neuper@37969
|
275 |
Thm ("and_commute",num_str @{thm and_commute}),
|
neuper@38001
|
276 |
Thm ("or_commute",num_str @{thm or_commute}),
|
neuper@37954
|
277 |
|
neuper@37969
|
278 |
Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
|
neuper@37954
|
279 |
|
neuper@37969
|
280 |
Thm ("root_ge0",num_str @{thm root_ge0}),
|
neuper@37969
|
281 |
Thm ("root_add_ge0",num_str @{thm root_add_ge0}),
|
neuper@37969
|
282 |
Thm ("root_ge0_1",num_str @{thm root_ge0_1}),
|
neuper@37969
|
283 |
Thm ("root_ge0_2",num_str @{thm root_ge0_2}),
|
neuper@37954
|
284 |
|
neuper@37954
|
285 |
Calc ("Atools.is'_const",eval_const "#is_const_"),
|
neuper@37981
|
286 |
Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_e"),
|
neuper@37954
|
287 |
Calc ("Tools.matches",eval_matches ""),
|
neuper@37954
|
288 |
Calc ("Test.contains'_root",
|
neuper@37954
|
289 |
eval_contains_root"#contains_root_"),
|
neuper@37954
|
290 |
|
neuper@38014
|
291 |
Calc ("Groups.plus_class.plus",eval_binop "#add_"),
|
neuper@38034
|
292 |
Calc ("Groups.times_class.times",eval_binop "#mult_"),
|
neuper@37982
|
293 |
Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
|
neuper@37954
|
294 |
Calc ("Atools.pow" ,eval_binop "#power_"),
|
neuper@37954
|
295 |
|
neuper@38045
|
296 |
Calc ("Orderings.ord_class.less",eval_equ "#less_"),
|
neuper@38045
|
297 |
Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
|
neuper@37954
|
298 |
|
neuper@37954
|
299 |
Calc ("Atools.ident",eval_ident "#ident_")],
|
neuper@48763
|
300 |
scr = Prog ((term_of o the o (parse thy)) "empty_script")
|
neuper@37954
|
301 |
}:rls;
|
neuper@38001
|
302 |
*}
|
neuper@38001
|
303 |
ML {*
|
neuper@37954
|
304 |
|
neuper@37967
|
305 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
neuper@37954
|
306 |
[("testerls", prep_rls testerls)
|
neuper@37954
|
307 |
]);
|
neuper@37954
|
308 |
|
neuper@37954
|
309 |
|
neuper@37954
|
310 |
(*make () dissappear*)
|
neuper@37954
|
311 |
val rearrange_assoc =
|
neuper@37954
|
312 |
Rls{id = "rearrange_assoc", preconds = [],
|
neuper@37954
|
313 |
rew_ord = ("e_rew_ord",e_rew_ord),
|
neuper@42451
|
314 |
erls = e_rls, srls = e_rls, calc = [], errpatts = [],
|
neuper@37954
|
315 |
rules =
|
neuper@37974
|
316 |
[Thm ("sym_add_assoc",num_str (@{thm add_assoc} RS @{thm sym})),
|
neuper@37969
|
317 |
Thm ("sym_rmult_assoc",num_str (@{thm rmult_assoc} RS @{thm sym}))],
|
neuper@48763
|
318 |
scr = Prog ((term_of o the o (parse thy)) "empty_script")
|
neuper@37954
|
319 |
}:rls;
|
neuper@37954
|
320 |
|
neuper@37954
|
321 |
val ac_plus_times =
|
neuper@37954
|
322 |
Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
|
neuper@42451
|
323 |
erls = e_rls, srls = e_rls, calc = [], errpatts = [],
|
neuper@37954
|
324 |
rules =
|
neuper@37969
|
325 |
[Thm ("radd_commute",num_str @{thm radd_commute}),
|
neuper@37969
|
326 |
Thm ("radd_left_commute",num_str @{thm radd_left_commute}),
|
neuper@37974
|
327 |
Thm ("add_assoc",num_str @{thm add_assoc}),
|
neuper@37969
|
328 |
Thm ("rmult_commute",num_str @{thm rmult_commute}),
|
neuper@37969
|
329 |
Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
|
neuper@37969
|
330 |
Thm ("rmult_assoc",num_str @{thm rmult_assoc})],
|
neuper@48763
|
331 |
scr = Prog ((term_of o the o (parse thy)) "empty_script")
|
neuper@37954
|
332 |
}:rls;
|
neuper@37954
|
333 |
|
neuper@37969
|
334 |
(*todo: replace by Rewrite("rnorm_equation_add",num_str @{thm rnorm_equation_add)*)
|
neuper@37954
|
335 |
val norm_equation =
|
neuper@37954
|
336 |
Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
|
neuper@42451
|
337 |
erls = tval_rls, srls = e_rls, calc = [], errpatts = [],
|
neuper@38001
|
338 |
rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add})
|
neuper@37954
|
339 |
],
|
neuper@48763
|
340 |
scr = Prog ((term_of o the o (parse thy)) "empty_script")
|
neuper@37954
|
341 |
}:rls;
|
neuper@38001
|
342 |
*}
|
neuper@38001
|
343 |
ML {*
|
neuper@37954
|
344 |
(** rule sets **)
|
neuper@37954
|
345 |
|
neuper@37954
|
346 |
val STest_simplify = (* vv--- not changed to real by parse*)
|
neuper@38001
|
347 |
"Script STest_simplify (t_t::'z) = " ^
|
neuper@37954
|
348 |
"(Repeat" ^
|
neuper@37954
|
349 |
" ((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
|
neuper@37954
|
350 |
" (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@ " ^
|
neuper@37954
|
351 |
" (Try (Repeat (Rewrite rdistr_right_assoc False))) @@ " ^
|
neuper@37954
|
352 |
" (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@" ^
|
neuper@37954
|
353 |
" (Try (Repeat (Rewrite rdistr_div_right False))) @@ " ^
|
neuper@37954
|
354 |
" (Try (Repeat (Rewrite rbinom_power_2 False))) @@ " ^
|
neuper@37954
|
355 |
|
neuper@37954
|
356 |
" (Try (Repeat (Rewrite radd_commute False))) @@ " ^
|
neuper@37954
|
357 |
" (Try (Repeat (Rewrite radd_left_commute False))) @@ " ^
|
neuper@37974
|
358 |
" (Try (Repeat (Rewrite add_assoc False))) @@ " ^
|
neuper@37954
|
359 |
" (Try (Repeat (Rewrite rmult_commute False))) @@ " ^
|
neuper@37954
|
360 |
" (Try (Repeat (Rewrite rmult_left_commute False))) @@ " ^
|
neuper@37954
|
361 |
" (Try (Repeat (Rewrite rmult_assoc False))) @@ " ^
|
neuper@37954
|
362 |
|
neuper@37954
|
363 |
" (Try (Repeat (Rewrite radd_real_const_eq False))) @@ " ^
|
neuper@37954
|
364 |
" (Try (Repeat (Rewrite radd_real_const False))) @@ " ^
|
neuper@37975
|
365 |
" (Try (Repeat (Calculate PLUS))) @@ " ^
|
neuper@37975
|
366 |
" (Try (Repeat (Calculate TIMES))) @@ " ^
|
neuper@37954
|
367 |
" (Try (Repeat (Calculate divide_))) @@" ^
|
neuper@37975
|
368 |
" (Try (Repeat (Calculate POWER))) @@ " ^
|
neuper@37954
|
369 |
|
neuper@37954
|
370 |
" (Try (Repeat (Rewrite rcollect_right False))) @@ " ^
|
neuper@37954
|
371 |
" (Try (Repeat (Rewrite rcollect_one_left False))) @@ " ^
|
neuper@37954
|
372 |
" (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@ " ^
|
neuper@37954
|
373 |
" (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@ " ^
|
neuper@37954
|
374 |
|
neuper@37954
|
375 |
" (Try (Repeat (Rewrite rshift_nominator False))) @@ " ^
|
neuper@37954
|
376 |
" (Try (Repeat (Rewrite rcancel_den False))) @@ " ^
|
neuper@37954
|
377 |
" (Try (Repeat (Rewrite rroot_square_inv False))) @@ " ^
|
neuper@37954
|
378 |
" (Try (Repeat (Rewrite rroot_times_root False))) @@ " ^
|
neuper@37954
|
379 |
" (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@ " ^
|
neuper@37954
|
380 |
" (Try (Repeat (Rewrite rsqare False))) @@ " ^
|
neuper@37954
|
381 |
" (Try (Repeat (Rewrite power_1 False))) @@ " ^
|
neuper@37954
|
382 |
" (Try (Repeat (Rewrite rtwo_of_the_same False))) @@ " ^
|
neuper@37954
|
383 |
" (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@ " ^
|
neuper@37954
|
384 |
|
neuper@37954
|
385 |
" (Try (Repeat (Rewrite rmult_1 False))) @@ " ^
|
neuper@37954
|
386 |
" (Try (Repeat (Rewrite rmult_1_right False))) @@ " ^
|
neuper@37954
|
387 |
" (Try (Repeat (Rewrite rmult_0 False))) @@ " ^
|
neuper@37954
|
388 |
" (Try (Repeat (Rewrite rmult_0_right False))) @@ " ^
|
neuper@37954
|
389 |
" (Try (Repeat (Rewrite radd_0 False))) @@ " ^
|
neuper@37954
|
390 |
" (Try (Repeat (Rewrite radd_0_right False)))) " ^
|
neuper@38001
|
391 |
" t_t)";
|
neuper@37954
|
392 |
|
neuper@38001
|
393 |
*}
|
neuper@38001
|
394 |
ML {*
|
neuper@37954
|
395 |
(* expects * distributed over + *)
|
neuper@37954
|
396 |
val Test_simplify =
|
neuper@37954
|
397 |
Rls{id = "Test_simplify", preconds = [],
|
neuper@40836
|
398 |
rew_ord = ("sqrt_right",sqrt_right false (Thy_Info.get_theory "Pure")),
|
neuper@37954
|
399 |
erls = tval_rls, srls = e_rls,
|
neuper@42451
|
400 |
calc=[(*since 040209 filled by prep_rls*)], errpatts = [],
|
neuper@37954
|
401 |
rules = [
|
neuper@37969
|
402 |
Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
|
neuper@37969
|
403 |
Thm ("radd_mult_distrib2",num_str @{thm radd_mult_distrib2}),
|
neuper@37969
|
404 |
Thm ("rdistr_right_assoc",num_str @{thm rdistr_right_assoc}),
|
neuper@37969
|
405 |
Thm ("rdistr_right_assoc_p",num_str @{thm rdistr_right_assoc_p}),
|
neuper@37969
|
406 |
Thm ("rdistr_div_right",num_str @{thm rdistr_div_right}),
|
neuper@37969
|
407 |
Thm ("rbinom_power_2",num_str @{thm rbinom_power_2}),
|
neuper@37954
|
408 |
|
neuper@37969
|
409 |
Thm ("radd_commute",num_str @{thm radd_commute}),
|
neuper@37969
|
410 |
Thm ("radd_left_commute",num_str @{thm radd_left_commute}),
|
neuper@37974
|
411 |
Thm ("add_assoc",num_str @{thm add_assoc}),
|
neuper@37969
|
412 |
Thm ("rmult_commute",num_str @{thm rmult_commute}),
|
neuper@37969
|
413 |
Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
|
neuper@37969
|
414 |
Thm ("rmult_assoc",num_str @{thm rmult_assoc}),
|
neuper@37954
|
415 |
|
neuper@37969
|
416 |
Thm ("radd_real_const_eq",num_str @{thm radd_real_const_eq}),
|
neuper@37969
|
417 |
Thm ("radd_real_const",num_str @{thm radd_real_const}),
|
neuper@37954
|
418 |
(* these 2 rules are invers to distr_div_right wrt. termination.
|
neuper@37954
|
419 |
thus they MUST be done IMMEDIATELY before calc *)
|
neuper@38014
|
420 |
Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@38034
|
421 |
Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
neuper@48789
|
422 |
Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
|
neuper@37954
|
423 |
Calc ("Atools.pow", eval_binop "#power_"),
|
neuper@37954
|
424 |
|
neuper@37969
|
425 |
Thm ("rcollect_right",num_str @{thm rcollect_right}),
|
neuper@37969
|
426 |
Thm ("rcollect_one_left",num_str @{thm rcollect_one_left}),
|
neuper@37969
|
427 |
Thm ("rcollect_one_left_assoc",num_str @{thm rcollect_one_left_assoc}),
|
neuper@37969
|
428 |
Thm ("rcollect_one_left_assoc_p",num_str @{thm rcollect_one_left_assoc_p}),
|
neuper@37954
|
429 |
|
neuper@37969
|
430 |
Thm ("rshift_nominator",num_str @{thm rshift_nominator}),
|
neuper@37969
|
431 |
Thm ("rcancel_den",num_str @{thm rcancel_den}),
|
neuper@37969
|
432 |
Thm ("rroot_square_inv",num_str @{thm rroot_square_inv}),
|
neuper@37969
|
433 |
Thm ("rroot_times_root",num_str @{thm rroot_times_root}),
|
neuper@37969
|
434 |
Thm ("rroot_times_root_assoc_p",num_str @{thm rroot_times_root_assoc_p}),
|
neuper@37969
|
435 |
Thm ("rsqare",num_str @{thm rsqare}),
|
neuper@38001
|
436 |
Thm ("power_1",num_str @{thm power_1}),
|
neuper@37969
|
437 |
Thm ("rtwo_of_the_same",num_str @{thm rtwo_of_the_same}),
|
neuper@37969
|
438 |
Thm ("rtwo_of_the_same_assoc_p",num_str @{thm rtwo_of_the_same_assoc_p}),
|
neuper@37954
|
439 |
|
neuper@37969
|
440 |
Thm ("rmult_1",num_str @{thm rmult_1}),
|
neuper@37969
|
441 |
Thm ("rmult_1_right",num_str @{thm rmult_1_right}),
|
neuper@37969
|
442 |
Thm ("rmult_0",num_str @{thm rmult_0}),
|
neuper@37969
|
443 |
Thm ("rmult_0_right",num_str @{thm rmult_0_right}),
|
neuper@37969
|
444 |
Thm ("radd_0",num_str @{thm radd_0}),
|
neuper@37969
|
445 |
Thm ("radd_0_right",num_str @{thm radd_0_right})
|
neuper@37954
|
446 |
],
|
neuper@48763
|
447 |
scr = Prog ((term_of o the o (parse thy)) "empty_script")
|
neuper@37954
|
448 |
(*since 040209 filled by prep_rls: STest_simplify*)
|
neuper@37954
|
449 |
}:rls;
|
neuper@38001
|
450 |
*}
|
neuper@38001
|
451 |
ML {*
|
neuper@37954
|
452 |
|
neuper@37954
|
453 |
(** rule sets **)
|
neuper@37954
|
454 |
|
neuper@37954
|
455 |
|
neuper@37954
|
456 |
|
neuper@37954
|
457 |
(*isolate the root in a root-equation*)
|
neuper@37954
|
458 |
val isolate_root =
|
neuper@37954
|
459 |
Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
|
neuper@42451
|
460 |
erls=tval_rls,srls = e_rls, calc=[], errpatts = [],
|
neuper@37969
|
461 |
rules = [Thm ("rroot_to_lhs",num_str @{thm rroot_to_lhs}),
|
neuper@37969
|
462 |
Thm ("rroot_to_lhs_mult",num_str @{thm rroot_to_lhs_mult}),
|
neuper@37969
|
463 |
Thm ("rroot_to_lhs_add_mult",num_str @{thm rroot_to_lhs_add_mult}),
|
neuper@37969
|
464 |
Thm ("risolate_root_add",num_str @{thm risolate_root_add}),
|
neuper@37969
|
465 |
Thm ("risolate_root_mult",num_str @{thm risolate_root_mult}),
|
neuper@37969
|
466 |
Thm ("risolate_root_div",num_str @{thm risolate_root_div}) ],
|
neuper@48763
|
467 |
scr = Prog ((term_of o the o (parse thy))
|
neuper@37954
|
468 |
"empty_script")
|
neuper@37954
|
469 |
}:rls;
|
neuper@37954
|
470 |
|
neuper@37954
|
471 |
(*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
|
neuper@37954
|
472 |
val isolate_bdv =
|
neuper@37954
|
473 |
Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
|
neuper@42451
|
474 |
erls=tval_rls,srls = e_rls, calc= [], errpatts = [],
|
neuper@37954
|
475 |
rules =
|
neuper@37969
|
476 |
[Thm ("risolate_bdv_add",num_str @{thm risolate_bdv_add}),
|
neuper@37969
|
477 |
Thm ("risolate_bdv_mult_add",num_str @{thm risolate_bdv_mult_add}),
|
neuper@37969
|
478 |
Thm ("risolate_bdv_mult",num_str @{thm risolate_bdv_mult}),
|
neuper@38001
|
479 |
Thm ("mult_square",num_str @{thm mult_square}),
|
neuper@38001
|
480 |
Thm ("constant_square",num_str @{thm constant_square}),
|
neuper@38001
|
481 |
Thm ("constant_mult_square",num_str @{thm constant_mult_square})
|
neuper@37954
|
482 |
],
|
neuper@48763
|
483 |
scr = Prog ((term_of o the o (parse thy))
|
neuper@37954
|
484 |
"empty_script")
|
neuper@37954
|
485 |
}:rls;
|
neuper@38001
|
486 |
*}
|
neuper@38001
|
487 |
ML {*
|
neuper@37954
|
488 |
|
neuper@37954
|
489 |
(* association list for calculate_, calculate
|
neuper@38014
|
490 |
"Groups.plus_class.plus" etc. not usable in scripts *)
|
neuper@37954
|
491 |
val calclist =
|
neuper@37954
|
492 |
[
|
neuper@37954
|
493 |
(*as Tools.ML*)
|
neuper@37954
|
494 |
("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
|
neuper@37954
|
495 |
("matches",("Tools.matches",eval_matches "#matches_")),
|
neuper@37954
|
496 |
("lhs" ,("Tools.lhs" ,eval_lhs "")),
|
neuper@37954
|
497 |
(*aus Atools.ML*)
|
neuper@38014
|
498 |
("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
|
neuper@38034
|
499 |
("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
|
neuper@48789
|
500 |
("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
|
neuper@37954
|
501 |
("POWER" ,("Atools.pow" ,eval_binop "#power_")),
|
neuper@37954
|
502 |
("is_const",("Atools.is'_const",eval_const "#is_const_")),
|
neuper@38045
|
503 |
("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
|
neuper@38045
|
504 |
("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")),
|
neuper@37954
|
505 |
("ident" ,("Atools.ident",eval_ident "#ident_")),
|
neuper@37954
|
506 |
(*von hier (ehem.SqRoot*)
|
neuper@37982
|
507 |
("sqrt" ,("NthRoot.sqrt" ,eval_sqrt "#sqrt_")),
|
neuper@37981
|
508 |
("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_e")),
|
neuper@37954
|
509 |
("Test.contains_root",("contains'_root",
|
neuper@37954
|
510 |
eval_contains_root"#contains_root_"))
|
neuper@37954
|
511 |
];
|
neuper@37954
|
512 |
|
neuper@37967
|
513 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
neuper@37954
|
514 |
[("Test_simplify", prep_rls Test_simplify),
|
neuper@37954
|
515 |
("tval_rls", prep_rls tval_rls),
|
neuper@37954
|
516 |
("isolate_root", prep_rls isolate_root),
|
neuper@37954
|
517 |
("isolate_bdv", prep_rls isolate_bdv),
|
neuper@37954
|
518 |
("matches",
|
neuper@37954
|
519 |
prep_rls (append_rls "matches" testerls
|
neuper@37954
|
520 |
[Calc ("Tools.matches",eval_matches "#matches_")]))
|
neuper@37954
|
521 |
]);
|
neuper@37954
|
522 |
|
neuper@38001
|
523 |
*}
|
neuper@38001
|
524 |
ML {*
|
neuper@37954
|
525 |
(** problem types **)
|
neuper@37954
|
526 |
store_pbt
|
neuper@37972
|
527 |
(prep_pbt thy "pbl_test" [] e_pblID
|
neuper@37954
|
528 |
(["test"],
|
neuper@37954
|
529 |
[],
|
neuper@37954
|
530 |
e_rls, NONE, []));
|
neuper@37954
|
531 |
store_pbt
|
neuper@37972
|
532 |
(prep_pbt thy "pbl_test_equ" [] e_pblID
|
neuper@37954
|
533 |
(["equation","test"],
|
neuper@37981
|
534 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@37981
|
535 |
("#Where" ,["matches (?a = ?b) e_e"]),
|
neuper@38012
|
536 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
537 |
],
|
neuper@37954
|
538 |
assoc_rls "matches",
|
neuper@37981
|
539 |
SOME "solve (e_e::bool, v_v)", []));
|
neuper@37954
|
540 |
|
neuper@37954
|
541 |
store_pbt
|
neuper@37972
|
542 |
(prep_pbt thy "pbl_test_uni" [] e_pblID
|
neuper@37954
|
543 |
(["univariate","equation","test"],
|
neuper@37981
|
544 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@37981
|
545 |
("#Where" ,["matches (?a = ?b) e_e"]),
|
neuper@38011
|
546 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
547 |
],
|
neuper@37954
|
548 |
assoc_rls "matches",
|
neuper@37981
|
549 |
SOME "solve (e_e::bool, v_v)", []));
|
neuper@37954
|
550 |
|
neuper@37954
|
551 |
store_pbt
|
neuper@37972
|
552 |
(prep_pbt thy "pbl_test_uni_lin" [] e_pblID
|
neuper@37954
|
553 |
(["linear","univariate","equation","test"],
|
neuper@37981
|
554 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@38001
|
555 |
("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
|
neuper@38001
|
556 |
"(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
|
neuper@38012
|
557 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
558 |
],
|
neuper@37954
|
559 |
assoc_rls "matches",
|
neuper@37981
|
560 |
SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]));
|
neuper@37954
|
561 |
|
neuper@37954
|
562 |
(*25.8.01 ------
|
neuper@37954
|
563 |
store_pbt
|
neuper@37972
|
564 |
(prep_pbt thy
|
neuper@37972
|
565 |
(["thy"],
|
neuper@38001
|
566 |
[("#Given" ,"boolTestGiven g_g"),
|
neuper@37994
|
567 |
("#Find" ,"boolTestFind f_f")
|
neuper@37954
|
568 |
],
|
neuper@37954
|
569 |
[]));
|
neuper@37954
|
570 |
|
neuper@37954
|
571 |
store_pbt
|
neuper@37972
|
572 |
(prep_pbt thy
|
neuper@37972
|
573 |
(["testeq","thy"],
|
neuper@38001
|
574 |
[("#Given" ,"boolTestGiven g_g"),
|
neuper@37994
|
575 |
("#Find" ,"boolTestFind f_f")
|
neuper@37954
|
576 |
],
|
neuper@37954
|
577 |
[]));
|
neuper@37954
|
578 |
|
neuper@37954
|
579 |
|
neuper@40836
|
580 |
val ttt = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "(matches ( v_v = 0) e_e)";
|
neuper@37954
|
581 |
|
neuper@37954
|
582 |
------ 25.8.01*)
|
neuper@37954
|
583 |
|
neuper@38001
|
584 |
*}
|
neuper@38001
|
585 |
ML {*
|
neuper@37954
|
586 |
(** methods **)
|
neuper@37954
|
587 |
store_met
|
neuper@40836
|
588 |
(prep_met (Thy_Info.get_theory "Diff") "met_test" [] e_metID
|
neuper@37954
|
589 |
(["Test"],
|
neuper@37954
|
590 |
[],
|
neuper@37954
|
591 |
{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
|
neuper@42425
|
592 |
crls=Atools_erls, errpats = [], nrls = e_rls}, "empty_script"));
|
neuper@38001
|
593 |
*}
|
neuper@38001
|
594 |
ML {*
|
neuper@37954
|
595 |
store_met
|
neuper@37972
|
596 |
(prep_met thy "met_test_solvelin" [] e_metID
|
neuper@37954
|
597 |
(["Test","solve_linear"]:metID,
|
neuper@37981
|
598 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@37981
|
599 |
("#Where" ,["matches (?a = ?b) e_e"]),
|
neuper@38012
|
600 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
601 |
],
|
neuper@38001
|
602 |
{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
|
neuper@38001
|
603 |
prls = assoc_rls "matches", calc = [], crls = tval_rls,
|
neuper@42425
|
604 |
errpats = [], nrls = Test_simplify},
|
neuper@38001
|
605 |
"Script Solve_linear (e_e::bool) (v_v::real)= " ^
|
neuper@38001
|
606 |
"(let e_e = " ^
|
neuper@38001
|
607 |
" Repeat " ^
|
neuper@38001
|
608 |
" (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ " ^
|
neuper@37981
|
609 |
" (Rewrite_Set Test_simplify False))) e_e" ^
|
neuper@38001
|
610 |
" in [e_e::bool])"
|
neuper@37954
|
611 |
)
|
neuper@37972
|
612 |
(*, prep_met thy (*test for equations*)
|
neuper@37954
|
613 |
(["Test","testeq"]:metID,
|
neuper@38001
|
614 |
[("#Given" ,["boolTestGiven g_g"]),
|
neuper@37994
|
615 |
("#Find" ,["boolTestFind f_f"])
|
neuper@37954
|
616 |
],
|
neuper@37954
|
617 |
{rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
|
neuper@37954
|
618 |
asm_thm=[("square_equation_left","")]},
|
neuper@38001
|
619 |
"Script Testeq (e_q::bool) = " ^
|
neuper@37954
|
620 |
"Repeat " ^
|
neuper@38001
|
621 |
" (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^
|
neuper@37981
|
622 |
" e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^
|
neuper@37981
|
623 |
" e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^
|
neuper@37981
|
624 |
" in e_e) Until (is_root_free e_e)" (*deleted*)
|
neuper@37954
|
625 |
)
|
neuper@37954
|
626 |
, ---------27.4.02*)
|
neuper@37954
|
627 |
);
|
neuper@37954
|
628 |
|
neuper@38001
|
629 |
*}
|
neuper@38001
|
630 |
ML {*
|
neuper@37954
|
631 |
|
neuper@37967
|
632 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
neuper@37954
|
633 |
[("norm_equation", prep_rls norm_equation),
|
neuper@37954
|
634 |
("ac_plus_times", prep_rls ac_plus_times),
|
neuper@37954
|
635 |
("rearrange_assoc", prep_rls rearrange_assoc)
|
neuper@37954
|
636 |
]);
|
neuper@37954
|
637 |
|
neuper@37954
|
638 |
|
neuper@37954
|
639 |
fun bin_o (Const (op_,(Type ("fun",
|
neuper@37954
|
640 |
[Type (s2,[]),Type ("fun",
|
neuper@37954
|
641 |
[Type (s4,tl4),Type (s5,tl5)])])))) =
|
neuper@37954
|
642 |
if (s2=s4)andalso(s4=s5)then[op_]else[]
|
neuper@37954
|
643 |
| bin_o _ = [];
|
neuper@37954
|
644 |
|
neuper@37954
|
645 |
fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)
|
neuper@37954
|
646 |
| bin_op t = bin_o t;
|
neuper@37954
|
647 |
fun is_bin_op t = ((bin_op t)<>[]);
|
neuper@37954
|
648 |
|
neuper@37954
|
649 |
fun bin_op_arg1 ((Const (op_,(Type ("fun",
|
neuper@37954
|
650 |
[Type (s2,[]),Type ("fun",
|
neuper@37954
|
651 |
[Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
|
neuper@37954
|
652 |
arg1;
|
neuper@37954
|
653 |
fun bin_op_arg2 ((Const (op_,(Type ("fun",
|
neuper@37954
|
654 |
[Type (s2,[]),Type ("fun",
|
neuper@37954
|
655 |
[Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
|
neuper@37954
|
656 |
arg2;
|
neuper@37954
|
657 |
|
neuper@37954
|
658 |
|
neuper@37954
|
659 |
exception NO_EQUATION_TERM;
|
neuper@41922
|
660 |
fun is_equation ((Const ("HOL.eq",(Type ("fun",
|
neuper@37954
|
661 |
[Type (_,[]),Type ("fun",
|
neuper@37954
|
662 |
[Type (_,[]),Type ("bool",[])])])))) $ _ $ _)
|
neuper@37954
|
663 |
= true
|
neuper@37954
|
664 |
| is_equation _ = false;
|
neuper@41922
|
665 |
fun equ_lhs ((Const ("HOL.eq",(Type ("fun",
|
neuper@37954
|
666 |
[Type (_,[]),Type ("fun",
|
neuper@37954
|
667 |
[Type (_,[]),Type ("bool",[])])])))) $ l $ r)
|
neuper@37954
|
668 |
= l
|
neuper@37954
|
669 |
| equ_lhs _ = raise NO_EQUATION_TERM;
|
neuper@41922
|
670 |
fun equ_rhs ((Const ("HOL.eq",(Type ("fun",
|
neuper@37954
|
671 |
[Type (_,[]),Type ("fun",
|
neuper@37954
|
672 |
[Type (_,[]),Type ("bool",[])])])))) $ l $ r)
|
neuper@37954
|
673 |
= r
|
neuper@37954
|
674 |
| equ_rhs _ = raise NO_EQUATION_TERM;
|
neuper@37954
|
675 |
|
neuper@37954
|
676 |
|
neuper@37954
|
677 |
fun atom (Const (_,Type (_,[]))) = true
|
neuper@37954
|
678 |
| atom (Free (_,Type (_,[]))) = true
|
neuper@37954
|
679 |
| atom (Var (_,Type (_,[]))) = true
|
neuper@37954
|
680 |
(*| atom (_ (_,"?DUMMY" )) = true ..ML-error *)
|
neuper@37954
|
681 |
| atom((Const ("Bin.integ_of_bin",_)) $ _) = true
|
neuper@37954
|
682 |
| atom _ = false;
|
neuper@37954
|
683 |
|
neuper@37954
|
684 |
fun varids (Const (s,Type (_,[]))) = [strip_thy s]
|
neuper@37954
|
685 |
| varids (Free (s,Type (_,[]))) = if is_no s then []
|
neuper@37954
|
686 |
else [strip_thy s]
|
neuper@37954
|
687 |
| varids (Var((s,_),Type (_,[]))) = [strip_thy s]
|
neuper@37954
|
688 |
(*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
|
neuper@37954
|
689 |
| varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
|
neuper@37954
|
690 |
| varids (Abs(a,T,t)) = union op = [a] (varids t)
|
neuper@37954
|
691 |
| varids (t1 $ t2) = union op = (varids t1) (varids t2)
|
neuper@37954
|
692 |
| varids _ = [];
|
neuper@37954
|
693 |
(*> val t = term_of (hd (parse Diophant.thy "x"));
|
neuper@37954
|
694 |
val t = Free ("x","?DUMMY") : term
|
neuper@37954
|
695 |
> varids t;
|
neuper@37954
|
696 |
val it = [] : string list [] !!! *)
|
neuper@37954
|
697 |
|
neuper@37954
|
698 |
|
neuper@37954
|
699 |
fun bin_ops_only ((Const op_) $ t1 $ t2) =
|
neuper@37954
|
700 |
if(is_bin_op (Const op_))
|
neuper@37954
|
701 |
then(bin_ops_only t1)andalso(bin_ops_only t2)
|
neuper@37954
|
702 |
else false
|
neuper@37954
|
703 |
| bin_ops_only t =
|
neuper@37954
|
704 |
if atom t then true else bin_ops_only t;
|
neuper@37954
|
705 |
|
neuper@37954
|
706 |
fun polynomial opl t bdVar = (* bdVar TODO *)
|
neuper@37954
|
707 |
subset op = (bin_op t, opl) andalso (bin_ops_only t);
|
neuper@37954
|
708 |
|
neuper@37954
|
709 |
fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)
|
neuper@37954
|
710 |
andalso polynomial opl (equ_lhs t) bdVar
|
neuper@37954
|
711 |
andalso polynomial opl (equ_rhs t) bdVar
|
neuper@37954
|
712 |
andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
|
neuper@37954
|
713 |
subset op = (varids bdVar, varids (equ_lhs t)));
|
neuper@37954
|
714 |
|
neuper@37954
|
715 |
(*fun max is =
|
neuper@37954
|
716 |
let fun max_ m [] = m
|
neuper@37954
|
717 |
| max_ m (i::is) = if m<i then max_ i is else max_ m is;
|
neuper@37954
|
718 |
in max_ (hd is) is end;
|
neuper@37954
|
719 |
> max [1,5,3,7,4,2];
|
neuper@37954
|
720 |
val it = 7 : int *)
|
neuper@37954
|
721 |
|
neuper@37954
|
722 |
fun max (a,b) = if a < b then b else a;
|
neuper@37954
|
723 |
|
neuper@37954
|
724 |
fun degree addl mul bdVar t =
|
neuper@37954
|
725 |
let
|
neuper@37954
|
726 |
fun deg _ _ v (Const (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
|
neuper@37954
|
727 |
| deg _ _ v (Free (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
|
neuper@37954
|
728 |
| deg _ _ v (Var((s,_),Type (_,[]))) = if v=strip_thy s then 1 else 0
|
neuper@37954
|
729 |
(*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
|
neuper@37954
|
730 |
| deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0
|
neuper@37954
|
731 |
| deg addl mul v (h $ t1 $ t2) =
|
neuper@37954
|
732 |
if subset op = (bin_op h, addl)
|
neuper@37954
|
733 |
then max (deg addl mul v t1 ,deg addl mul v t2)
|
neuper@37954
|
734 |
else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)
|
neuper@37954
|
735 |
in if polynomial (addl @ [mul]) t bdVar
|
neuper@37954
|
736 |
then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option)
|
neuper@37954
|
737 |
end;
|
neuper@37954
|
738 |
fun degree_ addl mul bdVar t = (* do not export *)
|
neuper@37954
|
739 |
let fun opt (SOME i)= i
|
neuper@37954
|
740 |
| opt NONE = 0
|
neuper@37954
|
741 |
in opt (degree addl mul bdVar t) end;
|
neuper@37954
|
742 |
|
neuper@37954
|
743 |
|
neuper@37954
|
744 |
fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2;
|
neuper@37954
|
745 |
|
neuper@37954
|
746 |
fun linear_equ addl mul bdVar t =
|
neuper@37954
|
747 |
if is_equation t
|
neuper@37954
|
748 |
then let val degl = degree_ addl mul bdVar (equ_lhs t);
|
neuper@37954
|
749 |
val degr = degree_ addl mul bdVar (equ_rhs t)
|
neuper@37954
|
750 |
in if (degl>0 orelse degr>0)andalso max(degl,degr)<2
|
neuper@37954
|
751 |
then true else false
|
neuper@37954
|
752 |
end
|
neuper@37954
|
753 |
else false;
|
neuper@37954
|
754 |
(* strip_thy op_ before *)
|
neuper@37954
|
755 |
fun is_div_op (dv,(Const (op_,(Type ("fun",
|
neuper@37954
|
756 |
[Type (s2,[]),Type ("fun",
|
neuper@37954
|
757 |
[Type (s4,tl4),Type (s5,tl5)])])))) )= (dv = strip_thy op_)
|
neuper@37954
|
758 |
| is_div_op _ = false;
|
neuper@37954
|
759 |
|
neuper@37954
|
760 |
fun is_denom bdVar div_op t =
|
neuper@37954
|
761 |
let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
|
neuper@37954
|
762 |
| is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
|
neuper@37954
|
763 |
| is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
|
neuper@37954
|
764 |
| is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
|
neuper@37954
|
765 |
| is bool[v]dv (h$n$d) =
|
neuper@37954
|
766 |
if is_div_op(dv,h)
|
neuper@37954
|
767 |
then (is false[v]dv n)orelse(is true[v]dv d)
|
neuper@37954
|
768 |
else (is bool [v]dv n)orelse(is bool[v]dv d)
|
neuper@37954
|
769 |
in is false (varids bdVar) (strip_thy div_op) t end;
|
neuper@37954
|
770 |
|
neuper@37954
|
771 |
|
neuper@37954
|
772 |
fun rational t div_op bdVar =
|
neuper@37954
|
773 |
is_denom bdVar div_op t andalso bin_ops_only t;
|
neuper@37954
|
774 |
|
neuper@38001
|
775 |
*}
|
neuper@38001
|
776 |
ML {*
|
neuper@37954
|
777 |
|
neuper@37954
|
778 |
(** problem types **)
|
neuper@37954
|
779 |
|
neuper@37954
|
780 |
store_pbt
|
neuper@37972
|
781 |
(prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
|
neuper@37954
|
782 |
(["plain_square","univariate","equation","test"],
|
neuper@37981
|
783 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@38001
|
784 |
("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
|
neuper@38001
|
785 |
"(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
|
neuper@37981
|
786 |
"(matches (?a + v_v ^^^2 = 0) e_e) |" ^
|
neuper@37981
|
787 |
"(matches ( v_v ^^^2 = 0) e_e)"]),
|
neuper@38012
|
788 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
789 |
],
|
neuper@37954
|
790 |
assoc_rls "matches",
|
neuper@37981
|
791 |
SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
|
neuper@37954
|
792 |
(*
|
neuper@38001
|
793 |
val e_e = (term_of o the o (parse thy)) "e_e::bool";
|
neuper@37954
|
794 |
val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
|
neuper@37954
|
795 |
val env = [(e_,ve)];
|
neuper@37954
|
796 |
|
neuper@37954
|
797 |
val pre = (term_of o the o (parse thy))
|
neuper@38001
|
798 |
"(matches (a + b*v_v ^^^2 = 0, e_e::bool)) |" ^
|
neuper@38001
|
799 |
"(matches ( b*v_v ^^^2 = 0, e_e::bool)) |" ^
|
neuper@37981
|
800 |
"(matches (a + v_v ^^^2 = 0, e_e::bool)) |" ^
|
neuper@37981
|
801 |
"(matches ( v_v ^^^2 = 0, e_e::bool))";
|
neuper@37954
|
802 |
val prei = subst_atomic env pre;
|
neuper@37954
|
803 |
val cpre = (cterm_of thy) prei;
|
neuper@37954
|
804 |
|
neuper@37954
|
805 |
val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;
|
neuper@37954
|
806 |
val ct = "True | False | False | False" : cterm
|
neuper@37954
|
807 |
|
neuper@37954
|
808 |
> val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
|
neuper@37954
|
809 |
> val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
|
neuper@37954
|
810 |
> val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
|
neuper@41928
|
811 |
val ct = "HOL.True" : cterm
|
neuper@37954
|
812 |
|
neuper@37954
|
813 |
*)
|
neuper@37954
|
814 |
|
neuper@38001
|
815 |
*}
|
neuper@38001
|
816 |
ML {*
|
neuper@37954
|
817 |
store_pbt
|
neuper@37972
|
818 |
(prep_pbt thy "pbl_test_uni_poly" [] e_pblID
|
neuper@37954
|
819 |
(["polynomial","univariate","equation","test"],
|
neuper@38001
|
820 |
[("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
|
neuper@41928
|
821 |
("#Where" ,["HOL.False"]),
|
neuper@38012
|
822 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
823 |
],
|
neuper@37981
|
824 |
e_rls, SOME "solve (e_e::bool, v_v)", []));
|
neuper@37954
|
825 |
|
neuper@37954
|
826 |
store_pbt
|
neuper@37972
|
827 |
(prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
|
neuper@37954
|
828 |
(["degree_two","polynomial","univariate","equation","test"],
|
neuper@38001
|
829 |
[("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
|
neuper@38012
|
830 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
831 |
],
|
neuper@38001
|
832 |
e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
|
neuper@37954
|
833 |
|
neuper@37954
|
834 |
store_pbt
|
neuper@37972
|
835 |
(prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
|
neuper@37954
|
836 |
(["pq_formula","degree_two","polynomial","univariate","equation","test"],
|
neuper@38001
|
837 |
[("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
|
neuper@38012
|
838 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
839 |
],
|
neuper@38001
|
840 |
e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
|
neuper@37954
|
841 |
|
neuper@37954
|
842 |
store_pbt
|
neuper@37972
|
843 |
(prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
|
neuper@37954
|
844 |
(["abc_formula","degree_two","polynomial","univariate","equation","test"],
|
neuper@38001
|
845 |
[("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
|
neuper@38012
|
846 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
847 |
],
|
neuper@38001
|
848 |
e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
|
neuper@37954
|
849 |
|
neuper@38001
|
850 |
*}
|
neuper@38001
|
851 |
ML {*
|
neuper@37954
|
852 |
store_pbt
|
neuper@37972
|
853 |
(prep_pbt thy "pbl_test_uni_root" [] e_pblID
|
neuper@37954
|
854 |
(["squareroot","univariate","equation","test"],
|
neuper@37981
|
855 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@42008
|
856 |
("#Where" ,["precond_rootpbl v_v"]),
|
neuper@38012
|
857 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
858 |
],
|
neuper@37954
|
859 |
append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
|
neuper@37954
|
860 |
eval_contains_root "#contains_root_")],
|
neuper@37981
|
861 |
SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]]));
|
neuper@37954
|
862 |
|
neuper@37954
|
863 |
store_pbt
|
neuper@37972
|
864 |
(prep_pbt thy "pbl_test_uni_norm" [] e_pblID
|
neuper@37954
|
865 |
(["normalize","univariate","equation","test"],
|
neuper@37981
|
866 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@37954
|
867 |
("#Where" ,[]),
|
neuper@38012
|
868 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
869 |
],
|
neuper@37981
|
870 |
e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]]));
|
neuper@37954
|
871 |
|
neuper@37954
|
872 |
store_pbt
|
neuper@37972
|
873 |
(prep_pbt thy "pbl_test_uni_roottest" [] e_pblID
|
neuper@37954
|
874 |
(["sqroot-test","univariate","equation","test"],
|
neuper@37981
|
875 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@42008
|
876 |
("#Where" ,["precond_rootpbl v_v"]),
|
neuper@38012
|
877 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
878 |
],
|
neuper@37981
|
879 |
e_rls, SOME "solve (e_e::bool, v_v)", []));
|
neuper@37954
|
880 |
|
neuper@41934
|
881 |
store_pbt
|
neuper@41934
|
882 |
(prep_pbt thy "pbl_test_intsimp" [] e_pblID
|
neuper@41934
|
883 |
(["inttype","test"],
|
neuper@41934
|
884 |
[("#Given" ,["intTestGiven t_t"]),
|
neuper@41934
|
885 |
("#Where" ,[]),
|
neuper@41934
|
886 |
("#Find" ,["intTestFind s_s"])
|
neuper@41934
|
887 |
],
|
neuper@41935
|
888 |
e_rls, NONE, [["Test","intsimp"]]));
|
neuper@41934
|
889 |
(*
|
neuper@41934
|
890 |
show_ptyps();
|
neuper@41934
|
891 |
get_pbt ["inttype","test"];
|
neuper@41934
|
892 |
*)
|
neuper@41934
|
893 |
|
neuper@38001
|
894 |
*}
|
neuper@41934
|
895 |
|
neuper@38001
|
896 |
ML {*
|
neuper@37954
|
897 |
store_met
|
neuper@37972
|
898 |
(prep_met thy "met_test_sqrt" [] e_metID
|
neuper@37954
|
899 |
(*root-equation, version for tests before 8.01.01*)
|
neuper@37954
|
900 |
(["Test","sqrt-equ-test"]:metID,
|
neuper@37981
|
901 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@37981
|
902 |
("#Where" ,["contains_root (e_e::bool)"]),
|
neuper@38012
|
903 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
904 |
],
|
neuper@37954
|
905 |
{rew_ord'="e_rew_ord",rls'=tval_rls,
|
neuper@37954
|
906 |
srls =append_rls "srls_contains_root" e_rls
|
neuper@37954
|
907 |
[Calc ("Test.contains'_root",eval_contains_root "")],
|
neuper@37954
|
908 |
prls =append_rls "prls_contains_root" e_rls
|
neuper@37954
|
909 |
[Calc ("Test.contains'_root",eval_contains_root "")],
|
neuper@37954
|
910 |
calc=[],
|
neuper@42425
|
911 |
crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
|
neuper@37954
|
912 |
asm_thm=[("square_equation_left",""),
|
neuper@37954
|
913 |
("square_equation_right","")]*)},
|
neuper@37982
|
914 |
"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
|
neuper@37981
|
915 |
"(let e_e = " ^
|
neuper@37981
|
916 |
" ((While (contains_root e_e) Do" ^
|
neuper@37954
|
917 |
" ((Rewrite square_equation_left True) @@" ^
|
neuper@37954
|
918 |
" (Try (Rewrite_Set Test_simplify False)) @@" ^
|
neuper@37954
|
919 |
" (Try (Rewrite_Set rearrange_assoc False)) @@" ^
|
neuper@37954
|
920 |
" (Try (Rewrite_Set isolate_root False)) @@" ^
|
neuper@37954
|
921 |
" (Try (Rewrite_Set Test_simplify False)))) @@" ^
|
neuper@37954
|
922 |
" (Try (Rewrite_Set norm_equation False)) @@" ^
|
neuper@37954
|
923 |
" (Try (Rewrite_Set Test_simplify False)) @@" ^
|
neuper@37991
|
924 |
" (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
|
neuper@37954
|
925 |
" (Try (Rewrite_Set Test_simplify False)))" ^
|
neuper@37981
|
926 |
" e_e" ^
|
neuper@38001
|
927 |
" in [e_e::bool])"
|
neuper@37954
|
928 |
));
|
neuper@37954
|
929 |
|
neuper@38001
|
930 |
*}
|
neuper@38001
|
931 |
ML {*
|
neuper@37954
|
932 |
store_met
|
neuper@37972
|
933 |
(prep_met thy "met_test_sqrt2" [] e_metID
|
neuper@37954
|
934 |
(*root-equation ... for test-*.sml until 8.01*)
|
neuper@37954
|
935 |
(["Test","squ-equ-test2"]:metID,
|
neuper@37981
|
936 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@38012
|
937 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
938 |
],
|
neuper@37954
|
939 |
{rew_ord'="e_rew_ord",rls'=tval_rls,
|
neuper@37954
|
940 |
srls = append_rls "srls_contains_root" e_rls
|
neuper@37954
|
941 |
[Calc ("Test.contains'_root",eval_contains_root"")],
|
neuper@37954
|
942 |
prls=e_rls,calc=[],
|
neuper@42425
|
943 |
crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
|
neuper@37954
|
944 |
asm_thm=[("square_equation_left",""),
|
neuper@37954
|
945 |
("square_equation_right","")]*)},
|
neuper@37982
|
946 |
"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
|
neuper@37981
|
947 |
"(let e_e = " ^
|
neuper@37981
|
948 |
" ((While (contains_root e_e) Do" ^
|
neuper@37954
|
949 |
" ((Rewrite square_equation_left True) @@" ^
|
neuper@37954
|
950 |
" (Try (Rewrite_Set Test_simplify False)) @@" ^
|
neuper@37954
|
951 |
" (Try (Rewrite_Set rearrange_assoc False)) @@" ^
|
neuper@37954
|
952 |
" (Try (Rewrite_Set isolate_root False)) @@" ^
|
neuper@37954
|
953 |
" (Try (Rewrite_Set Test_simplify False)))) @@" ^
|
neuper@37954
|
954 |
" (Try (Rewrite_Set norm_equation False)) @@" ^
|
neuper@37954
|
955 |
" (Try (Rewrite_Set Test_simplify False)) @@" ^
|
neuper@37991
|
956 |
" (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
|
neuper@37954
|
957 |
" (Try (Rewrite_Set Test_simplify False)))" ^
|
neuper@37991
|
958 |
" e_e;" ^
|
neuper@38001
|
959 |
" (L_L::bool list) = Tac subproblem_equation_dummy; " ^
|
neuper@37991
|
960 |
" L_L = Tac solve_equation_dummy " ^
|
neuper@37991
|
961 |
" in Check_elementwise L_L {(v_v::real). Assumptions})"
|
neuper@37954
|
962 |
));
|
neuper@37954
|
963 |
|
neuper@38001
|
964 |
*}
|
neuper@38001
|
965 |
ML {*
|
neuper@37954
|
966 |
store_met
|
neuper@37972
|
967 |
(prep_met thy "met_test_squ_sub" [] e_metID
|
neuper@37954
|
968 |
(*tests subproblem fixed linear*)
|
neuper@37954
|
969 |
(["Test","squ-equ-test-subpbl1"]:metID,
|
neuper@37981
|
970 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@42008
|
971 |
("#Where" ,["precond_rootmet v_v"]),
|
neuper@38012
|
972 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
973 |
],
|
neuper@42008
|
974 |
{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
|
neuper@42008
|
975 |
prls = append_rls "prls_met_test_squ_sub" e_rls
|
neuper@42010
|
976 |
[Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
|
neuper@42425
|
977 |
calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
|
neuper@42025
|
978 |
"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
|
neuper@42025
|
979 |
" (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
|
neuper@42025
|
980 |
" (Try (Rewrite_Set Test_simplify False))) e_e; " ^
|
neuper@42025
|
981 |
" (L_L::bool list) = " ^
|
neuper@42025
|
982 |
" (SubProblem (Test', " ^
|
neuper@42025
|
983 |
" [linear,univariate,equation,test]," ^
|
neuper@42025
|
984 |
" [Test,solve_linear]) " ^
|
neuper@42025
|
985 |
" [BOOL e_e, REAL v_v]) " ^
|
neuper@42025
|
986 |
" in Check_elementwise L_L {(v_v::real). Assumptions}) "
|
neuper@37954
|
987 |
));
|
neuper@37954
|
988 |
|
neuper@38001
|
989 |
*}
|
neuper@38001
|
990 |
ML {*
|
neuper@37954
|
991 |
store_met
|
neuper@37972
|
992 |
(prep_met thy "met_test_squ_sub2" [] e_metID
|
neuper@37954
|
993 |
(*tests subproblem fixed degree 2*)
|
neuper@37954
|
994 |
(["Test","squ-equ-test-subpbl2"]:metID,
|
neuper@37981
|
995 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@38012
|
996 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
997 |
],
|
neuper@37954
|
998 |
{rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
|
neuper@42425
|
999 |
crls=tval_rls, errpats = [], nrls = e_rls(*,
|
neuper@37954
|
1000 |
asm_rls=[],asm_thm=[("square_equation_left",""),
|
neuper@37954
|
1001 |
("square_equation_right","")]*)},
|
neuper@37982
|
1002 |
"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
|
neuper@37991
|
1003 |
" (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
|
neuper@38001
|
1004 |
"(L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^
|
neuper@38001
|
1005 |
" [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^
|
neuper@37991
|
1006 |
"in Check_elementwise L_L {(v_v::real). Assumptions})"
|
neuper@37954
|
1007 |
));
|
neuper@37954
|
1008 |
|
neuper@38001
|
1009 |
*}
|
neuper@38001
|
1010 |
ML {*
|
neuper@37954
|
1011 |
store_met
|
neuper@37972
|
1012 |
(prep_met thy "met_test_squ_nonterm" [] e_metID
|
neuper@37954
|
1013 |
(*root-equation: see foils..., but notTerminating*)
|
neuper@37954
|
1014 |
(["Test","square_equation...notTerminating"]:metID,
|
neuper@37981
|
1015 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@38012
|
1016 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
1017 |
],
|
neuper@37954
|
1018 |
{rew_ord'="e_rew_ord",rls'=tval_rls,
|
neuper@37954
|
1019 |
srls = append_rls "srls_contains_root" e_rls
|
neuper@37954
|
1020 |
[Calc ("Test.contains'_root",eval_contains_root"")],
|
neuper@37954
|
1021 |
prls=e_rls,calc=[],
|
neuper@42425
|
1022 |
crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
|
neuper@37954
|
1023 |
asm_thm=[("square_equation_left",""),
|
neuper@37954
|
1024 |
("square_equation_right","")]*)},
|
neuper@37982
|
1025 |
"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
|
neuper@37981
|
1026 |
"(let e_e = " ^
|
neuper@37981
|
1027 |
" ((While (contains_root e_e) Do" ^
|
neuper@37954
|
1028 |
" ((Rewrite square_equation_left True) @@" ^
|
neuper@37954
|
1029 |
" (Try (Rewrite_Set Test_simplify False)) @@" ^
|
neuper@37954
|
1030 |
" (Try (Rewrite_Set rearrange_assoc False)) @@" ^
|
neuper@37954
|
1031 |
" (Try (Rewrite_Set isolate_root False)) @@" ^
|
neuper@37954
|
1032 |
" (Try (Rewrite_Set Test_simplify False)))) @@" ^
|
neuper@37954
|
1033 |
" (Try (Rewrite_Set norm_equation False)) @@" ^
|
neuper@37954
|
1034 |
" (Try (Rewrite_Set Test_simplify False)))" ^
|
neuper@37991
|
1035 |
" e_e;" ^
|
neuper@38001
|
1036 |
" (L_L::bool list) = " ^
|
neuper@38001
|
1037 |
" (SubProblem (Test',[linear,univariate,equation,test]," ^
|
neuper@38001
|
1038 |
" [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
|
neuper@37991
|
1039 |
"in Check_elementwise L_L {(v_v::real). Assumptions})"
|
neuper@37954
|
1040 |
));
|
neuper@37954
|
1041 |
|
neuper@38001
|
1042 |
*}
|
neuper@38001
|
1043 |
ML {*
|
neuper@37954
|
1044 |
store_met
|
neuper@37972
|
1045 |
(prep_met thy "met_test_eq1" [] e_metID
|
neuper@37954
|
1046 |
(*root-equation1:*)
|
neuper@37954
|
1047 |
(["Test","square_equation1"]:metID,
|
neuper@37981
|
1048 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@38012
|
1049 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
1050 |
],
|
neuper@37954
|
1051 |
{rew_ord'="e_rew_ord",rls'=tval_rls,
|
neuper@37954
|
1052 |
srls = append_rls "srls_contains_root" e_rls
|
neuper@37954
|
1053 |
[Calc ("Test.contains'_root",eval_contains_root"")],
|
neuper@37954
|
1054 |
prls=e_rls,calc=[],
|
neuper@42425
|
1055 |
crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
|
neuper@37954
|
1056 |
asm_thm=[("square_equation_left",""),
|
neuper@37954
|
1057 |
("square_equation_right","")]*)},
|
neuper@37982
|
1058 |
"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
|
neuper@37981
|
1059 |
"(let e_e = " ^
|
neuper@37981
|
1060 |
" ((While (contains_root e_e) Do" ^
|
neuper@37954
|
1061 |
" ((Rewrite square_equation_left True) @@" ^
|
neuper@37954
|
1062 |
" (Try (Rewrite_Set Test_simplify False)) @@" ^
|
neuper@37954
|
1063 |
" (Try (Rewrite_Set rearrange_assoc False)) @@" ^
|
neuper@37954
|
1064 |
" (Try (Rewrite_Set isolate_root False)) @@" ^
|
neuper@37954
|
1065 |
" (Try (Rewrite_Set Test_simplify False)))) @@" ^
|
neuper@37954
|
1066 |
" (Try (Rewrite_Set norm_equation False)) @@" ^
|
neuper@37954
|
1067 |
" (Try (Rewrite_Set Test_simplify False)))" ^
|
neuper@37991
|
1068 |
" e_e;" ^
|
neuper@38001
|
1069 |
" (L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^
|
neuper@38001
|
1070 |
" [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
|
neuper@37991
|
1071 |
" in Check_elementwise L_L {(v_v::real). Assumptions})"
|
neuper@37954
|
1072 |
));
|
neuper@37954
|
1073 |
|
neuper@38001
|
1074 |
*}
|
neuper@38001
|
1075 |
ML {*
|
neuper@37954
|
1076 |
store_met
|
neuper@37972
|
1077 |
(prep_met thy "met_test_squ2" [] e_metID
|
neuper@37954
|
1078 |
(*root-equation2*)
|
neuper@37954
|
1079 |
(["Test","square_equation2"]:metID,
|
neuper@37981
|
1080 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@38012
|
1081 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
1082 |
],
|
neuper@37954
|
1083 |
{rew_ord'="e_rew_ord",rls'=tval_rls,
|
neuper@37954
|
1084 |
srls = append_rls "srls_contains_root" e_rls
|
neuper@37954
|
1085 |
[Calc ("Test.contains'_root",eval_contains_root"")],
|
neuper@37954
|
1086 |
prls=e_rls,calc=[],
|
neuper@42425
|
1087 |
crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
|
neuper@37954
|
1088 |
asm_thm=[("square_equation_left",""),
|
neuper@37954
|
1089 |
("square_equation_right","")]*)},
|
neuper@37982
|
1090 |
"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
|
neuper@37981
|
1091 |
"(let e_e = " ^
|
neuper@37981
|
1092 |
" ((While (contains_root e_e) Do" ^
|
neuper@37954
|
1093 |
" (((Rewrite square_equation_left True) Or " ^
|
neuper@37954
|
1094 |
" (Rewrite square_equation_right True)) @@" ^
|
neuper@37954
|
1095 |
" (Try (Rewrite_Set Test_simplify False)) @@" ^
|
neuper@37954
|
1096 |
" (Try (Rewrite_Set rearrange_assoc False)) @@" ^
|
neuper@37954
|
1097 |
" (Try (Rewrite_Set isolate_root False)) @@" ^
|
neuper@37954
|
1098 |
" (Try (Rewrite_Set Test_simplify False)))) @@" ^
|
neuper@37954
|
1099 |
" (Try (Rewrite_Set norm_equation False)) @@" ^
|
neuper@37954
|
1100 |
" (Try (Rewrite_Set Test_simplify False)))" ^
|
neuper@37991
|
1101 |
" e_e;" ^
|
neuper@38001
|
1102 |
" (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
|
neuper@38001
|
1103 |
" [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
|
neuper@37991
|
1104 |
" in Check_elementwise L_L {(v_v::real). Assumptions})"
|
neuper@37954
|
1105 |
));
|
neuper@37954
|
1106 |
|
neuper@38001
|
1107 |
*}
|
neuper@38001
|
1108 |
ML {*
|
neuper@37954
|
1109 |
store_met
|
neuper@37972
|
1110 |
(prep_met thy "met_test_squeq" [] e_metID
|
neuper@37954
|
1111 |
(*root-equation*)
|
neuper@37954
|
1112 |
(["Test","square_equation"]:metID,
|
neuper@37981
|
1113 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@38012
|
1114 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
1115 |
],
|
neuper@37954
|
1116 |
{rew_ord'="e_rew_ord",rls'=tval_rls,
|
neuper@37954
|
1117 |
srls = append_rls "srls_contains_root" e_rls
|
neuper@37954
|
1118 |
[Calc ("Test.contains'_root",eval_contains_root"")],
|
neuper@37954
|
1119 |
prls=e_rls,calc=[],
|
neuper@42425
|
1120 |
crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
|
neuper@37954
|
1121 |
asm_thm=[("square_equation_left",""),
|
neuper@37954
|
1122 |
("square_equation_right","")]*)},
|
neuper@37982
|
1123 |
"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
|
neuper@37981
|
1124 |
"(let e_e = " ^
|
neuper@37981
|
1125 |
" ((While (contains_root e_e) Do" ^
|
neuper@37954
|
1126 |
" (((Rewrite square_equation_left True) Or" ^
|
neuper@37954
|
1127 |
" (Rewrite square_equation_right True)) @@" ^
|
neuper@37954
|
1128 |
" (Try (Rewrite_Set Test_simplify False)) @@" ^
|
neuper@37954
|
1129 |
" (Try (Rewrite_Set rearrange_assoc False)) @@" ^
|
neuper@37954
|
1130 |
" (Try (Rewrite_Set isolate_root False)) @@" ^
|
neuper@37954
|
1131 |
" (Try (Rewrite_Set Test_simplify False)))) @@" ^
|
neuper@37954
|
1132 |
" (Try (Rewrite_Set norm_equation False)) @@" ^
|
neuper@37954
|
1133 |
" (Try (Rewrite_Set Test_simplify False)))" ^
|
neuper@37991
|
1134 |
" e_e;" ^
|
neuper@38001
|
1135 |
" (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
|
neuper@38001
|
1136 |
" [no_met]) [BOOL e_e, REAL v_v])" ^
|
neuper@37991
|
1137 |
" in Check_elementwise L_L {(v_v::real). Assumptions})"
|
neuper@37954
|
1138 |
) ); (*#######*)
|
neuper@37954
|
1139 |
|
neuper@38001
|
1140 |
*}
|
neuper@38001
|
1141 |
ML {*
|
neuper@37954
|
1142 |
store_met
|
neuper@37972
|
1143 |
(prep_met thy "met_test_eq_plain" [] e_metID
|
neuper@37954
|
1144 |
(*solve_plain_square*)
|
neuper@37954
|
1145 |
(["Test","solve_plain_square"]:metID,
|
neuper@37981
|
1146 |
[("#Given",["equality e_e","solveFor v_v"]),
|
neuper@38001
|
1147 |
("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
|
neuper@38001
|
1148 |
"(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
|
neuper@37981
|
1149 |
"(matches (?a + v_v ^^^2 = 0) e_e) |" ^
|
neuper@37981
|
1150 |
"(matches ( v_v ^^^2 = 0) e_e)"]),
|
neuper@38012
|
1151 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
1152 |
],
|
neuper@37954
|
1153 |
{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
|
neuper@37954
|
1154 |
prls = assoc_rls "matches",
|
neuper@42425
|
1155 |
crls=tval_rls, errpats = [], nrls = e_rls(*,
|
neuper@37954
|
1156 |
asm_rls=[],asm_thm=[]*)},
|
neuper@37982
|
1157 |
"Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
|
neuper@37981
|
1158 |
" (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^
|
neuper@37954
|
1159 |
" (Try (Rewrite_Set Test_simplify False)) @@ " ^
|
neuper@37954
|
1160 |
" ((Rewrite square_equality_0 False) Or " ^
|
neuper@37954
|
1161 |
" (Rewrite square_equality True)) @@ " ^
|
neuper@37981
|
1162 |
" (Try (Rewrite_Set tval_rls False))) e_e " ^
|
neuper@37981
|
1163 |
" in ((Or_to_List e_e)::bool list))"
|
neuper@37954
|
1164 |
));
|
neuper@37954
|
1165 |
|
neuper@38001
|
1166 |
*}
|
neuper@41935
|
1167 |
|
neuper@38001
|
1168 |
ML {*
|
neuper@37954
|
1169 |
store_met
|
neuper@37972
|
1170 |
(prep_met thy "met_test_norm_univ" [] e_metID
|
neuper@37954
|
1171 |
(["Test","norm_univar_equation"]:metID,
|
neuper@37981
|
1172 |
[("#Given",["equality e_e","solveFor v_v"]),
|
neuper@37954
|
1173 |
("#Where" ,[]),
|
neuper@38012
|
1174 |
("#Find" ,["solutions v_v'i'"])
|
neuper@37954
|
1175 |
],
|
neuper@37954
|
1176 |
{rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
|
neuper@37954
|
1177 |
calc=[],
|
neuper@42425
|
1178 |
crls=tval_rls, errpats = [], nrls = e_rls},
|
neuper@37982
|
1179 |
"Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
|
neuper@37981
|
1180 |
" (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
|
neuper@37981
|
1181 |
" (Try (Rewrite_Set Test_simplify False))) e_e " ^
|
neuper@38001
|
1182 |
" in (SubProblem (Test',[univariate,equation,test], " ^
|
neuper@38001
|
1183 |
" [no_met]) [BOOL e_e, REAL v_v]))"
|
neuper@37954
|
1184 |
));
|
neuper@37954
|
1185 |
|
neuper@41934
|
1186 |
(*17.9.02 aus SqRoot.ML------------------------------^^^---*)
|
neuper@37954
|
1187 |
|
neuper@41934
|
1188 |
store_met
|
neuper@41934
|
1189 |
(prep_met thy "met_test_intsimp" [] e_metID
|
neuper@41934
|
1190 |
(["Test","intsimp"]:metID,
|
neuper@41934
|
1191 |
[("#Given" ,["intTestGiven t_t"]),
|
neuper@41934
|
1192 |
("#Where" ,[]),
|
neuper@41934
|
1193 |
("#Find" ,["intTestFind s_s"])
|
neuper@41934
|
1194 |
],
|
neuper@41934
|
1195 |
{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
|
neuper@42425
|
1196 |
prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},
|
neuper@41934
|
1197 |
"Script STest_simplify (t_t::int) = " ^
|
neuper@41934
|
1198 |
"(Repeat " ^
|
neuper@41934
|
1199 |
" ((Try (Calculate PLUS)) @@ " ^
|
neuper@41935
|
1200 |
" (Try (Calculate TIMES))) t_t::int)"
|
neuper@41934
|
1201 |
));
|
neuper@37954
|
1202 |
|
neuper@38001
|
1203 |
*}
|
neuper@41934
|
1204 |
|
neuper@38001
|
1205 |
ML {*
|
neuper@37954
|
1206 |
(*8.4.03 aus Poly.ML--------------------------------vvv---
|
neuper@37954
|
1207 |
make_polynomial ---> make_poly
|
neuper@37954
|
1208 |
^-- for user ^-- for systest _ONLY_*)
|
neuper@37954
|
1209 |
|
neuper@37954
|
1210 |
local (*. for make_polytest .*)
|
neuper@37954
|
1211 |
|
neuper@37954
|
1212 |
open Term; (* for type order = EQUAL | LESS | GREATER *)
|
neuper@37954
|
1213 |
|
neuper@37954
|
1214 |
fun pr_ord EQUAL = "EQUAL"
|
neuper@37954
|
1215 |
| pr_ord LESS = "LESS"
|
neuper@37954
|
1216 |
| pr_ord GREATER = "GREATER";
|
neuper@37954
|
1217 |
|
neuper@37954
|
1218 |
fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
|
neuper@37954
|
1219 |
(case a of
|
neuper@37954
|
1220 |
"Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
|
neuper@37954
|
1221 |
| _ => (((a, 0), T), 0))
|
neuper@37954
|
1222 |
| dest_hd' (Free (a, T)) = (((a, 0), T), 1)
|
neuper@37954
|
1223 |
| dest_hd' (Var v) = (v, 2)
|
neuper@37954
|
1224 |
| dest_hd' (Bound i) = ((("", i), dummyT), 3)
|
neuper@37954
|
1225 |
| dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
|
neuper@37954
|
1226 |
(* RL *)
|
neuper@37954
|
1227 |
fun get_order_pow (t $ (Free(order,_))) =
|
neuper@37954
|
1228 |
(case int_of_str (order) of
|
neuper@37954
|
1229 |
SOME d => d
|
neuper@37954
|
1230 |
| NONE => 0)
|
neuper@37954
|
1231 |
| get_order_pow _ = 0;
|
neuper@37954
|
1232 |
|
neuper@37954
|
1233 |
fun size_of_term' (Const(str,_) $ t) =
|
neuper@37954
|
1234 |
if "Atools.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
|
neuper@37954
|
1235 |
| size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
|
neuper@37954
|
1236 |
| size_of_term' (f$t) = size_of_term' f + size_of_term' t
|
neuper@37954
|
1237 |
| size_of_term' _ = 1;
|
neuper@38001
|
1238 |
fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
|
neuper@38053
|
1239 |
(case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
|
neuper@38053
|
1240 |
| ord => ord)
|
neuper@38001
|
1241 |
| term_ord' pr thy (t, u) =
|
neuper@38053
|
1242 |
(if pr then
|
neuper@38053
|
1243 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
|
neuper@38053
|
1244 |
val _ = tracing ("t= f@ts= \"" ^ term2str f ^ "\" @ \"[" ^
|
neuper@38053
|
1245 |
commas(map term2str ts) ^ "]\"")
|
neuper@38053
|
1246 |
val _ = tracing ("u= g@us= \"" ^ term2str g ^"\" @ \"[" ^
|
neuper@38053
|
1247 |
commas(map term2str us) ^"]\"")
|
neuper@38053
|
1248 |
val _ = tracing ("size_of_term(t,u)= (" ^
|
neuper@38053
|
1249 |
string_of_int (size_of_term' t) ^ ", " ^
|
neuper@38053
|
1250 |
string_of_int (size_of_term' u) ^ ")")
|
neuper@38053
|
1251 |
val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g))
|
neuper@38053
|
1252 |
val _ = tracing ("terms_ord(ts,us) = " ^
|
neuper@38053
|
1253 |
(pr_ord o terms_ord str false) (ts,us));
|
neuper@38053
|
1254 |
val _ = tracing "-------"
|
neuper@37954
|
1255 |
in () end
|
neuper@37954
|
1256 |
else ();
|
neuper@37954
|
1257 |
case int_ord (size_of_term' t, size_of_term' u) of
|
neuper@37954
|
1258 |
EQUAL =>
|
neuper@37954
|
1259 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
|
neuper@37954
|
1260 |
(case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
|
neuper@37954
|
1261 |
| ord => ord)
|
neuper@37954
|
1262 |
end
|
neuper@37954
|
1263 |
| ord => ord)
|
neuper@37954
|
1264 |
and hd_ord (f, g) = (* ~ term.ML *)
|
neuper@37991
|
1265 |
prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
|
neuper@37954
|
1266 |
and terms_ord str pr (ts, us) =
|
neuper@37991
|
1267 |
list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
|
neuper@37954
|
1268 |
in
|
neuper@37954
|
1269 |
|
neuper@37954
|
1270 |
fun ord_make_polytest (pr:bool) thy (_:subst) tu =
|
neuper@37954
|
1271 |
(term_ord' pr thy(***) tu = LESS );
|
neuper@37954
|
1272 |
|
neuper@37954
|
1273 |
end;(*local*)
|
neuper@38001
|
1274 |
*}
|
neuper@38001
|
1275 |
ML {*
|
neuper@37954
|
1276 |
|
neuper@37954
|
1277 |
rew_ord' := overwritel (!rew_ord',
|
neuper@37954
|
1278 |
[("termlessI", termlessI),
|
neuper@37954
|
1279 |
("ord_make_polytest", ord_make_polytest false thy)
|
neuper@37954
|
1280 |
]);
|
neuper@37954
|
1281 |
|
neuper@37954
|
1282 |
(*WN060510 this was a preparation for prep_rls ...
|
neuper@37954
|
1283 |
val scr_make_polytest =
|
neuper@38001
|
1284 |
"Script Expand_binomtest t_t =" ^
|
neuper@37954
|
1285 |
"(Repeat " ^
|
neuper@37954
|
1286 |
"((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
|
neuper@37954
|
1287 |
|
neuper@52062
|
1288 |
" (Try (Repeat (Rewrite distrib_right False))) @@ " ^
|
neuper@52062
|
1289 |
" (Try (Repeat (Rewrite distrib_left False))) @@ " ^
|
neuper@37971
|
1290 |
" (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
|
neuper@37971
|
1291 |
" (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
|
neuper@37954
|
1292 |
|
neuper@37971
|
1293 |
" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
|
neuper@37971
|
1294 |
" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
|
neuper@37971
|
1295 |
" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
|
neuper@37954
|
1296 |
|
neuper@48763
|
1297 |
" (Try (Repeat (Rewrite mult_commute False))) @@ " ^
|
neuper@37954
|
1298 |
" (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
|
neuper@48763
|
1299 |
" (Try (Repeat (Rewrite mult_assoc False))) @@ " ^
|
neuper@37971
|
1300 |
" (Try (Repeat (Rewrite add_commute False))) @@ " ^
|
neuper@37971
|
1301 |
" (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
|
neuper@37971
|
1302 |
" (Try (Repeat (Rewrite add_assoc False))) @@ " ^
|
neuper@37954
|
1303 |
|
neuper@37954
|
1304 |
" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
|
neuper@37954
|
1305 |
" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
|
neuper@37954
|
1306 |
" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
|
neuper@37954
|
1307 |
" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
|
neuper@37954
|
1308 |
|
neuper@37954
|
1309 |
" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
|
neuper@37954
|
1310 |
" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
|
neuper@37954
|
1311 |
|
neuper@37954
|
1312 |
" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
|
neuper@37954
|
1313 |
" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
|
neuper@37954
|
1314 |
|
neuper@37975
|
1315 |
" (Try (Repeat (Calculate PLUS ))) @@ " ^
|
neuper@37975
|
1316 |
" (Try (Repeat (Calculate TIMES ))) @@ " ^
|
neuper@37975
|
1317 |
" (Try (Repeat (Calculate POWER)))) " ^
|
neuper@38001
|
1318 |
" t_t)";
|
neuper@37954
|
1319 |
-----------------------------------------------------*)
|
neuper@37954
|
1320 |
|
neuper@37954
|
1321 |
val make_polytest =
|
neuper@37954
|
1322 |
Rls{id = "make_polytest", preconds = []:term list,
|
neuper@40836
|
1323 |
rew_ord = ("ord_make_polytest", ord_make_polytest false (Thy_Info.get_theory "Poly")),
|
neuper@37954
|
1324 |
erls = testerls, srls = Erls,
|
neuper@38014
|
1325 |
calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
|
neuper@38034
|
1326 |
("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
|
neuper@37954
|
1327 |
("POWER", ("Atools.pow", eval_binop "#power_"))
|
neuper@42451
|
1328 |
], errpatts = [],
|
neuper@37969
|
1329 |
rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
|
neuper@37954
|
1330 |
(*"a - b = a + (-1) * b"*)
|
neuper@52062
|
1331 |
Thm ("distrib_right" ,num_str @{thm distrib_right}),
|
neuper@37954
|
1332 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
neuper@52062
|
1333 |
Thm ("distrib_left",num_str @{thm distrib_left}),
|
neuper@37954
|
1334 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
neuper@37965
|
1335 |
Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
|
neuper@37954
|
1336 |
(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
|
neuper@37982
|
1337 |
Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
|
neuper@37954
|
1338 |
(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
|
neuper@37965
|
1339 |
Thm ("mult_1_left",num_str @{thm mult_1_left}),
|
neuper@37954
|
1340 |
(*"1 * z = z"*)
|
neuper@37965
|
1341 |
Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
|
neuper@37954
|
1342 |
(*"0 * z = 0"*)
|
neuper@37965
|
1343 |
Thm ("add_0_left",num_str @{thm add_0_left}),
|
neuper@37954
|
1344 |
(*"0 + z = z"*)
|
neuper@37954
|
1345 |
|
neuper@37954
|
1346 |
(*AC-rewriting*)
|
neuper@48763
|
1347 |
Thm ("mult_commute",num_str @{thm mult_commute}),
|
neuper@37954
|
1348 |
(* z * w = w * z *)
|
neuper@37969
|
1349 |
Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
|
neuper@37954
|
1350 |
(*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
|
neuper@48763
|
1351 |
Thm ("mult_assoc",num_str @{thm mult_assoc}),
|
neuper@37954
|
1352 |
(*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
|
neuper@37965
|
1353 |
Thm ("add_commute",num_str @{thm add_commute}),
|
neuper@37954
|
1354 |
(*z + w = w + z*)
|
neuper@37965
|
1355 |
Thm ("add_left_commute",num_str @{thm add_left_commute}),
|
neuper@37954
|
1356 |
(*x + (y + z) = y + (x + z)*)
|
neuper@37965
|
1357 |
Thm ("add_assoc",num_str @{thm add_assoc}),
|
neuper@37954
|
1358 |
(*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
|
neuper@37954
|
1359 |
|
neuper@37969
|
1360 |
Thm ("sym_realpow_twoI",
|
neuper@37969
|
1361 |
num_str (@{thm realpow_twoI} RS @{thm sym})),
|
neuper@37954
|
1362 |
(*"r1 * r1 = r1 ^^^ 2"*)
|
neuper@37969
|
1363 |
Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
|
neuper@37954
|
1364 |
(*"r * r ^^^ n = r ^^^ (n + 1)"*)
|
neuper@37969
|
1365 |
Thm ("sym_real_mult_2",
|
neuper@37969
|
1366 |
num_str (@{thm real_mult_2} RS @{thm sym})),
|
neuper@37954
|
1367 |
(*"z1 + z1 = 2 * z1"*)
|
neuper@37969
|
1368 |
Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
|
neuper@37954
|
1369 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37954
|
1370 |
|
neuper@37969
|
1371 |
Thm ("real_num_collect",num_str @{thm real_num_collect}),
|
neuper@37954
|
1372 |
(*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
|
neuper@37969
|
1373 |
Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
|
neuper@37954
|
1374 |
(*"[| l is_const; m is_const |] ==>
|
neuper@37954
|
1375 |
l * n + (m * n + k) = (l + m) * n + k"*)
|
neuper@37969
|
1376 |
Thm ("real_one_collect",num_str @{thm real_one_collect}),
|
neuper@37954
|
1377 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
neuper@37969
|
1378 |
Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
|
neuper@37954
|
1379 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37954
|
1380 |
|
neuper@38014
|
1381 |
Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@38034
|
1382 |
Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
neuper@37954
|
1383 |
Calc ("Atools.pow", eval_binop "#power_")
|
neuper@37954
|
1384 |
],
|
neuper@48763
|
1385 |
scr = EmptyScr(*Prog ((term_of o the o (parse thy))
|
neuper@37954
|
1386 |
scr_make_polytest)*)
|
neuper@38001
|
1387 |
}:rls;
|
neuper@38001
|
1388 |
*}
|
neuper@38001
|
1389 |
ML {*
|
neuper@38001
|
1390 |
(*WN060510 this was done before 'fun prep_rls' ...------------------------
|
neuper@37954
|
1391 |
val scr_expand_binomtest =
|
neuper@38001
|
1392 |
"Script Expand_binomtest t_t =" ^
|
neuper@37954
|
1393 |
"(Repeat " ^
|
neuper@37954
|
1394 |
"((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
|
neuper@37954
|
1395 |
" (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
|
neuper@37954
|
1396 |
" (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
|
neuper@37954
|
1397 |
" (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
|
neuper@37954
|
1398 |
" (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
|
neuper@37954
|
1399 |
" (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
|
neuper@37954
|
1400 |
|
neuper@37971
|
1401 |
" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
|
neuper@37971
|
1402 |
" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
|
neuper@37971
|
1403 |
" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
|
neuper@37954
|
1404 |
|
neuper@37975
|
1405 |
" (Try (Repeat (Calculate PLUS ))) @@ " ^
|
neuper@37975
|
1406 |
" (Try (Repeat (Calculate TIMES ))) @@ " ^
|
neuper@37975
|
1407 |
" (Try (Repeat (Calculate POWER))) @@ " ^
|
neuper@37954
|
1408 |
|
neuper@37954
|
1409 |
" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
|
neuper@37954
|
1410 |
" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
|
neuper@37954
|
1411 |
" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
|
neuper@37954
|
1412 |
" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
|
neuper@37954
|
1413 |
|
neuper@37954
|
1414 |
" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
|
neuper@37954
|
1415 |
" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
|
neuper@37954
|
1416 |
|
neuper@37954
|
1417 |
" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
|
neuper@37954
|
1418 |
" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
|
neuper@37954
|
1419 |
|
neuper@37975
|
1420 |
" (Try (Repeat (Calculate PLUS ))) @@ " ^
|
neuper@37975
|
1421 |
" (Try (Repeat (Calculate TIMES ))) @@ " ^
|
neuper@37975
|
1422 |
" (Try (Repeat (Calculate POWER)))) " ^
|
neuper@38001
|
1423 |
" t_t)";
|
neuper@38001
|
1424 |
--------------------------------------------------------------------------*)
|
neuper@37954
|
1425 |
|
neuper@37954
|
1426 |
val expand_binomtest =
|
neuper@37954
|
1427 |
Rls{id = "expand_binomtest", preconds = [],
|
neuper@37954
|
1428 |
rew_ord = ("termlessI",termlessI),
|
neuper@37954
|
1429 |
erls = testerls, srls = Erls,
|
neuper@38014
|
1430 |
calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
|
neuper@38034
|
1431 |
("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
|
neuper@37954
|
1432 |
("POWER", ("Atools.pow", eval_binop "#power_"))
|
neuper@42451
|
1433 |
], errpatts = [],
|
neuper@38001
|
1434 |
rules =
|
neuper@38001
|
1435 |
[Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
|
neuper@37954
|
1436 |
(*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
|
neuper@38001
|
1437 |
Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
|
neuper@37954
|
1438 |
(*"(a + b)*(a + b) = ...*)
|
neuper@38001
|
1439 |
Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),
|
neuper@38001
|
1440 |
(*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
|
neuper@38001
|
1441 |
Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),
|
neuper@38001
|
1442 |
(*"(a - b)*(a - b) = ...*)
|
neuper@38001
|
1443 |
Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),
|
neuper@38001
|
1444 |
(*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
|
neuper@38001
|
1445 |
Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),
|
neuper@38001
|
1446 |
(*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
|
neuper@38001
|
1447 |
(*RL 020915*)
|
neuper@38001
|
1448 |
Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
|
neuper@38001
|
1449 |
(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
|
neuper@38001
|
1450 |
Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
|
neuper@38001
|
1451 |
(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
|
neuper@38001
|
1452 |
Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
|
neuper@38001
|
1453 |
(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
|
neuper@38001
|
1454 |
Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
|
neuper@38001
|
1455 |
(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
|
neuper@38001
|
1456 |
Thm ("realpow_multI",num_str @{thm realpow_multI}),
|
neuper@38001
|
1457 |
(*(a*b)^^^n = a^^^n * b^^^n*)
|
neuper@38001
|
1458 |
Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
|
neuper@38001
|
1459 |
(* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
|
neuper@38001
|
1460 |
Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
|
neuper@38001
|
1461 |
(* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
|
neuper@37954
|
1462 |
|
neuper@37954
|
1463 |
|
neuper@52062
|
1464 |
(* Thm ("distrib_right" ,num_str @{thm distrib_right}),
|
neuper@38001
|
1465 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
neuper@52062
|
1466 |
Thm ("distrib_left",num_str @{thm distrib_left}),
|
neuper@38001
|
1467 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
neuper@38001
|
1468 |
Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
|
neuper@38001
|
1469 |
(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
|
neuper@38001
|
1470 |
Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
|
neuper@38001
|
1471 |
(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
|
neuper@38001
|
1472 |
*)
|
neuper@38001
|
1473 |
|
neuper@38001
|
1474 |
Thm ("mult_1_left",num_str @{thm mult_1_left}),
|
neuper@38001
|
1475 |
(*"1 * z = z"*)
|
neuper@38001
|
1476 |
Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
|
neuper@38001
|
1477 |
(*"0 * z = 0"*)
|
neuper@38001
|
1478 |
Thm ("add_0_left",num_str @{thm add_0_left}),
|
neuper@38001
|
1479 |
(*"0 + z = z"*)
|
neuper@37954
|
1480 |
|
neuper@38014
|
1481 |
Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@38034
|
1482 |
Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
neuper@38001
|
1483 |
Calc ("Atools.pow", eval_binop "#power_"),
|
neuper@38001
|
1484 |
(*
|
neuper@48763
|
1485 |
Thm ("mult_commute",num_str @{thm mult_commute}),
|
neuper@38001
|
1486 |
(*AC-rewriting*)
|
neuper@38001
|
1487 |
Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
|
neuper@48763
|
1488 |
Thm ("mult_assoc",num_str @{thm mult_assoc}),
|
neuper@38001
|
1489 |
Thm ("add_commute",num_str @{thm add_commute}),
|
neuper@38001
|
1490 |
Thm ("add_left_commute",num_str @{thm add_left_commute}),
|
neuper@38001
|
1491 |
Thm ("add_assoc",num_str @{thm add_assoc}),
|
neuper@38001
|
1492 |
*)
|
neuper@38001
|
1493 |
|
neuper@38001
|
1494 |
Thm ("sym_realpow_twoI",
|
neuper@38001
|
1495 |
num_str (@{thm realpow_twoI} RS @{thm sym})),
|
neuper@38001
|
1496 |
(*"r1 * r1 = r1 ^^^ 2"*)
|
neuper@38001
|
1497 |
Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
|
neuper@38001
|
1498 |
(*"r * r ^^^ n = r ^^^ (n + 1)"*)
|
neuper@38001
|
1499 |
(*Thm ("sym_real_mult_2",
|
neuper@38001
|
1500 |
num_str (@{thm real_mult_2} RS @{thm sym})),
|
neuper@38001
|
1501 |
(*"z1 + z1 = 2 * z1"*)*)
|
neuper@38001
|
1502 |
Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
|
neuper@38001
|
1503 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37954
|
1504 |
|
neuper@38001
|
1505 |
Thm ("real_num_collect",num_str @{thm real_num_collect}),
|
neuper@38001
|
1506 |
(*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
|
neuper@38001
|
1507 |
Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
|
neuper@38001
|
1508 |
(*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
|
neuper@38001
|
1509 |
Thm ("real_one_collect",num_str @{thm real_one_collect}),
|
neuper@38001
|
1510 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
neuper@38001
|
1511 |
Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
|
neuper@38001
|
1512 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37954
|
1513 |
|
neuper@38014
|
1514 |
Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@38034
|
1515 |
Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
neuper@38001
|
1516 |
Calc ("Atools.pow", eval_binop "#power_")
|
neuper@38001
|
1517 |
],
|
neuper@37954
|
1518 |
scr = EmptyScr
|
neuper@37954
|
1519 |
(*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
|
neuper@37954
|
1520 |
}:rls;
|
neuper@37954
|
1521 |
|
neuper@37954
|
1522 |
|
neuper@37967
|
1523 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
neuper@37954
|
1524 |
[("make_polytest", prep_rls make_polytest),
|
neuper@37954
|
1525 |
("expand_binomtest", prep_rls expand_binomtest)
|
neuper@37954
|
1526 |
]);
|
neuper@37954
|
1527 |
*}
|
neuper@37906
|
1528 |
|
neuper@37906
|
1529 |
end
|