1.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Tue Mar 06 14:25:08 2012 +0100
1.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Mar 08 14:33:34 2012 +0100
1.3 @@ -12,6 +12,8 @@
1.4 "----------- Logic.unvarify_global ----------------------";
1.5 "----------- eval_drop_questionmarks --------------------";
1.6 "----------- = me for met_partial_fraction --------------";
1.7 +"----------- progr.vers.2: check erls for multiply_ansatz";
1.8 +"----------- progr.vers.2: improve program --------------";
1.9 "--------------------------------------------------------";
1.10 "--------------------------------------------------------";
1.11 "--------------------------------------------------------";
1.12 @@ -219,3 +221,81 @@
1.13 if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then()
1.14 else error "= me .. met_partial_fraction broken";
1.15
1.16 +"----------- progr.vers.2: check erls for multiply_ansatz";
1.17 +"----------- progr.vers.2: check erls for multiply_ansatz";
1.18 +"----------- progr.vers.2: check erls for multiply_ansatz";
1.19 +(*test for outcommented 3 lines in script: is norm_Rational strong enough?*)
1.20 +val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))";
1.21 +val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t;
1.22 +term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
1.23 +
1.24 +val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*)
1.25 +term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
1.26 + "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
1.27 +
1.28 +val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
1.29 +if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then ()
1.30 +else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
1.31 +
1.32 +(*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
1.33 +val xxx = append_rls "multiply_ansatz_erls" norm_Rational
1.34 + [Calc ("HOL.eq",eval_equal "#equal_")];
1.35 +
1.36 +val multiply_ansatz = prep_rls(
1.37 + Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.38 + erls = xxx,
1.39 + srls = Erls, calc = [],
1.40 + rules =
1.41 + [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
1.42 + ],
1.43 + scr = EmptyScr}:rls);
1.44 +
1.45 +rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*)
1.46 +rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?: GOON*)
1.47 +
1.48 +"----------- progr.vers.2: improve program --------------";
1.49 +"----------- progr.vers.2: improve program --------------";
1.50 +"----------- progr.vers.2: improve program --------------";
1.51 +(*WN120318 stopped due to much effort with the test above*)
1.52 + "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
1.53 + " (let f_f = Take f_f; " ^
1.54 + " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
1.55 + " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
1.56 + " (numer::real) = get_numerator f_f; " ^(*numer: 24*)
1.57 + " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)
1.58 + " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)
1.59 + " (L_L::bool list) = (SubProblem (PolyEq', " ^
1.60 + " [abcFormula, degree_2, polynomial, univariate, equation], " ^
1.61 + " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)
1.62 + " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)
1.63 + " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *)
1.64 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
1.65 + " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
1.66 +(*this has been tested below by rewrite_set_
1.67 + " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**)
1.68 + " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**)
1.69 + " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
1.70 +NEXT try to outcomment the very next line..*)
1.71 + " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
1.72 + " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
1.73 + " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*)
1.74 + " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: -1 / 4*)
1.75 + " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
1.76 + " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
1.77 + " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
1.78 + " (sol_a::bool list) = " ^
1.79 + " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
1.80 + " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
1.81 + " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
1.82 + " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
1.83 + " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
1.84 + " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
1.85 + " (sol_b::bool list) = " ^
1.86 + " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
1.87 + " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
1.88 + " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
1.89 + " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
1.90 + " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)
1.91 + " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.92 + " in pbz)"
1.93 +