1 (* collecting all knowledge for Root
9 (* use"../knowledge/Root.ML";
10 use"IsacKnowledge/Root.ML";
14 use_thy"IsacKnowledge/Isac";
19 "******* Root.ML begin *******";
20 theory' := overwritel (!theory', [("Root.thy",Root.thy)]);
21 (*-------------------------functions---------------------*)
22 (*evaluation square-root over the integers*)
23 fun eval_sqrt (thmid:string) (op_:string) (t as
24 (Const(op0,t0) $ arg)) thy =
27 (case int_of_str n1 of
31 let val fact = squfact ni;
33 then Some ("#sqrt #"^(string_of_int ni)^" = #"
34 ^(string_of_int (if ni = 0 then 0
36 Trueprop $ mk_equality (t, term_of_num t1 fact))
37 else if fact = 1 then None
38 else Some ("#sqrt #"^(string_of_int ni)^" = sqrt (#"
39 ^(string_of_int fact)^" * #"
40 ^(string_of_int fact)^" * #"
41 ^(string_of_int (ni div (fact*fact))^")"),
45 (mk_factroot op0 t1 fact
46 (ni div (fact*fact))))))
51 | eval_sqrt _ _ _ _ = None;
52 (*val (thmid, op_, t as Const(op0,t0) $ arg) = ("","", str2term "sqrt 0");
53 > eval_sqrt thmid op_ t thy;
54 > val Free (n1,t1) = arg;
55 > val Some ni = int_of_str n1;
58 calclist':= overwritel (!calclist',
59 [("SQRT" ,("Root.sqrt" ,eval_sqrt "#sqrt_"))
60 (*different types for 'sqrt 4' --- 'Calculate sqrt_'*)
64 local (* Vers. 7.10.99.A *)
66 open Term; (* for type order = EQUAL | LESS | GREATER *)
68 fun pr_ord EQUAL = "EQUAL"
69 | pr_ord LESS = "LESS"
70 | pr_ord GREATER = "GREATER";
72 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
73 (case a of "Root.sqrt" => ((("|||", 0), T), 0) (*WN greatest *)
74 | _ => (((a, 0), T), 0))
75 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
76 | dest_hd' (Var v) = (v, 2)
77 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
78 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
79 fun size_of_term' (Const(str,_) $ t) =
80 (case str of "Root.sqrt" => (1000 + size_of_term' t)
81 | _ => 1 + size_of_term' t)
82 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
83 | size_of_term' (f $ t) = size_of_term' f + size_of_term' t
84 | size_of_term' _ = 1;
85 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
86 (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
87 | term_ord' pr thy (t, u) =
90 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
91 val _=writeln("t= f@ts= \""^
92 ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
93 (commas(map(string_of_cterm o cterm_of (sign_of thy)) ts))^"]\"");
94 val _=writeln("u= g@us= \""^
95 ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
96 (commas(map(string_of_cterm o cterm_of (sign_of thy)) us))^"]\"");
97 val _=writeln("size_of_term(t,u)= ("^
98 (string_of_int(size_of_term' t))^", "^
99 (string_of_int(size_of_term' u))^")");
100 val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
101 val _=writeln("terms_ord(ts,us) = "^
102 ((pr_ord o terms_ord str false)(ts,us)));
103 val _=writeln("-------");
106 case int_ord (size_of_term' t, size_of_term' u) of
108 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
109 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
113 and hd_ord (f, g) = (* ~ term.ML *)
114 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
115 and terms_ord str pr (ts, us) =
116 list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
119 (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
120 by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1
121 (2) hd_ord: greater to right, 'sqrt' < numerals < variables
122 (3) terms_ord: recurs. on args, greater to right
126 pr: print trace, WN0509 'sqrt_right true' not used anymore
128 subst: no bound variables, only Root.sqrt
129 tu: the terms to compare (t1, t2) ... *)
130 fun sqrt_right (pr:bool) thy (_:subst) tu =
131 (term_ord' pr thy(***) tu = LESS );
134 rew_ord' := overwritel (!rew_ord',
135 [("termlessI", termlessI),
136 ("sqrt_right", sqrt_right false ProtoPure.thy)
139 (*-------------------------rulse-------------------------*)
141 append_rls "Root_crls" Atools_erls
142 [Thm ("real_unari_minus",num_str real_unari_minus),
143 Calc ("Root.sqrt" ,eval_sqrt "#sqrt_"),
144 Calc ("HOL.divide",eval_cancel "#divide_"),
145 Calc ("Atools.pow" ,eval_binop "#power_"),
146 Calc ("op +", eval_binop "#add_"),
147 Calc ("op -", eval_binop "#sub_"),
148 Calc ("op *", eval_binop "#mult_"),
149 Calc ("op =",eval_equal "#equal_")
153 append_rls "Root_erls" Atools_erls
154 [Thm ("real_unari_minus",num_str real_unari_minus),
155 Calc ("Root.sqrt" ,eval_sqrt "#sqrt_"),
156 Calc ("HOL.divide",eval_cancel "#divide_"),
157 Calc ("Atools.pow" ,eval_binop "#power_"),
158 Calc ("op +", eval_binop "#add_"),
159 Calc ("op -", eval_binop "#sub_"),
160 Calc ("op *", eval_binop "#mult_"),
161 Calc ("op =",eval_equal "#equal_")
164 ruleset' := overwritelthy thy (!ruleset',
165 [("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*)
168 val make_rooteq = prep_rls(
169 Rls{id = "make_rooteq", preconds = []:term list,
170 rew_ord = ("sqrt_right", sqrt_right false Root.thy),
171 erls = Atools_erls, srls = Erls,
174 rules = [Thm ("real_diff_minus",num_str real_diff_minus),
175 (*"a - b = a + (-1) * b"*)
177 Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
178 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
179 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
180 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
181 Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
182 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
183 Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
184 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
186 Thm ("real_mult_1",num_str real_mult_1),
188 Thm ("real_mult_0",num_str real_mult_0),
190 Thm ("real_add_zero_left",num_str real_add_zero_left),
193 Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
194 Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
195 Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
196 Thm ("real_add_commute",num_str real_add_commute), (**)
197 Thm ("real_add_left_commute",num_str real_add_left_commute), (**)
198 Thm ("real_add_assoc",num_str real_add_assoc), (**)
200 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
201 (*"r1 * r1 = r1 ^^^ 2"*)
202 Thm ("realpow_plus_1",num_str realpow_plus_1),
203 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
204 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
205 (*"z1 + z1 = 2 * z1"*)
206 Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
207 (*"z1 + (z1 + k) = 2 * z1 + k"*)
209 Thm ("real_num_collect",num_str real_num_collect),
210 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
211 Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
212 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
213 Thm ("real_one_collect",num_str real_one_collect),
214 (*"m is_const ==> n + m * n = (1 + m) * n"*)
215 Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
216 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
218 Calc ("op +", eval_binop "#add_"),
219 Calc ("op *", eval_binop "#mult_"),
220 Calc ("Atools.pow", eval_binop "#power_")
222 scr = Script ((term_of o the o (parse thy)) "empty_script")
224 ruleset' := overwritelthy thy (!ruleset',
225 [("make_rooteq", make_rooteq)
228 val expand_rootbinoms = prep_rls(
229 Rls{id = "expand_rootbinoms", preconds = [],
230 rew_ord = ("termlessI",termlessI),
231 erls = Atools_erls, srls = Erls,
234 rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
235 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
236 Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
237 (*"(a + b)*(a + b) = ...*)
238 Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
239 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
240 Thm ("real_minus_binom_times",num_str real_minus_binom_times),
241 (*"(a - b)*(a - b) = ...*)
242 Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
243 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
244 Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
245 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
247 Thm ("real_pp_binom_times",num_str real_pp_binom_times),
248 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
249 Thm ("real_pm_binom_times",num_str real_pm_binom_times),
250 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
251 Thm ("real_mp_binom_times",num_str real_mp_binom_times),
252 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
253 Thm ("real_mm_binom_times",num_str real_mm_binom_times),
254 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
255 Thm ("realpow_mul",num_str realpow_mul),
256 (*(a*b)^^^n = a^^^n * b^^^n*)
258 Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
259 Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
260 Thm ("real_add_zero_left",num_str real_add_zero_left), (*"0 + z = z"*)
262 Calc ("op +", eval_binop "#add_"),
263 Calc ("op -", eval_binop "#sub_"),
264 Calc ("op *", eval_binop "#mult_"),
265 Calc ("HOL.divide" ,eval_cancel "#divide_"),
266 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
267 Calc ("Atools.pow", eval_binop "#power_"),
269 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
270 (*"r1 * r1 = r1 ^^^ 2"*)
271 Thm ("realpow_plus_1",num_str realpow_plus_1),
272 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
273 Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
274 (*"z1 + (z1 + k) = 2 * z1 + k"*)
276 Thm ("real_num_collect",num_str real_num_collect),
277 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
278 Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
279 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
280 Thm ("real_one_collect",num_str real_one_collect),
281 (*"m is_const ==> n + m * n = (1 + m) * n"*)
282 Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
283 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
285 Calc ("op +", eval_binop "#add_"),
286 Calc ("op -", eval_binop "#sub_"),
287 Calc ("op *", eval_binop "#mult_"),
288 Calc ("HOL.divide" ,eval_cancel "#divide_"),
289 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
290 Calc ("Atools.pow", eval_binop "#power_")
292 scr = Script ((term_of o the o (parse thy)) "empty_script")
296 ruleset' := overwritelthy thy (!ruleset',
297 [("expand_rootbinoms", expand_rootbinoms)
299 "******* Root.ML end *******";