1 (* theory collecting all knowledge for Root
9 theory Root imports Poly begin
13 (*sqrt :: "real => real" Isabelle "NthRoot.sqrt"*)
14 nroot :: "[real, real] => real"
16 axiomatization where (*.not contained in Isabelle2002,
17 stated as axioms, TODO: prove as theorems;
18 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
20 root_plus_minus: "0 <= b ==>
21 (a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))" and
22 root_false: "b < 0 ==> (a^^^2 = b) = False" and
24 (* for expand_rootbinom *)
25 real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
26 real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
27 real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
28 real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
29 real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
30 real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
31 realpow_mul: "(a*b)^^^n = a^^^n * b^^^n" and
33 real_diff_minus: "a - b = a + (-1) * b" and
34 real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
35 real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
36 real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
37 real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
38 real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
39 real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
41 real_root_positive: "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)" and
42 real_root_negative: "a < 0 ==> (x ^^^ 2 = a) = False"
47 (*-------------------------functions---------------------*)
48 (*evaluation square-root over the integers*)
49 fun eval_sqrt (thmid:string) (op_:string) (t as
50 (Const(op0,t0) $ arg)) thy =
53 (case TermC.int_of_str_opt n1 of
57 let val fact = TermC.squfact ni;
59 then SOME ("#sqrt #"^(string_of_int ni)^" = #"
60 ^(string_of_int (if ni = 0 then 0
62 HOLogic.Trueprop $ TermC.mk_equality (t, TermC.term_of_num t1 fact))
63 else if fact = 1 then NONE
64 else SOME ("#sqrt #"^(string_of_int ni)^" = sqrt (#"
65 ^(string_of_int fact)^" * #"
66 ^(string_of_int fact)^" * #"
67 ^(string_of_int (ni div (fact*fact))^")"),
71 (TermC.mk_factroot op0 t1 fact
72 (ni div (fact*fact))))))
77 | eval_sqrt _ _ _ _ = NONE;
78 (*val (thmid, op_, t as Const(op0,t0) $ arg) = ("","", str2term "sqrt 0");
79 > eval_sqrt thmid op_ t thy;
80 > val Free (n1,t1) = arg;
81 > val SOME ni = int_of_str n1;
84 setup {* KEStore_Elems.add_calcs
85 [("SQRT", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))
86 (*different types for 'sqrt 4' --- 'Calculate SQRT'*)] *}
88 local (* Vers. 7.10.99.A *)
90 open Term; (* for type order = EQUAL | LESS | GREATER *)
92 fun pr_ord EQUAL = "EQUAL"
93 | pr_ord LESS = "LESS"
94 | pr_ord GREATER = "GREATER";
96 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
97 (case a of "NthRoot.sqrt" => ((("|||", 0), T), 0) (*WN greatest *)
98 | _ => (((a, 0), T), 0))
99 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
100 | dest_hd' (Var v) = (v, 2)
101 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
102 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
103 fun size_of_term' (Const(str,_) $ t) =
104 (case str of "NthRoot.sqrt" => (1000 + size_of_term' t)
105 | _ => 1 + size_of_term' t)
106 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
107 | size_of_term' (f $ t) = size_of_term' f + size_of_term' t
108 | size_of_term' _ = 1;
109 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
110 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
112 | term_ord' pr thy (t, u) =
115 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
116 val _ = tracing ("t= f@ts= \"" ^ term2str f ^"\" @ \"[" ^
117 commas (map term2str ts) ^ "]\"");
118 val _ = tracing ("u= g@us= \"" ^ term2str g ^"\" @ \"[" ^
119 commas (map term2str us) ^ "]\"");
120 val _ = tracing ("size_of_term(t,u)= (" ^
121 string_of_int(size_of_term' t) ^", " ^
122 string_of_int(size_of_term' u) ^")");
123 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
124 val _ = tracing ("terms_ord(ts,us) = " ^
125 (pr_ord o terms_ord str false) (ts,us));
126 val _=tracing("-------");
129 case int_ord (size_of_term' t, size_of_term' u) of
131 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
132 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
136 and hd_ord (f, g) = (* ~ term.ML *)
137 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
138 (dest_hd' f, dest_hd' g)
139 and terms_ord str pr (ts, us) =
140 list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
143 (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
144 by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1
145 (2) hd_ord: greater to right, 'sqrt' < numerals < variables
146 (3) terms_ord: recurs. on args, greater to right
150 pr: print trace, WN0509 'sqrt_right true' not used anymore
152 subst: no bound variables, only Root.sqrt
153 tu: the terms to compare (t1, t2) ... *)
154 fun sqrt_right (pr:bool) thy (_:subst) tu =
155 (term_ord' pr thy(***) tu = LESS );
158 rew_ord' := overwritel (!rew_ord',
159 [("termlessI", termlessI),
160 ("sqrt_right", sqrt_right false @{theory "Pure"})
163 (*-------------------------rulse-------------------------*)
165 append_rls "Root_crls" Atools_erls
166 [Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),
167 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
168 Calc ("Rings.divide_class.divide",eval_cancel "#divide_e"),
169 Calc ("Atools.pow" ,eval_binop "#power_"),
170 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
171 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
172 Calc ("Groups.times_class.times", eval_binop "#mult_"),
173 Calc ("HOL.eq",eval_equal "#equal_")
177 append_rls "Root_erls" Atools_erls
178 [Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),
179 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
180 Calc ("Rings.divide_class.divide",eval_cancel "#divide_e"),
181 Calc ("Atools.pow" ,eval_binop "#power_"),
182 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
183 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
184 Calc ("Groups.times_class.times", eval_binop "#mult_"),
185 Calc ("HOL.eq",eval_equal "#equal_")
188 setup {* KEStore_Elems.add_rlss [("Root_erls", (Context.theory_name @{theory}, Root_erls))] *}
191 val make_rooteq = prep_rls'(
192 Rls{id = "make_rooteq", preconds = []:term list,
193 rew_ord = ("sqrt_right", sqrt_right false thy),
194 erls = Atools_erls, srls = Erls,
195 calc = [], errpatts = [],
196 rules = [Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
197 (*"a - b = a + (-1) * b"*)
199 Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
200 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
201 Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
202 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
203 Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
204 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
205 Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
206 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
208 Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
210 Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
212 Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
215 Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
217 Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
219 Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
221 Thm ("add_commute",TermC.num_str @{thm add.commute}),
223 Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
225 Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
228 Thm ("sym_realpow_twoI",
229 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
230 (*"r1 * r1 = r1 ^^^ 2"*)
231 Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
232 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
233 Thm ("sym_real_mult_2",
234 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
235 (*"z1 + z1 = 2 * z1"*)
236 Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
237 (*"z1 + (z1 + k) = 2 * z1 + k"*)
239 Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
240 (*"[| l is_const; m is_const |]==> l * n + m * n = (l + m) * n"*)
241 Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
242 (*"[| l is_const; m is_const |] ==>
243 l * n + (m * n + k) = (l + m) * n + k"*)
244 Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
245 (*"m is_const ==> n + m * n = (1 + m) * n"*)
246 Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
247 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
249 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
250 Calc ("Groups.times_class.times", eval_binop "#mult_"),
251 Calc ("Atools.pow", eval_binop "#power_")
253 scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
256 setup {* KEStore_Elems.add_rlss [("make_rooteq", (Context.theory_name @{theory}, make_rooteq))] *}
259 val prep_rls' = LTool.prep_rls @{theory};
261 val expand_rootbinoms = prep_rls'(
262 Rls{id = "expand_rootbinoms", preconds = [],
263 rew_ord = ("termlessI",termlessI),
264 erls = Atools_erls, srls = Erls,
265 calc = [], errpatts = [],
266 rules = [Thm ("real_plus_binom_pow2" ,TermC.num_str @{thm real_plus_binom_pow2}),
267 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
268 Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),
269 (*"(a + b)*(a + b) = ...*)
270 Thm ("real_minus_binom_pow2" ,TermC.num_str @{thm real_minus_binom_pow2}),
271 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
272 Thm ("real_minus_binom_times",TermC.num_str @{thm real_minus_binom_times}),
273 (*"(a - b)*(a - b) = ...*)
274 Thm ("real_plus_minus_binom1",TermC.num_str @{thm real_plus_minus_binom1}),
275 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
276 Thm ("real_plus_minus_binom2",TermC.num_str @{thm real_plus_minus_binom2}),
277 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
279 Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}),
280 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
281 Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}),
282 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
283 Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}),
284 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
285 Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}),
286 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
287 Thm ("realpow_mul",TermC.num_str @{thm realpow_mul}),
288 (*(a*b)^^^n = a^^^n * b^^^n*)
290 Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}), (*"1 * z = z"*)
291 Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}), (*"0 * z = 0"*)
292 Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
295 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
296 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
297 Calc ("Groups.times_class.times", eval_binop "#mult_"),
298 Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
299 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
300 Calc ("Atools.pow", eval_binop "#power_"),
302 Thm ("sym_realpow_twoI",
303 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
304 (*"r1 * r1 = r1 ^^^ 2"*)
305 Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
306 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
307 Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
308 (*"z1 + (z1 + k) = 2 * z1 + k"*)
310 Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
311 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
312 Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
313 (*"[| l is_const; m is_const |] ==>
314 l * n + (m * n + k) = (l + m) * n + k"*)
315 Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
316 (*"m is_const ==> n + m * n = (1 + m) * n"*)
317 Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
318 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
320 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
321 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
322 Calc ("Groups.times_class.times", eval_binop "#mult_"),
323 Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
324 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
325 Calc ("Atools.pow", eval_binop "#power_")
327 scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
330 setup {* KEStore_Elems.add_rlss
331 [("expand_rootbinoms", (Context.theory_name @{theory}, expand_rootbinoms))] *}