1.1 --- a/src/Tools/isac/IsacKnowledge/Root.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,299 +0,0 @@
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"IsacKnowledge/Root.ML";
1.14 - use"Root.ML";
1.15 -
1.16 - remove_thy"Root";
1.17 - use_thy"IsacKnowledge/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 *******";