for demo at innsbruck 071206, demos outcommented (version_isac = "WN071206-log-demo")
1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/LogExp.ML Mon Dec 03 19:11:27 2007 +0100
1.3 @@ -0,0 +1,37 @@
1.4 +(* all outcommented in order to demonstrate authoring:
1.5 + WN071203
1.6 +*)
1.7 +
1.8 +(** interface isabelle -- isac **)
1.9 +theory' := overwritel (!theory', [("LogExp.thy",LogExp.thy)]);
1.10 +
1.11 +(*-------------------------------------------------------------------*
1.12 +
1.13 +(** problems **)
1.14 +store_pbt
1.15 + (prep_pbt LogExp.thy "pbl_test_equ_univ_log" [] e_pblID
1.16 + (["logarithmic","univariate","equation"],
1.17 + [("#Given" ,["equality e_","solveFor v_"]),
1.18 + ("#Where" ,["matches ((?a log ?v_) = ?b) e_"]),
1.19 + ("#Find" ,["solutions v_i_"])
1.20 + ],
1.21 + PolyEq_prls, Some "solve (e_::bool, v_)",
1.22 + [["Test","solve_log"]]));
1.23 +
1.24 +(** methods **)
1.25 +store_met
1.26 + (prep_met LogExp.thy "met_equ_log" [] e_metID
1.27 + (["Equation","solve_log"],
1.28 + [("#Given" ,["equality e_","solveFor v_"]),
1.29 + ("#Where" ,["matches ((?a log ?v_) = ?b) e_"]),
1.30 + ("#Find" ,["solutions v_i_"])
1.31 + ],
1.32 + {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
1.33 + calc=[],crls=PolyEq_crls, nrls=norm_Rational},
1.34 + "Script Solve_log (e_::bool) (v_::real) = \
1.35 + \(let e_ = ((Rewrite equality_power False) @@ \
1.36 + \ (Rewrite exp_invers_log False) @@ \
1.37 + \ (Rewrite_Set norm_Poly False)) e_ \
1.38 + \ in [e_])"
1.39 + ));
1.40 +*-------------------------------------------------------------------*)
2.1 --- a/src/sml/IsacKnowledge/LogExp.thy Mon Dec 03 15:59:34 2007 +0100
2.2 +++ b/src/sml/IsacKnowledge/LogExp.thy Mon Dec 03 19:11:27 2007 +0100
2.3 @@ -1,13 +1,28 @@
2.4 -(* all outcommented for demonstrating authoring:
2.5 +(* all outcommented in order to demonstrate authoring:
2.6 WN071203
2.7 +remove_thy"LogExp";
2.8 +use_thy"IsacKnowledge/LogExp";
2.9 +use_thy"IsacKnowledge/Isac";
2.10 *)
2.11 -LogExp = Real +
2.12 +LogExp = PolyEq +
2.13
2.14 -(*----------------------------------------------------------*)
2.15 +(*----------------------------------------------------------*
2.16 consts
2.17
2.18 ln :: "real => real"
2.19 - alog :: "[real, real] => real" ("_ log _" 80)
2.20 exp :: "real => real" ("E'_ ^^^ _" 80)
2.21 + alog :: "[real, real] => real" ("_ log _" 90)
2.22 +
2.23 + (*Script-names*)
2.24 + Solve'_log :: "[bool,real, bool list] \
2.25 + \=> bool list"
2.26 + ("((Script Solve'_log (_ _=))// (_))" 9)
2.27 +
2.28 +rules
2.29 +
2.30 + equality_pow "0 < a ==> (l = r) = (a^^^l = a^^^r)"
2.31 + equality_power "((a log b) = c) = (a^^^(a log b) = a^^^c)"
2.32 + exp_invers_log "a^^^(a log b) = b"
2.33 +*----------------------------------------------------------*)
2.34
2.35 end
2.36 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/sml/IsacKnowledge/Test.ML Mon Dec 03 19:11:27 2007 +0100
3.3 @@ -0,0 +1,1301 @@
3.4 +(* SML functions for rational arithmetic
3.5 + WN.22.10.99
3.6 + use"../knowledge/Test.ML";
3.7 + use"IsacKnowledge/Test.ML";
3.8 + use"Test.ML";
3.9 + *)
3.10 +
3.11 +
3.12 +(** interface isabelle -- isac **)
3.13 +
3.14 +theory' := overwritel (!theory', [("Test.thy",Test.thy)]);
3.15 +
3.16 +(** evaluation of numerals and predicates **)
3.17 +
3.18 +(*does a term contain a root ?*)
3.19 +fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy =
3.20 + if strip_thy op0 <> "is'_root'_free"
3.21 + then raise error ("eval_root_free: wrong "^op0)
3.22 + else if const_in (strip_thy op0) arg
3.23 + then Some (mk_thmid thmid ""
3.24 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
3.25 + Trueprop $ (mk_equality (t, false_as_term)))
3.26 + else Some (mk_thmid thmid ""
3.27 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
3.28 + Trueprop $ (mk_equality (t, true_as_term)))
3.29 + | eval_root_free _ _ _ _ = None;
3.30 +
3.31 +(*does a term contain a root ?*)
3.32 +fun eval_contains_root (thmid:string) _
3.33 + (t as (Const("Test.contains'_root",t0) $ arg)) thy =
3.34 + if "sqrt" mem (ids_of arg)
3.35 + then Some (mk_thmid thmid ""
3.36 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
3.37 + Trueprop $ (mk_equality (t, true_as_term)))
3.38 + else Some (mk_thmid thmid ""
3.39 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
3.40 + Trueprop $ (mk_equality (t, false_as_term)))
3.41 + | eval_contains_root _ _ _ _ = None;
3.42 +
3.43 +calclist':= overwritel (!calclist',
3.44 + [("is_root_free", ("Test.is'_root'_free",
3.45 + eval_root_free"#is_root_free_")),
3.46 + ("contains_root", ("Test.contains'_root",
3.47 + eval_contains_root"#contains_root_"))
3.48 + ]);
3.49 +
3.50 +(** term order **)
3.51 +fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
3.52 +
3.53 +(** rule sets **)
3.54 +
3.55 +val testerls =
3.56 + Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
3.57 + erls = e_rls, srls = Erls,
3.58 + calc = [],
3.59 + rules = [Thm ("refl",num_str refl),
3.60 + Thm ("le_refl",num_str le_refl),
3.61 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
3.62 + Thm ("not_true",num_str not_true),
3.63 + Thm ("not_false",num_str not_false),
3.64 + Thm ("and_true",and_true),
3.65 + Thm ("and_false",and_false),
3.66 + Thm ("or_true",or_true),
3.67 + Thm ("or_false",or_false),
3.68 + Thm ("and_commute",num_str and_commute),
3.69 + Thm ("or_commute",num_str or_commute),
3.70 +
3.71 + Calc ("Atools.is'_const",eval_const "#is_const_"),
3.72 + Calc ("Tools.matches",eval_matches ""),
3.73 +
3.74 + Calc ("op +",eval_binop "#add_"),
3.75 + Calc ("op *",eval_binop "#mult_"),
3.76 + Calc ("Atools.pow" ,eval_binop "#power_"),
3.77 +
3.78 + Calc ("op <",eval_equ "#less_"),
3.79 + Calc ("op <=",eval_equ "#less_equal_"),
3.80 +
3.81 + Calc ("Atools.ident",eval_ident "#ident_")],
3.82 + scr = Script ((term_of o the o (parse thy))
3.83 + "empty_script")
3.84 + }:rls;
3.85 +
3.86 +(*.for evaluation of conditions in rewrite rules.*)
3.87 +(*FIXXXXXXME 10.8.02: handle like _simplify*)
3.88 +val tval_rls =
3.89 + Rls{id = "tval_rls", preconds = [],
3.90 + rew_ord = ("sqrt_right",sqrt_right false ProtoPure.thy),
3.91 + erls=testerls,srls = e_rls,
3.92 + calc=[],
3.93 + rules = [Thm ("refl",num_str refl),
3.94 + Thm ("le_refl",num_str le_refl),
3.95 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
3.96 + Thm ("not_true",num_str not_true),
3.97 + Thm ("not_false",num_str not_false),
3.98 + Thm ("and_true",and_true),
3.99 + Thm ("and_false",and_false),
3.100 + Thm ("or_true",or_true),
3.101 + Thm ("or_false",or_false),
3.102 + Thm ("and_commute",num_str and_commute),
3.103 + Thm ("or_commute",num_str or_commute),
3.104 +
3.105 + Thm ("real_diff_minus",num_str real_diff_minus),
3.106 +
3.107 + Thm ("root_ge0",num_str root_ge0),
3.108 + Thm ("root_add_ge0",num_str root_add_ge0),
3.109 + Thm ("root_ge0_1",num_str root_ge0_1),
3.110 + Thm ("root_ge0_2",num_str root_ge0_2),
3.111 +
3.112 + Calc ("Atools.is'_const",eval_const "#is_const_"),
3.113 + Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_"),
3.114 + Calc ("Tools.matches",eval_matches ""),
3.115 + Calc ("Test.contains'_root",
3.116 + eval_contains_root"#contains_root_"),
3.117 +
3.118 + Calc ("op +",eval_binop "#add_"),
3.119 + Calc ("op *",eval_binop "#mult_"),
3.120 + Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
3.121 + Calc ("Atools.pow" ,eval_binop "#power_"),
3.122 +
3.123 + Calc ("op <",eval_equ "#less_"),
3.124 + Calc ("op <=",eval_equ "#less_equal_"),
3.125 +
3.126 + Calc ("Atools.ident",eval_ident "#ident_")],
3.127 + scr = Script ((term_of o the o (parse thy))
3.128 + "empty_script")
3.129 + }:rls;
3.130 +
3.131 +
3.132 +ruleset' := overwritelthy thy (!ruleset',
3.133 + [("testerls", prep_rls testerls)
3.134 + ]);
3.135 +
3.136 +
3.137 +(*make () dissappear*)
3.138 +val rearrange_assoc =
3.139 + Rls{id = "rearrange_assoc", preconds = [],
3.140 + rew_ord = ("e_rew_ord",e_rew_ord),
3.141 + erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
3.142 + rules =
3.143 + [Thm ("sym_radd_assoc",num_str (radd_assoc RS sym)),
3.144 + Thm ("sym_rmult_assoc",num_str (rmult_assoc RS sym))],
3.145 + scr = Script ((term_of o the o (parse thy))
3.146 + "empty_script")
3.147 + }:rls;
3.148 +
3.149 +val ac_plus_times =
3.150 + Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
3.151 + erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
3.152 + rules =
3.153 + [Thm ("radd_commute",radd_commute),
3.154 + Thm ("radd_left_commute",radd_left_commute),
3.155 + Thm ("radd_assoc",radd_assoc),
3.156 + Thm ("rmult_commute",rmult_commute),
3.157 + Thm ("rmult_left_commute",rmult_left_commute),
3.158 + Thm ("rmult_assoc",rmult_assoc)],
3.159 + scr = Script ((term_of o the o (parse thy))
3.160 + "empty_script")
3.161 + }:rls;
3.162 +
3.163 +(*todo: replace by Rewrite("rnorm_equation_add",num_str rnorm_equation_add)*)
3.164 +val norm_equation =
3.165 + Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
3.166 + erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
3.167 + rules = [Thm ("rnorm_equation_add",num_str rnorm_equation_add)
3.168 + ],
3.169 + scr = Script ((term_of o the o (parse thy))
3.170 + "empty_script")
3.171 + }:rls;
3.172 +
3.173 +(** rule sets **)
3.174 +
3.175 +val STest_simplify = (* vv--- not changed to real by parse*)
3.176 + "Script STest_simplify (t_::'z) = \
3.177 + \(Repeat\
3.178 + \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
3.179 + \ (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@ \
3.180 + \ (Try (Repeat (Rewrite rdistr_right_assoc False))) @@ \
3.181 + \ (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@\
3.182 + \ (Try (Repeat (Rewrite rdistr_div_right False))) @@ \
3.183 + \ (Try (Repeat (Rewrite rbinom_power_2 False))) @@ \
3.184 +
3.185 + \ (Try (Repeat (Rewrite radd_commute False))) @@ \
3.186 + \ (Try (Repeat (Rewrite radd_left_commute False))) @@ \
3.187 + \ (Try (Repeat (Rewrite radd_assoc False))) @@ \
3.188 + \ (Try (Repeat (Rewrite rmult_commute False))) @@ \
3.189 + \ (Try (Repeat (Rewrite rmult_left_commute False))) @@ \
3.190 + \ (Try (Repeat (Rewrite rmult_assoc False))) @@ \
3.191 +
3.192 + \ (Try (Repeat (Rewrite radd_real_const_eq False))) @@ \
3.193 + \ (Try (Repeat (Rewrite radd_real_const False))) @@ \
3.194 + \ (Try (Repeat (Calculate plus))) @@ \
3.195 + \ (Try (Repeat (Calculate times))) @@ \
3.196 + \ (Try (Repeat (Calculate divide_))) @@\
3.197 + \ (Try (Repeat (Calculate power_))) @@ \
3.198 +
3.199 + \ (Try (Repeat (Rewrite rcollect_right False))) @@ \
3.200 + \ (Try (Repeat (Rewrite rcollect_one_left False))) @@ \
3.201 + \ (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@ \
3.202 + \ (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@ \
3.203 +
3.204 + \ (Try (Repeat (Rewrite rshift_nominator False))) @@ \
3.205 + \ (Try (Repeat (Rewrite rcancel_den False))) @@ \
3.206 + \ (Try (Repeat (Rewrite rroot_square_inv False))) @@ \
3.207 + \ (Try (Repeat (Rewrite rroot_times_root False))) @@ \
3.208 + \ (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@ \
3.209 + \ (Try (Repeat (Rewrite rsqare False))) @@ \
3.210 + \ (Try (Repeat (Rewrite power_1 False))) @@ \
3.211 + \ (Try (Repeat (Rewrite rtwo_of_the_same False))) @@ \
3.212 + \ (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@ \
3.213 +
3.214 + \ (Try (Repeat (Rewrite rmult_1 False))) @@ \
3.215 + \ (Try (Repeat (Rewrite rmult_1_right False))) @@ \
3.216 + \ (Try (Repeat (Rewrite rmult_0 False))) @@ \
3.217 + \ (Try (Repeat (Rewrite rmult_0_right False))) @@ \
3.218 + \ (Try (Repeat (Rewrite radd_0 False))) @@ \
3.219 + \ (Try (Repeat (Rewrite radd_0_right False)))) \
3.220 + \ t_)";
3.221 +
3.222 +
3.223 +(* expects * distributed over + *)
3.224 +val Test_simplify =
3.225 + Rls{id = "Test_simplify", preconds = [],
3.226 + rew_ord = ("sqrt_right",sqrt_right false ProtoPure.thy),
3.227 + erls = tval_rls, srls = e_rls,
3.228 + calc=[(*since 040209 filled by prep_rls*)],
3.229 + (*asm_thm = [],*)
3.230 + rules = [
3.231 + Thm ("real_diff_minus",num_str real_diff_minus),
3.232 + Thm ("radd_mult_distrib2",num_str radd_mult_distrib2),
3.233 + Thm ("rdistr_right_assoc",num_str rdistr_right_assoc),
3.234 + Thm ("rdistr_right_assoc_p",num_str rdistr_right_assoc_p),
3.235 + Thm ("rdistr_div_right",num_str rdistr_div_right),
3.236 + Thm ("rbinom_power_2",num_str rbinom_power_2),
3.237 +
3.238 + Thm ("radd_commute",num_str radd_commute),
3.239 + Thm ("radd_left_commute",num_str radd_left_commute),
3.240 + Thm ("radd_assoc",num_str radd_assoc),
3.241 + Thm ("rmult_commute",num_str rmult_commute),
3.242 + Thm ("rmult_left_commute",num_str rmult_left_commute),
3.243 + Thm ("rmult_assoc",num_str rmult_assoc),
3.244 +
3.245 + Thm ("radd_real_const_eq",num_str radd_real_const_eq),
3.246 + Thm ("radd_real_const",num_str radd_real_const),
3.247 + (* these 2 rules are invers to distr_div_right wrt. termination.
3.248 + thus they MUST be done IMMEDIATELY before calc *)
3.249 + Calc ("op +", eval_binop "#add_"),
3.250 + Calc ("op *", eval_binop "#mult_"),
3.251 + Calc ("HOL.divide", eval_cancel "#divide_"),
3.252 + Calc ("Atools.pow", eval_binop "#power_"),
3.253 +
3.254 + Thm ("rcollect_right",num_str rcollect_right),
3.255 + Thm ("rcollect_one_left",num_str rcollect_one_left),
3.256 + Thm ("rcollect_one_left_assoc",num_str rcollect_one_left_assoc),
3.257 + Thm ("rcollect_one_left_assoc_p",num_str rcollect_one_left_assoc_p),
3.258 +
3.259 + Thm ("rshift_nominator",num_str rshift_nominator),
3.260 + Thm ("rcancel_den",num_str rcancel_den),
3.261 + Thm ("rroot_square_inv",num_str rroot_square_inv),
3.262 + Thm ("rroot_times_root",num_str rroot_times_root),
3.263 + Thm ("rroot_times_root_assoc_p",num_str rroot_times_root_assoc_p),
3.264 + Thm ("rsqare",num_str rsqare),
3.265 + Thm ("power_1",num_str power_1),
3.266 + Thm ("rtwo_of_the_same",num_str rtwo_of_the_same),
3.267 + Thm ("rtwo_of_the_same_assoc_p",num_str rtwo_of_the_same_assoc_p),
3.268 +
3.269 + Thm ("rmult_1",num_str rmult_1),
3.270 + Thm ("rmult_1_right",num_str rmult_1_right),
3.271 + Thm ("rmult_0",num_str rmult_0),
3.272 + Thm ("rmult_0_right",num_str rmult_0_right),
3.273 + Thm ("radd_0",num_str radd_0),
3.274 + Thm ("radd_0_right",num_str radd_0_right)
3.275 + ],
3.276 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.277 + (*since 040209 filled by prep_rls: STest_simplify*)
3.278 + }:rls;
3.279 +
3.280 +
3.281 +
3.282 +
3.283 +
3.284 +(** rule sets **)
3.285 +
3.286 +
3.287 +
3.288 +(*isolate the root in a root-equation*)
3.289 +val isolate_root =
3.290 + Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
3.291 + erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
3.292 + rules = [Thm ("rroot_to_lhs",num_str rroot_to_lhs),
3.293 + Thm ("rroot_to_lhs_mult",num_str rroot_to_lhs_mult),
3.294 + Thm ("rroot_to_lhs_add_mult",num_str rroot_to_lhs_add_mult),
3.295 + Thm ("risolate_root_add",num_str risolate_root_add),
3.296 + Thm ("risolate_root_mult",num_str risolate_root_mult),
3.297 + Thm ("risolate_root_div",num_str risolate_root_div) ],
3.298 + scr = Script ((term_of o the o (parse thy))
3.299 + "empty_script")
3.300 + }:rls;
3.301 +
3.302 +(*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
3.303 +val isolate_bdv =
3.304 + Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
3.305 + erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
3.306 + rules =
3.307 + [Thm ("risolate_bdv_add",num_str risolate_bdv_add),
3.308 + Thm ("risolate_bdv_mult_add",num_str risolate_bdv_mult_add),
3.309 + Thm ("risolate_bdv_mult",num_str risolate_bdv_mult),
3.310 + Thm ("mult_square",num_str mult_square),
3.311 + Thm ("constant_square",num_str constant_square),
3.312 + Thm ("constant_mult_square",num_str constant_mult_square)
3.313 + ],
3.314 + scr = Script ((term_of o the o (parse thy))
3.315 + "empty_script")
3.316 + }:rls;
3.317 +
3.318 +
3.319 +
3.320 +
3.321 +(* association list for calculate_, calculate
3.322 + "op +" etc. not usable in scripts *)
3.323 +val calclist =
3.324 + [
3.325 + (*as Tools.ML*)
3.326 + ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
3.327 + ("matches",("Tools.matches",eval_matches "#matches_")),
3.328 + ("lhs" ,("Tools.lhs" ,eval_lhs "")),
3.329 + (*aus Atools.ML*)
3.330 + ("plus" ,("op +" ,eval_binop "#add_")),
3.331 + ("times" ,("op *" ,eval_binop "#mult_")),
3.332 + ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
3.333 + ("power_" ,("Atools.pow" ,eval_binop "#power_")),
3.334 + ("is_const",("Atools.is'_const",eval_const "#is_const_")),
3.335 + ("le" ,("op <" ,eval_equ "#less_")),
3.336 + ("leq" ,("op <=" ,eval_equ "#less_equal_")),
3.337 + ("ident" ,("Atools.ident",eval_ident "#ident_")),
3.338 + (*von hier (ehem.SqRoot*)
3.339 + ("sqrt" ,("Root.sqrt" ,eval_sqrt "#sqrt_")),
3.340 + ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_")),
3.341 + ("Test.contains_root",("contains'_root",
3.342 + eval_contains_root"#contains_root_"))
3.343 + ];
3.344 +
3.345 +ruleset' := overwritelthy thy (!ruleset',
3.346 + [("Test_simplify", prep_rls Test_simplify),
3.347 + ("tval_rls", prep_rls tval_rls),
3.348 + ("isolate_root", prep_rls isolate_root),
3.349 + ("isolate_bdv", prep_rls isolate_bdv),
3.350 + ("matches",
3.351 + prep_rls (append_rls "matches" testerls
3.352 + [Calc ("Tools.matches",eval_matches "#matches_")]))
3.353 + ]);
3.354 +
3.355 +(** problem types **)
3.356 +store_pbt
3.357 + (prep_pbt Test.thy "pbl_test" [] e_pblID
3.358 + (["test"],
3.359 + [],
3.360 + e_rls, None, []));
3.361 +store_pbt
3.362 + (prep_pbt Test.thy "pbl_test_equ" [] e_pblID
3.363 + (["equation","test"],
3.364 + [("#Given" ,["equality e_","solveFor v_"]),
3.365 + ("#Where" ,["matches (?a = ?b) e_"]),
3.366 + ("#Find" ,["solutions v_i_"])
3.367 + ],
3.368 + assoc_rls "matches",
3.369 + Some "solve (e_::bool, v_)", []));
3.370 +
3.371 +store_pbt
3.372 + (prep_pbt Test.thy "pbl_test_uni" [] e_pblID
3.373 + (["univariate","equation","test"],
3.374 + [("#Given" ,["equality e_","solveFor v_"]),
3.375 + ("#Where" ,["matches (?a = ?b) e_"]),
3.376 + ("#Find" ,["solutions v_i_"])
3.377 + ],
3.378 + assoc_rls "matches",
3.379 + Some "solve (e_::bool, v_)", []));
3.380 +
3.381 +store_pbt
3.382 + (prep_pbt Test.thy "pbl_test_uni_lin" [] e_pblID
3.383 + (["linear","univariate","equation","test"],
3.384 + [("#Given" ,["equality e_","solveFor v_"]),
3.385 + ("#Where" ,["(matches ( v_ = 0) e_) | (matches ( ?b*v_ = 0) e_) |\
3.386 + \(matches (?a+v_ = 0) e_) | (matches (?a+?b*v_ = 0) e_) "]),
3.387 + ("#Find" ,["solutions v_i_"])
3.388 + ],
3.389 + assoc_rls "matches",
3.390 + Some "solve (e_::bool, v_)", [["Test","solve_linear"]]));
3.391 +
3.392 +(*25.8.01 ------
3.393 +store_pbt
3.394 + (prep_pbt Test.thy
3.395 + (["Test.thy"],
3.396 + [("#Given" ,"boolTestGiven g_"),
3.397 + ("#Find" ,"boolTestFind f_")
3.398 + ],
3.399 + []));
3.400 +
3.401 +store_pbt
3.402 + (prep_pbt Test.thy
3.403 + (["testeq","Test.thy"],
3.404 + [("#Given" ,"boolTestGiven g_"),
3.405 + ("#Find" ,"boolTestFind f_")
3.406 + ],
3.407 + []));
3.408 +
3.409 +
3.410 +val ttt = (term_of o the o (parse Isac.thy)) "(matches ( v_ = 0) e_)";
3.411 +
3.412 + ------ 25.8.01*)
3.413 +
3.414 +
3.415 +(** methods **)
3.416 +store_met
3.417 + (prep_met Diff.thy "met_test" [] e_metID
3.418 + (["Test"],
3.419 + [],
3.420 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
3.421 + crls=Atools_erls, nrls=e_rls(*,
3.422 + asm_rls=[],asm_thm=[]*)}, "empty_script"));
3.423 +(*
3.424 +store_met
3.425 + (prep_met Script.thy
3.426 + (e_metID,(*empty method*)
3.427 + [],
3.428 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
3.429 + asm_rls=[],asm_thm=[]},
3.430 + "Undef"));*)
3.431 +store_met
3.432 + (prep_met Test.thy "met_test_solvelin" [] e_metID
3.433 + (["Test","solve_linear"]:metID,
3.434 + [("#Given" ,["equality e_","solveFor v_"]),
3.435 + ("#Where" ,["matches (?a = ?b) e_"]),
3.436 + ("#Find" ,["solutions v_i_"])
3.437 + ],
3.438 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,
3.439 + prls=assoc_rls "matches",
3.440 + calc=[],
3.441 + crls=tval_rls, nrls=Test_simplify},
3.442 + "Script Solve_linear (e_::bool) (v_::real)= \
3.443 + \(let e_ =\
3.444 + \ Repeat\
3.445 + \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
3.446 + \ (Rewrite_Set Test_simplify False))) e_\
3.447 + \ in [e_::bool])"
3.448 + )
3.449 +(*, prep_met Test.thy (*test for equations*)
3.450 + (["Test","testeq"]:metID,
3.451 + [("#Given" ,["boolTestGiven g_"]),
3.452 + ("#Find" ,["boolTestFind f_"])
3.453 + ],
3.454 + {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
3.455 + asm_thm=[("square_equation_left","")]},
3.456 + "Script Testeq (eq_::bool) = \
3.457 + \Repeat \
3.458 + \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False eq_)); \
3.459 + \ e_ = Try (Repeat (Rewrite square_equation_left True e_)); \
3.460 + \ e_ = Try (Repeat (Rewrite rmult_0 False e_)) \
3.461 + \ in e_) Until (is_root_free e_)" (*deleted*)
3.462 + )
3.463 +, ---------27.4.02*)
3.464 +);
3.465 +
3.466 +
3.467 +
3.468 +
3.469 +ruleset' := overwritelthy thy (!ruleset',
3.470 + [("norm_equation", prep_rls norm_equation),
3.471 + ("ac_plus_times", prep_rls ac_plus_times),
3.472 + ("rearrange_assoc", prep_rls rearrange_assoc)
3.473 + ]);
3.474 +
3.475 +
3.476 +fun bin_o (Const (op_,(Type ("fun",
3.477 + [Type (s2,[]),Type ("fun",
3.478 + [Type (s4,tl4),Type (s5,tl5)])])))) =
3.479 + if (s2=s4)andalso(s4=s5)then[op_]else[]
3.480 + | bin_o _ = [];
3.481 +
3.482 +fun bin_op (t1 $ t2) = (bin_op t1) union (bin_op t2)
3.483 + | bin_op t = bin_o t;
3.484 +fun is_bin_op t = ((bin_op t)<>[]);
3.485 +
3.486 +fun bin_op_arg1 ((Const (op_,(Type ("fun",
3.487 + [Type (s2,[]),Type ("fun",
3.488 + [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
3.489 + arg1;
3.490 +fun bin_op_arg2 ((Const (op_,(Type ("fun",
3.491 + [Type (s2,[]),Type ("fun",
3.492 + [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
3.493 + arg2;
3.494 +
3.495 +
3.496 +exception NO_EQUATION_TERM;
3.497 +fun is_equation ((Const ("op =",(Type ("fun",
3.498 + [Type (_,[]),Type ("fun",
3.499 + [Type (_,[]),Type ("bool",[])])])))) $ _ $ _)
3.500 + = true
3.501 + | is_equation _ = false;
3.502 +fun equ_lhs ((Const ("op =",(Type ("fun",
3.503 + [Type (_,[]),Type ("fun",
3.504 + [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
3.505 + = l
3.506 + | equ_lhs _ = raise NO_EQUATION_TERM;
3.507 +fun equ_rhs ((Const ("op =",(Type ("fun",
3.508 + [Type (_,[]),Type ("fun",
3.509 + [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
3.510 + = r
3.511 + | equ_rhs _ = raise NO_EQUATION_TERM;
3.512 +
3.513 +
3.514 +fun atom (Const (_,Type (_,[]))) = true
3.515 + | atom (Free (_,Type (_,[]))) = true
3.516 + | atom (Var (_,Type (_,[]))) = true
3.517 +(*| atom (_ (_,"?DUMMY" )) = true ..ML-error *)
3.518 + | atom((Const ("Bin.integ_of_bin",_)) $ _) = true
3.519 + | atom _ = false;
3.520 +
3.521 +fun varids (Const (s,Type (_,[]))) = [strip_thy s]
3.522 + | varids (Free (s,Type (_,[]))) = if is_no s then []
3.523 + else [strip_thy s]
3.524 + | varids (Var((s,_),Type (_,[]))) = [strip_thy s]
3.525 +(*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
3.526 + | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
3.527 + | varids (Abs(a,T,t)) = [a] union (varids t)
3.528 + | varids (t1 $ t2) = (varids t1) union (varids t2)
3.529 + | varids _ = [];
3.530 +(*> val t = term_of (hd (parse Diophant.thy "x"));
3.531 +val t = Free ("x","?DUMMY") : term
3.532 +> varids t;
3.533 +val it = [] : string list [] !!! *)
3.534 +
3.535 +
3.536 +fun bin_ops_only ((Const op_) $ t1 $ t2) =
3.537 + if(is_bin_op (Const op_))
3.538 + then(bin_ops_only t1)andalso(bin_ops_only t2)
3.539 + else false
3.540 + | bin_ops_only t =
3.541 + if atom t then true else bin_ops_only t;
3.542 +
3.543 +fun polynomial opl t bdVar = (* bdVar TODO *)
3.544 + (bin_op t) subset opl andalso (bin_ops_only t);
3.545 +
3.546 +fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)
3.547 + andalso polynomial opl (equ_lhs t) bdVar
3.548 + andalso polynomial opl (equ_rhs t) bdVar
3.549 + andalso ((varids bdVar) subset (varids (equ_lhs t))
3.550 + orelse(varids bdVar) subset (varids (equ_lhs t)));
3.551 +
3.552 +(*fun max is =
3.553 + let fun max_ m [] = m
3.554 + | max_ m (i::is) = if m<i then max_ i is else max_ m is;
3.555 + in max_ (hd is) is end;
3.556 +> max [1,5,3,7,4,2];
3.557 +val it = 7 : int *)
3.558 +
3.559 +fun max (a,b) = if a < b then b else a;
3.560 +
3.561 +fun degree addl mul bdVar t =
3.562 +let
3.563 +fun deg _ _ v (Const (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
3.564 + | deg _ _ v (Free (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
3.565 + | deg _ _ v (Var((s,_),Type (_,[]))) = if v=strip_thy s then 1 else 0
3.566 +(*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
3.567 + | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0
3.568 + | deg addl mul v (h $ t1 $ t2) =
3.569 + if(bin_op h)subset addl
3.570 + then max (deg addl mul v t1 ,deg addl mul v t2)
3.571 + else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)
3.572 +in if polynomial (addl @ [mul]) t bdVar
3.573 + then Some (deg addl mul (id_of bdVar) t) else (None:int option)
3.574 +end;
3.575 +fun degree_ addl mul bdVar t = (* do not export *)
3.576 + let fun opt (Some i)= i
3.577 + | opt None = 0
3.578 +in opt (degree addl mul bdVar t) end;
3.579 +
3.580 +
3.581 +fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2;
3.582 +
3.583 +fun linear_equ addl mul bdVar t =
3.584 + if is_equation t
3.585 + then let val degl = degree_ addl mul bdVar (equ_lhs t);
3.586 + val degr = degree_ addl mul bdVar (equ_rhs t)
3.587 + in if (degl>0 orelse degr>0)andalso max(degl,degr)<2
3.588 + then true else false
3.589 + end
3.590 + else false;
3.591 +(* strip_thy op_ before *)
3.592 +fun is_div_op (dv,(Const (op_,(Type ("fun",
3.593 + [Type (s2,[]),Type ("fun",
3.594 + [Type (s4,tl4),Type (s5,tl5)])])))) )= (dv = strip_thy op_)
3.595 + | is_div_op _ = false;
3.596 +
3.597 +fun is_denom bdVar div_op t =
3.598 + let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
3.599 + | is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
3.600 + | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
3.601 + | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
3.602 + | is bool[v]dv (h$n$d) =
3.603 + if is_div_op(dv,h)
3.604 + then (is false[v]dv n)orelse(is true[v]dv d)
3.605 + else (is bool [v]dv n)orelse(is bool[v]dv d)
3.606 +in is false (varids bdVar) (strip_thy div_op) t end;
3.607 +
3.608 +
3.609 +fun rational t div_op bdVar =
3.610 + is_denom bdVar div_op t andalso bin_ops_only t;
3.611 +
3.612 +
3.613 +
3.614 +(** problem types **)
3.615 +
3.616 +store_pbt
3.617 + (prep_pbt Test.thy "pbl_test_uni_plain2" [] e_pblID
3.618 + (["plain_square","univariate","equation","test"],
3.619 + [("#Given" ,["equality e_","solveFor v_"]),
3.620 + ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |\
3.621 + \(matches ( ?b*v_ ^^^2 = 0) e_) |\
3.622 + \(matches (?a + v_ ^^^2 = 0) e_) |\
3.623 + \(matches ( v_ ^^^2 = 0) e_)"]),
3.624 + ("#Find" ,["solutions v_i_"])
3.625 + ],
3.626 + assoc_rls "matches",
3.627 + Some "solve (e_::bool, v_)", [["Test","solve_plain_square"]]));
3.628 +(*
3.629 + val e_ = (term_of o the o (parse thy)) "e_::bool";
3.630 + val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
3.631 + val env = [(e_,ve)];
3.632 +
3.633 + val pre = (term_of o the o (parse thy))
3.634 + "(matches (a + b*v_ ^^^2 = 0, e_::bool)) |\
3.635 + \(matches ( b*v_ ^^^2 = 0, e_::bool)) |\
3.636 + \(matches (a + v_ ^^^2 = 0, e_::bool)) |\
3.637 + \(matches ( v_ ^^^2 = 0, e_::bool))";
3.638 + val prei = subst_atomic env pre;
3.639 + val cpre = cterm_of (sign_of thy) prei;
3.640 +
3.641 + val Some (ct,_) = rewrite_set_ thy false tval_rls cpre;
3.642 +val ct = "True | False | False | False" : cterm
3.643 +
3.644 +> val Some (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
3.645 +> val Some (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
3.646 +> val Some (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
3.647 +val ct = "True" : cterm
3.648 +
3.649 +*)
3.650 +
3.651 +store_pbt
3.652 + (prep_pbt Test.thy "pbl_test_uni_poly" [] e_pblID
3.653 + (["polynomial","univariate","equation","test"],
3.654 + [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
3.655 + ("#Where" ,["False"]),
3.656 + ("#Find" ,["solutions v_i_"])
3.657 + ],
3.658 + e_rls, Some "solve (e_::bool, v_)", []));
3.659 +
3.660 +store_pbt
3.661 + (prep_pbt Test.thy "pbl_test_uni_poly_deg2" [] e_pblID
3.662 + (["degree_two","polynomial","univariate","equation","test"],
3.663 + [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
3.664 + ("#Find" ,["solutions v_i_"])
3.665 + ],
3.666 + e_rls, Some "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));
3.667 +
3.668 +store_pbt
3.669 + (prep_pbt Test.thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
3.670 + (["pq_formula","degree_two","polynomial","univariate","equation","test"],
3.671 + [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
3.672 + ("#Find" ,["solutions v_i_"])
3.673 + ],
3.674 + e_rls, Some "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));
3.675 +
3.676 +store_pbt
3.677 + (prep_pbt Test.thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
3.678 + (["abc_formula","degree_two","polynomial","univariate","equation","test"],
3.679 + [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_"]),
3.680 + ("#Find" ,["solutions v_i_"])
3.681 + ],
3.682 + e_rls, Some "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_)", []));
3.683 +
3.684 +store_pbt
3.685 + (prep_pbt Test.thy "pbl_test_uni_root" [] e_pblID
3.686 + (["squareroot","univariate","equation","test"],
3.687 + [("#Given" ,["equality e_","solveFor v_"]),
3.688 + ("#Where" ,["contains_root (e_::bool)"]),
3.689 + ("#Find" ,["solutions v_i_"])
3.690 + ],
3.691 + append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
3.692 + eval_contains_root "#contains_root_")],
3.693 + Some "solve (e_::bool, v_)", [["Test","square_equation"]]));
3.694 +
3.695 +store_pbt
3.696 + (prep_pbt Test.thy "pbl_test_uni_norm" [] e_pblID
3.697 + (["normalize","univariate","equation","test"],
3.698 + [("#Given" ,["equality e_","solveFor v_"]),
3.699 + ("#Where" ,[]),
3.700 + ("#Find" ,["solutions v_i_"])
3.701 + ],
3.702 + e_rls, Some "solve (e_::bool, v_)", [["Test","norm_univar_equation"]]));
3.703 +
3.704 +store_pbt
3.705 + (prep_pbt Test.thy "pbl_test_uni_roottest" [] e_pblID
3.706 + (["sqroot-test","univariate","equation","test"],
3.707 + [("#Given" ,["equality e_","solveFor v_"]),
3.708 + (*("#Where" ,["contains_root (e_::bool)"]),*)
3.709 + ("#Find" ,["solutions v_i_"])
3.710 + ],
3.711 + e_rls, Some "solve (e_::bool, v_)", []));
3.712 +
3.713 +(*
3.714 +(#ppc o get_pbt) ["sqroot-test","univariate","equation"];
3.715 + *)
3.716 +
3.717 +
3.718 +store_met
3.719 + (prep_met Test.thy "met_test_sqrt" [] e_metID
3.720 +(*root-equation, version for tests before 8.01.01*)
3.721 + (["Test","sqrt-equ-test"]:metID,
3.722 + [("#Given" ,["equality e_","solveFor v_"]),
3.723 + ("#Where" ,["contains_root (e_::bool)"]),
3.724 + ("#Find" ,["solutions v_i_"])
3.725 + ],
3.726 + {rew_ord'="e_rew_ord",rls'=tval_rls,
3.727 + srls =append_rls "srls_contains_root" e_rls
3.728 + [Calc ("Test.contains'_root",eval_contains_root "")],
3.729 + prls =append_rls "prls_contains_root" e_rls
3.730 + [Calc ("Test.contains'_root",eval_contains_root "")],
3.731 + calc=[],
3.732 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
3.733 + asm_thm=[("square_equation_left",""),
3.734 + ("square_equation_right","")]*)},
3.735 + "Script Solve_root_equation (e_::bool) (v_::real) = \
3.736 + \(let e_ = \
3.737 + \ ((While (contains_root e_) Do\
3.738 + \ ((Rewrite square_equation_left True) @@\
3.739 + \ (Try (Rewrite_Set Test_simplify False)) @@\
3.740 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
3.741 + \ (Try (Rewrite_Set isolate_root False)) @@\
3.742 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
3.743 + \ (Try (Rewrite_Set norm_equation False)) @@\
3.744 + \ (Try (Rewrite_Set Test_simplify False)) @@\
3.745 + \ (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
3.746 + \ (Try (Rewrite_Set Test_simplify False)))\
3.747 + \ e_\
3.748 + \ in [e_::bool])"
3.749 + ));
3.750 +
3.751 +store_met
3.752 + (prep_met Test.thy "met_test_sqrt2" [] e_metID
3.753 +(*root-equation ... for test-*.sml until 8.01*)
3.754 + (["Test","squ-equ-test2"]:metID,
3.755 + [("#Given" ,["equality e_","solveFor v_"]),
3.756 + ("#Find" ,["solutions v_i_"])
3.757 + ],
3.758 + {rew_ord'="e_rew_ord",rls'=tval_rls,
3.759 + srls = append_rls "srls_contains_root" e_rls
3.760 + [Calc ("Test.contains'_root",eval_contains_root"")],
3.761 + prls=e_rls,calc=[],
3.762 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
3.763 + asm_thm=[("square_equation_left",""),
3.764 + ("square_equation_right","")]*)},
3.765 + "Script Solve_root_equation (e_::bool) (v_::real) = \
3.766 + \(let e_ = \
3.767 + \ ((While (contains_root e_) Do\
3.768 + \ ((Rewrite square_equation_left True) @@\
3.769 + \ (Try (Rewrite_Set Test_simplify False)) @@\
3.770 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
3.771 + \ (Try (Rewrite_Set isolate_root False)) @@\
3.772 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
3.773 + \ (Try (Rewrite_Set norm_equation False)) @@\
3.774 + \ (Try (Rewrite_Set Test_simplify False)) @@\
3.775 + \ (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
3.776 + \ (Try (Rewrite_Set Test_simplify False)))\
3.777 + \ e_;\
3.778 + \ (L_::bool list) = Tac subproblem_equation_dummy; \
3.779 + \ L_ = Tac solve_equation_dummy \
3.780 + \ in Check_elementwise L_ {(v_::real). Assumptions})"
3.781 + ));
3.782 +
3.783 +store_met
3.784 + (prep_met Test.thy "met_test_squ_sub" [] e_metID
3.785 +(*tests subproblem fixed linear*)
3.786 + (["Test","squ-equ-test-subpbl1"]:metID,
3.787 + [("#Given" ,["equality e_","solveFor v_"]),
3.788 + ("#Find" ,["solutions v_i_"])
3.789 + ],
3.790 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
3.791 + crls=tval_rls, nrls=Test_simplify},
3.792 + "Script Solve_root_equation (e_::bool) (v_::real) = \
3.793 + \ (let e_ = ((Try (Rewrite_Set norm_equation False)) @@ \
3.794 + \ (Try (Rewrite_Set Test_simplify False))) e_; \
3.795 + \(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\
3.796 + \ [Test,solve_linear]) [bool_ e_, real_ v_])\
3.797 + \in Check_elementwise L_ {(v_::real). Assumptions})"
3.798 + ));
3.799 +
3.800 +store_met
3.801 + (prep_met Test.thy "met_test_squ_sub2" [] e_metID
3.802 + (*tests subproblem fixed degree 2*)
3.803 + (["Test","squ-equ-test-subpbl2"]:metID,
3.804 + [("#Given" ,["equality e_","solveFor v_"]),
3.805 + ("#Find" ,["solutions v_i_"])
3.806 + ],
3.807 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
3.808 + crls=tval_rls, nrls=e_rls(*,
3.809 + asm_rls=[],asm_thm=[("square_equation_left",""),
3.810 + ("square_equation_right","")]*)},
3.811 + "Script Solve_root_equation (e_::bool) (v_::real) = \
3.812 + \ (let e_ = Try (Rewrite_Set norm_equation False) e_; \
3.813 + \(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\
3.814 + \ [Test,solve_by_pq_formula]) [bool_ e_, real_ v_])\
3.815 + \in Check_elementwise L_ {(v_::real). Assumptions})"
3.816 + ));
3.817 +
3.818 +store_met
3.819 + (prep_met Test.thy "met_test_squ_nonterm" [] e_metID
3.820 + (*root-equation: see foils..., but notTerminating*)
3.821 + (["Test","square_equation...notTerminating"]:metID,
3.822 + [("#Given" ,["equality e_","solveFor v_"]),
3.823 + ("#Find" ,["solutions v_i_"])
3.824 + ],
3.825 + {rew_ord'="e_rew_ord",rls'=tval_rls,
3.826 + srls = append_rls "srls_contains_root" e_rls
3.827 + [Calc ("Test.contains'_root",eval_contains_root"")],
3.828 + prls=e_rls,calc=[],
3.829 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
3.830 + asm_thm=[("square_equation_left",""),
3.831 + ("square_equation_right","")]*)},
3.832 + "Script Solve_root_equation (e_::bool) (v_::real) = \
3.833 + \(let e_ = \
3.834 + \ ((While (contains_root e_) Do\
3.835 + \ ((Rewrite square_equation_left True) @@\
3.836 + \ (Try (Rewrite_Set Test_simplify False)) @@\
3.837 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
3.838 + \ (Try (Rewrite_Set isolate_root False)) @@\
3.839 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
3.840 + \ (Try (Rewrite_Set norm_equation False)) @@\
3.841 + \ (Try (Rewrite_Set Test_simplify False)))\
3.842 + \ e_;\
3.843 + \ (L_::bool list) = \
3.844 + \ (SubProblem (Test_,[linear,univariate,equation,test],\
3.845 + \ [Test,solve_linear]) [bool_ e_, real_ v_])\
3.846 + \in Check_elementwise L_ {(v_::real). Assumptions})"
3.847 + ));
3.848 +
3.849 +store_met
3.850 + (prep_met Test.thy "met_test_eq1" [] e_metID
3.851 +(*root-equation1:*)
3.852 + (["Test","square_equation1"]:metID,
3.853 + [("#Given" ,["equality e_","solveFor v_"]),
3.854 + ("#Find" ,["solutions v_i_"])
3.855 + ],
3.856 + {rew_ord'="e_rew_ord",rls'=tval_rls,
3.857 + srls = append_rls "srls_contains_root" e_rls
3.858 + [Calc ("Test.contains'_root",eval_contains_root"")],
3.859 + prls=e_rls,calc=[],
3.860 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
3.861 + asm_thm=[("square_equation_left",""),
3.862 + ("square_equation_right","")]*)},
3.863 + "Script Solve_root_equation (e_::bool) (v_::real) = \
3.864 + \(let e_ = \
3.865 + \ ((While (contains_root e_) Do\
3.866 + \ ((Rewrite square_equation_left True) @@\
3.867 + \ (Try (Rewrite_Set Test_simplify False)) @@\
3.868 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
3.869 + \ (Try (Rewrite_Set isolate_root False)) @@\
3.870 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
3.871 + \ (Try (Rewrite_Set norm_equation False)) @@\
3.872 + \ (Try (Rewrite_Set Test_simplify False)))\
3.873 + \ e_;\
3.874 + \ (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\
3.875 + \ [Test,solve_linear]) [bool_ e_, real_ v_])\
3.876 + \ in Check_elementwise L_ {(v_::real). Assumptions})"
3.877 + ));
3.878 +
3.879 +store_met
3.880 + (prep_met Test.thy "met_test_squ2" [] e_metID
3.881 + (*root-equation2*)
3.882 + (["Test","square_equation2"]:metID,
3.883 + [("#Given" ,["equality e_","solveFor v_"]),
3.884 + ("#Find" ,["solutions v_i_"])
3.885 + ],
3.886 + {rew_ord'="e_rew_ord",rls'=tval_rls,
3.887 + srls = append_rls "srls_contains_root" e_rls
3.888 + [Calc ("Test.contains'_root",eval_contains_root"")],
3.889 + prls=e_rls,calc=[],
3.890 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
3.891 + asm_thm=[("square_equation_left",""),
3.892 + ("square_equation_right","")]*)},
3.893 + "Script Solve_root_equation (e_::bool) (v_::real) = \
3.894 + \(let e_ = \
3.895 + \ ((While (contains_root e_) Do\
3.896 + \ (((Rewrite square_equation_left True) Or \
3.897 + \ (Rewrite square_equation_right True)) @@\
3.898 + \ (Try (Rewrite_Set Test_simplify False)) @@\
3.899 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
3.900 + \ (Try (Rewrite_Set isolate_root False)) @@\
3.901 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
3.902 + \ (Try (Rewrite_Set norm_equation False)) @@\
3.903 + \ (Try (Rewrite_Set Test_simplify False)))\
3.904 + \ e_;\
3.905 + \ (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test],\
3.906 + \ [Test,solve_plain_square]) [bool_ e_, real_ v_])\
3.907 + \ in Check_elementwise L_ {(v_::real). Assumptions})"
3.908 + ));
3.909 +
3.910 +store_met
3.911 + (prep_met Test.thy "met_test_squeq" [] e_metID
3.912 + (*root-equation*)
3.913 + (["Test","square_equation"]:metID,
3.914 + [("#Given" ,["equality e_","solveFor v_"]),
3.915 + ("#Find" ,["solutions v_i_"])
3.916 + ],
3.917 + {rew_ord'="e_rew_ord",rls'=tval_rls,
3.918 + srls = append_rls "srls_contains_root" e_rls
3.919 + [Calc ("Test.contains'_root",eval_contains_root"")],
3.920 + prls=e_rls,calc=[],
3.921 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],
3.922 + asm_thm=[("square_equation_left",""),
3.923 + ("square_equation_right","")]*)},
3.924 + "Script Solve_root_equation (e_::bool) (v_::real) = \
3.925 + \(let e_ = \
3.926 + \ ((While (contains_root e_) Do\
3.927 + \ (((Rewrite square_equation_left True) Or\
3.928 + \ (Rewrite square_equation_right True)) @@\
3.929 + \ (Try (Rewrite_Set Test_simplify False)) @@\
3.930 + \ (Try (Rewrite_Set rearrange_assoc False)) @@\
3.931 + \ (Try (Rewrite_Set isolate_root False)) @@\
3.932 + \ (Try (Rewrite_Set Test_simplify False)))) @@\
3.933 + \ (Try (Rewrite_Set norm_equation False)) @@\
3.934 + \ (Try (Rewrite_Set Test_simplify False)))\
3.935 + \ e_;\
3.936 + \ (L_::bool list) = (SubProblem (Test_,[univariate,equation,test],\
3.937 + \ [no_met]) [bool_ e_, real_ v_])\
3.938 + \ in Check_elementwise L_ {(v_::real). Assumptions})"
3.939 + ) ); (*#######*)
3.940 +
3.941 +store_met
3.942 + (prep_met Test.thy "met_test_eq_plain" [] e_metID
3.943 + (*solve_plain_square*)
3.944 + (["Test","solve_plain_square"]:metID,
3.945 + [("#Given",["equality e_","solveFor v_"]),
3.946 + ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |\
3.947 + \(matches ( ?b*v_ ^^^2 = 0) e_) |\
3.948 + \(matches (?a + v_ ^^^2 = 0) e_) |\
3.949 + \(matches ( v_ ^^^2 = 0) e_)"]),
3.950 + ("#Find" ,["solutions v_i_"])
3.951 + ],
3.952 + {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
3.953 + prls = assoc_rls "matches",
3.954 + crls=tval_rls, nrls=e_rls(*,
3.955 + asm_rls=[],asm_thm=[]*)},
3.956 + "Script Solve_plain_square (e_::bool) (v_::real) = \
3.957 + \ (let e_ = ((Try (Rewrite_Set isolate_bdv False)) @@ \
3.958 + \ (Try (Rewrite_Set Test_simplify False)) @@ \
3.959 + \ ((Rewrite square_equality_0 False) Or \
3.960 + \ (Rewrite square_equality True)) @@ \
3.961 + \ (Try (Rewrite_Set tval_rls False))) e_ \
3.962 + \ in ((Or_to_List e_)::bool list))"
3.963 + ));
3.964 +
3.965 +store_met
3.966 + (prep_met Test.thy "met_test_norm_univ" [] e_metID
3.967 + (["Test","norm_univar_equation"]:metID,
3.968 + [("#Given",["equality e_","solveFor v_"]),
3.969 + ("#Where" ,[]),
3.970 + ("#Find" ,["solutions v_i_"])
3.971 + ],
3.972 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
3.973 + calc=[],
3.974 + crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},
3.975 + "Script Norm_univar_equation (e_::bool) (v_::real) = \
3.976 + \ (let e_ = ((Try (Rewrite rnorm_equation_add False)) @@ \
3.977 + \ (Try (Rewrite_Set Test_simplify False))) e_ \
3.978 + \ in (SubProblem (Test_,[univariate,equation,test], \
3.979 + \ [no_met]) [bool_ e_, real_ v_]))"
3.980 + ));
3.981 +
3.982 +
3.983 +
3.984 +(*17.9.02 aus SqRoot.ML------------------------------^^^---*)
3.985 +
3.986 +(*8.4.03 aus Poly.ML--------------------------------vvv---
3.987 + make_polynomial ---> make_poly
3.988 + ^-- for user ^-- for systest _ONLY_*)
3.989 +
3.990 +local (*. for make_polytest .*)
3.991 +
3.992 +open Term; (* for type order = EQUAL | LESS | GREATER *)
3.993 +
3.994 +fun pr_ord EQUAL = "EQUAL"
3.995 + | pr_ord LESS = "LESS"
3.996 + | pr_ord GREATER = "GREATER";
3.997 +
3.998 +fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
3.999 + (case a of
3.1000 + "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
3.1001 + | _ => (((a, 0), T), 0))
3.1002 + | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
3.1003 + | dest_hd' (Var v) = (v, 2)
3.1004 + | dest_hd' (Bound i) = ((("", i), dummyT), 3)
3.1005 + | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
3.1006 +(* RL *)
3.1007 +fun get_order_pow (t $ (Free(order,_))) =
3.1008 + (case int_of_str (order) of
3.1009 + Some d => d
3.1010 + | None => 0)
3.1011 + | get_order_pow _ = 0;
3.1012 +
3.1013 +fun size_of_term' (Const(str,_) $ t) =
3.1014 + if "Atools.pow"= str then 1000 + size_of_term' t else 1 + size_of_term' t (*WN*)
3.1015 + | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
3.1016 + | size_of_term' (f$t) = size_of_term' f + size_of_term' t
3.1017 + | size_of_term' _ = 1;
3.1018 +
3.1019 +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
3.1020 + (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
3.1021 + | term_ord' pr thy (t, u) =
3.1022 + (if pr then
3.1023 + let
3.1024 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
3.1025 + val _=writeln("t= f@ts= \""^
3.1026 + ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
3.1027 + (commas(map(string_of_cterm o cterm_of (sign_of thy)) ts))^"]\"");
3.1028 + val _=writeln("u= g@us= \""^
3.1029 + ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
3.1030 + (commas(map(string_of_cterm o cterm_of (sign_of thy)) us))^"]\"");
3.1031 + val _=writeln("size_of_term(t,u)= ("^
3.1032 + (string_of_int(size_of_term' t))^", "^
3.1033 + (string_of_int(size_of_term' u))^")");
3.1034 + val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
3.1035 + val _=writeln("terms_ord(ts,us) = "^
3.1036 + ((pr_ord o terms_ord str false)(ts,us)));
3.1037 + val _=writeln("-------");
3.1038 + in () end
3.1039 + else ();
3.1040 + case int_ord (size_of_term' t, size_of_term' u) of
3.1041 + EQUAL =>
3.1042 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
3.1043 + (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
3.1044 + | ord => ord)
3.1045 + end
3.1046 + | ord => ord)
3.1047 +and hd_ord (f, g) = (* ~ term.ML *)
3.1048 + prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
3.1049 +and terms_ord str pr (ts, us) =
3.1050 + list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
3.1051 +in
3.1052 +
3.1053 +fun ord_make_polytest (pr:bool) thy (_:subst) tu =
3.1054 + (term_ord' pr thy(***) tu = LESS );
3.1055 +
3.1056 +end;(*local*)
3.1057 +
3.1058 +rew_ord' := overwritel (!rew_ord',
3.1059 +[("termlessI", termlessI),
3.1060 + ("ord_make_polytest", ord_make_polytest false thy)
3.1061 + ]);
3.1062 +
3.1063 +(*WN060510 this was a preparation for prep_rls ...
3.1064 +val scr_make_polytest =
3.1065 +"Script Expand_binomtest t_ =\
3.1066 +\(Repeat \
3.1067 +\((Try (Repeat (Rewrite real_diff_minus False))) @@ \
3.1068 +
3.1069 +\ (Try (Repeat (Rewrite real_add_mult_distrib False))) @@ \
3.1070 +\ (Try (Repeat (Rewrite real_add_mult_distrib2 False))) @@ \
3.1071 +\ (Try (Repeat (Rewrite real_diff_mult_distrib False))) @@ \
3.1072 +\ (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ \
3.1073 +
3.1074 +\ (Try (Repeat (Rewrite real_mult_1 False))) @@ \
3.1075 +\ (Try (Repeat (Rewrite real_mult_0 False))) @@ \
3.1076 +\ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \
3.1077 +
3.1078 +\ (Try (Repeat (Rewrite real_mult_commute False))) @@ \
3.1079 +\ (Try (Repeat (Rewrite real_mult_left_commute False))) @@ \
3.1080 +\ (Try (Repeat (Rewrite real_mult_assoc False))) @@ \
3.1081 +\ (Try (Repeat (Rewrite real_add_commute False))) @@ \
3.1082 +\ (Try (Repeat (Rewrite real_add_left_commute False))) @@ \
3.1083 +\ (Try (Repeat (Rewrite real_add_assoc False))) @@ \
3.1084 +
3.1085 +\ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \
3.1086 +\ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \
3.1087 +\ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \
3.1088 +\ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \
3.1089 +
3.1090 +\ (Try (Repeat (Rewrite real_num_collect False))) @@ \
3.1091 +\ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
3.1092 +
3.1093 +\ (Try (Repeat (Rewrite real_one_collect False))) @@ \
3.1094 +\ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
3.1095 +
3.1096 +\ (Try (Repeat (Calculate plus ))) @@ \
3.1097 +\ (Try (Repeat (Calculate times ))) @@ \
3.1098 +\ (Try (Repeat (Calculate power_)))) \
3.1099 +\ t_)";
3.1100 +-----------------------------------------------------*)
3.1101 +
3.1102 +val make_polytest =
3.1103 + Rls{id = "make_polytest", preconds = []:term list, rew_ord = ("ord_make_polytest",
3.1104 + ord_make_polytest false Poly.thy),
3.1105 + erls = testerls, srls = Erls,
3.1106 + calc = [("plus" , ("op +", eval_binop "#add_")),
3.1107 + ("times" , ("op *", eval_binop "#mult_")),
3.1108 + ("power_", ("Atools.pow", eval_binop "#power_"))
3.1109 + ],
3.1110 + (*asm_thm = [],*)
3.1111 + rules = [Thm ("real_diff_minus",num_str real_diff_minus),
3.1112 + (*"a - b = a + (-1) * b"*)
3.1113 + Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
3.1114 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
3.1115 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
3.1116 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
3.1117 + Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
3.1118 + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
3.1119 + Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
3.1120 + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
3.1121 + Thm ("real_mult_1",num_str real_mult_1),
3.1122 + (*"1 * z = z"*)
3.1123 + Thm ("real_mult_0",num_str real_mult_0),
3.1124 + (*"0 * z = 0"*)
3.1125 + Thm ("real_add_zero_left",num_str real_add_zero_left),
3.1126 + (*"0 + z = z"*)
3.1127 +
3.1128 + (*AC-rewriting*)
3.1129 + Thm ("real_mult_commute",num_str real_mult_commute),
3.1130 + (* z * w = w * z *)
3.1131 + Thm ("real_mult_left_commute",num_str real_mult_left_commute),
3.1132 + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
3.1133 + Thm ("real_mult_assoc",num_str real_mult_assoc),
3.1134 + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
3.1135 + Thm ("real_add_commute",num_str real_add_commute),
3.1136 + (*z + w = w + z*)
3.1137 + Thm ("real_add_left_commute",num_str real_add_left_commute),
3.1138 + (*x + (y + z) = y + (x + z)*)
3.1139 + Thm ("real_add_assoc",num_str real_add_assoc),
3.1140 + (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
3.1141 +
3.1142 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
3.1143 + (*"r1 * r1 = r1 ^^^ 2"*)
3.1144 + Thm ("realpow_plus_1",num_str realpow_plus_1),
3.1145 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
3.1146 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
3.1147 + (*"z1 + z1 = 2 * z1"*)
3.1148 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
3.1149 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
3.1150 +
3.1151 + Thm ("real_num_collect",num_str real_num_collect),
3.1152 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
3.1153 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
3.1154 + (*"[| l is_const; m is_const |] ==>
3.1155 + l * n + (m * n + k) = (l + m) * n + k"*)
3.1156 + Thm ("real_one_collect",num_str real_one_collect),
3.1157 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
3.1158 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
3.1159 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
3.1160 +
3.1161 + Calc ("op +", eval_binop "#add_"),
3.1162 + Calc ("op *", eval_binop "#mult_"),
3.1163 + Calc ("Atools.pow", eval_binop "#power_")
3.1164 + ],
3.1165 + scr = EmptyScr(*Script ((term_of o the o (parse thy))
3.1166 + scr_make_polytest)*)
3.1167 + }:rls;
3.1168 +(*WN060510 this was done before 'fun prep_rls' ...
3.1169 +val scr_expand_binomtest =
3.1170 +"Script Expand_binomtest t_ =\
3.1171 +\(Repeat \
3.1172 +\((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ \
3.1173 +\ (Try (Repeat (Rewrite real_plus_binom_times False))) @@ \
3.1174 +\ (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ \
3.1175 +\ (Try (Repeat (Rewrite real_minus_binom_times False))) @@ \
3.1176 +\ (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ \
3.1177 +\ (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ \
3.1178 +
3.1179 +\ (Try (Repeat (Rewrite real_mult_1 False))) @@ \
3.1180 +\ (Try (Repeat (Rewrite real_mult_0 False))) @@ \
3.1181 +\ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \
3.1182 +
3.1183 +\ (Try (Repeat (Calculate plus ))) @@ \
3.1184 +\ (Try (Repeat (Calculate times ))) @@ \
3.1185 +\ (Try (Repeat (Calculate power_))) @@ \
3.1186 +
3.1187 +\ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \
3.1188 +\ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \
3.1189 +\ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \
3.1190 +\ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \
3.1191 +
3.1192 +\ (Try (Repeat (Rewrite real_num_collect False))) @@ \
3.1193 +\ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
3.1194 +
3.1195 +\ (Try (Repeat (Rewrite real_one_collect False))) @@ \
3.1196 +\ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
3.1197 +
3.1198 +\ (Try (Repeat (Calculate plus ))) @@ \
3.1199 +\ (Try (Repeat (Calculate times ))) @@ \
3.1200 +\ (Try (Repeat (Calculate power_)))) \
3.1201 +\ t_)";
3.1202 +------------------------------------------------------*)
3.1203 +
3.1204 +val expand_binomtest =
3.1205 + Rls{id = "expand_binomtest", preconds = [],
3.1206 + rew_ord = ("termlessI",termlessI),
3.1207 + erls = testerls, srls = Erls,
3.1208 + calc = [("plus" , ("op +", eval_binop "#add_")),
3.1209 + ("times" , ("op *", eval_binop "#mult_")),
3.1210 + ("power_", ("Atools.pow", eval_binop "#power_"))
3.1211 + ],
3.1212 + (*asm_thm = [],*)
3.1213 + rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
3.1214 + (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
3.1215 + Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
3.1216 + (*"(a + b)*(a + b) = ...*)
3.1217 + Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
3.1218 + (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
3.1219 + Thm ("real_minus_binom_times",num_str real_minus_binom_times),
3.1220 + (*"(a - b)*(a - b) = ...*)
3.1221 + Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
3.1222 + (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
3.1223 + Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
3.1224 + (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
3.1225 + (*RL 020915*)
3.1226 + Thm ("real_pp_binom_times",num_str real_pp_binom_times),
3.1227 + (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
3.1228 + Thm ("real_pm_binom_times",num_str real_pm_binom_times),
3.1229 + (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
3.1230 + Thm ("real_mp_binom_times",num_str real_mp_binom_times),
3.1231 + (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
3.1232 + Thm ("real_mm_binom_times",num_str real_mm_binom_times),
3.1233 + (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
3.1234 + Thm ("realpow_multI",num_str realpow_multI),
3.1235 + (*(a*b)^^^n = a^^^n * b^^^n*)
3.1236 + Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
3.1237 + (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
3.1238 + Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),
3.1239 + (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
3.1240 +
3.1241 +
3.1242 + (* Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
3.1243 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
3.1244 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
3.1245 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
3.1246 + Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
3.1247 + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
3.1248 + Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
3.1249 + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
3.1250 + *)
3.1251 +
3.1252 + Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
3.1253 + Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
3.1254 + Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*)
3.1255 +
3.1256 + Calc ("op +", eval_binop "#add_"),
3.1257 + Calc ("op *", eval_binop "#mult_"),
3.1258 + Calc ("Atools.pow", eval_binop "#power_"),
3.1259 + (*
3.1260 + Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
3.1261 + Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
3.1262 + Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
3.1263 + Thm ("real_add_commute",num_str real_add_commute), (**)
3.1264 + Thm ("real_add_left_commute",num_str real_add_left_commute), (**)
3.1265 + Thm ("real_add_assoc",num_str real_add_assoc), (**)
3.1266 + *)
3.1267 +
3.1268 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
3.1269 + (*"r1 * r1 = r1 ^^^ 2"*)
3.1270 + Thm ("realpow_plus_1",num_str realpow_plus_1),
3.1271 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
3.1272 + (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
3.1273 + (*"z1 + z1 = 2 * z1"*)*)
3.1274 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
3.1275 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
3.1276 +
3.1277 + Thm ("real_num_collect",num_str real_num_collect),
3.1278 + (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
3.1279 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
3.1280 + (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
3.1281 + Thm ("real_one_collect",num_str real_one_collect),
3.1282 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
3.1283 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
3.1284 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
3.1285 +
3.1286 + Calc ("op +", eval_binop "#add_"),
3.1287 + Calc ("op *", eval_binop "#mult_"),
3.1288 + Calc ("Atools.pow", eval_binop "#power_")
3.1289 + ],
3.1290 + scr = EmptyScr
3.1291 +(*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
3.1292 + }:rls;
3.1293 +
3.1294 +
3.1295 +ruleset' := overwritelthy thy (!ruleset',
3.1296 + [("make_polytest", prep_rls make_polytest),
3.1297 + ("expand_binomtest", prep_rls expand_binomtest)
3.1298 + ]);
3.1299 +
3.1300 +
3.1301 +
3.1302 +
3.1303 +
3.1304 +
4.1 --- a/src/sml/ROOT.ML Mon Dec 03 15:59:34 2007 +0100
4.2 +++ b/src/sml/ROOT.ML Mon Dec 03 19:11:27 2007 +0100
4.3 @@ -12,7 +12,7 @@
4.4
4.5 (*.please change HERE and in RCODE-root accordingly,
4.6 if you store a new heap ...*)
4.7 -val version_isac = "WN0710-calcResponse";
4.8 +val version_isac = "WN071206-log-demo";
4.9
4.10 print_depth 1;(*reduces verbosity of stdout*)
4.11
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/smltest/IsacKnowledge/logexp.sml Mon Dec 03 19:11:27 2007 +0100
5.3 @@ -0,0 +1,61 @@
5.4 +(* testexamples for LogExp, logarithms and exponential functions and terms
5.5 +
5.6 +use"../smltest/IsacKnowledge/logexp.sml";
5.7 +*)
5.8 +
5.9 +val thy = LogExp.thy;
5.10 +"-----------------------------------------------------------------";
5.11 +"table of contents -----------------------------------------------";
5.12 +"-----------------------------------------------------------------";
5.13 +"----------- setup presentation innsbruck ------------------------";
5.14 +"-----------------------------------------------------------------";
5.15 +"-----------------------------------------------------------------";
5.16 +"-----------------------------------------------------------------";
5.17 +
5.18 +
5.19 +"----------- setup presentation innsbruck ------------------------";
5.20 +"----------- setup presentation innsbruck ------------------------";
5.21 +"----------- setup presentation innsbruck ------------------------";
5.22 +(*
5.23 +NOT INCLUDED IN ROOT.ML and RTEST-root.sml, since the pbl and met
5.24 +defined in IsacKnowledge/Test.ML are out-commented
5.25 +in order to allow for demonstration of authoring !
5.26 +
5.27 +equality_power;
5.28 +exp_invers_log;
5.29 +(* WN071203 ???... wrong thy ?!? because parsing with Isac.thy works ?
5.30 +refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"]
5.31 + ["equation","test"];
5.32 +*)
5.33 +
5.34 +val t = str2term "(2 log x)";
5.35 +val t = str2term "(2 log x) = 3";
5.36 +val t = str2term "matches ((?a log x) = ?b) ((2 log x) = 3)";
5.37 +atomty t;
5.38 +
5.39 +
5.40 +val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"];
5.41 +val (dI',pI',mI') =
5.42 + ("Isac.thy",["logarithmic","univariate","equation","test"],
5.43 + ["Test","solve_log"]);
5.44 +val p = e_pos'; val c = [];
5.45 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.46 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.47 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.48 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.49 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.50 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.51 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.52 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.53 +case nxt of ("Apply_Method",_) => ()
5.54 + | _ => raise error "logexp.sml setup innsbruck";
5.55 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.56 +
5.57 +
5.58 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.59 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.60 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.61 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.62 +show_pt pt;
5.63 +
5.64 +*-------------------------------------------------------------------*)