1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Tue Mar 06 14:25:08 2012 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Mar 08 14:33:34 2012 +0100
1.3 @@ -99,10 +99,17 @@
1.4 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
1.5 ansatz_3rd_order: "n / (a*b*c) = A/a + B/b + C/c" and
1.6 ansatz_4th_order: "n / (a*b*c*d) = A/a + B/b + C/c + D/d" and
1.7 + (*version 1*)
1.8 equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)" and
1.9 equival_trans_3rd_order: "(n/(a*b*c) = A/a + B/b + C/c) = (n = A*b*c + B*a*c + C*a*b)" and
1.10 equival_trans_4th_order: "(n/(a*b*c*d) = A/a + B/b + C/c + D/d) =
1.11 - (n = A*b*c*d + B*a*c*d + C*a*b*d + D*a*b*c)"
1.12 + (n = A*b*c*d + B*a*c*d + C*a*b*d + D*a*b*c)" and
1.13 + (*version 2: not yet used, see partial_fractions.sml*)
1.14 + multiply_2nd_order: "x = a*b ==> (n/x = A/a + B/b) = (a*b*n/x = A*b + B*a)" and
1.15 + multiply_3rd_order: "x = a*b*c ==>
1.16 + (n/x = A/a + B/b + C/c) = (a*b*c*n/x = A*b*c + B*a*c + C*a*b)" and
1.17 + multiply_4th_order: "x = a*b*c*d ==>
1.18 + (n/x = A/a + B/b + C/c + D/d) = (a*b*c*d*n/x = A*b*c*d + B*a*c*d + C*a*b*d + D*a*b*c)"
1.19
1.20 ML {*
1.21 val ansatz_rls = prep_rls(
1.22 @@ -113,9 +120,7 @@
1.23 Thm ("ansatz_3rd_order",num_str @{thm ansatz_3rd_order})
1.24 ],
1.25 scr = EmptyScr}:rls);
1.26 -*}
1.27
1.28 -ML {*
1.29 val equival_trans = prep_rls(
1.30 Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.31 erls = Erls, srls = Erls, calc = [],
1.32 @@ -124,12 +129,22 @@
1.33 Thm ("equival_trans_3rd_order",num_str @{thm equival_trans_3rd_order})
1.34 ],
1.35 scr = EmptyScr}:rls);
1.36 +
1.37 +val multiply_ansatz = prep_rls(
1.38 + Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.39 + erls = Erls,
1.40 + srls = Erls, calc = [],
1.41 + rules =
1.42 + [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
1.43 + ],
1.44 + scr = EmptyScr}:rls);
1.45 *}
1.46
1.47 text {*store the rule set for math engine*}
1.48 ML {*
1.49 ruleset' := overwritelthy @{theory} (!ruleset',
1.50 [("ansatz_rls", ansatz_rls),
1.51 + ("multiply_ansatz", multiply_ansatz),
1.52 ("equival_trans", equival_trans)
1.53 ]);
1.54 *}
1.55 @@ -140,6 +155,7 @@
1.56 decomposedFunction :: "real => una"
1.57
1.58 ML {*
1.59 +check_guhs_unique := false; (*WN120307 REMOVE after editing*)
1.60 store_pbt
1.61 (prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID
1.62 (["partial_fraction", "rational", "simplification"],
2.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Tue Mar 06 14:25:08 2012 +0100
2.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Mar 08 14:33:34 2012 +0100
2.3 @@ -12,6 +12,8 @@
2.4 "----------- Logic.unvarify_global ----------------------";
2.5 "----------- eval_drop_questionmarks --------------------";
2.6 "----------- = me for met_partial_fraction --------------";
2.7 +"----------- progr.vers.2: check erls for multiply_ansatz";
2.8 +"----------- progr.vers.2: improve program --------------";
2.9 "--------------------------------------------------------";
2.10 "--------------------------------------------------------";
2.11 "--------------------------------------------------------";
2.12 @@ -219,3 +221,81 @@
2.13 if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then()
2.14 else error "= me .. met_partial_fraction broken";
2.15
2.16 +"----------- progr.vers.2: check erls for multiply_ansatz";
2.17 +"----------- progr.vers.2: check erls for multiply_ansatz";
2.18 +"----------- progr.vers.2: check erls for multiply_ansatz";
2.19 +(*test for outcommented 3 lines in script: is norm_Rational strong enough?*)
2.20 +val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))";
2.21 +val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t;
2.22 +term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
2.23 +
2.24 +val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*)
2.25 +term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
2.26 + "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
2.27 +
2.28 +val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
2.29 +if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then ()
2.30 +else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
2.31 +
2.32 +(*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
2.33 +val xxx = append_rls "multiply_ansatz_erls" norm_Rational
2.34 + [Calc ("HOL.eq",eval_equal "#equal_")];
2.35 +
2.36 +val multiply_ansatz = prep_rls(
2.37 + Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
2.38 + erls = xxx,
2.39 + srls = Erls, calc = [],
2.40 + rules =
2.41 + [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
2.42 + ],
2.43 + scr = EmptyScr}:rls);
2.44 +
2.45 +rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*)
2.46 +rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?: GOON*)
2.47 +
2.48 +"----------- progr.vers.2: improve program --------------";
2.49 +"----------- progr.vers.2: improve program --------------";
2.50 +"----------- progr.vers.2: improve program --------------";
2.51 +(*WN120318 stopped due to much effort with the test above*)
2.52 + "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
2.53 + " (let f_f = Take f_f; " ^
2.54 + " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
2.55 + " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
2.56 + " (numer::real) = get_numerator f_f; " ^(*numer: 24*)
2.57 + " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)
2.58 + " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)
2.59 + " (L_L::bool list) = (SubProblem (PolyEq', " ^
2.60 + " [abcFormula, degree_2, polynomial, univariate, equation], " ^
2.61 + " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)
2.62 + " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)
2.63 + " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *)
2.64 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
2.65 + " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
2.66 +(*this has been tested below by rewrite_set_
2.67 + " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**)
2.68 + " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**)
2.69 + " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
2.70 +NEXT try to outcomment the very next line..*)
2.71 + " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
2.72 + " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
2.73 + " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*)
2.74 + " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: -1 / 4*)
2.75 + " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
2.76 + " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
2.77 + " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
2.78 + " (sol_a::bool list) = " ^
2.79 + " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
2.80 + " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
2.81 + " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
2.82 + " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
2.83 + " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
2.84 + " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
2.85 + " (sol_b::bool list) = " ^
2.86 + " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
2.87 + " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
2.88 + " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
2.89 + " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
2.90 + " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)
2.91 + " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
2.92 + " in pbz)"
2.93 +
3.1 --- a/test/Tools/isac/Test_Some.thy Tue Mar 06 14:25:08 2012 +0100
3.2 +++ b/test/Tools/isac/Test_Some.thy Thu Mar 08 14:33:34 2012 +0100
3.3 @@ -1,50 +1,31 @@
3.4
3.5 theory Test_Some imports Isac begin
3.6
3.7 -use"../../../test/Tools/isac/Knowledge/biegelinie.sml"
3.8 +use"../../../test/Tools/isac/Knowledge/partial_fractions.sml"
3.9
3.10 ML {*
3.11 -val thy = @{theory "Biegelinie"};
3.12 *}
3.13 ML {*
3.14 -val ctxt = thy2ctxt' "Biegelinie";
3.15 *}
3.16 ML {*
3.17 -"----------- Bsp 7.27 me -----------------------------------------";
3.18 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
3.19 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
3.20 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
3.21 - "FunktionsVariable x"];
3.22 -val (dI',pI',mI') =
3.23 - ("Biegelinie",["MomentBestimmte","Biegelinien"],
3.24 - ["IntegrierenUndKonstanteBestimmen"]);
3.25 -val p = e_pos'; val c = [];
3.26 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.27 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.28 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.29 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.30 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.31 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.32 -
3.33 -val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
3.34 -(*if itms2str_ ctxt pits = ... all 5 model-items*)
3.35 -val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
3.36 -if itms2str_ ctxt mits = "[]" then ()
3.37 -else error "biegelinie.sml: Bsp 7.27 #2";
3.38 -
3.39 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.40 -case nxt of (_,Add_Given "FunktionsVariable x") => ()
3.41 - | _ => error "biegelinie.sml: Bsp 7.27 #4a";
3.42 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.43 +*}
3.44 +ML {*
3.45 *}
3.46 ML {*
3.47 -val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
3.48 *}
3.49 ML {*
3.50 -(*if itms2str_ ctxt mits = ... all 6 guard-items*)
3.51 -case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
3.52 - | _ => error "biegelinie.sml: Bsp 7.27 #4b";
3.53 -(*=========================^^^ correct until here ^^^===========================*)
3.54 +*}
3.55 +ML {* (*==================*)
3.56 +*}
3.57 +ML {*
3.58 +*}
3.59 +ML {*
3.60 +*}
3.61 +ML {*
3.62 +*}
3.63 +ML {*
3.64 +*}
3.65 +ML {* (*==================*)
3.66 *}
3.67 ML {*
3.68 *}
3.69 @@ -53,87 +34,12 @@
3.70 ML {*
3.71 *}
3.72 ML {*
3.73 -*}
3.74 -ML {*
3.75 -*}
3.76 -ML {*
3.77 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.78 -*}
3.79 -ML {*
3.80 -nxt
3.81 -*}
3.82 -ML {*
3.83 -print_depth 999;
3.84 -val ("Empty_Tac", xxx) = nxt; (*<<<-----------------------------------------------*)
3.85 -print_depth 999;
3.86 -*}
3.87 -ML {*
3.88 -*}
3.89 -ML {* (*==================*)
3.90 -"----------- Bsp 7.27 autoCalculate ------------------------------";
3.91 - states:=[];
3.92 - CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
3.93 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
3.94 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
3.95 - "FunktionsVariable x"],
3.96 - ("Biegelinie",
3.97 - ["MomentBestimmte","Biegelinien"],
3.98 - ["IntegrierenUndKonstanteBestimmen"]))];
3.99 - moveActiveRoot 1;
3.100 - autoCalculate 1 CompleteCalcHead;
3.101 -
3.102 - fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
3.103 -(*
3.104 -> val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
3.105 -> is = e_scrstate;
3.106 -val it = true : bool
3.107 -*)
3.108 - autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
3.109 - val ((pt,_),_) = get_calc 1;
3.110 - case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
3.111 - | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
3.112 -
3.113 - autoCalculate 1 CompleteCalc;
3.114 -val ((pt,p),_) = get_calc 1;
3.115 -(*=== inhibit exn 110722=============================================================
3.116 -if p = ([], Res) andalso length (children pt) = 23 andalso
3.117 -term2str (get_obj g_res pt (fst p)) =
3.118 -"y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
3.119 -then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
3.120 -=== inhibit exn 110722=============================================================*)
3.121 -
3.122 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
3.123 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
3.124 - show_pt pt;
3.125 -
3.126 -(*check all formulae for getTactic*)
3.127 - getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
3.128 - getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
3.129 - getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
3.130 - getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
3.131 - getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
3.132 - getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
3.133 -*}
3.134 -ML {*
3.135 -*}
3.136 -ML {*
3.137 -
3.138 -*}
3.139 -ML {*
3.140 -*}
3.141 -ML {* (*==================*)
3.142 -*}
3.143 -ML {*
3.144 -*}
3.145 -ML {*
3.146 "~~~~~ fun , args:"; val () = ();
3.147 *}
3.148 end
3.149
3.150 -
3.151 -(*============ inhibit exn WN120305 ==============================================
3.152 -============ inhibit exn WN120305 ==============================================*)
3.153 -
3.154 +(*============ inhibit exn WN120306 ==============================================
3.155 +============ inhibit exn WN120306 ==============================================*)
3.156
3.157 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
3.158 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)