1.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml	Mon Dec 19 14:41:41 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Thu Jan 05 17:43:48 2012 +0100
     1.3 @@ -6,10 +6,11 @@
     1.4  "--------------------------------------------------------";
     1.5  "table of contents --------------------------------------";
     1.6  "--------------------------------------------------------";
     1.7 -"----------- Test of function factors_from_solution ---------";
     1.8 -"--------------------------------------------------------";
     1.9  "----------- why helpless here ? ------------------------";
    1.10  "----------- why not nxt = Model_Problem here ? ---------";
    1.11 +"----------- fun factors_from_solution ------------------";
    1.12 +"----------- Logic.unvarify_global ----------------------";
    1.13 +"----------- eval_drop_questionmarks --------------------";
    1.14  "--------------------------------------------------------";
    1.15  "--------------------------------------------------------";
    1.16  "--------------------------------------------------------";
    1.17 @@ -66,14 +67,46 @@
    1.18  See TODO.txt
    1.19  *)
    1.20  
    1.21 -"----------- Test of function factors_from_solution ---------";
    1.22 -"----------- Test of function factors_from_solution ---------";
    1.23 -"----------- Test of function factors_from_solution ---------";
    1.24 -
    1.25 +"----------- fun factors_from_solution ------------------";
    1.26 +"----------- fun factors_from_solution ------------------";
    1.27 +"----------- fun factors_from_solution ------------------";
    1.28 +val ctxt = ProofContext.init_global @{theory Isac};
    1.29  val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
    1.30  val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
    1.31  if term2str t' =
    1.32   "factors_from_solution [z = 1 / 2, z = -1 / 4] =\n(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
    1.33  then () else error "factors_from_solution broken";
    1.34  
    1.35 +"----------- Logic.unvarify_global ----------------------";
    1.36 +"----------- Logic.unvarify_global ----------------------";
    1.37 +"----------- Logic.unvarify_global ----------------------";
    1.38 +val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global
    1.39 +val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global
    1.40  
    1.41 +val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the;
    1.42 +val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
    1.43 +
    1.44 +val test = HOLogic.mk_binop "Groups.plus_class.plus"
    1.45 +  (HOLogic.mk_binop "Rings.inverse_class.divide" (A_var, denom1),
    1.46 +   HOLogic.mk_binop "Rings.inverse_class.divide" (B_var, denom2));
    1.47 +
    1.48 +if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
    1.49 +  else error "HOLogic.mk_binop broken ?";
    1.50 +
    1.51 +(* Logic.unvarify_global test
    1.52 +---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"
    1.53 +thus we need another fun var2free in termC.sml*)
    1.54 +
    1.55 +"----------- eval_drop_questionmarks --------------------";
    1.56 +"----------- eval_drop_questionmarks --------------------";
    1.57 +"----------- eval_drop_questionmarks --------------------";
    1.58 +if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))"
    1.59 +then () else error "test setup (ctxt!) probably changed";
    1.60 +
    1.61 +val t = Const ("Partial_Fractions.drop_questionmarks", HOLogic.realT --> HOLogic.realT) $ test;
    1.62 +
    1.63 +val SOME (_, t') = eval_drop_questionmarks "drop_questionmarks" 0 t @{theory Isac};
    1.64 +if term2str t' = "drop_questionmarks (?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))) =" ^
    1.65 +  "\nA / (z + -1 * (1 / 2)) + B / (z + -1 * (-1 / 4))"
    1.66 +then () else error "eval_drop_questionmarks broken";
    1.67 +