1.1 --- a/test/Tools/isac/Interpret/calchead.sml	Tue Sep 20 18:09:46 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/calchead.sml	Thu Sep 22 14:24:34 2011 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4  "--------- regression test fun is_copy_named ------------";
     1.5  "--------- regr.test fun cpy_nam ------------------------";
     1.6  "--------- check specify phase --------------------------";
     1.7 +"--------- check: fmz matches pbt -----------------------";
     1.8  "--------------------------------------------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11 @@ -724,3 +725,51 @@
    1.12  "----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
    1.13  if nxt = ("Add_Given", Add_Given "integrateBy x") then ()
    1.14  else error "clchead.sml: check specify phase step 2";
    1.15 +
    1.16 +"--------- check: fmz matches pbt -----------------------";
    1.17 +"--------- check: fmz matches pbt -----------------------";
    1.18 +"--------- check: fmz matches pbt -----------------------";
    1.19 +"101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";
    1.20 +"the following fmz caused the above error";
    1.21 +val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
    1.22 +val pI = ["plus_minus","polynom","vereinfachen"];
    1.23 +
    1.24 +"----- this fmz is transformed to this internal format (TERM --> Pure.term):";
    1.25 +val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \<Rightarrow> prop"*)) $ _]),
    1.26 +      (*#############################^^^^^^^^^ defined by Isabelle*)
    1.27 +      (2, [1], "#Find", Const ("Simplify.normalform", _ (*"RealDef.real \<Rightarrow> Tools.una"*)),
    1.28 +                            [Free ("N", _ (*"RealDef.real"*))])],
    1.29 +     _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
    1.30 +"#undef means: the element with description TERM in fmz did not match ";
    1.31 +"with any element of pbl (fetched by pI), because there we have Simplify.Term";
    1.32 +"defined in Simplify.thy";
    1.33 +
    1.34 +"So we try out how to create Simplify.Term:";
    1.35 +"----- trial 1";
    1.36 +val Const ("Pure.term", _) $ Free ("ttt", _) = str2term "TERM ttt";
    1.37 +"           ^^^^^^^^^ see above";
    1.38 +atomwy t;
    1.39 +
    1.40 +"----- trial 2";
    1.41 +val Free ("term", _) $ Free ("ttt", _) = str2term "term ttt";
    1.42 +"   ^^^^^^^^^^^ means, that no appropriate Const has be found (descriptions are all Const !)";
    1.43 +atomwy t;
    1.44 +
    1.45 +"----- trial 3";
    1.46 +val Const ("Simplify.Term", _) $ Free ("ttt", _) = str2term "Term ttt";
    1.47 +"           ^^^^^^^^^^^^^^ this is what in Simplify.thy has been defined ";
    1.48 +"                          and unsed in pbl [plus_minus,polynom,vereinfachen]";
    1.49 +atomwy t;
    1.50 +
    1.51 +"----- so this is the correct fmz:";
    1.52 +val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
    1.53 +val ([(1, [1], "#Given", Const ("Simplify.Term", _), [Const ("Groups.plus_class.plus", _) $ _ $ _]),
    1.54 +      (*########################^^^^^^^^^ defined in Simplify.thy*)
    1.55 +      (2, [1], "#Find", Const ("Simplify.normalform", _ ),
    1.56 +                            [Free ("N", _ )])],
    1.57 +     _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
    1.58 +
    1.59 +"----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";
    1.60 +val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
    1.61 +     ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;
    1.62 +