1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Mar 08 12:30:46 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sat Mar 10 17:20:15 2018 +0100
1.3 @@ -136,7 +136,7 @@
1.4 Thm ("integral_var", @{thm integral_var}),
1.5 Thm ("integral_add", @{thm integral_add}),
1.6 Thm ("integral_mult", @{thm integral_mult}),
1.7 - Thm ("integral_pow", @{thm integral_pow}),
1.8 + Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
1.9 Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
1.10 ],
1.11 scr = EmptyScr};
2.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Mar 08 12:30:46 2018 +0100
2.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Sat Mar 10 17:20:15 2018 +0100
2.3 @@ -44,7 +44,7 @@
2.4
2.5 fun rewrite__ thy i bdv tless rls put_asm thm ct =
2.6 let
2.7 - val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
2.8 + val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: lrd list)
2.9 (((TermC.inst_bdv bdv) o Calc.norm o #prop o Thm.rep_thm) thm) ct
2.10 in if rew then SOME (t', distinct asms) else NONE end
2.11 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
2.12 @@ -127,7 +127,7 @@
2.13 let
2.14 (* attention with cp to test/..: unbound thy, i, bdv, rls TODO1803? pull out to rewrite__*)
2.15 datatype switch = Appl | Noap;
2.16 - fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Ttools.rew_once? *)
2.17 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Tools.rew_once? *)
2.18 | rew_once ruls asm ct Appl [] =
2.19 (case rls of Rls _ => rew_once ruls asm ct Noap ruls
2.20 | Seq _ => (ct, asm)
2.21 @@ -141,7 +141,8 @@
2.22 NONE => rew_once ruls asm ct apno thms
2.23 | SOME (ct', asm') =>
2.24 (trace1 i (" rewrites to: " ^ t2str thy ct');
2.25 - rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
2.26 + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
2.27 + (* once again try the same rule, e.g. associativity against "()"*)
2.28 | Calc (cc as (op_, _)) =>
2.29 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
2.30 val ct = TermC.uminus_to_string ct
3.1 --- a/src/Tools/isac/ProgLang/termC.sml Thu Mar 08 12:30:46 2018 +0100
3.2 +++ b/src/Tools/isac/ProgLang/termC.sml Sat Mar 10 17:20:15 2018 +0100
3.3 @@ -76,8 +76,8 @@
3.4 val var2free: term -> term
3.5 val vars: term -> term list
3.6 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.7 + val scala_of_term: term -> string
3.8 val atomtyp(*<-- atom_typ TODO*): typ -> unit
3.9 - val scala_of_term: term -> string
3.10 val atomty: term -> unit
3.11 val atomw: term -> unit
3.12 val atomwy: term -> unit
4.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Mar 08 12:30:46 2018 +0100
4.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sat Mar 10 17:20:15 2018 +0100
4.3 @@ -178,7 +178,7 @@
4.4 "----------- simplify by ruleset reducing make_ratpoly_in";
4.5 val thy = @{theory "Isac"};
4.6 "===== test 1";
4.7 -val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
4.8 +val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
4.9
4.10 "----- stepwise from the rulesets in simplify_Integral and below-----";
4.11 val rls = norm_Rational_noadd_fractions;
4.12 @@ -199,6 +199,7 @@
4.13 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
4.14
4.15 "===== test 4";
4.16 +val subs = [(str2t "bdv::real", str2t "x::real")];
4.17 val rls =
4.18 (append_rls "separate_bdv" collect_bdv
4.19 [Thm ("separate_bdv", num_str @{thm separate_bdv}),
5.1 --- a/test/Tools/isac/Test_Isac.thy Thu Mar 08 12:30:46 2018 +0100
5.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Mar 10 17:20:15 2018 +0100
5.3 @@ -294,73 +294,80 @@
5.4 ML_file "Knowledge/integrate.sml"
5.5
5.6 ML {*
5.7 -"~~~~~ fun xxx, args:"; val () = ();
5.8 +*} ML {*
5.9 +"----------- integrate by ruleset -----------------------";
5.10 +"----------- integrate by ruleset -----------------------";
5.11 +"----------- integrate by ruleset -----------------------";
5.12 +val thy = @{theory "Integrate"};
5.13 +val rls = integration_rules;
5.14 +val subs = [(@{term "bdv::real"}, @{term "x::real"})];
5.15 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.16 +
5.17 +val t = (Thm.term_of o the o (parse thy)) "Integral x D x";
5.18 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.19 +if term2str res = "x ^^^ 2 / 2" then () else error "Integral x D x changed";
5.20 +
5.21 +val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
5.22 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.23 +if term2str res = "c * (x ^^^ 3 / 3) + c_2 * x" then () else error "Integral c * x ^^^ 2 + c_2 D x";
5.24 +
5.25 +val rls = add_new_c;
5.26 +val t = (Thm.term_of o the o (parse thy)) "c * (x ^^^ 3 / 3) + c_2 * x";
5.27 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.28 +if term2str res = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
5.29 +else error "integrate.sml: diff.behav. in add_new_c simpl.";
5.30 +
5.31 +val t = (Thm.term_of o the o (parse thy)) "F x = x ^^^ 3 / 3 + x";
5.32 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.33 +if term2str res = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
5.34 +else error "integrate.sml: diff.behav. in add_new_c equation";
5.35 +
5.36 +val rls = simplify_Integral;
5.37 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.38 +val t = (Thm.term_of o the o (parse thy)) "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
5.39 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.40 +if term2str res = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
5.41 +then () else error "integrate.sml: diff.behav. in simplify_I #1";
5.42 +
5.43 +val rls = integration;
5.44 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.45 +val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
5.46 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.47 +if term2str res = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
5.48 +then () else error "integrate.sml: diff.behav. in integration #1";
5.49 +
5.50 +val t = (Thm.term_of o the o (parse thy)) "Integral 3*x^^^2 + 2*x + 1 D x";
5.51 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.52 +*} ML {*
5.53 +term2str res = "c + x + 2 / 2 * x ^^^ 2 + x ^^^ 3";
5.54 +*} ML {*
5.55 +if term2str res = "c + x + x ^^^ 2 + x ^^^ 3" then ()
5.56 +else error "integrate.sml: diff.behav. in integration #2";
5.57 *} ML {*
5.58
5.59 +val t = (Thm.term_of o the o (parse thy))
5.60 + "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
5.61 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.62 +"Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
5.63 *} ML {*
5.64 +term2str res = "c + 1 / EI * (L * q_0 / (2 * 2) * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
5.65 *} ML {*
5.66 -val thy = @{theory "Isac"};
5.67 -"===== test 1";
5.68 -val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
5.69 +if term2str res = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
5.70 +then () else error "integrate.sml: diff.behav. in integration #3";
5.71
5.72 -"----- stepwise from the rulesets in simplify_Integral and below-----";
5.73 -val rls = norm_Rational_noadd_fractions;
5.74 -case rewrite_set_inst_ thy true subs rls t of
5.75 - SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
5.76 - | NONE => ();
5.77 +val t = (Thm.term_of o the o (parse thy)) ("Integral " ^ term2str res ^ " D x");
5.78 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.79 +*} ML {*
5.80 +*} ML {* (* folgefehler --------------------------------- ^^^^^^^^^^^ *)
5.81 +if term2str res = "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
5.82 +then () else error "integrate.sml: diff.behav. in integration #4";
5.83
5.84 -"===== test 2";
5.85 -val rls = order_add_mult_in;
5.86 -val SOME (t,[]) = rewrite_set_ thy true rls t;
5.87 -if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
5.88 -else error "integrate.sml simplify by ruleset order_add_mult_in #2";
5.89 -
5.90 -"===== test 3";
5.91 -val rls = discard_parentheses;
5.92 -val SOME (t,[]) = rewrite_set_ thy true rls t;
5.93 -if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
5.94 -else error "integrate.sml simplify by ruleset discard_parenth.. #3";
5.95 -
5.96 -"===== test 4";
5.97 -val rls =
5.98 - (append_rls "separate_bdv" collect_bdv
5.99 - [Thm ("separate_bdv", num_str @{thm separate_bdv}),
5.100 - (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
5.101 - Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
5.102 - (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
5.103 - Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
5.104 - (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
5.105 - Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})
5.106 - (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
5.107 - ]);
5.108 -(*show_types := true; --- do we need type-constraint in thms? *)
5.109 -@{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
5.110 -@{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
5.111 -@{thm separate_1_bdv}; (*::?'a*)
5.112 -val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)
5.113 -@{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
5.114 -(*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
5.115 -
5.116 +"----------- rewrite 3rd integration in 7.27 ------------";
5.117 *} ML {*
5.118 -"~~~~~ fun xxx, args:"; val () = ();
5.119 -(*//==========================================================================================\\*)
5.120 *} ML {*
5.121 *} ML {*
5.122 *} ML {*
5.123 *} ML {*
5.124 -*} ML {*
5.125 -(*\\==========================================================================================//*)
5.126 -"~~~~~ fun xxx, args:"; val () = ();
5.127 -*} ML {*
5.128 -(* isabisac <> isabisac15 *)
5.129 -(*val SOME (t, []) = rewrite_set_inst_ thy true subs rls t; isabisac15 *)
5.130 - val NONE = rewrite_set_inst_ thy true subs rls t; (* isabisac *)
5.131 -*} text {*
5.132 -if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
5.133 -else error "integrate.sml simplify by ruleset separate_bdv.. #4";
5.134 -
5.135 -"===== test 5";
5.136 -*} ML {*
5.137 *}
5.138
5.139
5.140 @@ -368,6 +375,17 @@
5.141
5.142
5.143
5.144 +
5.145 +
5.146 +
5.147 +
5.148 +
5.149 +
5.150 +
5.151 +
5.152 +
5.153 +
5.154 +
5.155 ML_file "Knowledge/eqsystem.sml"
5.156 ML_file "Knowledge/test.sml"
5.157 ML_file "Knowledge/polyminus.sml"