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@60269
|
47 |
fun eval_sqrt (_ : string) (_ : string) (t as
|
walther@60269
|
48 |
(Const(op0, _) $ arg)) _(*thy*) =
|
neuper@37950
|
49 |
(case arg of
|
neuper@37950
|
50 |
Free (n1,t1) =>
|
walther@59875
|
51 |
(case TermC.int_opt_of_string n1 of
|
neuper@37950
|
52 |
SOME ni =>
|
neuper@37950
|
53 |
if ni < 0 then NONE
|
neuper@37950
|
54 |
else
|
walther@59878
|
55 |
let val fact = Eval.squfact ni;
|
neuper@37950
|
56 |
in if fact*fact = ni
|
neuper@37950
|
57 |
then SOME ("#sqrt #"^(string_of_int ni)^" = #"
|
neuper@37950
|
58 |
^(string_of_int (if ni = 0 then 0
|
neuper@37950
|
59 |
else ni div fact)),
|
wneuper@59390
|
60 |
HOLogic.Trueprop $ TermC.mk_equality (t, TermC.term_of_num t1 fact))
|
neuper@37950
|
61 |
else if fact = 1 then NONE
|
neuper@37950
|
62 |
else SOME ("#sqrt #"^(string_of_int ni)^" = sqrt (#"
|
neuper@37950
|
63 |
^(string_of_int fact)^" * #"
|
neuper@37950
|
64 |
^(string_of_int fact)^" * #"
|
neuper@37950
|
65 |
^(string_of_int (ni div (fact*fact))^")"),
|
wneuper@59390
|
66 |
HOLogic.Trueprop $
|
wneuper@59389
|
67 |
(TermC.mk_equality
|
neuper@37950
|
68 |
(t,
|
wneuper@59389
|
69 |
(TermC.mk_factroot op0 t1 fact
|
neuper@37950
|
70 |
(ni div (fact*fact))))))
|
neuper@37950
|
71 |
end
|
neuper@37950
|
72 |
| NONE => NONE)
|
neuper@37950
|
73 |
| _ => NONE)
|
neuper@37950
|
74 |
|
neuper@37950
|
75 |
| eval_sqrt _ _ _ _ = NONE;
|
walther@59997
|
76 |
(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", str2term "sqrt 0");
|
neuper@37950
|
77 |
> eval_sqrt thmid op_ t thy;
|
neuper@37950
|
78 |
> val Free (n1,t1) = arg;
|
neuper@37950
|
79 |
> val SOME ni = int_of_str n1;
|
neuper@37950
|
80 |
*)
|
wneuper@59472
|
81 |
\<close>
|
wneuper@59472
|
82 |
setup \<open>KEStore_Elems.add_calcs
|
s1210629013@52145
|
83 |
[("SQRT", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))
|
wneuper@59472
|
84 |
(*different types for 'sqrt 4' --- 'Calculate SQRT'*)]\<close>
|
wneuper@59472
|
85 |
ML \<open>
|
neuper@37950
|
86 |
local (* Vers. 7.10.99.A *)
|
neuper@37950
|
87 |
|
neuper@37950
|
88 |
open Term; (* for type order = EQUAL | LESS | GREATER *)
|
neuper@37950
|
89 |
|
neuper@37950
|
90 |
fun pr_ord EQUAL = "EQUAL"
|
neuper@37950
|
91 |
| pr_ord LESS = "LESS"
|
neuper@37950
|
92 |
| pr_ord GREATER = "GREATER";
|
neuper@37950
|
93 |
|
neuper@37950
|
94 |
fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
|
neuper@37982
|
95 |
(case a of "NthRoot.sqrt" => ((("|||", 0), T), 0) (*WN greatest *)
|
neuper@37950
|
96 |
| _ => (((a, 0), T), 0))
|
neuper@37950
|
97 |
| dest_hd' (Free (a, T)) = (((a, 0), T), 1)
|
neuper@37950
|
98 |
| dest_hd' (Var v) = (v, 2)
|
neuper@37950
|
99 |
| dest_hd' (Bound i) = ((("", i), dummyT), 3)
|
walther@60269
|
100 |
| dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
|
walther@60269
|
101 |
| dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";
|
neuper@37950
|
102 |
fun size_of_term' (Const(str,_) $ t) =
|
neuper@37982
|
103 |
(case str of "NthRoot.sqrt" => (1000 + size_of_term' t)
|
neuper@37950
|
104 |
| _ => 1 + size_of_term' t)
|
neuper@37950
|
105 |
| size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
|
neuper@37950
|
106 |
| size_of_term' (f $ t) = size_of_term' f + size_of_term' t
|
neuper@37950
|
107 |
| size_of_term' _ = 1;
|
neuper@37950
|
108 |
fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
|
neuper@38053
|
109 |
(case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
|
neuper@38053
|
110 |
| ord => ord)
|
walther@60269
|
111 |
| term_ord' pr _(*thy*) (t, u) =
|
neuper@38053
|
112 |
(if pr then
|
neuper@37950
|
113 |
let
|
neuper@38053
|
114 |
val (f, ts) = strip_comb t and (g, us) = strip_comb u;
|
walther@59868
|
115 |
val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^"\" @ \"[" ^
|
walther@59868
|
116 |
commas (map UnparseC.term ts) ^ "]\"");
|
walther@59868
|
117 |
val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
|
walther@59868
|
118 |
commas (map UnparseC.term us) ^ "]\"");
|
neuper@38053
|
119 |
val _ = tracing ("size_of_term(t,u)= (" ^
|
neuper@38053
|
120 |
string_of_int(size_of_term' t) ^", " ^
|
neuper@38053
|
121 |
string_of_int(size_of_term' u) ^")");
|
neuper@38053
|
122 |
val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
|
neuper@38053
|
123 |
val _ = tracing ("terms_ord(ts,us) = " ^
|
neuper@38053
|
124 |
(pr_ord o terms_ord str false) (ts,us));
|
neuper@38053
|
125 |
val _=tracing("-------");
|
neuper@37950
|
126 |
in () end
|
neuper@38053
|
127 |
else ();
|
neuper@38053
|
128 |
case int_ord (size_of_term' t, size_of_term' u) of
|
neuper@38053
|
129 |
EQUAL =>
|
neuper@38053
|
130 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
|
neuper@38053
|
131 |
(case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
|
neuper@38053
|
132 |
| ord => ord)
|
neuper@38053
|
133 |
end
|
neuper@38053
|
134 |
| ord => ord)
|
neuper@37950
|
135 |
and hd_ord (f, g) = (* ~ term.ML *)
|
neuper@37982
|
136 |
prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
|
neuper@37982
|
137 |
(dest_hd' f, dest_hd' g)
|
walther@60269
|
138 |
and terms_ord _(*str*) pr (ts, us) =
|
walther@59881
|
139 |
list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
|
neuper@37950
|
140 |
|
neuper@37950
|
141 |
in
|
neuper@37950
|
142 |
(* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
|
neuper@37950
|
143 |
by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1
|
neuper@37950
|
144 |
(2) hd_ord: greater to right, 'sqrt' < numerals < variables
|
neuper@37950
|
145 |
(3) terms_ord: recurs. on args, greater to right
|
neuper@37950
|
146 |
*)
|
neuper@37950
|
147 |
|
neuper@37950
|
148 |
(*args
|
neuper@37950
|
149 |
pr: print trace, WN0509 'sqrt_right true' not used anymore
|
neuper@37950
|
150 |
thy:
|
neuper@37950
|
151 |
subst: no bound variables, only Root.sqrt
|
neuper@37950
|
152 |
tu: the terms to compare (t1, t2) ... *)
|
walther@59910
|
153 |
fun sqrt_right (pr:bool) thy (_: subst) tu =
|
neuper@37950
|
154 |
(term_ord' pr thy(***) tu = LESS );
|
neuper@37950
|
155 |
end;
|
neuper@37950
|
156 |
|
walther@59857
|
157 |
Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
|
neuper@37950
|
158 |
[("termlessI", termlessI),
|
wneuper@59397
|
159 |
("sqrt_right", sqrt_right false @{theory "Pure"})
|
neuper@37950
|
160 |
]);
|
neuper@37950
|
161 |
|
neuper@37950
|
162 |
(*-------------------------rulse-------------------------*)
|
neuper@37950
|
163 |
val Root_crls =
|
walther@59852
|
164 |
Rule_Set.append_rules "Root_crls" Atools_erls
|
walther@59871
|
165 |
[Rule.Thm ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
|
wenzelm@60294
|
166 |
\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
|
wenzelm@60294
|
167 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
wenzelm@60294
|
168 |
\<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
|
wenzelm@60294
|
169 |
\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
|
wenzelm@60294
|
170 |
\<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
|
wenzelm@60294
|
171 |
\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
|
wenzelm@60294
|
172 |
\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")
|
neuper@37950
|
173 |
];
|
neuper@37950
|
174 |
|
neuper@37950
|
175 |
val Root_erls =
|
walther@59852
|
176 |
Rule_Set.append_rules "Root_erls" Atools_erls
|
walther@59871
|
177 |
[Rule.Thm ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
|
wenzelm@60294
|
178 |
\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
|
wenzelm@60294
|
179 |
\<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
wenzelm@60294
|
180 |
\<^rule_eval>\<open>Transcendental.powr\<close> (**)(eval_binop "#power_"),
|
wenzelm@60294
|
181 |
\<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(eval_binop "#add_"),
|
wenzelm@60294
|
182 |
\<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(eval_binop "#sub_"),
|
wenzelm@60294
|
183 |
\<^rule_eval>\<open>Groups.times_class.times\<close> (**)(eval_binop "#mult_"),
|
wenzelm@60294
|
184 |
\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")
|
neuper@37950
|
185 |
];
|
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,
|
wenzelm@60291
|
192 |
rew_ord = ("sqrt_right", sqrt_right false \<^theory>),
|
walther@59851
|
193 |
erls = Atools_erls, srls = Rule_Set.Empty,
|
neuper@42451
|
194 |
calc = [], errpatts = [],
|
walther@59871
|
195 |
rules = [Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
|
neuper@37950
|
196 |
(*"a - b = a + (-1) * b"*)
|
neuper@37950
|
197 |
|
walther@59871
|
198 |
Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
|
neuper@37950
|
199 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
walther@59871
|
200 |
Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
|
neuper@37950
|
201 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
walther@59871
|
202 |
Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
|
neuper@37950
|
203 |
(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
|
walther@59871
|
204 |
Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
|
neuper@37950
|
205 |
(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
|
neuper@37950
|
206 |
|
walther@59871
|
207 |
Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
|
neuper@37950
|
208 |
(*"1 * z = z"*)
|
walther@59871
|
209 |
Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
|
neuper@37950
|
210 |
(*"0 * z = 0"*)
|
walther@59871
|
211 |
Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
|
neuper@37950
|
212 |
(*"0 + z = z"*)
|
neuper@37950
|
213 |
|
walther@59877
|
214 |
Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
|
neuper@37950
|
215 |
(*AC-rewriting*)
|
walther@59871
|
216 |
Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
|
neuper@37950
|
217 |
(**)
|
walther@59877
|
218 |
Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
|
neuper@37950
|
219 |
(**)
|
walther@59877
|
220 |
Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
|
neuper@37950
|
221 |
(**)
|
walther@59877
|
222 |
Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
|
neuper@37950
|
223 |
(**)
|
walther@59877
|
224 |
Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
|
neuper@37950
|
225 |
(**)
|
neuper@37950
|
226 |
|
wneuper@59416
|
227 |
Rule.Thm ("sym_realpow_twoI",
|
walther@59871
|
228 |
ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
|
walther@60260
|
229 |
(*"r1 * r1 = r1 \<up> 2"*)
|
walther@59871
|
230 |
Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
|
walther@60260
|
231 |
(*"r * r \<up> n = r \<up> (n + 1)"*)
|
wneuper@59416
|
232 |
Rule.Thm ("sym_real_mult_2",
|
walther@59871
|
233 |
ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
|
neuper@37950
|
234 |
(*"z1 + z1 = 2 * z1"*)
|
walther@59871
|
235 |
Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
|
neuper@37950
|
236 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37950
|
237 |
|
walther@59871
|
238 |
Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
|
neuper@37950
|
239 |
(*"[| l is_const; m is_const |]==> l * n + m * n = (l + m) * n"*)
|
walther@59871
|
240 |
Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
|
neuper@37950
|
241 |
(*"[| l is_const; m is_const |] ==>
|
neuper@37950
|
242 |
l * n + (m * n + k) = (l + m) * n + k"*)
|
walther@59871
|
243 |
Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
|
neuper@37950
|
244 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
walther@59871
|
245 |
Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
|
neuper@37950
|
246 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37950
|
247 |
|
wenzelm@60294
|
248 |
\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
|
wenzelm@60294
|
249 |
\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
|
wenzelm@60294
|
250 |
\<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
|
neuper@37950
|
251 |
],
|
walther@59878
|
252 |
scr = Rule.Empty_Prog
|
wneuper@59406
|
253 |
});
|
wneuper@59472
|
254 |
\<close>
|
wenzelm@60289
|
255 |
rule_set_knowledge make_rooteq = make_rooteq
|
wneuper@59472
|
256 |
ML \<open>
|
neuper@37950
|
257 |
|
walther@59618
|
258 |
val prep_rls' = Auto_Prog.prep_rls @{theory};
|
s1210629013@55444
|
259 |
|
s1210629013@55444
|
260 |
val expand_rootbinoms = prep_rls'(
|
walther@59851
|
261 |
Rule_Def.Repeat{id = "expand_rootbinoms", preconds = [],
|
neuper@37950
|
262 |
rew_ord = ("termlessI",termlessI),
|
walther@59851
|
263 |
erls = Atools_erls, srls = Rule_Set.Empty,
|
neuper@42451
|
264 |
calc = [], errpatts = [],
|
walther@59871
|
265 |
rules = [Rule.Thm ("real_plus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
|
walther@60260
|
266 |
(*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
|
walther@59871
|
267 |
Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
|
neuper@37950
|
268 |
(*"(a + b)*(a + b) = ...*)
|
walther@59871
|
269 |
Rule.Thm ("real_minus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
|
walther@60260
|
270 |
(*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
|
walther@59871
|
271 |
Rule.Thm ("real_minus_binom_times",ThmC.numerals_to_Free @{thm real_minus_binom_times}),
|
neuper@37950
|
272 |
(*"(a - b)*(a - b) = ...*)
|
walther@59871
|
273 |
Rule.Thm ("real_plus_minus_binom1",ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),
|
walther@60260
|
274 |
(*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
|
walther@59871
|
275 |
Rule.Thm ("real_plus_minus_binom2",ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
|
walther@60260
|
276 |
(*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
|
neuper@37950
|
277 |
(*RL 020915*)
|
walther@59871
|
278 |
Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}),
|
neuper@37950
|
279 |
(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
|
walther@59871
|
280 |
Rule.Thm ("real_pm_binom_times",ThmC.numerals_to_Free @{thm real_pm_binom_times}),
|
neuper@37950
|
281 |
(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
|
walther@59871
|
282 |
Rule.Thm ("real_mp_binom_times",ThmC.numerals_to_Free @{thm real_mp_binom_times}),
|
neuper@37950
|
283 |
(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
|
walther@59871
|
284 |
Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}),
|
neuper@37950
|
285 |
(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
|
walther@59871
|
286 |
Rule.Thm ("realpow_mul",ThmC.numerals_to_Free @{thm realpow_mul}),
|
walther@60260
|
287 |
(*(a*b) \<up> n = a \<up> n * b \<up> n*)
|
neuper@37950
|
288 |
|
walther@59871
|
289 |
Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}), (*"1 * z = z"*)
|
walther@59871
|
290 |
Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}), (*"0 * z = 0"*)
|
walther@59871
|
291 |
Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
|
neuper@37950
|
292 |
(*"0 + z = z"*)
|
neuper@37950
|
293 |
|
wenzelm@60294
|
294 |
\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
|
wenzelm@60294
|
295 |
\<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
|
wenzelm@60294
|
296 |
\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
|
wenzelm@60294
|
297 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
wenzelm@60294
|
298 |
\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
|
wenzelm@60294
|
299 |
\<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
|
neuper@37950
|
300 |
|
wneuper@59416
|
301 |
Rule.Thm ("sym_realpow_twoI",
|
walther@59871
|
302 |
ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
|
walther@60260
|
303 |
(*"r1 * r1 = r1 \<up> 2"*)
|
walther@59871
|
304 |
Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
|
walther@60260
|
305 |
(*"r * r \<up> n = r \<up> (n + 1)"*)
|
walther@59871
|
306 |
Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
|
neuper@37950
|
307 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37950
|
308 |
|
walther@59871
|
309 |
Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
|
neuper@37950
|
310 |
(*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
|
walther@59871
|
311 |
Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
|
neuper@37950
|
312 |
(*"[| l is_const; m is_const |] ==>
|
neuper@37950
|
313 |
l * n + (m * n + k) = (l + m) * n + k"*)
|
walther@59871
|
314 |
Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
|
neuper@37950
|
315 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
walther@59871
|
316 |
Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
|
neuper@37950
|
317 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37950
|
318 |
|
wenzelm@60294
|
319 |
\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
|
wenzelm@60294
|
320 |
\<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
|
wenzelm@60294
|
321 |
\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
|
wenzelm@60294
|
322 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
wenzelm@60294
|
323 |
\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
|
wenzelm@60294
|
324 |
\<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
|
neuper@37950
|
325 |
],
|
walther@59878
|
326 |
scr = Rule.Empty_Prog
|
wneuper@59406
|
327 |
});
|
wneuper@59472
|
328 |
\<close>
|
wenzelm@60289
|
329 |
rule_set_knowledge expand_rootbinoms = expand_rootbinoms
|
walther@60278
|
330 |
ML \<open>
|
walther@60278
|
331 |
\<close> ML \<open>
|
walther@60278
|
332 |
\<close> ML \<open>
|
walther@60278
|
333 |
\<close>
|
neuper@37906
|
334 |
end
|