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@52148
|
16 |
axiomatization where (*.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 ==>
|
walther@60242
|
21 |
(a \<up> 2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))" and
|
walther@60242
|
22 |
root_false: "b < 0 ==> (a \<up> 2 = b) = False" and
|
neuper@37906
|
23 |
|
neuper@37906
|
24 |
(* for expand_rootbinom *)
|
neuper@52148
|
25 |
real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
|
neuper@52148
|
26 |
real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
|
neuper@52148
|
27 |
real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
|
neuper@52148
|
28 |
real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
|
walther@60242
|
29 |
real_plus_binom_pow3: "(a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" and
|
walther@60242
|
30 |
real_minus_binom_pow3: "(a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3" and
|
walther@60242
|
31 |
realpow_mul: "(a*b) \<up> n = a \<up> n * b \<up> n" and
|
neuper@37906
|
32 |
|
neuper@52148
|
33 |
real_diff_minus: "a - b = a + (-1) * b" and
|
walther@60242
|
34 |
real_plus_binom_times: "(a + b)*(a + b) = a \<up> 2 + 2*a*b + b \<up> 2" and
|
walther@60242
|
35 |
real_minus_binom_times: "(a - b)*(a - b) = a \<up> 2 - 2*a*b + b \<up> 2" and
|
walther@60242
|
36 |
real_plus_binom_pow2: "(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2" and
|
walther@60242
|
37 |
real_minus_binom_pow2: "(a - b) \<up> 2 = a \<up> 2 - 2*a*b + b \<up> 2" and
|
walther@60242
|
38 |
real_plus_minus_binom1: "(a + b)*(a - b) = a \<up> 2 - b \<up> 2" and
|
walther@60242
|
39 |
real_plus_minus_binom2: "(a - b)*(a + b) = a \<up> 2 - b \<up> 2" and
|
neuper@37906
|
40 |
|
walther@60242
|
41 |
real_root_positive: "0 <= a ==> (x \<up> 2 = a) = (x = sqrt a)" and
|
walther@60242
|
42 |
real_root_negative: "a < 0 ==> (x \<up> 2 = a) = False"
|
neuper@37906
|
43 |
|
wneuper@59472
|
44 |
ML \<open>
|
neuper@37950
|
45 |
(*-------------------------functions---------------------*)
|
neuper@37950
|
46 |
(*evaluation square-root over the integers*)
|
Walther@60504
|
47 |
fun eval_sqrt (_ : string) (_ : string) t (_: Proof.context) =
|
wenzelm@60381
|
48 |
(case t of
|
wenzelm@60381
|
49 |
Const (op0, _) $ num =>
|
wenzelm@60381
|
50 |
(case try HOLogic.dest_number num of
|
wenzelm@60381
|
51 |
SOME (T, ni)=>
|
wenzelm@60381
|
52 |
if ni < 0 then NONE
|
wenzelm@60381
|
53 |
else
|
wenzelm@60381
|
54 |
let val fact = Eval.squfact ni;
|
wenzelm@60381
|
55 |
in
|
walther@60317
|
56 |
if fact * fact = ni
|
wenzelm@60381
|
57 |
then
|
walther@60317
|
58 |
SOME ("#sqrt #" ^ string_of_int ni ^ " = #"
|
wenzelm@60381
|
59 |
^ string_of_int (if ni = 0 then 0 else ni div fact),
|
wenzelm@60381
|
60 |
HOLogic.Trueprop $ TermC.mk_equality (t, TermC.term_of_num T fact))
|
wenzelm@60381
|
61 |
else if fact = 1 then NONE
|
wenzelm@60381
|
62 |
else
|
walther@60317
|
63 |
SOME ("#sqrt #" ^ string_of_int ni ^ " = sqrt (#"
|
wenzelm@60381
|
64 |
^ string_of_int fact ^ " * #" ^ string_of_int fact ^ " * #"
|
wenzelm@60381
|
65 |
^ string_of_int (ni div (fact * fact)) ^ ")",
|
wenzelm@60381
|
66 |
HOLogic.Trueprop $ TermC.mk_equality
|
walther@60317
|
67 |
(t, (TermC.mk_factroot op0 T fact (ni div (fact*fact)))))
|
wenzelm@60381
|
68 |
end
|
wenzelm@60381
|
69 |
| NONE => NONE)
|
wenzelm@60381
|
70 |
| _ => NONE);
|
wenzelm@60381
|
71 |
|
Walther@60567
|
72 |
(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", TermC.parse_test @{context} "sqrt 0");
|
neuper@37950
|
73 |
> eval_sqrt thmid op_ t thy;
|
neuper@37950
|
74 |
> val Free (n1,t1) = arg;
|
neuper@37950
|
75 |
> val SOME ni = int_of_str n1;
|
neuper@37950
|
76 |
*)
|
wneuper@59472
|
77 |
\<close>
|
wenzelm@60381
|
78 |
|
wenzelm@60313
|
79 |
calculation SQRT (sqrt) = \<open>eval_sqrt "#sqrt_"\<close>
|
wenzelm@60313
|
80 |
(*different types for 'sqrt 4' --- 'Calculate SQRT'*)
|
wneuper@59472
|
81 |
ML \<open>
|
neuper@37950
|
82 |
local (* Vers. 7.10.99.A *)
|
neuper@37950
|
83 |
|
neuper@37950
|
84 |
open Term; (* for type order = EQUAL | LESS | GREATER *)
|
neuper@37950
|
85 |
|
neuper@37950
|
86 |
fun pr_ord EQUAL = "EQUAL"
|
neuper@37950
|
87 |
| pr_ord LESS = "LESS"
|
neuper@37950
|
88 |
| pr_ord GREATER = "GREATER";
|
neuper@37950
|
89 |
|
neuper@37950
|
90 |
fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
|
wenzelm@60309
|
91 |
(case a of \<^const_name>\<open>sqrt\<close> => ((("|||", 0), T), 0) (*WN greatest *)
|
neuper@37950
|
92 |
| _ => (((a, 0), T), 0))
|
walther@60317
|
93 |
| dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)
|
neuper@37950
|
94 |
| dest_hd' (Var v) = (v, 2)
|
neuper@37950
|
95 |
| dest_hd' (Bound i) = ((("", i), dummyT), 3)
|
walther@60269
|
96 |
| dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
|
walther@60269
|
97 |
| dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";
|
neuper@37950
|
98 |
fun size_of_term' (Const(str,_) $ t) =
|
wenzelm@60309
|
99 |
(case str of \<^const_name>\<open>sqrt\<close> => (1000 + size_of_term' t)
|
neuper@37950
|
100 |
| _ => 1 + size_of_term' t)
|
neuper@37950
|
101 |
| size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
|
neuper@37950
|
102 |
| size_of_term' (f $ t) = size_of_term' f + size_of_term' t
|
neuper@37950
|
103 |
| size_of_term' _ = 1;
|
neuper@37950
|
104 |
fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
|
neuper@38053
|
105 |
(case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
|
neuper@38053
|
106 |
| ord => ord)
|
walther@60269
|
107 |
| term_ord' pr _(*thy*) (t, u) =
|
neuper@38053
|
108 |
(if pr then
|
neuper@37950
|
109 |
let
|
neuper@38053
|
110 |
val (f, ts) = strip_comb t and (g, us) = strip_comb u;
|
walther@59868
|
111 |
val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^"\" @ \"[" ^
|
walther@59868
|
112 |
commas (map UnparseC.term ts) ^ "]\"");
|
walther@59868
|
113 |
val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
|
walther@59868
|
114 |
commas (map UnparseC.term us) ^ "]\"");
|
neuper@38053
|
115 |
val _ = tracing ("size_of_term(t,u)= (" ^
|
neuper@38053
|
116 |
string_of_int(size_of_term' t) ^", " ^
|
neuper@38053
|
117 |
string_of_int(size_of_term' u) ^")");
|
neuper@38053
|
118 |
val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
|
neuper@38053
|
119 |
val _ = tracing ("terms_ord(ts,us) = " ^
|
neuper@38053
|
120 |
(pr_ord o terms_ord str false) (ts,us));
|
neuper@38053
|
121 |
val _=tracing("-------");
|
neuper@37950
|
122 |
in () end
|
neuper@38053
|
123 |
else ();
|
neuper@38053
|
124 |
case int_ord (size_of_term' t, size_of_term' u) of
|
neuper@38053
|
125 |
EQUAL =>
|
neuper@38053
|
126 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
|
neuper@38053
|
127 |
(case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
|
neuper@38053
|
128 |
| ord => ord)
|
neuper@38053
|
129 |
end
|
neuper@38053
|
130 |
| ord => ord)
|
neuper@37950
|
131 |
and hd_ord (f, g) = (* ~ term.ML *)
|
neuper@37982
|
132 |
prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
|
neuper@37982
|
133 |
(dest_hd' f, dest_hd' g)
|
walther@60269
|
134 |
and terms_ord _(*str*) pr (ts, us) =
|
walther@59881
|
135 |
list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
|
neuper@37950
|
136 |
|
neuper@37950
|
137 |
in
|
neuper@37950
|
138 |
(* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
|
neuper@37950
|
139 |
by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1
|
neuper@37950
|
140 |
(2) hd_ord: greater to right, 'sqrt' < numerals < variables
|
neuper@37950
|
141 |
(3) terms_ord: recurs. on args, greater to right
|
neuper@37950
|
142 |
*)
|
neuper@37950
|
143 |
|
neuper@37950
|
144 |
(*args
|
neuper@37950
|
145 |
pr: print trace, WN0509 'sqrt_right true' not used anymore
|
neuper@37950
|
146 |
thy:
|
neuper@37950
|
147 |
subst: no bound variables, only Root.sqrt
|
neuper@37950
|
148 |
tu: the terms to compare (t1, t2) ... *)
|
walther@60324
|
149 |
fun sqrt_right (pr:bool) thy (_: subst) (ts, us) =
|
walther@60324
|
150 |
(term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
|
neuper@37950
|
151 |
end;
|
Walther@60506
|
152 |
\<close> ML \<open>
|
Walther@60506
|
153 |
\<close>
|
Walther@60547
|
154 |
setup \<open>KEStore_Elems.add_rew_ords [
|
Walther@60506
|
155 |
("termlessI", termlessI),
|
Walther@60506
|
156 |
("sqrt_right", sqrt_right false @{theory "Pure"})]\<close>
|
neuper@37950
|
157 |
|
Walther@60506
|
158 |
ML \<open>
|
Walther@60506
|
159 |
(*------------------------- rules -------------------------*)
|
neuper@37950
|
160 |
val Root_crls =
|
walther@60358
|
161 |
Rule_Set.append_rules "Root_crls" Atools_erls [
|
walther@60358
|
162 |
\<^rule_thm>\<open>real_unari_minus\<close>,
|
walther@60358
|
163 |
\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
|
walther@60358
|
164 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
Walther@60515
|
165 |
\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
|
Walther@60515
|
166 |
\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
|
Walther@60515
|
167 |
\<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
|
Walther@60515
|
168 |
\<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
|
walther@60358
|
169 |
\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")];
|
neuper@37950
|
170 |
|
neuper@37950
|
171 |
val Root_erls =
|
walther@60358
|
172 |
Rule_Set.append_rules "Root_erls" Atools_erls [
|
walther@60358
|
173 |
\<^rule_thm>\<open>real_unari_minus\<close>,
|
walther@60358
|
174 |
\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
|
walther@60358
|
175 |
\<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
Walther@60515
|
176 |
\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
|
Walther@60515
|
177 |
\<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(Calc_Binop.numeric "#add_"),
|
Walther@60515
|
178 |
\<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(Calc_Binop.numeric "#sub_"),
|
Walther@60515
|
179 |
\<^rule_eval>\<open>Groups.times_class.times\<close> (**)(Calc_Binop.numeric "#mult_"),
|
walther@60358
|
180 |
\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")];
|
walther@60384
|
181 |
val Root_erls =
|
walther@60384
|
182 |
Rule_Set.append_erls_rules "Root_erls_erls" Root_erls [
|
walther@60384
|
183 |
\<^rule_thm>\<open>not_false\<close>,
|
walther@60384
|
184 |
\<^rule_thm>\<open>not_true\<close>,
|
walther@60384
|
185 |
\<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_")];
|
wneuper@59472
|
186 |
\<close>
|
wenzelm@60289
|
187 |
rule_set_knowledge Root_erls = Root_erls
|
wneuper@59472
|
188 |
ML \<open>
|
neuper@37950
|
189 |
|
s1210629013@55444
|
190 |
val make_rooteq = prep_rls'(
|
walther@59851
|
191 |
Rule_Def.Repeat{id = "make_rooteq", preconds = []:term list,
|
walther@60358
|
192 |
rew_ord = ("sqrt_right", sqrt_right false \<^theory>),
|
walther@60358
|
193 |
erls = Atools_erls, srls = Rule_Set.Empty,
|
walther@60358
|
194 |
calc = [], errpatts = [],
|
walther@60358
|
195 |
rules = [
|
walther@60358
|
196 |
\<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
|
neuper@37950
|
197 |
|
walther@60358
|
198 |
\<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
walther@60358
|
199 |
\<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
walther@60358
|
200 |
\<^rule_thm>\<open>left_diff_distrib\<close>, (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
|
walther@60358
|
201 |
\<^rule_thm>\<open>right_diff_distrib\<close>, (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
|
neuper@37950
|
202 |
|
walther@60358
|
203 |
\<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
|
walther@60358
|
204 |
\<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
|
walther@60358
|
205 |
\<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
|
neuper@37950
|
206 |
|
walther@60358
|
207 |
(*AC-rewriting*)
|
walther@60358
|
208 |
\<^rule_thm>\<open>mult.commute\<close>,
|
walther@60358
|
209 |
\<^rule_thm>\<open>real_mult_left_commute\<close>,
|
walther@60358
|
210 |
\<^rule_thm>\<open>mult.assoc\<close>,
|
walther@60358
|
211 |
\<^rule_thm>\<open>add.commute\<close>,
|
walther@60358
|
212 |
\<^rule_thm>\<open>add.left_commute\<close>,
|
walther@60358
|
213 |
\<^rule_thm>\<open>add.assoc\<close>,
|
neuper@37950
|
214 |
|
walther@60358
|
215 |
\<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
|
walther@60358
|
216 |
\<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
|
walther@60358
|
217 |
\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
|
walther@60358
|
218 |
\<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37950
|
219 |
|
walther@60385
|
220 |
\<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==> l * n + m * n = (l + m) * n"*)
|
walther@60385
|
221 |
\<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
|
walther@60385
|
222 |
\<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
|
walther@60385
|
223 |
\<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
|
walther@60358
|
224 |
|
Walther@60515
|
225 |
\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
|
Walther@60515
|
226 |
\<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
|
Walther@60515
|
227 |
\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
|
walther@60358
|
228 |
scr = Rule.Empty_Prog});
|
wneuper@59472
|
229 |
\<close>
|
wenzelm@60289
|
230 |
rule_set_knowledge make_rooteq = make_rooteq
|
wneuper@59472
|
231 |
ML \<open>
|
neuper@37950
|
232 |
|
walther@59618
|
233 |
val prep_rls' = Auto_Prog.prep_rls @{theory};
|
s1210629013@55444
|
234 |
|
s1210629013@55444
|
235 |
val expand_rootbinoms = prep_rls'(
|
walther@60358
|
236 |
Rule_Def.Repeat {
|
walther@60358
|
237 |
id = "expand_rootbinoms", preconds = [], rew_ord = ("termlessI",termlessI),
|
walther@60358
|
238 |
erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
239 |
rules = [
|
walther@60358
|
240 |
\<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
|
walther@60358
|
241 |
\<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*)
|
walther@60358
|
242 |
\<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
|
walther@60358
|
243 |
\<^rule_thm>\<open>real_minus_binom_times\<close>, (*"(a - b)*(a - b) = ...*)
|
walther@60358
|
244 |
\<^rule_thm>\<open>real_plus_minus_binom1\<close>, (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
|
walther@60358
|
245 |
\<^rule_thm>\<open>real_plus_minus_binom2\<close>, (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
|
walther@60358
|
246 |
(*RL 020915*)
|
walther@60358
|
247 |
\<^rule_thm>\<open>real_pp_binom_times\<close>, (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
|
walther@60358
|
248 |
\<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
|
walther@60358
|
249 |
\<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
|
walther@60358
|
250 |
\<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
|
walther@60358
|
251 |
\<^rule_thm>\<open>realpow_mul\<close>, (*(a*b) \<up> n = a \<up> n * b \<up> n*)
|
walther@60358
|
252 |
|
walther@60358
|
253 |
\<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
|
walther@60358
|
254 |
\<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
|
walther@60358
|
255 |
\<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
|
walther@60358
|
256 |
|
Walther@60515
|
257 |
\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
|
Walther@60515
|
258 |
\<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
|
Walther@60515
|
259 |
\<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
|
walther@60358
|
260 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
walther@60358
|
261 |
\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
|
Walther@60515
|
262 |
\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
|
walther@60358
|
263 |
|
walther@60358
|
264 |
\<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
|
walther@60358
|
265 |
\<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
|
walther@60358
|
266 |
\<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
|
walther@60358
|
267 |
|
walther@60385
|
268 |
\<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==>l * n + m * n = (l + m) * n"*)
|
walther@60385
|
269 |
\<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
|
walther@60385
|
270 |
\<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
|
walther@60385
|
271 |
\<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
|
walther@60358
|
272 |
|
Walther@60515
|
273 |
\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
|
Walther@60515
|
274 |
\<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
|
Walther@60515
|
275 |
\<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
|
walther@60358
|
276 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
walther@60358
|
277 |
\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
|
Walther@60515
|
278 |
\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
|
walther@60358
|
279 |
scr = Rule.Empty_Prog});
|
wneuper@59472
|
280 |
\<close>
|
wenzelm@60289
|
281 |
rule_set_knowledge expand_rootbinoms = expand_rootbinoms
|
walther@60278
|
282 |
ML \<open>
|
walther@60278
|
283 |
\<close> ML \<open>
|
walther@60278
|
284 |
\<close> ML \<open>
|
walther@60278
|
285 |
\<close>
|
neuper@37906
|
286 |
end
|