1.1 --- a/src/Tools/isac/IsacKnowledge/Test.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,1301 +0,0 @@
1.4 -(* SML functions for rational arithmetic
1.5 - WN.22.10.99
1.6 - use"../knowledge/Test.ML";
1.7 - use"IsacKnowledge/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 -