1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Dec 19 14:41:41 2011 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Jan 05 17:43:48 2012 +0100
1.3 @@ -23,7 +23,8 @@
1.4
1.5 consts
1.6
1.7 - factors_from_solution :: "bool list => real"
1.8 + factors_from_solution :: "bool list => real"
1.9 + drop_questionmarks :: "'a => 'a"
1.10
1.11 subsection {*get the denominator out of a fraction*}
1.12 text {*this functions have been stored in Rationals.thy and can be put into rule sets*}
1.13 @@ -81,7 +82,7 @@
1.14 *}
1.15
1.16 ML {*
1.17 -(*("factors_from_solution", ("Equation.factors_from_solution", eval_factors_from_solution ""))*)
1.18 +(*("factors_from_solution", ("Partial_Fractions.factors_from_solution", eval_factors_from_solution ""))*)
1.19 fun eval_factors_from_solution (thmid:string) _
1.20 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
1.21 ((let val prod = factors_from_solution sol
1.22 @@ -93,9 +94,33 @@
1.23 | eval_factors_from_solution _ _ _ _ = NONE;
1.24 *}
1.25
1.26 +ML {*
1.27 +(*("drop_questionmarks", ("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks ""))*)
1.28 +fun eval_drop_questionmarks (thmid:string) _
1.29 + (t as Const ("Partial_Fractions.drop_questionmarks", _) $ tm) thy =
1.30 + if contains_Var tm
1.31 + then
1.32 + let
1.33 + val tm' = var2free tm
1.34 + in SOME (mk_thmid thmid ""
1.35 + (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) tm') "",
1.36 + Trueprop $ (mk_equality (t, tm')))
1.37 + end
1.38 + else NONE
1.39 + | eval_drop_questionmarks _ _ _ _ = NONE;
1.40 +
1.41 +calclist':= overwritel (!calclist',
1.42 + [("drop_questionmarks", ("Partial_Fractions.drop'_questionmarks", eval_drop_questionmarks ""))
1.43 + ]);
1.44 +*}
1.45 +
1.46 +
1.47 +
1.48 +text {* this definition's scope is all Isac; so no equation etc with "A" would be possible:
1.49 consts
1.50 A :: "real"
1.51 B :: "real"
1.52 +*}
1.53
1.54 axiomatization where
1.55 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
2.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Mon Dec 19 14:41:41 2011 +0100
2.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Thu Jan 05 17:43:48 2012 +0100
2.3 @@ -302,7 +302,20 @@
2.4 in if t'' = e_term
2.5 then NONE else SOME (t'', asm'')
2.6 end;
2.7 -
2.8 +fun rewrite_terms_ thy ord erls equs t =
2.9 + let
2.10 + fun rew_ (t', asm') [] _ = (t', asm')
2.11 + | rew_ (t', asm') (rules as r::rs) t =
2.12 + let
2.13 + val (t'', asm'', lrd, rew) = rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t
2.14 + in
2.15 + if rew
2.16 + then rew_ (t'', asm' @ asm'') rules t''
2.17 + else rew_ (t', asm') rs t'
2.18 + end
2.19 + val (t'', asm'') = rew_ (e_term, []) equs t
2.20 + in if t'' = e_term then NONE else SOME (t'', asm'')
2.21 + end;
2.22
2.23 (*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
2.24 fun calculate_ thy isa_fn ct =
3.1 --- a/src/Tools/isac/ProgLang/termC.sml Mon Dec 19 14:41:41 2011 +0100
3.2 +++ b/src/Tools/isac/ProgLang/termC.sml Thu Jan 05 17:43:48 2012 +0100
3.3 @@ -233,7 +233,7 @@
3.4 handle _ => error ("free2int: "^term_detail2str t))
3.5 | free2int t = error ("free2int: "^term_detail2str t);
3.6
3.7 -(*27.8.01: unused*)
3.8 +(*compare Logic.unvarify_global: rejects Free*)
3.9 fun var2free (t as Const(s,T)) = t
3.10 | var2free (t as Free(s,T)) = t
3.11 | var2free (Var((s,i),T)) = Free(s,T)
4.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Dec 19 14:41:41 2011 +0100
4.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Jan 05 17:43:48 2012 +0100
4.3 @@ -489,6 +489,13 @@
4.4 ML {*Context.theory_name thy = "Isac"(*==================================================*)*}
4.5
4.6 subsubsection {*Build a rule-set for ansatz*}
4.7 +text {* the "ansatz" rules violate the principle that each variable on
4.8 + the right-hand-side must also occur on the left-hand-side of the rule:
4.9 + A, B, etc don't.
4.10 + Thus the rewriter marks these variables with question marks: ?A, ?B, etc.
4.11 + These question marks are dropped by a function, which can be included
4.12 + into a ruleset by Calc.
4.13 + *}
4.14 ML {*
4.15 val ansatz_rls = prep_rls(
4.16 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
4.17 @@ -500,8 +507,12 @@
4.18 scr = EmptyScr});
4.19 *}
4.20 ML {*
4.21 +trace_rewrite := true;
4.22 val SOME (ttttt,_) = rewrite_set_ @{theory Isac} false ansatz_rls expr';
4.23 -term2str ttttt;
4.24 +*}
4.25 +ML {*
4.26 +term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
4.27 +term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
4.28 *}
4.29
4.30
4.31 @@ -602,6 +613,8 @@
4.32
4.33 subsubsection {*substitute expression with solutions*}
4.34 ML {*
4.35 +f2str fa;
4.36 +f2str fb
4.37 *}
4.38 ML {*thy*}
4.39
4.40 @@ -766,12 +779,11 @@
4.41 Calc("Tools.lhs", eval_lhs"eval_lhs_"), (*<=== ONLY USED*)
4.42 Calc("Tools.rhs", eval_rhs"eval_rhs_"), (*<=== ONLY USED*)
4.43 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
4.44 - Calc("Rational.get_denominator",
4.45 - eval_get_denominator "Rational.get_denominator"),
4.46 - Calc("Rational.get_numerator",
4.47 - eval_get_numerator "Rational.get_numerator"),
4.48 + Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
4.49 + Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
4.50 Calc("Partial_Fractions.factors_from_solution",
4.51 - eval_factors_from_solution "Partial_Fractions.factors_from_solution")
4.52 + eval_factors_from_solution "#factors_from_solution"),
4.53 + Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")
4.54 ],
4.55 scr = EmptyScr};
4.56 *}
4.57 @@ -789,47 +801,49 @@
4.58 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls,
4.59 prls = e_rls,
4.60 crls = e_rls, nrls = e_rls},
4.61 -"Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
4.62 -" (let X = Take X_eq;" ^
4.63 -" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
4.64 -" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
4.65 -" (X'_z::real) = lhs X';" ^ (**)
4.66 -" (zzz::real) = argument_in X'_z;" ^ (**)
4.67 -" (funterm::real) = rhs X';" ^ (*drop X' z = for equation solving*)
4.68 -" (denom::real) = get_denominator funterm;" ^ (*get_denominator*)
4.69 -" (num::real) = get_numerator funterm; " ^ (*get_numerator*)
4.70 -" (equ::bool) = (denom = (0::real));" ^
4.71 -
4.72 -" (L_L::bool list) = (SubProblem (PolyEq'," ^
4.73 -" [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^
4.74 -" [BOOL equ, REAL zzz]); " ^
4.75 -
4.76 -
4.77 -" (facs::real) = factors_from_solution L_L;" ^
4.78 -
4.79 -" (eql::real) = Take (num / facs);" ^
4.80 -" (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql;"^
4.81 -
4.82 -" (eq::bool) = Take (eql = eqr);"^ (*Maybe possible to use HOLogic.mk_eq ??*)
4.83 -" eq = (Try (Rewrite_Set equival_trans False)) eq;"^
4.84 -
4.85 -" (z1::real) = (rhs (NTH 1 L_L));"^ (*prepare equliation for a - eq_a therfor subsitude z with solution 1 - z1*)
4.86 -" (eq_a::bool) = (Substitute [zzz=z1]) eq;"^
4.87 -" eq_a = (Rewrite_Set norm_Rational False) eq_a;"^
4.88 -
4.89 -" (aaa::real) = argument_in (rhs eq_a);"^
4.90 -
4.91 -" x = Take aaa;"^
4.92 -
4.93 -
4.94 -"(* (A::bool list) = (SubProblem (PolyEq'," ^
4.95 -" [univariate,equation],[no_met])" ^
4.96 -" [BOOL eq_a, REAL aaa]);*)"^
4.97 -
4.98 -" (x::real) = 3"^(*only here that the last step of the ptree is visible in tracing output*)
4.99 -
4.100 -" in X)"
4.101 - ));
4.102 + "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
4.103 + " (let X = Take X_eq;" ^
4.104 +(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
4.105 + " X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
4.106 +(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
4.107 + " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
4.108 +(*([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
4.109 + " (X'_z::real) = lhs X';" ^ (**)
4.110 + " (zzz::real) = argument_in X'_z;" ^ (**)
4.111 + " (funterm::real) = rhs X';" ^ (*drop X' z = for equation solving*)
4.112 + " (denom::real) = get_denominator funterm;" ^ (*get_denominator*)
4.113 + " (num::real) = get_numerator funterm; " ^ (*get_numerator*)
4.114 + " (equ::bool) = (denom = (0::real));" ^
4.115 + " (L_L::bool list) = (SubProblem (PolyEq'," ^
4.116 + " [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^
4.117 + " [BOOL equ, REAL zzz]); " ^
4.118 +(*([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)*)
4.119 +(*([3], Res), [z = 1 / 2, z = -1 / 4]*)
4.120 + " (facs::real) = factors_from_solution L_L;" ^
4.121 + " (eql::real) = Take (num / facs);" ^
4.122 +(*([4], Frm), 24 / ((z + -1 * (1 / 2)) * (z + -1 * (-1 / 4)))*)
4.123 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql;"^
4.124 +(*([4], Res), ?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))*)
4.125 + " (eq::bool) = Take (eql = eqr);"^ (*Maybe possible to use HOLogic.mk_eq ??*)
4.126 +(*([5], Frm), 24 / ((z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))) = ?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))*)
4.127 + " eq = (Try (Rewrite_Set equival_trans False)) eq;"^
4.128 +(*([5], Res), 24 = ?A * (z + -1 * (-1 / 4)) + ?B * (z + -1 * (1 / 2))*)
4.129 + " eq = drop_questionmarks eq;"^
4.130 +(*GOON: trace_script shows "(24 = A * (z + -1 * (-1 / 4)) + B * (z + -1 * (1 / 2))"
4.131 +without "?" BUT THEN WRONG "*** upd_env_opt: (NONE,24 = ?A * ..."*)
4.132 + " (z1::real) = (rhs (NTH 1 L_L));"^ (*prepare equliation for a - eq_a therfor subsitude z with solution 1 - z1*)
4.133 + " (eq_a::bool) = (Substitute [zzz=z1]) eq;"^
4.134 +(*([6], Res), 24 = ?A * (1 / 2 + -1 * (-1 / 4)) + ?B * (1 / 2 + -1 * (1 / 2))*)
4.135 + " eq_a = (Rewrite_Set norm_Rational False) eq_a;"^
4.136 +(*([7], Res), 24 = ?A * 3 / 4*)
4.137 + " (aaa::real) = argument_in (rhs eq_a);"^
4.138 + " x = Take aaa;"^
4.139 + "(* (A::bool list) = (SubProblem (PolyEq'," ^
4.140 + " [univariate,equation],[no_met])" ^
4.141 + " [BOOL eq_a, REAL A]);*)"^ (*GOON: probably doesn't work ?*)
4.142 + " (x::real) = 3"^(*only here that the last step of the ptree is visible in tracing output*)
4.143 + " in X)"
4.144 + ));
4.145 *}
4.146
4.147
4.148 @@ -862,8 +876,7 @@
4.149 val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
4.150 ["SignalProcessing","Z_Transform","inverse"]);
4.151 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
4.152 -*}
4.153 -ML {*
4.154 +(*([], Frm), Problem (Isac, [inverse, Z_Transform, SignalProcessing])*)
4.155 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
4.156 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
4.157 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
4.158 @@ -871,8 +884,11 @@
4.159 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
4.160 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
4.161 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))"; (*TODO naming!*)
4.162 +(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
4.163 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
4.164 +(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
4.165 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = SubProblem";
4.166 +(*([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
4.167 *}
4.168 text {* Instead of nxt = Subproblem above we had Empty_Tac; the search for the reason
4.169 considered the following points:
4.170 @@ -898,6 +914,7 @@
4.171
4.172 ML {*
4.173 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Model_Problem";
4.174 +(*([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)*)
4.175 *}
4.176 text {* Instead of nxt = Model_Problem above we had Empty_Tac; the search for the reason
4.177 considered the following points:difference in the arguments
4.178 @@ -911,6 +928,7 @@
4.179 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Find solutions z_i";
4.180 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Specify_Theory Isac";
4.181 *}
4.182 +
4.183 text {* We had "nxt = Empty_Tac instead Specify_Theory;
4.184 the search for the reason considered the following points:
4.185 # was there an error message ? NO --ok
4.186 @@ -939,66 +957,46 @@
4.187 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";
4.188 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";
4.189 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplify";
4.190 -show_pt pt;
4.191 +(*([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0)*)
4.192 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.193 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.194 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.195 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.196 +(*([3,4], Res), [z = 1 / 2, z = -1 / 4])*)
4.197 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.198 +(*([3], Res), [z = 1 / 2, z = -1 / 4]*)
4.199 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.200 +(*([4], Frm), 24 / ((z + -1 * (1 / 2)) * (z + -1 * (-1 / 4)))*)
4.201 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.202 +(*([4], Res), ?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))*)
4.203 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.204 +(*([5], Frm), 24 / ((z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))) = ?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))*)
4.205 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.206 +(*([5], Res), 24 = ?A * (z + -1 * (-1 / 4)) + ?B * (z + -1 * (1 / 2))*)
4.207 +*}
4.208 +ML {* (*GOON: trace_script shows "(24 = A * (z + -1 * (-1 / 4)) + B * (z + -1 * (1 / 2))"
4.209 +without "?" BUT THEN WRONG "*** upd_env_opt: (NONE,24 = ?A * ..."*)
4.210 +trace_script := true;
4.211 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.212 +(*([6], Res), 24 = ?A * (1 / 2 + -1 * (-1 / 4)) + ?B * (1 / 2 + -1 * (1 / 2))*)
4.213 *}
4.214 ML {*
4.215 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.216 -*}
4.217 -ML {*
4.218 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.219 -*}
4.220 -ML {*
4.221 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.222 -*}
4.223 -ML {*
4.224 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.225 -*}
4.226 -ML {*
4.227 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.228 +(*([7], Res), 24 = ?A * 3 / 4*)
4.229 show_pt pt;
4.230 *}
4.231
4.232 ML {*
4.233 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.234 -show_pt pt;
4.235 -*}
4.236 -
4.237 -ML {*
4.238 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.239 -show_pt pt;
4.240 -*}
4.241 -
4.242 -ML {*
4.243 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.244 -show_pt pt;
4.245 -*}
4.246 -
4.247 -ML {*
4.248 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.249 -show_pt pt;
4.250 -*}
4.251 -
4.252 -ML {*
4.253 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.254 -show_pt pt;
4.255 -*}
4.256 -
4.257 -ML {*
4.258 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.259 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.260 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.261 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.262 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.263 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.264 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.265 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.266 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.267 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.268 -*}
4.269 -
4.270 -ML {*
4.271 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.272 -show_pt pt;
4.273 *}
4.274
4.275 section {*Write Tests for Crucial Details*}
5.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Mon Dec 19 14:41:41 2011 +0100
5.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Jan 05 17:43:48 2012 +0100
5.3 @@ -6,10 +6,11 @@
5.4 "--------------------------------------------------------";
5.5 "table of contents --------------------------------------";
5.6 "--------------------------------------------------------";
5.7 -"----------- Test of function factors_from_solution ---------";
5.8 -"--------------------------------------------------------";
5.9 "----------- why helpless here ? ------------------------";
5.10 "----------- why not nxt = Model_Problem here ? ---------";
5.11 +"----------- fun factors_from_solution ------------------";
5.12 +"----------- Logic.unvarify_global ----------------------";
5.13 +"----------- eval_drop_questionmarks --------------------";
5.14 "--------------------------------------------------------";
5.15 "--------------------------------------------------------";
5.16 "--------------------------------------------------------";
5.17 @@ -66,14 +67,46 @@
5.18 See TODO.txt
5.19 *)
5.20
5.21 -"----------- Test of function factors_from_solution ---------";
5.22 -"----------- Test of function factors_from_solution ---------";
5.23 -"----------- Test of function factors_from_solution ---------";
5.24 -
5.25 +"----------- fun factors_from_solution ------------------";
5.26 +"----------- fun factors_from_solution ------------------";
5.27 +"----------- fun factors_from_solution ------------------";
5.28 +val ctxt = ProofContext.init_global @{theory Isac};
5.29 val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
5.30 val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
5.31 if term2str t' =
5.32 "factors_from_solution [z = 1 / 2, z = -1 / 4] =\n(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
5.33 then () else error "factors_from_solution broken";
5.34
5.35 +"----------- Logic.unvarify_global ----------------------";
5.36 +"----------- Logic.unvarify_global ----------------------";
5.37 +"----------- Logic.unvarify_global ----------------------";
5.38 +val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global
5.39 +val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global
5.40
5.41 +val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the;
5.42 +val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
5.43 +
5.44 +val test = HOLogic.mk_binop "Groups.plus_class.plus"
5.45 + (HOLogic.mk_binop "Rings.inverse_class.divide" (A_var, denom1),
5.46 + HOLogic.mk_binop "Rings.inverse_class.divide" (B_var, denom2));
5.47 +
5.48 +if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
5.49 + else error "HOLogic.mk_binop broken ?";
5.50 +
5.51 +(* Logic.unvarify_global test
5.52 +---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"
5.53 +thus we need another fun var2free in termC.sml*)
5.54 +
5.55 +"----------- eval_drop_questionmarks --------------------";
5.56 +"----------- eval_drop_questionmarks --------------------";
5.57 +"----------- eval_drop_questionmarks --------------------";
5.58 +if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))"
5.59 +then () else error "test setup (ctxt!) probably changed";
5.60 +
5.61 +val t = Const ("Partial_Fractions.drop_questionmarks", HOLogic.realT --> HOLogic.realT) $ test;
5.62 +
5.63 +val SOME (_, t') = eval_drop_questionmarks "drop_questionmarks" 0 t @{theory Isac};
5.64 +if term2str t' = "drop_questionmarks (?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))) =" ^
5.65 + "\nA / (z + -1 * (1 / 2)) + B / (z + -1 * (-1 / 4))"
5.66 +then () else error "eval_drop_questionmarks broken";
5.67 +
6.1 --- a/test/Tools/isac/Test_Some.thy Mon Dec 19 14:41:41 2011 +0100
6.2 +++ b/test/Tools/isac/Test_Some.thy Thu Jan 05 17:43:48 2012 +0100
6.3 @@ -1,10 +1,11 @@
6.4
6.5 theory Test_Some imports Isac begin
6.6
6.7 -use"../../../test/Tools/isac/Knowledge/integrate.sml"
6.8 +use"../../../test/Tools/isac/Knowledge/partial_fractions.sml"
6.9
6.10 ML {* (*==================*)
6.11 -
6.12 +*}
6.13 +ML {*
6.14 *}
6.15 ML {* (*==================*)
6.16 *}