1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/Root.ML Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,299 @@
1.4 +(* collecting all knowledge for Root
1.5 + created by:
1.6 + date:
1.7 + changed by: rlang
1.8 + last change by: rlang
1.9 + date: 02.10.24
1.10 +*)
1.11 +
1.12 +(* use"../knowledge/Root.ML";
1.13 + use"Knowledge/Root.ML";
1.14 + use"Root.ML";
1.15 +
1.16 + remove_thy"Root";
1.17 + use_thy"Knowledge/Isac";
1.18 +
1.19 + use"ROOT.ML";
1.20 + cd"knowledge";
1.21 + *)
1.22 +"******* Root.ML begin *******";
1.23 +theory' := overwritel (!theory', [("Root.thy",Root.thy)]);
1.24 +(*-------------------------functions---------------------*)
1.25 +(*evaluation square-root over the integers*)
1.26 +fun eval_sqrt (thmid:string) (op_:string) (t as
1.27 + (Const(op0,t0) $ arg)) thy =
1.28 + (case arg of
1.29 + Free (n1,t1) =>
1.30 + (case int_of_str n1 of
1.31 + SOME ni =>
1.32 + if ni < 0 then NONE
1.33 + else
1.34 + let val fact = squfact ni;
1.35 + in if fact*fact = ni
1.36 + then SOME ("#sqrt #"^(string_of_int ni)^" = #"
1.37 + ^(string_of_int (if ni = 0 then 0
1.38 + else ni div fact)),
1.39 + Trueprop $ mk_equality (t, term_of_num t1 fact))
1.40 + else if fact = 1 then NONE
1.41 + else SOME ("#sqrt #"^(string_of_int ni)^" = sqrt (#"
1.42 + ^(string_of_int fact)^" * #"
1.43 + ^(string_of_int fact)^" * #"
1.44 + ^(string_of_int (ni div (fact*fact))^")"),
1.45 + Trueprop $
1.46 + (mk_equality
1.47 + (t,
1.48 + (mk_factroot op0 t1 fact
1.49 + (ni div (fact*fact))))))
1.50 + end
1.51 + | NONE => NONE)
1.52 + | _ => NONE)
1.53 +
1.54 + | eval_sqrt _ _ _ _ = NONE;
1.55 +(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("","", str2term "sqrt 0");
1.56 +> eval_sqrt thmid op_ t thy;
1.57 +> val Free (n1,t1) = arg;
1.58 +> val SOME ni = int_of_str n1;
1.59 +*)
1.60 +
1.61 +calclist':= overwritel (!calclist',
1.62 + [("SQRT" ,("Root.sqrt" ,eval_sqrt "#sqrt_"))
1.63 + (*different types for 'sqrt 4' --- 'Calculate sqrt_'*)
1.64 + ]);
1.65 +
1.66 +
1.67 +local (* Vers. 7.10.99.A *)
1.68 +
1.69 +open Term; (* for type order = EQUAL | LESS | GREATER *)
1.70 +
1.71 +fun pr_ord EQUAL = "EQUAL"
1.72 + | pr_ord LESS = "LESS"
1.73 + | pr_ord GREATER = "GREATER";
1.74 +
1.75 +fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
1.76 + (case a of "Root.sqrt" => ((("|||", 0), T), 0) (*WN greatest *)
1.77 + | _ => (((a, 0), T), 0))
1.78 + | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
1.79 + | dest_hd' (Var v) = (v, 2)
1.80 + | dest_hd' (Bound i) = ((("", i), dummyT), 3)
1.81 + | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
1.82 +fun size_of_term' (Const(str,_) $ t) =
1.83 + (case str of "Root.sqrt" => (1000 + size_of_term' t)
1.84 + | _ => 1 + size_of_term' t)
1.85 + | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1.86 + | size_of_term' (f $ t) = size_of_term' f + size_of_term' t
1.87 + | size_of_term' _ = 1;
1.88 +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.89 + (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
1.90 + | term_ord' pr thy (t, u) =
1.91 + (if pr then
1.92 + let
1.93 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.94 + val _=writeln("t= f@ts= \""^
1.95 + ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
1.96 + (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
1.97 + val _=writeln("u= g@us= \""^
1.98 + ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
1.99 + (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
1.100 + val _=writeln("size_of_term(t,u)= ("^
1.101 + (string_of_int(size_of_term' t))^", "^
1.102 + (string_of_int(size_of_term' u))^")");
1.103 + val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
1.104 + val _=writeln("terms_ord(ts,us) = "^
1.105 + ((pr_ord o terms_ord str false)(ts,us)));
1.106 + val _=writeln("-------");
1.107 + in () end
1.108 + else ();
1.109 + case int_ord (size_of_term' t, size_of_term' u) of
1.110 + EQUAL =>
1.111 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1.112 + (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
1.113 + | ord => ord)
1.114 + end
1.115 + | ord => ord)
1.116 +and hd_ord (f, g) = (* ~ term.ML *)
1.117 + prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.118 +and terms_ord str pr (ts, us) =
1.119 + list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
1.120 +
1.121 +in
1.122 +(* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
1.123 + by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1
1.124 + (2) hd_ord: greater to right, 'sqrt' < numerals < variables
1.125 + (3) terms_ord: recurs. on args, greater to right
1.126 +*)
1.127 +
1.128 +(*args
1.129 + pr: print trace, WN0509 'sqrt_right true' not used anymore
1.130 + thy:
1.131 + subst: no bound variables, only Root.sqrt
1.132 + tu: the terms to compare (t1, t2) ... *)
1.133 +fun sqrt_right (pr:bool) thy (_:subst) tu =
1.134 + (term_ord' pr thy(***) tu = LESS );
1.135 +end;
1.136 +
1.137 +rew_ord' := overwritel (!rew_ord',
1.138 +[("termlessI", termlessI),
1.139 + ("sqrt_right", sqrt_right false (theory "Pure"))
1.140 + ]);
1.141 +
1.142 +(*-------------------------rulse-------------------------*)
1.143 +val Root_crls =
1.144 + append_rls "Root_crls" Atools_erls
1.145 + [Thm ("real_unari_minus",num_str real_unari_minus),
1.146 + Calc ("Root.sqrt" ,eval_sqrt "#sqrt_"),
1.147 + Calc ("HOL.divide",eval_cancel "#divide_"),
1.148 + Calc ("Atools.pow" ,eval_binop "#power_"),
1.149 + Calc ("op +", eval_binop "#add_"),
1.150 + Calc ("op -", eval_binop "#sub_"),
1.151 + Calc ("op *", eval_binop "#mult_"),
1.152 + Calc ("op =",eval_equal "#equal_")
1.153 + ];
1.154 +
1.155 +val Root_erls =
1.156 + append_rls "Root_erls" Atools_erls
1.157 + [Thm ("real_unari_minus",num_str real_unari_minus),
1.158 + Calc ("Root.sqrt" ,eval_sqrt "#sqrt_"),
1.159 + Calc ("HOL.divide",eval_cancel "#divide_"),
1.160 + Calc ("Atools.pow" ,eval_binop "#power_"),
1.161 + Calc ("op +", eval_binop "#add_"),
1.162 + Calc ("op -", eval_binop "#sub_"),
1.163 + Calc ("op *", eval_binop "#mult_"),
1.164 + Calc ("op =",eval_equal "#equal_")
1.165 + ];
1.166 +
1.167 +ruleset' := overwritelthy thy (!ruleset',
1.168 + [("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*)
1.169 + ]);
1.170 +
1.171 +val make_rooteq = prep_rls(
1.172 + Rls{id = "make_rooteq", preconds = []:term list,
1.173 + rew_ord = ("sqrt_right", sqrt_right false Root.thy),
1.174 + erls = Atools_erls, srls = Erls,
1.175 + calc = [],
1.176 + (*asm_thm = [],*)
1.177 + rules = [Thm ("real_diff_minus",num_str real_diff_minus),
1.178 + (*"a - b = a + (-1) * b"*)
1.179 +
1.180 + Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.181 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.182 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.183 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.184 + Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
1.185 + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.186 + Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
1.187 + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.188 +
1.189 + Thm ("real_mult_1",num_str real_mult_1),
1.190 + (*"1 * z = z"*)
1.191 + Thm ("real_mult_0",num_str real_mult_0),
1.192 + (*"0 * z = 0"*)
1.193 + Thm ("real_add_zero_left",num_str real_add_zero_left),
1.194 + (*"0 + z = z"*)
1.195 +
1.196 + Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
1.197 + Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
1.198 + Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
1.199 + Thm ("real_add_commute",num_str real_add_commute), (**)
1.200 + Thm ("real_add_left_commute",num_str real_add_left_commute), (**)
1.201 + Thm ("real_add_assoc",num_str real_add_assoc), (**)
1.202 +
1.203 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.204 + (*"r1 * r1 = r1 ^^^ 2"*)
1.205 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.206 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.207 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.208 + (*"z1 + z1 = 2 * z1"*)
1.209 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.210 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.211 +
1.212 + Thm ("real_num_collect",num_str real_num_collect),
1.213 + (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.214 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.215 + (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.216 + Thm ("real_one_collect",num_str real_one_collect),
1.217 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.218 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.219 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.220 +
1.221 + Calc ("op +", eval_binop "#add_"),
1.222 + Calc ("op *", eval_binop "#mult_"),
1.223 + Calc ("Atools.pow", eval_binop "#power_")
1.224 + ],
1.225 + scr = Script ((term_of o the o (parse thy)) "empty_script")
1.226 + }:rls);
1.227 +ruleset' := overwritelthy thy (!ruleset',
1.228 + [("make_rooteq", make_rooteq)
1.229 + ]);
1.230 +
1.231 +val expand_rootbinoms = prep_rls(
1.232 + Rls{id = "expand_rootbinoms", preconds = [],
1.233 + rew_ord = ("termlessI",termlessI),
1.234 + erls = Atools_erls, srls = Erls,
1.235 + calc = [],
1.236 + (*asm_thm = [],*)
1.237 + rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
1.238 + (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1.239 + Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.240 + (*"(a + b)*(a + b) = ...*)
1.241 + Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
1.242 + (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1.243 + Thm ("real_minus_binom_times",num_str real_minus_binom_times),
1.244 + (*"(a - b)*(a - b) = ...*)
1.245 + Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
1.246 + (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1.247 + Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
1.248 + (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1.249 + (*RL 020915*)
1.250 + Thm ("real_pp_binom_times",num_str real_pp_binom_times),
1.251 + (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1.252 + Thm ("real_pm_binom_times",num_str real_pm_binom_times),
1.253 + (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1.254 + Thm ("real_mp_binom_times",num_str real_mp_binom_times),
1.255 + (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
1.256 + Thm ("real_mm_binom_times",num_str real_mm_binom_times),
1.257 + (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
1.258 + Thm ("realpow_mul",num_str realpow_mul),
1.259 + (*(a*b)^^^n = a^^^n * b^^^n*)
1.260 +
1.261 + Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
1.262 + Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
1.263 + Thm ("real_add_zero_left",num_str real_add_zero_left), (*"0 + z = z"*)
1.264 +
1.265 + Calc ("op +", eval_binop "#add_"),
1.266 + Calc ("op -", eval_binop "#sub_"),
1.267 + Calc ("op *", eval_binop "#mult_"),
1.268 + Calc ("HOL.divide" ,eval_cancel "#divide_"),
1.269 + Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
1.270 + Calc ("Atools.pow", eval_binop "#power_"),
1.271 +
1.272 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.273 + (*"r1 * r1 = r1 ^^^ 2"*)
1.274 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.275 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.276 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.277 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.278 +
1.279 + Thm ("real_num_collect",num_str real_num_collect),
1.280 + (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.281 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.282 + (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.283 + Thm ("real_one_collect",num_str real_one_collect),
1.284 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.285 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.286 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.287 +
1.288 + Calc ("op +", eval_binop "#add_"),
1.289 + Calc ("op -", eval_binop "#sub_"),
1.290 + Calc ("op *", eval_binop "#mult_"),
1.291 + Calc ("HOL.divide" ,eval_cancel "#divide_"),
1.292 + Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
1.293 + Calc ("Atools.pow", eval_binop "#power_")
1.294 + ],
1.295 + scr = Script ((term_of o the o (parse thy)) "empty_script")
1.296 + }:rls);
1.297 +
1.298 +
1.299 +ruleset' := overwritelthy thy (!ruleset',
1.300 + [("expand_rootbinoms", expand_rootbinoms)
1.301 + ]);
1.302 +"******* Root.ML end *******";