1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/Test.ML Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,1301 @@
1.4 +(* SML functions for rational arithmetic
1.5 + WN.22.10.99
1.6 + use"../knowledge/Test.ML";
1.7 + use"Knowledge/Test.ML";
1.8 + use"Test.ML";
1.9 + *)
1.10 +
1.11 +
1.12 +(** interface isabelle -- isac **)
1.13 +
1.14 +theory' := overwritel (!theory', [("Test.thy",Test.thy)]);
1.15 +
1.16 +(** evaluation of numerals and predicates **)
1.17 +
1.18 +(*does a term contain a root ?*)
1.19 +fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy =
1.20 + if strip_thy op0 <> "is'_root'_free"
1.21 + then raise error ("eval_root_free: wrong "^op0)
1.22 + else if const_in (strip_thy op0) arg
1.23 + then SOME (mk_thmid thmid ""
1.24 + ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1.25 + Trueprop $ (mk_equality (t, false_as_term)))
1.26 + else SOME (mk_thmid thmid ""
1.27 + ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1.28 + Trueprop $ (mk_equality (t, true_as_term)))
1.29 + | eval_root_free _ _ _ _ = NONE;
1.30 +
1.31 +(*does a term contain a root ?*)
1.32 +fun eval_contains_root (thmid:string) _
1.33 + (t as (Const("Test.contains'_root",t0) $ arg)) thy =
1.34 + if member op = (ids_of arg) "sqrt"
1.35 + then SOME (mk_thmid thmid ""
1.36 + ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1.37 + Trueprop $ (mk_equality (t, true_as_term)))
1.38 + else SOME (mk_thmid thmid ""
1.39 + ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1.40 + Trueprop $ (mk_equality (t, false_as_term)))
1.41 + | eval_contains_root _ _ _ _ = NONE;
1.42 +
1.43 +calclist':= overwritel (!calclist',
1.44 + [("is_root_free", ("Test.is'_root'_free",
1.45 + eval_root_free"#is_root_free_")),
1.46 + ("contains_root", ("Test.contains'_root",
1.47 + eval_contains_root"#contains_root_"))
1.48 + ]);
1.49 +
1.50 +(** term order **)
1.51 +fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
1.52 +
1.53 +(** rule sets **)
1.54 +
1.55 +val testerls =
1.56 + Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
1.57 + erls = e_rls, srls = Erls,
1.58 + calc = [],
1.59 + rules = [Thm ("refl",num_str refl),
1.60 + Thm ("le_refl",num_str le_refl),
1.61 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
1.62 + Thm ("not_true",num_str not_true),
1.63 + Thm ("not_false",num_str not_false),
1.64 + Thm ("and_true",and_true),
1.65 + Thm ("and_false",and_false),
1.66 + Thm ("or_true",or_true),
1.67 + Thm ("or_false",or_false),
1.68 + Thm ("and_commute",num_str and_commute),
1.69 + Thm ("or_commute",num_str or_commute),
1.70 +
1.71 + Calc ("Atools.is'_const",eval_const "#is_const_"),
1.72 + Calc ("Tools.matches",eval_matches ""),
1.73 +
1.74 + Calc ("op +",eval_binop "#add_"),
1.75 + Calc ("op *",eval_binop "#mult_"),
1.76 + Calc ("Atools.pow" ,eval_binop "#power_"),
1.77 +
1.78 + Calc ("op <",eval_equ "#less_"),
1.79 + Calc ("op <=",eval_equ "#less_equal_"),
1.80 +
1.81 + Calc ("Atools.ident",eval_ident "#ident_")],
1.82 + scr = Script ((term_of o the o (parse thy))
1.83 + "empty_script")
1.84 + }:rls;
1.85 +
1.86 +(*.for evaluation of conditions in rewrite rules.*)
1.87 +(*FIXXXXXXME 10.8.02: handle like _simplify*)
1.88 +val tval_rls =
1.89 + Rls{id = "tval_rls", preconds = [],
1.90 + rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),
1.91 + erls=testerls,srls = e_rls,
1.92 + calc=[],
1.93 + rules = [Thm ("refl",num_str refl),
1.94 + Thm ("le_refl",num_str le_refl),
1.95 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
1.96 + Thm ("not_true",num_str not_true),
1.97 + Thm ("not_false",num_str not_false),
1.98 + Thm ("and_true",and_true),
1.99 + Thm ("and_false",and_false),
1.100 + Thm ("or_true",or_true),
1.101 + Thm ("or_false",or_false),
1.102 + Thm ("and_commute",num_str and_commute),
1.103 + Thm ("or_commute",num_str or_commute),
1.104 +
1.105 + Thm ("real_diff_minus",num_str real_diff_minus),
1.106 +
1.107 + Thm ("root_ge0",num_str root_ge0),
1.108 + Thm ("root_add_ge0",num_str root_add_ge0),
1.109 + Thm ("root_ge0_1",num_str root_ge0_1),
1.110 + Thm ("root_ge0_2",num_str root_ge0_2),
1.111 +
1.112 + Calc ("Atools.is'_const",eval_const "#is_const_"),
1.113 + Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_"),
1.114 + Calc ("Tools.matches",eval_matches ""),
1.115 + Calc ("Test.contains'_root",
1.116 + eval_contains_root"#contains_root_"),
1.117 +
1.118 + Calc ("op +",eval_binop "#add_"),
1.119 + Calc ("op *",eval_binop "#mult_"),
1.120 + Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
1.121 + Calc ("Atools.pow" ,eval_binop "#power_"),
1.122 +
1.123 + Calc ("op <",eval_equ "#less_"),
1.124 + Calc ("op <=",eval_equ "#less_equal_"),
1.125 +
1.126 + Calc ("Atools.ident",eval_ident "#ident_")],
1.127 + scr = Script ((term_of o the o (parse thy))
1.128 + "empty_script")
1.129 + }:rls;
1.130 +
1.131 +
1.132 +ruleset' := overwritelthy thy (!ruleset',
1.133 + [("testerls", prep_rls testerls)
1.134 + ]);
1.135 +
1.136 +
1.137 +(*make () dissappear*)
1.138 +val rearrange_assoc =
1.139 + Rls{id = "rearrange_assoc", preconds = [],
1.140 + rew_ord = ("e_rew_ord",e_rew_ord),
1.141 + erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
1.142 + rules =
1.143 + [Thm ("sym_radd_assoc",num_str (radd_assoc RS sym)),
1.144 + Thm ("sym_rmult_assoc",num_str (rmult_assoc RS sym))],
1.145 + scr = Script ((term_of o the o (parse thy))
1.146 + "empty_script")
1.147 + }:rls;
1.148 +
1.149 +val ac_plus_times =
1.150 + Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
1.151 + erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
1.152 + rules =
1.153 + [Thm ("radd_commute",radd_commute),
1.154 + Thm ("radd_left_commute",radd_left_commute),
1.155 + Thm ("radd_assoc",radd_assoc),
1.156 + Thm ("rmult_commute",rmult_commute),
1.157 + Thm ("rmult_left_commute",rmult_left_commute),
1.158 + Thm ("rmult_assoc",rmult_assoc)],
1.159 + scr = Script ((term_of o the o (parse thy))
1.160 + "empty_script")
1.161 + }:rls;
1.162 +
1.163 +(*todo: replace by Rewrite("rnorm_equation_add",num_str rnorm_equation_add)*)
1.164 +val norm_equation =
1.165 + Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.166 + erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
1.167 + rules = [Thm ("rnorm_equation_add",num_str rnorm_equation_add)
1.168 + ],
1.169 + scr = Script ((term_of o the o (parse thy))
1.170 + "empty_script")
1.171 + }:rls;
1.172 +
1.173 +(** rule sets **)
1.174 +
1.175 +val STest_simplify = (* vv--- not changed to real by parse*)
1.176 + "Script STest_simplify (t_::'z) = \
1.177 + \(Repeat\
1.178 + \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
1.179 + \ (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@ \
1.180 + \ (Try (Repeat (Rewrite rdistr_right_assoc False))) @@ \
1.181 + \ (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@\
1.182 + \ (Try (Repeat (Rewrite rdistr_div_right False))) @@ \
1.183 + \ (Try (Repeat (Rewrite rbinom_power_2 False))) @@ \
1.184 +
1.185 + \ (Try (Repeat (Rewrite radd_commute False))) @@ \
1.186 + \ (Try (Repeat (Rewrite radd_left_commute False))) @@ \
1.187 + \ (Try (Repeat (Rewrite radd_assoc False))) @@ \
1.188 + \ (Try (Repeat (Rewrite rmult_commute False))) @@ \
1.189 + \ (Try (Repeat (Rewrite rmult_left_commute False))) @@ \
1.190 + \ (Try (Repeat (Rewrite rmult_assoc False))) @@ \
1.191 +
1.192 + \ (Try (Repeat (Rewrite radd_real_const_eq False))) @@ \
1.193 + \ (Try (Repeat (Rewrite radd_real_const False))) @@ \
1.194 + \ (Try (Repeat (Calculate plus))) @@ \
1.195 + \ (Try (Repeat (Calculate times))) @@ \
1.196 + \ (Try (Repeat (Calculate divide_))) @@\
1.197 + \ (Try (Repeat (Calculate power_))) @@ \
1.198 +
1.199 + \ (Try (Repeat (Rewrite rcollect_right False))) @@ \
1.200 + \ (Try (Repeat (Rewrite rcollect_one_left False))) @@ \
1.201 + \ (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@ \
1.202 + \ (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@ \
1.203 +
1.204 + \ (Try (Repeat (Rewrite rshift_nominator False))) @@ \
1.205 + \ (Try (Repeat (Rewrite rcancel_den False))) @@ \
1.206 + \ (Try (Repeat (Rewrite rroot_square_inv False))) @@ \
1.207 + \ (Try (Repeat (Rewrite rroot_times_root False))) @@ \
1.208 + \ (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@ \
1.209 + \ (Try (Repeat (Rewrite rsqare False))) @@ \
1.210 + \ (Try (Repeat (Rewrite power_1 False))) @@ \
1.211 + \ (Try (Repeat (Rewrite rtwo_of_the_same False))) @@ \
1.212 + \ (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@ \
1.213 +
1.214 + \ (Try (Repeat (Rewrite rmult_1 False))) @@ \
1.215 + \ (Try (Repeat (Rewrite rmult_1_right False))) @@ \
1.216 + \ (Try (Repeat (Rewrite rmult_0 False))) @@ \
1.217 + \ (Try (Repeat (Rewrite rmult_0_right False))) @@ \
1.218 + \ (Try (Repeat (Rewrite radd_0 False))) @@ \
1.219 + \ (Try (Repeat (Rewrite radd_0_right False)))) \
1.220 + \ t_)";
1.221 +
1.222 +
1.223 +(* expects * distributed over + *)
1.224 +val Test_simplify =
1.225 + Rls{id = "Test_simplify", preconds = [],
1.226 + rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),
1.227 + erls = tval_rls, srls = e_rls,
1.228 + calc=[(*since 040209 filled by prep_rls*)],
1.229 + (*asm_thm = [],*)
1.230 + rules = [
1.231 + Thm ("real_diff_minus",num_str real_diff_minus),
1.232 + Thm ("radd_mult_distrib2",num_str radd_mult_distrib2),
1.233 + Thm ("rdistr_right_assoc",num_str rdistr_right_assoc),
1.234 + Thm ("rdistr_right_assoc_p",num_str rdistr_right_assoc_p),
1.235 + Thm ("rdistr_div_right",num_str rdistr_div_right),
1.236 + Thm ("rbinom_power_2",num_str rbinom_power_2),
1.237 +
1.238 + Thm ("radd_commute",num_str radd_commute),
1.239 + Thm ("radd_left_commute",num_str radd_left_commute),
1.240 + Thm ("radd_assoc",num_str radd_assoc),
1.241 + Thm ("rmult_commute",num_str rmult_commute),
1.242 + Thm ("rmult_left_commute",num_str rmult_left_commute),
1.243 + Thm ("rmult_assoc",num_str rmult_assoc),
1.244 +
1.245 + Thm ("radd_real_const_eq",num_str radd_real_const_eq),
1.246 + Thm ("radd_real_const",num_str radd_real_const),
1.247 + (* these 2 rules are invers to distr_div_right wrt. termination.
1.248 + thus they MUST be done IMMEDIATELY before calc *)
1.249 + Calc ("op +", eval_binop "#add_"),
1.250 + Calc ("op *", eval_binop "#mult_"),
1.251 + Calc ("HOL.divide", eval_cancel "#divide_"),
1.252 + Calc ("Atools.pow", eval_binop "#power_"),
1.253 +
1.254 + Thm ("rcollect_right",num_str rcollect_right),
1.255 + Thm ("rcollect_one_left",num_str rcollect_one_left),
1.256 + Thm ("rcollect_one_left_assoc",num_str rcollect_one_left_assoc),
1.257 + Thm ("rcollect_one_left_assoc_p",num_str rcollect_one_left_assoc_p),
1.258 +
1.259 + Thm ("rshift_nominator",num_str rshift_nominator),
1.260 + Thm ("rcancel_den",num_str rcancel_den),
1.261 + Thm ("rroot_square_inv",num_str rroot_square_inv),
1.262 + Thm ("rroot_times_root",num_str rroot_times_root),
1.263 + Thm ("rroot_times_root_assoc_p",num_str rroot_times_root_assoc_p),
1.264 + Thm ("rsqare",num_str rsqare),
1.265 + Thm ("power_1",num_str power_1),
1.266 + Thm ("rtwo_of_the_same",num_str rtwo_of_the_same),
1.267 + Thm ("rtwo_of_the_same_assoc_p",num_str rtwo_of_the_same_assoc_p),
1.268 +
1.269 + Thm ("rmult_1",num_str rmult_1),
1.270 + Thm ("rmult_1_right",num_str rmult_1_right),
1.271 + Thm ("rmult_0",num_str rmult_0),
1.272 + Thm ("rmult_0_right",num_str rmult_0_right),
1.273 + Thm ("radd_0",num_str radd_0),
1.274 + Thm ("radd_0_right",num_str radd_0_right)
1.275 + ],
1.276 + scr = Script ((term_of o the o (parse thy)) "empty_script")
1.277 + (*since 040209 filled by prep_rls: STest_simplify*)
1.278 + }:rls;
1.279 +
1.280 +
1.281 +
1.282 +
1.283 +
1.284 +(** rule sets **)
1.285 +
1.286 +
1.287 +
1.288 +(*isolate the root in a root-equation*)
1.289 +val isolate_root =
1.290 + Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.291 + erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
1.292 + rules = [Thm ("rroot_to_lhs",num_str rroot_to_lhs),
1.293 + Thm ("rroot_to_lhs_mult",num_str rroot_to_lhs_mult),
1.294 + Thm ("rroot_to_lhs_add_mult",num_str rroot_to_lhs_add_mult),
1.295 + Thm ("risolate_root_add",num_str risolate_root_add),
1.296 + Thm ("risolate_root_mult",num_str risolate_root_mult),
1.297 + Thm ("risolate_root_div",num_str risolate_root_div) ],
1.298 + scr = Script ((term_of o the o (parse thy))
1.299 + "empty_script")
1.300 + }:rls;
1.301 +
1.302 +(*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
1.303 +val isolate_bdv =
1.304 + Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.305 + erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
1.306 + rules =
1.307 + [Thm ("risolate_bdv_add",num_str risolate_bdv_add),
1.308 + Thm ("risolate_bdv_mult_add",num_str risolate_bdv_mult_add),
1.309 + Thm ("risolate_bdv_mult",num_str risolate_bdv_mult),
1.310 + Thm ("mult_square",num_str mult_square),
1.311 + Thm ("constant_square",num_str constant_square),
1.312 + Thm ("constant_mult_square",num_str constant_mult_square)
1.313 + ],
1.314 + scr = Script ((term_of o the o (parse thy))
1.315 + "empty_script")
1.316 + }:rls;
1.317 +
1.318 +
1.319 +
1.320 +
1.321 +(* association list for calculate_, calculate
1.322 + "op +" etc. not usable in scripts *)
1.323 +val calclist =
1.324 + [
1.325 + (*as Tools.ML*)
1.326 + ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
1.327 + ("matches",("Tools.matches",eval_matches "#matches_")),
1.328 + ("lhs" ,("Tools.lhs" ,eval_lhs "")),
1.329 + (*aus Atools.ML*)
1.330 + ("PLUS" ,("op +" ,eval_binop "#add_")),
1.331 + ("TIMES" ,("op *" ,eval_binop "#mult_")),
1.332 + ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
1.333 + ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
1.334 + ("is_const",("Atools.is'_const",eval_const "#is_const_")),
1.335 + ("le" ,("op <" ,eval_equ "#less_")),
1.336 + ("leq" ,("op <=" ,eval_equ "#less_equal_")),
1.337 + ("ident" ,("Atools.ident",eval_ident "#ident_")),
1.338 + (*von hier (ehem.SqRoot*)
1.339 + ("sqrt" ,("Root.sqrt" ,eval_sqrt "#sqrt_")),
1.340 + ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_")),
1.341 + ("Test.contains_root",("contains'_root",
1.342 + eval_contains_root"#contains_root_"))
1.343 + ];
1.344 +
1.345 +ruleset' := overwritelthy thy (!ruleset',
1.346 + [("Test_simplify", prep_rls Test_simplify),
1.347 + ("tval_rls", prep_rls tval_rls),
1.348 + ("isolate_root", prep_rls isolate_root),
1.349 + ("isolate_bdv", prep_rls isolate_bdv),
1.350 + ("matches",
1.351 + prep_rls (append_rls "matches" testerls
1.352 + [Calc ("Tools.matches",eval_matches "#matches_")]))
1.353 + ]);
1.354 +
1.355 +(** problem types **)
1.356 +store_pbt
1.357 + (prep_pbt Test.thy "pbl_test" [] e_pblID
1.358 + (["test"],
1.359 + [],
1.360 + e_rls, NONE, []));
1.361 +store_pbt
1.362 + (prep_pbt Test.thy "pbl_test_equ" [] e_pblID
1.363 + (["equation","test"],
1.364 + [("#Given" ,["equality e_","solveFor v_"]),
1.365 + ("#Where" ,["matches (?a = ?b) e_"]),
1.366 + ("#Find" ,["solutions v_i_"])
1.367 + ],
1.368 + assoc_rls "matches",
1.369 + SOME "solve (e_::bool, v_)", []));
1.370 +
1.371 +store_pbt
1.372 + (prep_pbt Test.thy "pbl_test_uni" [] e_pblID
1.373 + (["univariate","equation","test"],
1.374 + [("#Given" ,["equality e_","solveFor v_"]),
1.375 + ("#Where" ,["matches (?a = ?b) e_"]),
1.376 + ("#Find" ,["solutions v_i_"])
1.377 + ],
1.378 + assoc_rls "matches",
1.379 + SOME "solve (e_::bool, v_)", []));
1.380 +
1.381 +store_pbt
1.382 + (prep_pbt Test.thy "pbl_test_uni_lin" [] e_pblID
1.383 + (["linear","univariate","equation","test"],
1.384 + [("#Given" ,["equality e_","solveFor v_"]),
1.385 + ("#Where" ,["(matches ( v_ = 0) e_) | (matches ( ?b*v_ = 0) e_) |\
1.386 + \(matches (?a+v_ = 0) e_) | (matches (?a+?b*v_ = 0) e_) "]),
1.387 + ("#Find" ,["solutions v_i_"])
1.388 + ],
1.389 + assoc_rls "matches",
1.390 + SOME "solve (e_::bool, v_)", [["Test","solve_linear"]]));
1.391 +
1.392 +(*25.8.01 ------
1.393 +store_pbt
1.394 + (prep_pbt Test.thy
1.395 + (["Test.thy"],
1.396 + [("#Given" ,"boolTestGiven g_"),
1.397 + ("#Find" ,"boolTestFind f_")
1.398 + ],
1.399 + []));
1.400 +
1.401 +store_pbt
1.402 + (prep_pbt Test.thy
1.403 + (["testeq","Test.thy"],
1.404 + [("#Given" ,"boolTestGiven g_"),
1.405 + ("#Find" ,"boolTestFind f_")
1.406 + ],
1.407 + []));
1.408 +
1.409 +
1.410 +val ttt = (term_of o the o (parse Isac.thy)) "(matches ( v_ = 0) e_)";
1.411 +
1.412 + ------ 25.8.01*)
1.413 +
1.414 +
1.415 +(** methods **)
1.416 +store_met
1.417 + (prep_met Diff.thy "met_test" [] e_metID
1.418 + (["Test"],
1.419 + [],
1.420 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.421 + crls=Atools_erls, nrls=e_rls(*,
1.422 + asm_rls=[],asm_thm=[]*)}, "empty_script"));
1.423 +(*
1.424 +store_met
1.425 + (prep_met Script.thy
1.426 + (e_metID,(*empty method*)
1.427 + [],
1.428 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
1.429 + asm_rls=[],asm_thm=[]},
1.430 + "Undef"));*)
1.431 +store_met
1.432 + (prep_met Test.thy "met_test_solvelin" [] e_metID
1.433 + (["Test","solve_linear"]:metID,
1.434 + [("#Given" ,["equality e_","solveFor v_"]),
1.435 + ("#Where" ,["matches (?a = ?b) e_"]),
1.436 + ("#Find" ,["solutions v_i_"])
1.437 + ],
1.438 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,
1.439 + prls=assoc_rls "matches",
1.440 + calc=[],
1.441 + crls=tval_rls, nrls=Test_simplify},
1.442 + "Script Solve_linear (e_::bool) (v_::real)= \
1.443 + \(let e_ =\
1.444 + \ Repeat\
1.445 + \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.446 + \ (Rewrite_Set Test_simplify False))) e_\
1.447 + \ in [e_::bool])"
1.448 + )
1.449 +(*, prep_met Test.thy (*test for equations*)
1.450 + (["Test","testeq"]:metID,
1.451 + [("#Given" ,["boolTestGiven g_"]),
1.452 + ("#Find" ,["boolTestFind f_"])
1.453 + ],
1.454 + {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
1.455 + asm_thm=[("square_equation_left","")]},
1.456 + "Script Testeq (eq_::bool) = \
1.457 + \Repeat \
1.458 + \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False eq_)); \
1.459 + \ e_ = Try (Repeat (Rewrite square_equation_left True e_)); \
1.460 + \ e_ = Try (Repeat (Rewrite rmult_0 False e_)) \
1.461 + \ in e_) Until (is_root_free e_)" (*deleted*)
1.462 + )
1.463 +, ---------27.4.02*)
1.464 +);
1.465 +
1.466 +
1.467 +
1.468 +
1.469 +ruleset' := overwritelthy thy (!ruleset',
1.470 + [("norm_equation", prep_rls norm_equation),
1.471 + ("ac_plus_times", prep_rls ac_plus_times),
1.472 + ("rearrange_assoc", prep_rls rearrange_assoc)
1.473 + ]);
1.474 +
1.475 +
1.476 +fun bin_o (Const (op_,(Type ("fun",
1.477 + [Type (s2,[]),Type ("fun",
1.478 + [Type (s4,tl4),Type (s5,tl5)])])))) =
1.479 + if (s2=s4)andalso(s4=s5)then[op_]else[]
1.480 + | bin_o _ = [];
1.481 +
1.482 +fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)
1.483 + | bin_op t = bin_o t;
1.484 +fun is_bin_op t = ((bin_op t)<>[]);
1.485 +
1.486 +fun bin_op_arg1 ((Const (op_,(Type ("fun",
1.487 + [Type (s2,[]),Type ("fun",
1.488 + [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
1.489 + arg1;
1.490 +fun bin_op_arg2 ((Const (op_,(Type ("fun",
1.491 + [Type (s2,[]),Type ("fun",
1.492 + [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
1.493 + arg2;
1.494 +
1.495 +
1.496 +exception NO_EQUATION_TERM;
1.497 +fun is_equation ((Const ("op =",(Type ("fun",
1.498 + [Type (_,[]),Type ("fun",
1.499 + [Type (_,[]),Type ("bool",[])])])))) $ _ $ _)
1.500 + = true
1.501 + | is_equation _ = false;
1.502 +fun equ_lhs ((Const ("op =",(Type ("fun",
1.503 + [Type (_,[]),Type ("fun",
1.504 + [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
1.505 + = l
1.506 + | equ_lhs _ = raise NO_EQUATION_TERM;
1.507 +fun equ_rhs ((Const ("op =",(Type ("fun",
1.508 + [Type (_,[]),Type ("fun",
1.509 + [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
1.510 + = r
1.511 + | equ_rhs _ = raise NO_EQUATION_TERM;
1.512 +
1.513 +
1.514 +fun atom (Const (_,Type (_,[]))) = true
1.515 + | atom (Free (_,Type (_,[]))) = true
1.516 + | atom (Var (_,Type (_,[]))) = true
1.517 +(*| atom (_ (_,"?DUMMY" )) = true ..ML-error *)
1.518 + | atom((Const ("Bin.integ_of_bin",_)) $ _) = true
1.519 + | atom _ = false;
1.520 +
1.521 +fun varids (Const (s,Type (_,[]))) = [strip_thy s]
1.522 + | varids (Free (s,Type (_,[]))) = if is_no s then []
1.523 + else [strip_thy s]
1.524 + | varids (Var((s,_),Type (_,[]))) = [strip_thy s]
1.525 +(*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
1.526 + | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
1.527 + | varids (Abs(a,T,t)) = union op = [a] (varids t)
1.528 + | varids (t1 $ t2) = union op = (varids t1) (varids t2)
1.529 + | varids _ = [];
1.530 +(*> val t = term_of (hd (parse Diophant.thy "x"));
1.531 +val t = Free ("x","?DUMMY") : term
1.532 +> varids t;
1.533 +val it = [] : string list [] !!! *)
1.534 +
1.535 +
1.536 +fun bin_ops_only ((Const op_) $ t1 $ t2) =
1.537 + if(is_bin_op (Const op_))
1.538 + then(bin_ops_only t1)andalso(bin_ops_only t2)
1.539 + else false
1.540 + | bin_ops_only t =
1.541 + if atom t then true else bin_ops_only t;
1.542 +
1.543 +fun polynomial opl t bdVar = (* bdVar TODO *)
1.544 + subset op = (bin_op t, opl) andalso (bin_ops_only t);
1.545 +
1.546 +fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)
1.547 + andalso polynomial opl (equ_lhs t) bdVar
1.548 + andalso polynomial opl (equ_rhs t) bdVar
1.549 + andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
1.550 + subset op = (varids bdVar, varids (equ_lhs t)));
1.551 +
1.552 +(*fun max is =
1.553 + let fun max_ m [] = m
1.554 + | max_ m (i::is) = if m<i then max_ i is else max_ m is;
1.555 + in max_ (hd is) is end;
1.556 +> max [1,5,3,7,4,2];
1.557 +val it = 7 : int *)
1.558 +
1.559 +fun max (a,b) = if a < b then b else a;
1.560 +
1.561 +fun degree addl mul bdVar t =
1.562 +let
1.563 +fun deg _ _ v (Const (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
1.564 + | deg _ _ v (Free (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
1.565 + | deg _ _ v (Var((s,_),Type (_,[]))) = if v=strip_thy s then 1 else 0
1.566 +(*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
1.567 + | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0
1.568 + | deg addl mul v (h $ t1 $ t2) =
1.569 + if subset op = (bin_op h, addl)
1.570 + then max (deg addl mul v t1 ,deg addl mul v t2)
1.571 + else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)
1.572 +in if polynomial (addl @ [mul]) t bdVar
1.573 + then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option)
1.574 +end;
1.575 +fun degree_ addl mul bdVar t = (* do not export *)
1.576 + let fun opt (SOME i)= i
1.577 + | opt NONE = 0
1.578 +in opt (degree addl mul bdVar t) end;
1.579 +
1.580 +
1.581 +fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2;
1.582 +
1.583 +fun linear_equ addl mul bdVar t =
1.584 + if is_equation t
1.585 + then let val degl = degree_ addl mul bdVar (equ_lhs t);
1.586 + val degr = degree_ addl mul bdVar (equ_rhs t)
1.587 + in if (degl>0 orelse degr>0)andalso max(degl,degr)<2
1.588 + then true else false
1.589 + end
1.590 + else false;
1.591 +(* strip_thy op_ before *)
1.592 +fun is_div_op (dv,(Const (op_,(Type ("fun",
1.593 + [Type (s2,[]),Type ("fun",
1.594 + [Type (s4,tl4),Type (s5,tl5)])])))) )= (dv = strip_thy op_)
1.595 + | is_div_op _ = false;
1.596 +
1.597 +fun is_denom bdVar div_op t =
1.598 + let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
1.599 + | is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
1.600 + | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
1.601 + | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
1.602 + | is bool[v]dv (h$n$d) =
1.603 + if is_div_op(dv,h)
1.604 + then (is false[v]dv n)orelse(is true[v]dv d)
1.605 + else (is bool [v]dv n)orelse(is bool[v]dv d)
1.606 +in is false (varids bdVar) (strip_thy div_op) t end;
1.607 +
1.608 +
1.609 +fun rational t div_op bdVar =
1.610 + is_denom bdVar div_op t andalso bin_ops_only t;
1.611 +
1.612 +
1.613 +
1.614 +(** problem types **)
1.615 +
1.616 +store_pbt
1.617 + (prep_pbt Test.thy "pbl_test_uni_plain2" [] e_pblID
1.618 + (["plain_square","univariate","equation","test"],
1.619 + [("#Given" ,["equality e_","solveFor v_"]),
1.620 + ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |\
1.621 + \(matches ( ?b*v_ ^^^2 = 0) e_) |\
1.622 + \(matches (?a + v_ ^^^2 = 0) e_) |\
1.623 + \(matches ( v_ ^^^2 = 0) e_)"]),
1.624 + ("#Find" ,["solutions v_i_"])
1.625 + ],
1.626 + assoc_rls "matches",
1.627 + SOME "solve (e_::bool, v_)", [["Test","solve_plain_square"]]));
1.628 +(*
1.629 + val e_ = (term_of o the o (parse thy)) "e_::bool";
1.630 + val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
1.631 + val env = [(e_,ve)];
1.632 +
1.633 + val pre = (term_of o the o (parse thy))
1.634 + "(matches (a + b*v_ ^^^2 = 0, e_::bool)) |\
1.635 + \(matches ( b*v_ ^^^2 = 0, e_::bool)) |\
1.636 + \(matches (a + v_ ^^^2 = 0, e_::bool)) |\
1.637 + \(matches ( v_ ^^^2 = 0, e_::bool))";
1.638 + val prei = subst_atomic env pre;
1.639 + val cpre = (cterm_of thy) prei;
1.640 +
1.641 + val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;
1.642 +val ct = "True | False | False | False" : cterm
1.643 +
1.644 +> val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
1.645 +> val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
1.646 +> val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
1.647 +val ct = "True" : cterm
1.648 +
1.649 +*)
1.650 +
1.651 +store_pbt
1.652 + (prep_pbt Test.thy "pbl_test_uni_poly" [] e_pblID
1.653 + (["polynomial","univariate","equation","test"],
1.654 + [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
1.655 + ("#Where" ,["False"]),
1.656 + ("#Find" ,["solutions v_i_"])
1.657 + ],
1.658 + e_rls, SOME "solve (e_::bool, v_)", []));
1.659 +
1.660 +store_pbt
1.661 + (prep_pbt Test.thy "pbl_test_uni_poly_deg2" [] e_pblID
1.662 + (["degree_two","polynomial","univariate","equation","test"],
1.663 + [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
1.664 + ("#Find" ,["solutions v_i_"])
1.665 + ],
1.666 + e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));
1.667 +
1.668 +store_pbt
1.669 + (prep_pbt Test.thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
1.670 + (["pq_formula","degree_two","polynomial","univariate","equation","test"],
1.671 + [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
1.672 + ("#Find" ,["solutions v_i_"])
1.673 + ],
1.674 + e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));
1.675 +
1.676 +store_pbt
1.677 + (prep_pbt Test.thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
1.678 + (["abc_formula","degree_two","polynomial","univariate","equation","test"],
1.679 + [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_"]),
1.680 + ("#Find" ,["solutions v_i_"])
1.681 + ],
1.682 + e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_)", []));
1.683 +
1.684 +store_pbt
1.685 + (prep_pbt Test.thy "pbl_test_uni_root" [] e_pblID
1.686 + (["squareroot","univariate","equation","test"],
1.687 + [("#Given" ,["equality e_","solveFor v_"]),
1.688 + ("#Where" ,["contains_root (e_::bool)"]),
1.689 + ("#Find" ,["solutions v_i_"])
1.690 + ],
1.691 + append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
1.692 + eval_contains_root "#contains_root_")],
1.693 + SOME "solve (e_::bool, v_)", [["Test","square_equation"]]));
1.694 +
1.695 +store_pbt
1.696 + (prep_pbt Test.thy "pbl_test_uni_norm" [] e_pblID
1.697 + (["normalize","univariate","equation","test"],
1.698 + [("#Given" ,["equality e_","solveFor v_"]),
1.699 + ("#Where" ,[]),
1.700 + ("#Find" ,["solutions v_i_"])
1.701 + ],
1.702 + e_rls, SOME "solve (e_::bool, v_)", [["Test","norm_univar_equation"]]));
1.703 +
1.704 +store_pbt
1.705 + (prep_pbt Test.thy "pbl_test_uni_roottest" [] e_pblID
1.706 + (["sqroot-test","univariate","equation","test"],
1.707 + [("#Given" ,["equality e_","solveFor v_"]),
1.708 + (*("#Where" ,["contains_root (e_::bool)"]),*)
1.709 + ("#Find" ,["solutions v_i_"])
1.710 + ],
1.711 + e_rls, SOME "solve (e_::bool, v_)", []));
1.712 +
1.713 +(*
1.714 +(#ppc o get_pbt) ["sqroot-test","univariate","equation"];
1.715 + *)
1.716 +
1.717 +
1.718 +store_met
1.719 + (prep_met Test.thy "met_test_sqrt" [] e_metID
1.720 +(*root-equation, version for tests before 8.01.01*)
1.721 + (["Test","sqrt-equ-test"]:metID,
1.722 + [("#Given" ,["equality e_","solveFor v_"]),
1.723 + ("#Where" ,["contains_root (e_::bool)"]),
1.724 + ("#Find" ,["solutions v_i_"])
1.725 + ],
1.726 + {rew_ord'="e_rew_ord",rls'=tval_rls,
1.727 + srls =append_rls "srls_contains_root" e_rls
1.728 + [Calc ("Test.contains'_root",eval_contains_root "")],
1.729 + prls =append_rls "prls_contains_root" e_rls
1.730 + [Calc ("Test.contains'_root",eval_contains_root "")],
1.731 + calc=[],
1.732 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.733 + asm_thm=[("square_equation_left",""),
1.734 + ("square_equation_right","")]*)},
1.735 + "Script Solve_root_equation (e_::bool) (v_::real) = \
1.736 + \(let e_ = \
1.737 + \ ((While (contains_root e_) Do\
1.738 + \ ((Rewrite square_equation_left True) @@\
1.739 + \ (Try (Rewrite_Set Test_simplify False)) @@\
1.740 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
1.741 + \ (Try (Rewrite_Set isolate_root False)) @@\
1.742 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
1.743 + \ (Try (Rewrite_Set norm_equation False)) @@\
1.744 + \ (Try (Rewrite_Set Test_simplify False)) @@\
1.745 + \ (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.746 + \ (Try (Rewrite_Set Test_simplify False)))\
1.747 + \ e_\
1.748 + \ in [e_::bool])"
1.749 + ));
1.750 +
1.751 +store_met
1.752 + (prep_met Test.thy "met_test_sqrt2" [] e_metID
1.753 +(*root-equation ... for test-*.sml until 8.01*)
1.754 + (["Test","squ-equ-test2"]:metID,
1.755 + [("#Given" ,["equality e_","solveFor v_"]),
1.756 + ("#Find" ,["solutions v_i_"])
1.757 + ],
1.758 + {rew_ord'="e_rew_ord",rls'=tval_rls,
1.759 + srls = append_rls "srls_contains_root" e_rls
1.760 + [Calc ("Test.contains'_root",eval_contains_root"")],
1.761 + prls=e_rls,calc=[],
1.762 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.763 + asm_thm=[("square_equation_left",""),
1.764 + ("square_equation_right","")]*)},
1.765 + "Script Solve_root_equation (e_::bool) (v_::real) = \
1.766 + \(let e_ = \
1.767 + \ ((While (contains_root e_) Do\
1.768 + \ ((Rewrite square_equation_left True) @@\
1.769 + \ (Try (Rewrite_Set Test_simplify False)) @@\
1.770 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
1.771 + \ (Try (Rewrite_Set isolate_root False)) @@\
1.772 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
1.773 + \ (Try (Rewrite_Set norm_equation False)) @@\
1.774 + \ (Try (Rewrite_Set Test_simplify False)) @@\
1.775 + \ (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.776 + \ (Try (Rewrite_Set Test_simplify False)))\
1.777 + \ e_;\
1.778 + \ (L_::bool list) = Tac subproblem_equation_dummy; \
1.779 + \ L_ = Tac solve_equation_dummy \
1.780 + \ in Check_elementwise L_ {(v_::real). Assumptions})"
1.781 + ));
1.782 +
1.783 +store_met
1.784 + (prep_met Test.thy "met_test_squ_sub" [] e_metID
1.785 +(*tests subproblem fixed linear*)
1.786 + (["Test","squ-equ-test-subpbl1"]:metID,
1.787 + [("#Given" ,["equality e_","solveFor v_"]),
1.788 + ("#Find" ,["solutions v_i_"])
1.789 + ],
1.790 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
1.791 + crls=tval_rls, nrls=Test_simplify},
1.792 + "Script Solve_root_equation (e_::bool) (v_::real) = \
1.793 + \ (let e_ = ((Try (Rewrite_Set norm_equation False)) @@ \
1.794 + \ (Try (Rewrite_Set Test_simplify False))) e_; \
1.795 + \(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\
1.796 + \ [Test,solve_linear]) [bool_ e_, real_ v_])\
1.797 + \in Check_elementwise L_ {(v_::real). Assumptions})"
1.798 + ));
1.799 +
1.800 +store_met
1.801 + (prep_met Test.thy "met_test_squ_sub2" [] e_metID
1.802 + (*tests subproblem fixed degree 2*)
1.803 + (["Test","squ-equ-test-subpbl2"]:metID,
1.804 + [("#Given" ,["equality e_","solveFor v_"]),
1.805 + ("#Find" ,["solutions v_i_"])
1.806 + ],
1.807 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
1.808 + crls=tval_rls, nrls=e_rls(*,
1.809 + asm_rls=[],asm_thm=[("square_equation_left",""),
1.810 + ("square_equation_right","")]*)},
1.811 + "Script Solve_root_equation (e_::bool) (v_::real) = \
1.812 + \ (let e_ = Try (Rewrite_Set norm_equation False) e_; \
1.813 + \(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\
1.814 + \ [Test,solve_by_pq_formula]) [bool_ e_, real_ v_])\
1.815 + \in Check_elementwise L_ {(v_::real). Assumptions})"
1.816 + ));
1.817 +
1.818 +store_met
1.819 + (prep_met Test.thy "met_test_squ_nonterm" [] e_metID
1.820 + (*root-equation: see foils..., but notTerminating*)
1.821 + (["Test","square_equation...notTerminating"]:metID,
1.822 + [("#Given" ,["equality e_","solveFor v_"]),
1.823 + ("#Find" ,["solutions v_i_"])
1.824 + ],
1.825 + {rew_ord'="e_rew_ord",rls'=tval_rls,
1.826 + srls = append_rls "srls_contains_root" e_rls
1.827 + [Calc ("Test.contains'_root",eval_contains_root"")],
1.828 + prls=e_rls,calc=[],
1.829 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.830 + asm_thm=[("square_equation_left",""),
1.831 + ("square_equation_right","")]*)},
1.832 + "Script Solve_root_equation (e_::bool) (v_::real) = \
1.833 + \(let e_ = \
1.834 + \ ((While (contains_root e_) Do\
1.835 + \ ((Rewrite square_equation_left True) @@\
1.836 + \ (Try (Rewrite_Set Test_simplify False)) @@\
1.837 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
1.838 + \ (Try (Rewrite_Set isolate_root False)) @@\
1.839 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
1.840 + \ (Try (Rewrite_Set norm_equation False)) @@\
1.841 + \ (Try (Rewrite_Set Test_simplify False)))\
1.842 + \ e_;\
1.843 + \ (L_::bool list) = \
1.844 + \ (SubProblem (Test_,[linear,univariate,equation,test],\
1.845 + \ [Test,solve_linear]) [bool_ e_, real_ v_])\
1.846 + \in Check_elementwise L_ {(v_::real). Assumptions})"
1.847 + ));
1.848 +
1.849 +store_met
1.850 + (prep_met Test.thy "met_test_eq1" [] e_metID
1.851 +(*root-equation1:*)
1.852 + (["Test","square_equation1"]:metID,
1.853 + [("#Given" ,["equality e_","solveFor v_"]),
1.854 + ("#Find" ,["solutions v_i_"])
1.855 + ],
1.856 + {rew_ord'="e_rew_ord",rls'=tval_rls,
1.857 + srls = append_rls "srls_contains_root" e_rls
1.858 + [Calc ("Test.contains'_root",eval_contains_root"")],
1.859 + prls=e_rls,calc=[],
1.860 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.861 + asm_thm=[("square_equation_left",""),
1.862 + ("square_equation_right","")]*)},
1.863 + "Script Solve_root_equation (e_::bool) (v_::real) = \
1.864 + \(let e_ = \
1.865 + \ ((While (contains_root e_) Do\
1.866 + \ ((Rewrite square_equation_left True) @@\
1.867 + \ (Try (Rewrite_Set Test_simplify False)) @@\
1.868 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
1.869 + \ (Try (Rewrite_Set isolate_root False)) @@\
1.870 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
1.871 + \ (Try (Rewrite_Set norm_equation False)) @@\
1.872 + \ (Try (Rewrite_Set Test_simplify False)))\
1.873 + \ e_;\
1.874 + \ (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\
1.875 + \ [Test,solve_linear]) [bool_ e_, real_ v_])\
1.876 + \ in Check_elementwise L_ {(v_::real). Assumptions})"
1.877 + ));
1.878 +
1.879 +store_met
1.880 + (prep_met Test.thy "met_test_squ2" [] e_metID
1.881 + (*root-equation2*)
1.882 + (["Test","square_equation2"]:metID,
1.883 + [("#Given" ,["equality e_","solveFor v_"]),
1.884 + ("#Find" ,["solutions v_i_"])
1.885 + ],
1.886 + {rew_ord'="e_rew_ord",rls'=tval_rls,
1.887 + srls = append_rls "srls_contains_root" e_rls
1.888 + [Calc ("Test.contains'_root",eval_contains_root"")],
1.889 + prls=e_rls,calc=[],
1.890 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.891 + asm_thm=[("square_equation_left",""),
1.892 + ("square_equation_right","")]*)},
1.893 + "Script Solve_root_equation (e_::bool) (v_::real) = \
1.894 + \(let e_ = \
1.895 + \ ((While (contains_root e_) Do\
1.896 + \ (((Rewrite square_equation_left True) Or \
1.897 + \ (Rewrite square_equation_right True)) @@\
1.898 + \ (Try (Rewrite_Set Test_simplify False)) @@\
1.899 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
1.900 + \ (Try (Rewrite_Set isolate_root False)) @@\
1.901 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
1.902 + \ (Try (Rewrite_Set norm_equation False)) @@\
1.903 + \ (Try (Rewrite_Set Test_simplify False)))\
1.904 + \ e_;\
1.905 + \ (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test],\
1.906 + \ [Test,solve_plain_square]) [bool_ e_, real_ v_])\
1.907 + \ in Check_elementwise L_ {(v_::real). Assumptions})"
1.908 + ));
1.909 +
1.910 +store_met
1.911 + (prep_met Test.thy "met_test_squeq" [] e_metID
1.912 + (*root-equation*)
1.913 + (["Test","square_equation"]:metID,
1.914 + [("#Given" ,["equality e_","solveFor v_"]),
1.915 + ("#Find" ,["solutions v_i_"])
1.916 + ],
1.917 + {rew_ord'="e_rew_ord",rls'=tval_rls,
1.918 + srls = append_rls "srls_contains_root" e_rls
1.919 + [Calc ("Test.contains'_root",eval_contains_root"")],
1.920 + prls=e_rls,calc=[],
1.921 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.922 + asm_thm=[("square_equation_left",""),
1.923 + ("square_equation_right","")]*)},
1.924 + "Script Solve_root_equation (e_::bool) (v_::real) = \
1.925 + \(let e_ = \
1.926 + \ ((While (contains_root e_) Do\
1.927 + \ (((Rewrite square_equation_left True) Or\
1.928 + \ (Rewrite square_equation_right True)) @@\
1.929 + \ (Try (Rewrite_Set Test_simplify False)) @@\
1.930 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
1.931 + \ (Try (Rewrite_Set isolate_root False)) @@\
1.932 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
1.933 + \ (Try (Rewrite_Set norm_equation False)) @@\
1.934 + \ (Try (Rewrite_Set Test_simplify False)))\
1.935 + \ e_;\
1.936 + \ (L_::bool list) = (SubProblem (Test_,[univariate,equation,test],\
1.937 + \ [no_met]) [bool_ e_, real_ v_])\
1.938 + \ in Check_elementwise L_ {(v_::real). Assumptions})"
1.939 + ) ); (*#######*)
1.940 +
1.941 +store_met
1.942 + (prep_met Test.thy "met_test_eq_plain" [] e_metID
1.943 + (*solve_plain_square*)
1.944 + (["Test","solve_plain_square"]:metID,
1.945 + [("#Given",["equality e_","solveFor v_"]),
1.946 + ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |\
1.947 + \(matches ( ?b*v_ ^^^2 = 0) e_) |\
1.948 + \(matches (?a + v_ ^^^2 = 0) e_) |\
1.949 + \(matches ( v_ ^^^2 = 0) e_)"]),
1.950 + ("#Find" ,["solutions v_i_"])
1.951 + ],
1.952 + {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
1.953 + prls = assoc_rls "matches",
1.954 + crls=tval_rls, nrls=e_rls(*,
1.955 + asm_rls=[],asm_thm=[]*)},
1.956 + "Script Solve_plain_square (e_::bool) (v_::real) = \
1.957 + \ (let e_ = ((Try (Rewrite_Set isolate_bdv False)) @@ \
1.958 + \ (Try (Rewrite_Set Test_simplify False)) @@ \
1.959 + \ ((Rewrite square_equality_0 False) Or \
1.960 + \ (Rewrite square_equality True)) @@ \
1.961 + \ (Try (Rewrite_Set tval_rls False))) e_ \
1.962 + \ in ((Or_to_List e_)::bool list))"
1.963 + ));
1.964 +
1.965 +store_met
1.966 + (prep_met Test.thy "met_test_norm_univ" [] e_metID
1.967 + (["Test","norm_univar_equation"]:metID,
1.968 + [("#Given",["equality e_","solveFor v_"]),
1.969 + ("#Where" ,[]),
1.970 + ("#Find" ,["solutions v_i_"])
1.971 + ],
1.972 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
1.973 + calc=[],
1.974 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},
1.975 + "Script Norm_univar_equation (e_::bool) (v_::real) = \
1.976 + \ (let e_ = ((Try (Rewrite rnorm_equation_add False)) @@ \
1.977 + \ (Try (Rewrite_Set Test_simplify False))) e_ \
1.978 + \ in (SubProblem (Test_,[univariate,equation,test], \
1.979 + \ [no_met]) [bool_ e_, real_ v_]))"
1.980 + ));
1.981 +
1.982 +
1.983 +
1.984 +(*17.9.02 aus SqRoot.ML------------------------------^^^---*)
1.985 +
1.986 +(*8.4.03 aus Poly.ML--------------------------------vvv---
1.987 + make_polynomial ---> make_poly
1.988 + ^-- for user ^-- for systest _ONLY_*)
1.989 +
1.990 +local (*. for make_polytest .*)
1.991 +
1.992 +open Term; (* for type order = EQUAL | LESS | GREATER *)
1.993 +
1.994 +fun pr_ord EQUAL = "EQUAL"
1.995 + | pr_ord LESS = "LESS"
1.996 + | pr_ord GREATER = "GREATER";
1.997 +
1.998 +fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
1.999 + (case a of
1.1000 + "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
1.1001 + | _ => (((a, 0), T), 0))
1.1002 + | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
1.1003 + | dest_hd' (Var v) = (v, 2)
1.1004 + | dest_hd' (Bound i) = ((("", i), dummyT), 3)
1.1005 + | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
1.1006 +(* RL *)
1.1007 +fun get_order_pow (t $ (Free(order,_))) =
1.1008 + (case int_of_str (order) of
1.1009 + SOME d => d
1.1010 + | NONE => 0)
1.1011 + | get_order_pow _ = 0;
1.1012 +
1.1013 +fun size_of_term' (Const(str,_) $ t) =
1.1014 + if "Atools.pow"= str then 1000 + size_of_term' t else 1 + size_of_term' t (*WN*)
1.1015 + | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1.1016 + | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1.1017 + | size_of_term' _ = 1;
1.1018 +
1.1019 +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.1020 + (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
1.1021 + | term_ord' pr thy (t, u) =
1.1022 + (if pr then
1.1023 + let
1.1024 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.1025 + val _=writeln("t= f@ts= \""^
1.1026 + ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
1.1027 + (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
1.1028 + val _=writeln("u= g@us= \""^
1.1029 + ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
1.1030 + (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
1.1031 + val _=writeln("size_of_term(t,u)= ("^
1.1032 + (string_of_int(size_of_term' t))^", "^
1.1033 + (string_of_int(size_of_term' u))^")");
1.1034 + val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
1.1035 + val _=writeln("terms_ord(ts,us) = "^
1.1036 + ((pr_ord o terms_ord str false)(ts,us)));
1.1037 + val _=writeln("-------");
1.1038 + in () end
1.1039 + else ();
1.1040 + case int_ord (size_of_term' t, size_of_term' u) of
1.1041 + EQUAL =>
1.1042 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1.1043 + (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
1.1044 + | ord => ord)
1.1045 + end
1.1046 + | ord => ord)
1.1047 +and hd_ord (f, g) = (* ~ term.ML *)
1.1048 + prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.1049 +and terms_ord str pr (ts, us) =
1.1050 + list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
1.1051 +in
1.1052 +
1.1053 +fun ord_make_polytest (pr:bool) thy (_:subst) tu =
1.1054 + (term_ord' pr thy(***) tu = LESS );
1.1055 +
1.1056 +end;(*local*)
1.1057 +
1.1058 +rew_ord' := overwritel (!rew_ord',
1.1059 +[("termlessI", termlessI),
1.1060 + ("ord_make_polytest", ord_make_polytest false thy)
1.1061 + ]);
1.1062 +
1.1063 +(*WN060510 this was a preparation for prep_rls ...
1.1064 +val scr_make_polytest =
1.1065 +"Script Expand_binomtest t_ =\
1.1066 +\(Repeat \
1.1067 +\((Try (Repeat (Rewrite real_diff_minus False))) @@ \
1.1068 +
1.1069 +\ (Try (Repeat (Rewrite real_add_mult_distrib False))) @@ \
1.1070 +\ (Try (Repeat (Rewrite real_add_mult_distrib2 False))) @@ \
1.1071 +\ (Try (Repeat (Rewrite real_diff_mult_distrib False))) @@ \
1.1072 +\ (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ \
1.1073 +
1.1074 +\ (Try (Repeat (Rewrite real_mult_1 False))) @@ \
1.1075 +\ (Try (Repeat (Rewrite real_mult_0 False))) @@ \
1.1076 +\ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \
1.1077 +
1.1078 +\ (Try (Repeat (Rewrite real_mult_commute False))) @@ \
1.1079 +\ (Try (Repeat (Rewrite real_mult_left_commute False))) @@ \
1.1080 +\ (Try (Repeat (Rewrite real_mult_assoc False))) @@ \
1.1081 +\ (Try (Repeat (Rewrite real_add_commute False))) @@ \
1.1082 +\ (Try (Repeat (Rewrite real_add_left_commute False))) @@ \
1.1083 +\ (Try (Repeat (Rewrite real_add_assoc False))) @@ \
1.1084 +
1.1085 +\ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \
1.1086 +\ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \
1.1087 +\ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \
1.1088 +\ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \
1.1089 +
1.1090 +\ (Try (Repeat (Rewrite real_num_collect False))) @@ \
1.1091 +\ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
1.1092 +
1.1093 +\ (Try (Repeat (Rewrite real_one_collect False))) @@ \
1.1094 +\ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
1.1095 +
1.1096 +\ (Try (Repeat (Calculate plus ))) @@ \
1.1097 +\ (Try (Repeat (Calculate times ))) @@ \
1.1098 +\ (Try (Repeat (Calculate power_)))) \
1.1099 +\ t_)";
1.1100 +-----------------------------------------------------*)
1.1101 +
1.1102 +val make_polytest =
1.1103 + Rls{id = "make_polytest", preconds = []:term list, rew_ord = ("ord_make_polytest",
1.1104 + ord_make_polytest false Poly.thy),
1.1105 + erls = testerls, srls = Erls,
1.1106 + calc = [("PLUS" , ("op +", eval_binop "#add_")),
1.1107 + ("TIMES" , ("op *", eval_binop "#mult_")),
1.1108 + ("POWER", ("Atools.pow", eval_binop "#power_"))
1.1109 + ],
1.1110 + (*asm_thm = [],*)
1.1111 + rules = [Thm ("real_diff_minus",num_str real_diff_minus),
1.1112 + (*"a - b = a + (-1) * b"*)
1.1113 + Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.1114 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.1115 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.1116 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.1117 + Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
1.1118 + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.1119 + Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
1.1120 + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.1121 + Thm ("real_mult_1",num_str real_mult_1),
1.1122 + (*"1 * z = z"*)
1.1123 + Thm ("real_mult_0",num_str real_mult_0),
1.1124 + (*"0 * z = 0"*)
1.1125 + Thm ("real_add_zero_left",num_str real_add_zero_left),
1.1126 + (*"0 + z = z"*)
1.1127 +
1.1128 + (*AC-rewriting*)
1.1129 + Thm ("real_mult_commute",num_str real_mult_commute),
1.1130 + (* z * w = w * z *)
1.1131 + Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.1132 + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.1133 + Thm ("real_mult_assoc",num_str real_mult_assoc),
1.1134 + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.1135 + Thm ("real_add_commute",num_str real_add_commute),
1.1136 + (*z + w = w + z*)
1.1137 + Thm ("real_add_left_commute",num_str real_add_left_commute),
1.1138 + (*x + (y + z) = y + (x + z)*)
1.1139 + Thm ("real_add_assoc",num_str real_add_assoc),
1.1140 + (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.1141 +
1.1142 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.1143 + (*"r1 * r1 = r1 ^^^ 2"*)
1.1144 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.1145 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.1146 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.1147 + (*"z1 + z1 = 2 * z1"*)
1.1148 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.1149 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.1150 +
1.1151 + Thm ("real_num_collect",num_str real_num_collect),
1.1152 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.1153 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.1154 + (*"[| l is_const; m is_const |] ==>
1.1155 + l * n + (m * n + k) = (l + m) * n + k"*)
1.1156 + Thm ("real_one_collect",num_str real_one_collect),
1.1157 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.1158 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.1159 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.1160 +
1.1161 + Calc ("op +", eval_binop "#add_"),
1.1162 + Calc ("op *", eval_binop "#mult_"),
1.1163 + Calc ("Atools.pow", eval_binop "#power_")
1.1164 + ],
1.1165 + scr = EmptyScr(*Script ((term_of o the o (parse thy))
1.1166 + scr_make_polytest)*)
1.1167 + }:rls;
1.1168 +(*WN060510 this was done before 'fun prep_rls' ...
1.1169 +val scr_expand_binomtest =
1.1170 +"Script Expand_binomtest t_ =\
1.1171 +\(Repeat \
1.1172 +\((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ \
1.1173 +\ (Try (Repeat (Rewrite real_plus_binom_times False))) @@ \
1.1174 +\ (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ \
1.1175 +\ (Try (Repeat (Rewrite real_minus_binom_times False))) @@ \
1.1176 +\ (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ \
1.1177 +\ (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ \
1.1178 +
1.1179 +\ (Try (Repeat (Rewrite real_mult_1 False))) @@ \
1.1180 +\ (Try (Repeat (Rewrite real_mult_0 False))) @@ \
1.1181 +\ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \
1.1182 +
1.1183 +\ (Try (Repeat (Calculate plus ))) @@ \
1.1184 +\ (Try (Repeat (Calculate times ))) @@ \
1.1185 +\ (Try (Repeat (Calculate power_))) @@ \
1.1186 +
1.1187 +\ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \
1.1188 +\ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \
1.1189 +\ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \
1.1190 +\ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \
1.1191 +
1.1192 +\ (Try (Repeat (Rewrite real_num_collect False))) @@ \
1.1193 +\ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
1.1194 +
1.1195 +\ (Try (Repeat (Rewrite real_one_collect False))) @@ \
1.1196 +\ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
1.1197 +
1.1198 +\ (Try (Repeat (Calculate plus ))) @@ \
1.1199 +\ (Try (Repeat (Calculate times ))) @@ \
1.1200 +\ (Try (Repeat (Calculate power_)))) \
1.1201 +\ t_)";
1.1202 +------------------------------------------------------*)
1.1203 +
1.1204 +val expand_binomtest =
1.1205 + Rls{id = "expand_binomtest", preconds = [],
1.1206 + rew_ord = ("termlessI",termlessI),
1.1207 + erls = testerls, srls = Erls,
1.1208 + calc = [("PLUS" , ("op +", eval_binop "#add_")),
1.1209 + ("TIMES" , ("op *", eval_binop "#mult_")),
1.1210 + ("POWER", ("Atools.pow", eval_binop "#power_"))
1.1211 + ],
1.1212 + (*asm_thm = [],*)
1.1213 + rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
1.1214 + (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1.1215 + Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.1216 + (*"(a + b)*(a + b) = ...*)
1.1217 + Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
1.1218 + (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1.1219 + Thm ("real_minus_binom_times",num_str real_minus_binom_times),
1.1220 + (*"(a - b)*(a - b) = ...*)
1.1221 + Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
1.1222 + (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1.1223 + Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
1.1224 + (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1.1225 + (*RL 020915*)
1.1226 + Thm ("real_pp_binom_times",num_str real_pp_binom_times),
1.1227 + (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1.1228 + Thm ("real_pm_binom_times",num_str real_pm_binom_times),
1.1229 + (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1.1230 + Thm ("real_mp_binom_times",num_str real_mp_binom_times),
1.1231 + (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
1.1232 + Thm ("real_mm_binom_times",num_str real_mm_binom_times),
1.1233 + (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
1.1234 + Thm ("realpow_multI",num_str realpow_multI),
1.1235 + (*(a*b)^^^n = a^^^n * b^^^n*)
1.1236 + Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
1.1237 + (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1.1238 + Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),
1.1239 + (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1.1240 +
1.1241 +
1.1242 + (* Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.1243 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.1244 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.1245 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.1246 + Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
1.1247 + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.1248 + Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
1.1249 + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.1250 + *)
1.1251 +
1.1252 + Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
1.1253 + Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
1.1254 + Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*)
1.1255 +
1.1256 + Calc ("op +", eval_binop "#add_"),
1.1257 + Calc ("op *", eval_binop "#mult_"),
1.1258 + Calc ("Atools.pow", eval_binop "#power_"),
1.1259 + (*
1.1260 + Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
1.1261 + Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
1.1262 + Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
1.1263 + Thm ("real_add_commute",num_str real_add_commute), (**)
1.1264 + Thm ("real_add_left_commute",num_str real_add_left_commute), (**)
1.1265 + Thm ("real_add_assoc",num_str real_add_assoc), (**)
1.1266 + *)
1.1267 +
1.1268 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.1269 + (*"r1 * r1 = r1 ^^^ 2"*)
1.1270 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.1271 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.1272 + (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.1273 + (*"z1 + z1 = 2 * z1"*)*)
1.1274 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.1275 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.1276 +
1.1277 + Thm ("real_num_collect",num_str real_num_collect),
1.1278 + (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.1279 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.1280 + (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.1281 + Thm ("real_one_collect",num_str real_one_collect),
1.1282 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.1283 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.1284 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.1285 +
1.1286 + Calc ("op +", eval_binop "#add_"),
1.1287 + Calc ("op *", eval_binop "#mult_"),
1.1288 + Calc ("Atools.pow", eval_binop "#power_")
1.1289 + ],
1.1290 + scr = EmptyScr
1.1291 +(*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
1.1292 + }:rls;
1.1293 +
1.1294 +
1.1295 +ruleset' := overwritelthy thy (!ruleset',
1.1296 + [("make_polytest", prep_rls make_polytest),
1.1297 + ("expand_binomtest", prep_rls expand_binomtest)
1.1298 + ]);
1.1299 +
1.1300 +
1.1301 +
1.1302 +
1.1303 +
1.1304 +