1.1 --- a/test/Tools/isac/Knowledge/rational.sml Wed Mar 27 11:20:43 2019 +0100
1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Mar 27 19:14:47 2019 +0100
1.3 @@ -18,6 +18,7 @@
1.4 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
1.5 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
1.6 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
1.7 +"----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
1.8 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
1.9 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
1.10 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
1.11 @@ -423,6 +424,95 @@
1.12 val ((a', b'), c) = gcd_poly a b
1.13 *)
1.14
1.15 +"----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
1.16 +"----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
1.17 +"----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
1.18 +val thy = @{theory Isac(*Partial_Fractions*)}
1.19 +val ctxt = Proof_Context.init_global thy;
1.20 +
1.21 +(*---------- (1) with Free A, B ----------------------------------------------------------------*)
1.22 +val t = (the o (parseNEW ctxt)) "3 = A / 2 + A / 4 + (B / 2 + -1 * B / (2::real))";
1.23 + (* required for applying thms in rewriting ^^^^*)
1.24 +(* we get details from here..*)
1.25 +
1.26 +Celem.trace_rewrite := true;
1.27 +val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
1.28 +Celem.trace_rewrite := false;
1.29 +(* trace_rewrite:
1.30 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.31 + (* |||||||||||||||||||||||||||||||||||| *)
1.32 +
1.33 +val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 1 GUESS 1 GUESS 1 GUESS 1 *)
1.34 + "A / 2 + A / 4 + (B / 2 + -1 * B / (2::real))";
1.35 +"~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
1.36 +val NONE = (*case*) check_frac_sum t (*of*)
1.37 +
1.38 +(* trace_rewrite:
1.39 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.40 + (* |||||||||||||||||||||||||||| *)
1.41 +val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)
1.42 + "A / 4 + (B / 2 + -1 * B / (2::real))";
1.43 +"~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
1.44 +val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
1.45 +(*+*)if (term2str n1, term2str d1) = ("A" , "4") andalso
1.46 +(*+*) (term2str n2, term2str d2) = ("B / 2 + -1 * B / 2", "1")
1.47 +(*+*)then () else error "check_frac_sum (A / 4 + (B / 2 + -1 * B / (2::real))) changed";
1.48 +
1.49 + val vs = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord;
1.50 +val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =
1.51 + (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
1.52 +
1.53 +"~~~~~ fun poly_of_term , args:"; val (vs, t) = (vs, n1);
1.54 +val SOME [(1, [xxx, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];
1.55 +(*+*)if xxx = 1 then () else error "monom_of_term changed"
1.56 +
1.57 +"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Free (id, _))) =
1.58 + (vs, (1, replicate (length vs) 0), t);
1.59 +if vs = ["A", "B"] andalso c = 1 andalso id = "A"
1.60 +then () else error "monom_of_term Free changed";
1.61 +
1.62 +(*---------- (2) with Const AA, BB --------------------------------------------------------------*)
1.63 +val t = (the o (parseNEW ctxt)) "3 = AA / 2 + AA / 4 + (BB / 2 + -1 * BB / 2)";
1.64 + (*AA :: real*)
1.65 +(* we get details from here..*)
1.66 +
1.67 +Celem.trace_rewrite := true;
1.68 +val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
1.69 +Celem.trace_rewrite := false;
1.70 +(* trace_rewrite:
1.71 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.72 + (* |||||||||||||||||||||||||||||||||||| *)
1.73 +
1.74 +val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
1.75 + "AA / 2 + AA / 4 + (BB / 2 + -1 * BB / 2)";
1.76 +"~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
1.77 +val NONE = (*case*) check_frac_sum t (*of*)
1.78 +
1.79 +(* trace_rewrite:
1.80 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.81 + (* |||||||||||||||||||||||||||| *)
1.82 +val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
1.83 + "AA / 4 + (BB / 2 + -1 * BB / 2)";
1.84 +"~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
1.85 +val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
1.86 +(*+*)if (term2str n1, term2str d1) = ("AA" , "4") andalso
1.87 +(*+*) (term2str n2, term2str d2) = ("BB / 2 + -1 * BB / 2", "1")
1.88 +(*+*)then () else error "check_frac_sum (AA / 4 + (BB / 2 + -1 * BB / 2)) changed";
1.89 +
1.90 + val vs = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord;
1.91 +val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =
1.92 + (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
1.93 +
1.94 +"~~~~~ fun poly_of_term , args:"; val (vs, t) = (vs, n1);
1.95 +val SOME [(1, [xxx, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];
1.96 +(*+*)if xxx = 1 then () else error "monom_of_term changed"
1.97 +
1.98 +"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (id, _))) =
1.99 + (vs, (1, replicate (length vs) 0), t);
1.100 +if vs = ["AA", "BB"] andalso c = 1 andalso id = "Partial_Fractions.AA"
1.101 +then () else error "monom_of_term Const changed";
1.102 +
1.103 +
1.104 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
1.105 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
1.106 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";