wneuper/isa: test/Tools/isac/xmlsrc/thy-hierarchy.sml@73dc85c025ab

     1 (* Title: tests for sml/xmlsrc/thy-hierarchy.sml

     2    Authors: Walther Neuper 060113

     3    (c) due to copyright terms

     5 CAUTION with testing *2file functions -- they are actually writing to ~/tmp

     6 *)

     8 val thy = @{theory "Isac"};

    10 "-----------------------------------------------------------------";

    11 "table of contents -----------------------------------------------";

    12 "-----------------------------------------------------------------";

    13 "----------- assoc_rls -------------------------------------------";

    14 "----------- thm_hier --------------------------------------------";

    15 "----------- fun thydata2xml -------------------------------------";

    16 "----------- write xml to tmp ------------------------------------";

    17 "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";

    18 "----------- ### thes2file ... Exception- Match raised -----------";

    19 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";

    20 "----------- fun store_thm ---------------------------------------";

    21 "----------- fun insert_fillpats ---------------------------------";

    22 "----------- fun insert_errpatIDs --------------------------------";

    23 "-----------------------------------------------------------------";

    24 "-----------------------------------------------------------------";

    25 "-----------------------------------------------------------------";

    28 "----------- assoc_rls -------------------------------------------";

    29 "----------- assoc_rls -------------------------------------------";

    30 "----------- assoc_rls -------------------------------------------";

    31 val al = [(1,11),(2,22),(3,33)];

    32 overwrite (al, (2,2222));

    33 (*val it = [(1, 11), (2, 2222), (3, 33)] : (int * int) list*)

    35 val al = [("e_rls",("Atools",e_rls)),("e_rrls",("Atools",e_rrls))];

    36 val bl = [("e_rls",e_rls),("e_rrls",e_rrls)];

    37 val b = ("e_rls",("Atools",e_rrls));

    38 overwrite (al, b);

    39 overwritelthy thy (al, bl);

    41 case assoc' ((Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of

    42   SOME ("Tools", Rls _) => ()

    43 | _ => error "e_rls not in Theory_Data"

    45 assoc_rls "e_rls";

    48 "----------- thm_hier --------------------------------------------";

    49 "----------- thm_hier --------------------------------------------";

    50 "----------- thm_hier --------------------------------------------";

    51 (curry op:: "xxx") ["yyy","yyy","yyy"];

    52 map (curry op:: "xxx") [["yyy1"],["yyy2"],["yyy3"]];

    54 val thy' = "Integrate";

    55 val thy = assoc_thy (thyID2theory' thy');

    57 "WN120406.GOON --- restarted with 'isolate response' below, because it was very slow ?!?" ^

    58 "slow probably only because of print_depth 999 and large output";

    60 val thm = prop_of @{thm integral_var};

    62 (*-.-.-.-.-.-WN120406 isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

    64 "collect_thms thy'------------------------------------------------";

    65 (apfst single) ("Integrate.integral_var", thm);

    66 (strip_thy o #1) ("Integrate.integral_var", thm);

    68 (*cannot get this as arg from arg        ^^^^^^^^^^^^^^^^*)

    69     ("Integrate.integral_var", @{thm integral_var});

    70 (*thus new fun....*)

    72 makeHthm ("IsacKnowledge", thy') ("Integrate.integral_var", thm);

    73 (makeHthm ("IsacKnowledge", thy')) ("Integrate.integral_var", thm);

    74 map (makeHthm ("IsacKnowledge", thy')) (Theory.axioms_of thy);

    75 collect_thms' ("IsacKnowledge", thy');

    77 "collect_rlss thy'------------------------------------------------";

    78 makeHrls "IsacKnowledge" ("integration_rules", (thy', integration_rules));

    80 val thy' = "Test";

    81 val rlss = filter ((curry op= thy') o

    82 			   ((#1 o #2):(rls' * (theory' * rls)) -> theory'))

    83 			  (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));

    84 collect_rlss ("IsacKnowledge",thy');

    86 "collect_thy thy-------------------------------------------------";

    87 val thy' = "ListC";

    88 val thy = assoc_thy (thyID2theory' thy');

    89 ((collect_thms' ("IsacKnowledge",thy')) @

    90  (collect_rlss ("IsacKnowledge",thy')) @

    91  (collect_cals ("IsacKnowledge",thy')) @

    92  (collect_ords ("IsacKnowledge",thy')));

    93 collect_thy "IsacKnowledge" thy';

    95 "collect_thydata -------------------------------------------------";

    96 (*map rearrange_inv (! isab_thm_thy); dropped WN120321*)

    97 val xxx = hd (! isab_thm_thy);

    98 (single) xxx;

    99 (apfst ((curry op:: "Isabelle") o single)) xxx;

   101 map (apfst ( (curry op:: "Isabelle") o single) );

   102 map (apfst ((curry op:: "Isabelle") o single)) (! isab_thm_thy);

   104 "thy_hierarchy ---------------------------------------------------";

   105 val theID = ["IsacScripts", "ListC", "Theorems", "append_Cons"]:theID;

   106 val thydat as (theID, thydata) =

   107     (theID, Hthm {guh = theID2guh theID, mathauthors = [],

   108      coursedesign = [], thm = prop_of @{thm append_Cons}});

   110 val th = [] : thehier;

   111 val theID' = cut_theID th theID;

   112 val th = fill_parents th theID' theID;

   113 (* val th =

   114    [Ptyp ("IsacScripts",

   115             [Html {guh = "thy_ListG-thm-append_Cons", html = "", ...}],

   116             [Ptyp ("ListG", ...)])] : thehier *)

   117 (*show_thes*)(writeln o format_pblIDl o (scan [])) th;

   118 writeln (hierarchy_guh th);

   120 "~~~~~ fun collect_thydata, args:"; val () = ();

   121     val isab_thms = (! isab_thm_thy):  (thmDeriv * term) list

   122 val xxx = hd (! isab_thm_thy);

   123 (collect_isab "Isabelle") xxx;

   124 (map (collect_isab "Isabelle") (! isab_thm_thy));

   125 (* = [(["Isabelle", "HOL", "Theorems", "refl"],

   126            Hthm {guh = "thy_isab_HOL-thm-refl", thm = Const ("HOL.Trueprop...", ...,

   127              mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}),

   128           (["Isabelle", "Fun", "Theorems", ...],

   129            Hthm {guh = "thy_isab_Fun-thm-o_apply", thm = Const (......,

   130              mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}),

   131           (["Isabelle", "ListC", ...], ...), (["Isabelle", ...], ...), ([...], ...), ...]:

   132    (theID * thydata) list*)

   134 (! progthys);

   135 val xxx = hd (map Context.theory_name (! progthys)): theory';

   136 (collect_thy "IsacScripts") xxx;

   137 ((flat o (map (collect_thy "IsacScripts"))) (map Context.theory_name (! progthys)));

   138 (* = [(["IsacScripts", "Script", "Theorems", "arity_type_ID"],

   139            Hthm {guh = "thy_scri_Script-thm-arity_type_ID", thm = Const ("HOL.type_class...,

   140              mathauthors = ["isac-team"], coursedesign = []}),

   141           (["IsacScripts", "Script", "Theorems", ...],

   142                Hthm {guh = "thy_scri_Script-thm-arity_type_arg", thm = Const (...) $ Const (...),

   143                  mathauthors = ["isac-team"], coursedesign = []}),

   144           (["IsacScripts", "Tools", ...], ...), (["IsacScripts", ...], ...), ([...], ...), ...]:

   145    (theID * thydata) list*)

   147 print_depth 5;

   148 ((flat o (map (collect_thy "IsacKnowledge"))) (map Context.theory_name (! knowthys)));

   149 (* = [(["IsacKnowledge", "Inverse_Z_Transform", "Theorems", ...],

   150            Hthm {guh = "thy_isac_Inverse_Z_Transform-thm-rule1", thm =

   151                  Const (...) $ (Const (...) $ Const (... $ Bound 0 $ Const (...))))))),

   152                  mathauthors = ["isac-team"], coursedesign = []}),

   153           (["IsacKnowledge", "Inverse_Z_Transform", ...], ...),

   154           (["IsacKnowledge", ...], ...), ([...], ...), ...]:

   155    (theID * thydata) list*)

   156 "~~~~~ from collect_thydata return val:"; val () = ();

   158 val th = [] : thehier;

   159 val thydats = collect_thydata ();

   160 val th1 = the_hier th thydats (**** insert: not found [".. from fill_parents*);

   161 (*show_thes*)(writeln o format_pblIDl o (scan [])) th1;

   163 writeln (hierarchy_guh th);

   164 (*writeln (hierarchy_guh th);

   165 *)

   166 writeln (hierarchy_guh th1);

   167 (* <NODE>

   168     <ID> Isabelle </ID>

   169     <NO> 1 </NO>

   170     <CONTENTREF> thy_isab_Isabelle-part </CONTENTREF>

   171   </NODE>*)

   173 "thy_hierarchy2file ----------------------------------------------";

   174 show_thes();

   175 (*

   176 val path = "../../tmp/";

   177 thy_hierarchy2file path;

   178 *)

   180 get_the ["IsacKnowledge"];

   181 (*------------------------ WN120320

   182 get_the ["IsacKnowledge", "Test"];

   183 get_the ["IsacKnowledge", "Test", "Theorems"];

   184 get_the ["IsacKnowledge", "Test", "Theorems", "exp_pow"];

   185 get_the ["IsacKnowledge", "Test", "Rulesets"];

   186 WN120320 ----------------------- *)

   188 (* FIXXXXXXXXXME.WN060713 guh -- theID

   189 case get_the ["IsacKnowledge", "Test", "Rulesets", "Test_simplify"] of

   190     Hrls {guh = "thy_Test-rls-Test_simplify",thy_rls = ("Test", _),

   191           mathauthors = _,coursedesign = _} => ()

   192   | _ => error "thy-hierarchy.sml: [IsacKnowledge,Test,Rulesets]";

   193 *)

   194 -.-.-.-.-.-.-WN120406 isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

   197 "----------- fun thydata2xml -------------------------------------";

   198 "----------- fun thydata2xml -------------------------------------";

   199 "----------- fun thydata2xml -------------------------------------";

   200 (*========== inhibit exn AK110725 ================================================

   201 val theID = ["IsacScripts", "ListG", "Theorems", "append_Cons"];

   202 val thmdata = get_the theID;

   203 writeln(thydata2xml (theID, thmdata));

   205 val theID = ["IsacKnowledge", "Poly", "Rulesets", "norm_Poly"];

   206 val rlsdata = get_the theID;

   207 writeln(thydata2xml (theID, rlsdata));

   208 ========== inhibit exn AK110725 ================================================*)

   210 (*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]

   211   see sml/../datatypes.sml !

   212 val (thy', rls') = ("DiffApp", "Tools.rhs");

   213 thy_containing_rls thy' rls';

   214 print_depth 99; map #1 startsearch; print_depth 3;

   215 *)

   217 (*

   218 val path = "../../tmp/";

   219 thes2file path;

   220 *)

   222 "----------- write xml to tmp ------------------------------------";

   223 "----------- write xml to tmp ------------------------------------";

   224 "----------- write xml to tmp ------------------------------------";

   225 (*

   226 val path = "../../tmp/";

   228 pbl_hierarchy2file (path ^ "pbl/");

   229 pbls2file          (path ^ "pbl/");

   231 met_hierarchy2file (path ^ "met/");

   232 mets2file          (path ^ "met/");

   234 thy_hierarchy2file (path ^ "thy/");

   235 thes2file          (path ^ "thy/");

   236 *)

   239 "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";

   240 "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";

   241 "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";

   242 (*

   243 store_isa ["Isabelle"] ["THIS SHOULD not BE OVERWRITTEN below"];

   244 print_depth 99; get_the ["Isabelle"]; print_depth 3;

   245 print_depth 5; thehier;  print_depth 3;

   247 thehier := the_hier (! thehier) (collect_thydata ());

   248 print_depth 99; get_the ["Isabelle"]; print_depth 3;

   249 print_depth 5; thehier;  print_depth 3;

   250 *)

   252 case get_the ["IsacKnowledge", "Biegelinie", "Theorems"] of

   253    Html {mathauthors =

   254 	 ["Walther Neuper 2005 supported by a grant from NMI Austria"],...}=>()

   255  | _ => error "thy-hierarchy.sml: store_isa overwritten";

   257 case get_the ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"] of

   258    Hthm {mathauthors =

   259 	 ["Walther Neuper 2005 supported by a grant from NMI Austria"],...}=>()

   260  | _ => error "thy-hierarchy.sml: store_isa overwritten";

   262 (*

   263 print_depth 7;

   264 get_the ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"];

   265 print_depth 3;

   266 *)

   268 (*WN060728 strange behaviour:

   269 ### fun the_hier reports these not overwritten ?!?...(stored twice ?!?) ...

   271 val it = () : unit

   272 *** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"]

   273 *** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"]

   274 *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_minus1"]

   275 *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_2"]

   276 *** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"]

   277 *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_minus_eq1"]

   278 *** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"]

   279 *** insert: preserved ["Isabelle","RealDef","Theorems","real_minus_divide_eq"]

   280 *** insert: preserved ["IsacScripts","ListG","Theorems","induct"]

   281 *** insert: preserved ["IsacScripts","ListG","Theorems","simps_1"]

   282 *** insert: preserved ["IsacScripts","ListG","Theorems","simps_2"]

   283 val it = () : unit

   285 ### but those store_*d in Biegelinie.ML are NOT reported !?!?!?!?!?!?!

   286 ### however, '*** insert: not found' is NOT reported below, too....

   288 ----------------------------------

   289 *** insert: not found ... IS OK :

   290 comes from fill_parents

   291 ----------------------------------

   293 val it = () : unit

   294 *** insert: not found ["Isabelle","NatDef","Theorems","order_refl"]

   295 *** insert: not found ["Isabelle","NatDef","Theorems","order_refl"]*)

   297 "----------- ### thes2file ... Exception- Match raised -----------";

   298 "----------- ### thes2file ... Exception- Match raised -----------";

   299 "----------- ### thes2file ... Exception- Match raised -----------";

   300 writeln "what to do when you get,e.g. \n\

   301 \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\"]\n\

   302 \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"integration_rules\"]\n\

   303 \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"add_new_c\"]\n\

   304 \Exception- Match raised";

   306 val ptyp = hd (! thehier);

   307 val theID = ["IsacKnowledge","Integrate","Rulesets","add_new_c"];

   308 (*========== inhibit exn AK110725 ================================================

   309 val thydata = get_the theID;

   311 (* creates a file ...

   312 thydata2file "~/tmp/"[] theID thydata (*reports Exception- Match in question*);

   313 *)

   315 thydata2xml (theID, thydata) (*reports Exception- Match in question*);

   317 val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =

   318     (theID, thydata);

   319 rls2xml i thy_rls (*reports Exception- Match in question*);

   320 val (j, (thyID, Seq data)) = (i, thy_rls);

   321 (* evaluate this local fun ...

   322 rls2xm j (thyID, "Seq", data) (*reports Exception- Match in question*);

   323 *)

   324 val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,

   325 			 srls, calc, rules, scr})) =

   326     (j, (thyID, "Seq", data));

   327 rules2xml (j+2*i) thyID rules (*reports Exception- Match in question*);

   328 ============ inhibit exn AK110725 ==============================================*)

   330 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";

   331 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";

   332 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";

   333 val TESTdump = Unsynchronized.ref

   334   ("path": path, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp);

   336 fun TESTthenode (pa:path) ids po wfn (Ptyp (id, [n], ns)) TESTids =

   337     let val po' = lev_on po

   338     in

   339       if (ids@[id]) = TESTids

   340       then

   341         (TESTdump := (pa, ids, po', wfn, (Ptyp (id, [n], ns)));

   342           error "stopped before error, created TESTdump") (* this exn creates right signature*)

   343       else

   344         wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids

   345     end

   346 and TESTthenodes _ _ _ _ [] _ = ()

   347   | TESTthenodes pa ids po wfn (n::ns) TESTids =

   348       (TESTthenode pa ids po wfn n TESTids; TESTthenodes pa ids (lev_on po) wfn ns TESTids);

   350 (* /--- side effects from previous test files ---\*)

   351     val i = indentation;

   352     val j = indentation;

   353 (* \--- side effects from previous test files ---/*)

   354 "~~~~~ fun thes2file, args:"; val (p : path) = ("../../tmp/");

   355 (* recursively descend into thehier just before the error: *)

   356 (TESTthenodes p [] [0] thydata2file (! thehier)

   357   ["IsacKnowledge","Poly","Rulesets","norm_Poly"]

   358 handle _(* "stopped before error, created TESTdump" *) => ());

   359 val (pa, ids, po', wfn, (Ptyp (id, [n], ns))) = ! TESTdump;

   361 "~~~~~ fun thydata2file, args:"; val ((xmldata:path), (pos:pos), (theID:theID), thydata) =

   362   (pa, po', (ids@[id]), n);

   363 "~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =

   364   (theID:theID, thydata);

   365 "~~~~~ fun rls2xml, args:"; val (j, (thyID, Seq data)) = (i, thy_rls);

   366 "~~~~~ fun rls2xm, args:"; val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,

   367 		      srls, calc, errpatts, rules, scr})) = (j, (thyID, "Seq", data));

   368 "~~~~~ fun rules2xml, args:"; val (j, thyID, (r::rs)) = ((j+2*i), thyID, rules);

   369 "~~~~~ fun rule2xml, args:"; val (j, thyID, (Rls_ rls)) = (j, thyID, r);

   370 val rls' = (#id o rep_rls) rls;

   371 "~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = (thyID, rls');

   372 infix mem; (*from Isabelle2002*)

   373 fun x mem [] = false

   374   | x mem (y :: ys) = x = y orelse x mem ys;

   376     val rls' = strip_thy rls'

   377     val thy' = thyID2theory' thy'

   378     val dropthys =

   379       takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))

   380         (rev (!theory'));

   382 if map #1 dropthys = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", "Biegelinie",

   383   "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate",

   384   "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq",

   385   "LinEq", "Root", "Equation", "Rational"]

   386 then () else error "thy_containing_rls changed ancestors_rls for (Poly, discard_minus)";

   388     val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;

   389 		    val ancestors_rls =

   390 		      filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))

   391 		        (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));

   393 case assoc (ancestors_rls, rls') of

   394   SOME ("Poly", Rls {id = "discard_minus", ...}) => ()

   395 | _ => error "thy_containing_rls changed 2";

   397 "----------- fun store_thm ---------------------------------------";

   398 "----------- fun store_thm ---------------------------------------";

   399 "----------- fun store_thm ---------------------------------------";

   400 store_thm @{theory "Biegelinie"} "IsacKnowledge"

   401   ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})

   402 	    ["Walther Neuper 2005 supported by a grant from NMI Austria"];

   404 "~~~~~ fun store_thm, args:"; val (thy, part, (thmID : thmID, thm), (mathauthors : authors)) =

   405   (@{theory "Biegelinie"}, "IsacKnowledge",

   406     ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft}),

   407 	      ["Walther Neuper 2005 supported by a grant from NMI Austria"]);

   408     val guh = thm2guh (part, theory2thyID thy) thmID

   409     val theID = guh2theID guh;

   410 if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso

   411   theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]

   412 then () else error "store_thm: guh | theID changed";

   414 "----------- fun insert_fillpats ---------------------------------";

   415 "----------- fun insert_fillpats ---------------------------------";

   416 "----------- fun insert_fillpats ---------------------------------";

   417 (* vv--- this intermediate save/restore does not work and affects other tests ---vv

   418          see test/../calcelems.sml --- Unsynchronized.ref doesn't work any more ---

   420 val path = ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]: theID;

   422 (*save   *) val Hthm {guh, coursedesign, mathauthors, thm, fillpats = save_fillpats} = get_the path;

   424 val test_fillpats = [

   425   ("fill-d_d-arg",

   426     parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),

   427   ("test-fillpatt", e_term, "test-errpat")]: fillpat list;

   429 insert_fillpats path test_fillpats;

   430 val Hthm {fillpats, ...} = get_the path;

   431 case fillpats of

   432   [("fill-d_d-arg", _, "chain-rule-diff-both"), ("test-fillpatt", _, "test-errpat")] => ()

   433 | _ => error "insert_fillpats changed"

   435 (*restore*) insert_fillpats path save_fillpats;

   436 ^^^^^--- this intermediate save/restore does not work and affects other tests ---^^*)

   438 "----------- fun insert_errpatIDs --------------------------------";

   439 "----------- fun insert_errpatIDs --------------------------------";

   440 "----------- fun insert_errpatIDs --------------------------------";

   441 (* vv--- this intermediate save/restore does not work and affects other tests ---vv

   442          see test/../calcelems.sml --- Unsynchronized.ref doesn't work any more ---

   444 (* isolate test: 10 secs *) val original = (! thehier);

   446 (* still ununsed; planned for stepToErrorpattern *)

   447 val path = ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]: theID;

   448 val errpattIDs = ["chain-rule-diff-both", "test-errpatID"];

   450 insert_errpatIDs path errpattIDs;

   452 val Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)} = get_the path

   453 val Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, errpatts} = rls;

   455 if errpattIDs = ["chain-rule-diff-both", "test-errpatID"] then ()

   456 else error "insert_errpatIDs to norm_diff changed";

   458 (* isolate test: 10 secs *) thehier := original;

   459 ^^^^^--- this intermediate save/restore does not work and affects other tests ---^^*)

   461 insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]

   462  ([("fill-d_d-arg",

   463      parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),

   464    ("fill-both-args",

   465      parse_patt thy "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),

   466    ("fill-d_d",

   467      parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),

   468    ("fill-inner-deriv",

   469      parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),

   470    ("fill-all",

   471      parse_patt thy "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Mon, 27 Jan 2014 21:49:27 +0100
changeset 55359	73dc85c025ab
parent 52156	aa0884017d48
child 55397	71f7fd375e7d
permissions	-rw-r--r--