neuper@37906
|
1 |
(* theory collecting all knowledge for Root
|
neuper@37906
|
2 |
created by:
|
neuper@37906
|
3 |
date:
|
neuper@37906
|
4 |
changed by: rlang
|
neuper@37906
|
5 |
last change by: rlang
|
neuper@37906
|
6 |
date: 02.10.21
|
neuper@37906
|
7 |
*)
|
neuper@37906
|
8 |
|
neuper@37982
|
9 |
theory Root imports Poly begin
|
neuper@37906
|
10 |
|
neuper@37906
|
11 |
consts
|
neuper@37906
|
12 |
|
neuper@37982
|
13 |
(*sqrt :: "real => real" Isabelle "NthRoot.sqrt"*)
|
neuper@37950
|
14 |
nroot :: "[real, real] => real"
|
neuper@37906
|
15 |
|
neuper@37950
|
16 |
axioms (*.not contained in Isabelle2002,
|
neuper@37906
|
17 |
stated as axioms, TODO: prove as theorems;
|
neuper@37906
|
18 |
theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
|
neuper@37906
|
19 |
|
neuper@37982
|
20 |
root_plus_minus: "0 <= b ==>
|
neuper@37950
|
21 |
(a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))"
|
neuper@37982
|
22 |
root_false: "b < 0 ==> (a^^^2 = b) = False"
|
neuper@37906
|
23 |
|
neuper@37906
|
24 |
(* for expand_rootbinom *)
|
neuper@37982
|
25 |
real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
|
neuper@37982
|
26 |
real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
|
neuper@37982
|
27 |
real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
|
neuper@37982
|
28 |
real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
|
neuper@37982
|
29 |
real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
|
neuper@37982
|
30 |
real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
|
neuper@37982
|
31 |
realpow_mul: "(a*b)^^^n = a^^^n * b^^^n"
|
neuper@37906
|
32 |
|
neuper@37982
|
33 |
real_diff_minus: "a - b = a + (-1) * b"
|
neuper@37982
|
34 |
real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
|
neuper@37982
|
35 |
real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
|
neuper@37982
|
36 |
real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
|
neuper@37982
|
37 |
real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
|
neuper@37982
|
38 |
real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2"
|
neuper@37982
|
39 |
real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2"
|
neuper@37906
|
40 |
|
neuper@37982
|
41 |
real_root_positive: "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)"
|
neuper@37982
|
42 |
real_root_negative: "a < 0 ==> (x ^^^ 2 = a) = False"
|
neuper@37906
|
43 |
|
neuper@37950
|
44 |
ML {*
|
neuper@37972
|
45 |
val thy = @{theory};
|
neuper@37972
|
46 |
|
neuper@37950
|
47 |
(*-------------------------functions---------------------*)
|
neuper@37950
|
48 |
(*evaluation square-root over the integers*)
|
neuper@37950
|
49 |
fun eval_sqrt (thmid:string) (op_:string) (t as
|
neuper@37950
|
50 |
(Const(op0,t0) $ arg)) thy =
|
neuper@37950
|
51 |
(case arg of
|
neuper@37950
|
52 |
Free (n1,t1) =>
|
neuper@37950
|
53 |
(case int_of_str n1 of
|
neuper@37950
|
54 |
SOME ni =>
|
neuper@37950
|
55 |
if ni < 0 then NONE
|
neuper@37950
|
56 |
else
|
neuper@37950
|
57 |
let val fact = squfact ni;
|
neuper@37950
|
58 |
in if fact*fact = ni
|
neuper@37950
|
59 |
then SOME ("#sqrt #"^(string_of_int ni)^" = #"
|
neuper@37950
|
60 |
^(string_of_int (if ni = 0 then 0
|
neuper@37950
|
61 |
else ni div fact)),
|
neuper@37950
|
62 |
Trueprop $ mk_equality (t, term_of_num t1 fact))
|
neuper@37950
|
63 |
else if fact = 1 then NONE
|
neuper@37950
|
64 |
else SOME ("#sqrt #"^(string_of_int ni)^" = sqrt (#"
|
neuper@37950
|
65 |
^(string_of_int fact)^" * #"
|
neuper@37950
|
66 |
^(string_of_int fact)^" * #"
|
neuper@37950
|
67 |
^(string_of_int (ni div (fact*fact))^")"),
|
neuper@37950
|
68 |
Trueprop $
|
neuper@37950
|
69 |
(mk_equality
|
neuper@37950
|
70 |
(t,
|
neuper@37950
|
71 |
(mk_factroot op0 t1 fact
|
neuper@37950
|
72 |
(ni div (fact*fact))))))
|
neuper@37950
|
73 |
end
|
neuper@37950
|
74 |
| NONE => NONE)
|
neuper@37950
|
75 |
| _ => NONE)
|
neuper@37950
|
76 |
|
neuper@37950
|
77 |
| eval_sqrt _ _ _ _ = NONE;
|
neuper@37950
|
78 |
(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("","", str2term "sqrt 0");
|
neuper@37950
|
79 |
> eval_sqrt thmid op_ t thy;
|
neuper@37950
|
80 |
> val Free (n1,t1) = arg;
|
neuper@37950
|
81 |
> val SOME ni = int_of_str n1;
|
neuper@37950
|
82 |
*)
|
neuper@37950
|
83 |
|
neuper@37950
|
84 |
calclist':= overwritel (!calclist',
|
neuper@37982
|
85 |
[("SQRT" ,("NthRoot.sqrt" ,eval_sqrt "#sqrt_"))
|
neuper@37975
|
86 |
(*different types for 'sqrt 4' --- 'Calculate SQRT'*)
|
neuper@37950
|
87 |
]);
|
neuper@37950
|
88 |
|
neuper@37950
|
89 |
|
neuper@37950
|
90 |
local (* Vers. 7.10.99.A *)
|
neuper@37950
|
91 |
|
neuper@37950
|
92 |
open Term; (* for type order = EQUAL | LESS | GREATER *)
|
neuper@37950
|
93 |
|
neuper@37950
|
94 |
fun pr_ord EQUAL = "EQUAL"
|
neuper@37950
|
95 |
| pr_ord LESS = "LESS"
|
neuper@37950
|
96 |
| pr_ord GREATER = "GREATER";
|
neuper@37950
|
97 |
|
neuper@37950
|
98 |
fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
|
neuper@37982
|
99 |
(case a of "NthRoot.sqrt" => ((("|||", 0), T), 0) (*WN greatest *)
|
neuper@37950
|
100 |
| _ => (((a, 0), T), 0))
|
neuper@37950
|
101 |
| dest_hd' (Free (a, T)) = (((a, 0), T), 1)
|
neuper@37950
|
102 |
| dest_hd' (Var v) = (v, 2)
|
neuper@37950
|
103 |
| dest_hd' (Bound i) = ((("", i), dummyT), 3)
|
neuper@37950
|
104 |
| dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
|
neuper@37950
|
105 |
fun size_of_term' (Const(str,_) $ t) =
|
neuper@37982
|
106 |
(case str of "NthRoot.sqrt" => (1000 + size_of_term' t)
|
neuper@37950
|
107 |
| _ => 1 + size_of_term' t)
|
neuper@37950
|
108 |
| size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
|
neuper@37950
|
109 |
| size_of_term' (f $ t) = size_of_term' f + size_of_term' t
|
neuper@37950
|
110 |
| size_of_term' _ = 1;
|
neuper@37950
|
111 |
fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
|
neuper@37982
|
112 |
(case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
|
neuper@37950
|
113 |
| term_ord' pr thy (t, u) =
|
neuper@37950
|
114 |
(if pr then
|
neuper@37950
|
115 |
let
|
neuper@37950
|
116 |
val (f, ts) = strip_comb t and (g, us) = strip_comb u;
|
neuper@38015
|
117 |
val _=tracing("t= f@ts= \""^
|
neuper@37950
|
118 |
((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
|
neuper@37950
|
119 |
(commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
|
neuper@38015
|
120 |
val _=tracing("u= g@us= \""^
|
neuper@37950
|
121 |
((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
|
neuper@37950
|
122 |
(commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
|
neuper@38015
|
123 |
val _=tracing("size_of_term(t,u)= ("^
|
neuper@37950
|
124 |
(string_of_int(size_of_term' t))^", "^
|
neuper@37950
|
125 |
(string_of_int(size_of_term' u))^")");
|
neuper@38015
|
126 |
val _=tracing("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
|
neuper@38015
|
127 |
val _=tracing("terms_ord(ts,us) = "^
|
neuper@37950
|
128 |
((pr_ord o terms_ord str false)(ts,us)));
|
neuper@38015
|
129 |
val _=tracing("-------");
|
neuper@37950
|
130 |
in () end
|
neuper@37950
|
131 |
else ();
|
neuper@37950
|
132 |
case int_ord (size_of_term' t, size_of_term' u) of
|
neuper@37950
|
133 |
EQUAL =>
|
neuper@37950
|
134 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
|
neuper@37950
|
135 |
(case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
|
neuper@37950
|
136 |
| ord => ord)
|
neuper@37950
|
137 |
end
|
neuper@37950
|
138 |
| ord => ord)
|
neuper@37950
|
139 |
and hd_ord (f, g) = (* ~ term.ML *)
|
neuper@37982
|
140 |
prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
|
neuper@37982
|
141 |
(dest_hd' f, dest_hd' g)
|
neuper@37950
|
142 |
and terms_ord str pr (ts, us) =
|
neuper@37991
|
143 |
list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
|
neuper@37950
|
144 |
|
neuper@37950
|
145 |
in
|
neuper@37950
|
146 |
(* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
|
neuper@37950
|
147 |
by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1
|
neuper@37950
|
148 |
(2) hd_ord: greater to right, 'sqrt' < numerals < variables
|
neuper@37950
|
149 |
(3) terms_ord: recurs. on args, greater to right
|
neuper@37950
|
150 |
*)
|
neuper@37950
|
151 |
|
neuper@37950
|
152 |
(*args
|
neuper@37950
|
153 |
pr: print trace, WN0509 'sqrt_right true' not used anymore
|
neuper@37950
|
154 |
thy:
|
neuper@37950
|
155 |
subst: no bound variables, only Root.sqrt
|
neuper@37950
|
156 |
tu: the terms to compare (t1, t2) ... *)
|
neuper@37950
|
157 |
fun sqrt_right (pr:bool) thy (_:subst) tu =
|
neuper@37950
|
158 |
(term_ord' pr thy(***) tu = LESS );
|
neuper@37950
|
159 |
end;
|
neuper@37950
|
160 |
|
neuper@37950
|
161 |
rew_ord' := overwritel (!rew_ord',
|
neuper@37950
|
162 |
[("termlessI", termlessI),
|
neuper@37950
|
163 |
("sqrt_right", sqrt_right false (theory "Pure"))
|
neuper@37950
|
164 |
]);
|
neuper@37950
|
165 |
|
neuper@37950
|
166 |
(*-------------------------rulse-------------------------*)
|
neuper@37950
|
167 |
val Root_crls =
|
neuper@37950
|
168 |
append_rls "Root_crls" Atools_erls
|
neuper@37969
|
169 |
[Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
|
neuper@37982
|
170 |
Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
|
neuper@38014
|
171 |
Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"),
|
neuper@37950
|
172 |
Calc ("Atools.pow" ,eval_binop "#power_"),
|
neuper@38014
|
173 |
Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@38014
|
174 |
Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
|
neuper@38034
|
175 |
Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
neuper@37950
|
176 |
Calc ("op =",eval_equal "#equal_")
|
neuper@37950
|
177 |
];
|
neuper@37950
|
178 |
|
neuper@37950
|
179 |
val Root_erls =
|
neuper@37950
|
180 |
append_rls "Root_erls" Atools_erls
|
neuper@37969
|
181 |
[Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
|
neuper@37982
|
182 |
Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
|
neuper@38014
|
183 |
Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"),
|
neuper@37950
|
184 |
Calc ("Atools.pow" ,eval_binop "#power_"),
|
neuper@38014
|
185 |
Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@38014
|
186 |
Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
|
neuper@38034
|
187 |
Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
neuper@37950
|
188 |
Calc ("op =",eval_equal "#equal_")
|
neuper@37950
|
189 |
];
|
neuper@37950
|
190 |
|
neuper@37967
|
191 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
neuper@37950
|
192 |
[("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*)
|
neuper@37950
|
193 |
]);
|
neuper@37950
|
194 |
|
neuper@37950
|
195 |
val make_rooteq = prep_rls(
|
neuper@37950
|
196 |
Rls{id = "make_rooteq", preconds = []:term list,
|
neuper@37972
|
197 |
rew_ord = ("sqrt_right", sqrt_right false thy),
|
neuper@37950
|
198 |
erls = Atools_erls, srls = Erls,
|
neuper@37950
|
199 |
calc = [],
|
neuper@37950
|
200 |
(*asm_thm = [],*)
|
neuper@37969
|
201 |
rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
|
neuper@37950
|
202 |
(*"a - b = a + (-1) * b"*)
|
neuper@37950
|
203 |
|
neuper@37965
|
204 |
Thm ("left_distrib" ,num_str @{thm left_distrib}),
|
neuper@37950
|
205 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
neuper@37974
|
206 |
Thm ("right_distrib",num_str @{thm right_distrib}),
|
neuper@37950
|
207 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
neuper@37965
|
208 |
Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
|
neuper@37950
|
209 |
(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
|
neuper@37982
|
210 |
Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
|
neuper@37950
|
211 |
(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
|
neuper@37950
|
212 |
|
neuper@37965
|
213 |
Thm ("mult_1_left",num_str @{thm mult_1_left}),
|
neuper@37950
|
214 |
(*"1 * z = z"*)
|
neuper@37965
|
215 |
Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
|
neuper@37950
|
216 |
(*"0 * z = 0"*)
|
neuper@37965
|
217 |
Thm ("add_0_left",num_str @{thm add_0_left}),
|
neuper@37950
|
218 |
(*"0 + z = z"*)
|
neuper@37950
|
219 |
|
neuper@37969
|
220 |
Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
|
neuper@37950
|
221 |
(*AC-rewriting*)
|
neuper@37969
|
222 |
Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
|
neuper@37950
|
223 |
(**)
|
neuper@37969
|
224 |
Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
|
neuper@37950
|
225 |
(**)
|
neuper@37965
|
226 |
Thm ("add_commute",num_str @{thm add_commute}),
|
neuper@37950
|
227 |
(**)
|
neuper@37965
|
228 |
Thm ("add_left_commute",num_str @{thm add_left_commute}),
|
neuper@37950
|
229 |
(**)
|
neuper@37965
|
230 |
Thm ("add_assoc",num_str @{thm add_assoc}),
|
neuper@37950
|
231 |
(**)
|
neuper@37950
|
232 |
|
neuper@37969
|
233 |
Thm ("sym_realpow_twoI",
|
neuper@37969
|
234 |
num_str (@{thm realpow_twoI} RS @{thm sym})),
|
neuper@37950
|
235 |
(*"r1 * r1 = r1 ^^^ 2"*)
|
neuper@37969
|
236 |
Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
|
neuper@37950
|
237 |
(*"r * r ^^^ n = r ^^^ (n + 1)"*)
|
neuper@37969
|
238 |
Thm ("sym_real_mult_2",
|
neuper@37969
|
239 |
num_str (@{thm real_mult_2} RS @{thm sym})),
|
neuper@37950
|
240 |
(*"z1 + z1 = 2 * z1"*)
|
neuper@37969
|
241 |
Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
|
neuper@37950
|
242 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37950
|
243 |
|
neuper@37969
|
244 |
Thm ("real_num_collect",num_str @{thm real_num_collect}),
|
neuper@37950
|
245 |
(*"[| l is_const; m is_const |]==> l * n + m * n = (l + m) * n"*)
|
neuper@37969
|
246 |
Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
|
neuper@37950
|
247 |
(*"[| l is_const; m is_const |] ==>
|
neuper@37950
|
248 |
l * n + (m * n + k) = (l + m) * n + k"*)
|
neuper@37969
|
249 |
Thm ("real_one_collect",num_str @{thm real_one_collect}),
|
neuper@37950
|
250 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
neuper@37969
|
251 |
Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
|
neuper@37950
|
252 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37950
|
253 |
|
neuper@38014
|
254 |
Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@38034
|
255 |
Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
neuper@37950
|
256 |
Calc ("Atools.pow", eval_binop "#power_")
|
neuper@37950
|
257 |
],
|
neuper@37950
|
258 |
scr = Script ((term_of o the o (parse thy)) "empty_script")
|
neuper@37950
|
259 |
}:rls);
|
neuper@37967
|
260 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
neuper@37950
|
261 |
[("make_rooteq", make_rooteq)
|
neuper@37950
|
262 |
]);
|
neuper@37950
|
263 |
|
neuper@37950
|
264 |
val expand_rootbinoms = prep_rls(
|
neuper@37950
|
265 |
Rls{id = "expand_rootbinoms", preconds = [],
|
neuper@37950
|
266 |
rew_ord = ("termlessI",termlessI),
|
neuper@37950
|
267 |
erls = Atools_erls, srls = Erls,
|
neuper@37950
|
268 |
calc = [],
|
neuper@37950
|
269 |
(*asm_thm = [],*)
|
neuper@37969
|
270 |
rules = [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
|
neuper@37950
|
271 |
(*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
|
neuper@37969
|
272 |
Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
|
neuper@37950
|
273 |
(*"(a + b)*(a + b) = ...*)
|
neuper@37969
|
274 |
Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),
|
neuper@37950
|
275 |
(*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
|
neuper@37969
|
276 |
Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),
|
neuper@37950
|
277 |
(*"(a - b)*(a - b) = ...*)
|
neuper@37969
|
278 |
Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),
|
neuper@37950
|
279 |
(*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
|
neuper@37969
|
280 |
Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),
|
neuper@37950
|
281 |
(*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
|
neuper@37950
|
282 |
(*RL 020915*)
|
neuper@37969
|
283 |
Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
|
neuper@37950
|
284 |
(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
|
neuper@37969
|
285 |
Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
|
neuper@37950
|
286 |
(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
|
neuper@37969
|
287 |
Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
|
neuper@37950
|
288 |
(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
|
neuper@37969
|
289 |
Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
|
neuper@37950
|
290 |
(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
|
neuper@37969
|
291 |
Thm ("realpow_mul",num_str @{thm realpow_mul}),
|
neuper@37950
|
292 |
(*(a*b)^^^n = a^^^n * b^^^n*)
|
neuper@37950
|
293 |
|
neuper@37965
|
294 |
Thm ("mult_1_left",num_str @{thm mult_1_left}), (*"1 * z = z"*)
|
neuper@37965
|
295 |
Thm ("mult_zero_left",num_str @{thm mult_zero_left}), (*"0 * z = 0"*)
|
neuper@37965
|
296 |
Thm ("add_0_left",num_str @{thm add_0_left}),
|
neuper@37950
|
297 |
(*"0 + z = z"*)
|
neuper@37950
|
298 |
|
neuper@38014
|
299 |
Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@38014
|
300 |
Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
|
neuper@38034
|
301 |
Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
neuper@38014
|
302 |
Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
|
neuper@37982
|
303 |
Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
|
neuper@37950
|
304 |
Calc ("Atools.pow", eval_binop "#power_"),
|
neuper@37950
|
305 |
|
neuper@37969
|
306 |
Thm ("sym_realpow_twoI",
|
neuper@37969
|
307 |
num_str (@{thm realpow_twoI} RS @{thm sym})),
|
neuper@37950
|
308 |
(*"r1 * r1 = r1 ^^^ 2"*)
|
neuper@37969
|
309 |
Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
|
neuper@37950
|
310 |
(*"r * r ^^^ n = r ^^^ (n + 1)"*)
|
neuper@37969
|
311 |
Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
|
neuper@37950
|
312 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37950
|
313 |
|
neuper@37969
|
314 |
Thm ("real_num_collect",num_str @{thm real_num_collect}),
|
neuper@37950
|
315 |
(*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
|
neuper@37969
|
316 |
Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
|
neuper@37950
|
317 |
(*"[| l is_const; m is_const |] ==>
|
neuper@37950
|
318 |
l * n + (m * n + k) = (l + m) * n + k"*)
|
neuper@37969
|
319 |
Thm ("real_one_collect",num_str @{thm real_one_collect}),
|
neuper@37950
|
320 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
neuper@37969
|
321 |
Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
|
neuper@37950
|
322 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37950
|
323 |
|
neuper@38014
|
324 |
Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@38014
|
325 |
Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
|
neuper@38034
|
326 |
Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
neuper@38014
|
327 |
Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
|
neuper@37982
|
328 |
Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
|
neuper@37950
|
329 |
Calc ("Atools.pow", eval_binop "#power_")
|
neuper@37950
|
330 |
],
|
neuper@37950
|
331 |
scr = Script ((term_of o the o (parse thy)) "empty_script")
|
neuper@37950
|
332 |
}:rls);
|
neuper@37950
|
333 |
|
neuper@37950
|
334 |
|
neuper@37967
|
335 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
neuper@37950
|
336 |
[("expand_rootbinoms", expand_rootbinoms)
|
neuper@37950
|
337 |
]);
|
neuper@37950
|
338 |
*}
|
neuper@37950
|
339 |
|
neuper@37906
|
340 |
end
|