|
1 (* collecting all knowledge for Root |
|
2 created by: |
|
3 date: |
|
4 changed by: rlang |
|
5 last change by: rlang |
|
6 date: 02.10.24 |
|
7 *) |
|
8 |
|
9 (* use"../knowledge/Root.ML"; |
|
10 use"Knowledge/Root.ML"; |
|
11 use"Root.ML"; |
|
12 |
|
13 remove_thy"Root"; |
|
14 use_thy"Knowledge/Isac"; |
|
15 |
|
16 use"ROOT.ML"; |
|
17 cd"knowledge"; |
|
18 *) |
|
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 = |
|
25 (case arg of |
|
26 Free (n1,t1) => |
|
27 (case int_of_str n1 of |
|
28 SOME ni => |
|
29 if ni < 0 then NONE |
|
30 else |
|
31 let val fact = squfact ni; |
|
32 in if fact*fact = ni |
|
33 then SOME ("#sqrt #"^(string_of_int ni)^" = #" |
|
34 ^(string_of_int (if ni = 0 then 0 |
|
35 else ni div fact)), |
|
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))^")"), |
|
42 Trueprop $ |
|
43 (mk_equality |
|
44 (t, |
|
45 (mk_factroot op0 t1 fact |
|
46 (ni div (fact*fact)))))) |
|
47 end |
|
48 | NONE => NONE) |
|
49 | _ => NONE) |
|
50 |
|
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; |
|
56 *) |
|
57 |
|
58 calclist':= overwritel (!calclist', |
|
59 [("SQRT" ,("Root.sqrt" ,eval_sqrt "#sqrt_")) |
|
60 (*different types for 'sqrt 4' --- 'Calculate sqrt_'*) |
|
61 ]); |
|
62 |
|
63 |
|
64 local (* Vers. 7.10.99.A *) |
|
65 |
|
66 open Term; (* for type order = EQUAL | LESS | GREATER *) |
|
67 |
|
68 fun pr_ord EQUAL = "EQUAL" |
|
69 | pr_ord LESS = "LESS" |
|
70 | pr_ord GREATER = "GREATER"; |
|
71 |
|
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) = |
|
88 (if pr then |
|
89 let |
|
90 val (f, ts) = strip_comb t and (g, us) = strip_comb u; |
|
91 val _=writeln("t= f@ts= \""^ |
|
92 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^ |
|
93 (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\""); |
|
94 val _=writeln("u= g@us= \""^ |
|
95 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ |
|
96 (commas(map(Syntax.string_of_term (thy2ctxt 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("-------"); |
|
104 in () end |
|
105 else (); |
|
106 case int_ord (size_of_term' t, size_of_term' u) of |
|
107 EQUAL => |
|
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) |
|
110 | ord => ord) |
|
111 end |
|
112 | ord => ord) |
|
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); |
|
117 |
|
118 in |
|
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 |
|
123 *) |
|
124 |
|
125 (*args |
|
126 pr: print trace, WN0509 'sqrt_right true' not used anymore |
|
127 thy: |
|
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 ); |
|
132 end; |
|
133 |
|
134 rew_ord' := overwritel (!rew_ord', |
|
135 [("termlessI", termlessI), |
|
136 ("sqrt_right", sqrt_right false (theory "Pure")) |
|
137 ]); |
|
138 |
|
139 (*-------------------------rulse-------------------------*) |
|
140 val Root_crls = |
|
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_") |
|
150 ]; |
|
151 |
|
152 val Root_erls = |
|
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_") |
|
162 ]; |
|
163 |
|
164 ruleset' := overwritelthy thy (!ruleset', |
|
165 [("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*) |
|
166 ]); |
|
167 |
|
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, |
|
172 calc = [], |
|
173 (*asm_thm = [],*) |
|
174 rules = [Thm ("real_diff_minus",num_str real_diff_minus), |
|
175 (*"a - b = a + (-1) * b"*) |
|
176 |
|
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"*) |
|
185 |
|
186 Thm ("real_mult_1",num_str real_mult_1), |
|
187 (*"1 * z = z"*) |
|
188 Thm ("real_mult_0",num_str real_mult_0), |
|
189 (*"0 * z = 0"*) |
|
190 Thm ("real_add_zero_left",num_str real_add_zero_left), |
|
191 (*"0 + z = z"*) |
|
192 |
|
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), (**) |
|
199 |
|
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"*) |
|
208 |
|
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"*) |
|
217 |
|
218 Calc ("op +", eval_binop "#add_"), |
|
219 Calc ("op *", eval_binop "#mult_"), |
|
220 Calc ("Atools.pow", eval_binop "#power_") |
|
221 ], |
|
222 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
223 }:rls); |
|
224 ruleset' := overwritelthy thy (!ruleset', |
|
225 [("make_rooteq", make_rooteq) |
|
226 ]); |
|
227 |
|
228 val expand_rootbinoms = prep_rls( |
|
229 Rls{id = "expand_rootbinoms", preconds = [], |
|
230 rew_ord = ("termlessI",termlessI), |
|
231 erls = Atools_erls, srls = Erls, |
|
232 calc = [], |
|
233 (*asm_thm = [],*) |
|
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"*) |
|
246 (*RL 020915*) |
|
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*) |
|
257 |
|
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"*) |
|
261 |
|
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_"), |
|
268 |
|
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"*) |
|
275 |
|
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"*) |
|
284 |
|
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_") |
|
291 ], |
|
292 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
293 }:rls); |
|
294 |
|
295 |
|
296 ruleset' := overwritelthy thy (!ruleset', |
|
297 [("expand_rootbinoms", expand_rootbinoms) |
|
298 ]); |
|
299 "******* Root.ML end *******"; |