Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/diophanteq.sml
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 17 Mar 2011 10:11:18 +0100
branchdecompose-isar
changeset 41931 ca6aac81b893
child 41932 a5e894d9fd8a
permissions -rw-r--r--
intermed. usecase Diophant

term2str changed output for unknown reason, eg. test/../integrate.sml
"Integral 1 / EI *\n (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"
(*"Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" *)
plus 1 change in test/../reational.sml for unknown reason

Test_Isac.thy goes through again. 
     1 (* Title:  tests on DiophantEq.thy

     2    Author: Mathias Lehnfeld 2011

     3    (c) due to copyright terms

     4 12345678901234567890123456789012345678901234567890123456789012345678901234567890

     5         10        20        30        40        50        60        70        80

     6 *)

     7 "--------------------------------------------------------";

     8 "table of contents --------------------------------------";

     9 "--------------------------------------------------------";

    10 "----------- rewriting for usecase1 ---------------------";

    11 "----------- mathengine with usecase1 -------------------";

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

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

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

    15 

    16 (*apparently no way to do these tests within DiophantEq.thy:

    17 val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system

    18   from CalcTreeTest*)

    19 (*(*val thy = @{theory "Isac"};toplevel error from store_met?!?*)*)

    20 *)

    21 val thy = @{theory "DiophantEq"};

    22 val ctxt = ProofContext.init_global thy;

    23 

    24 "----------- rewriting for usecase1 ---------------------";

    25 "----------- rewriting for usecase1 ---------------------";

    26 "----------- rewriting for usecase1 ---------------------";

    27 val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int")];

    28 val t = parseNEW ctxt "xxx + 111 = abc + (123::int)";

    29 

    30 val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst 

    31   (num_str @{thm "int_isolate_add"}) t; term2str t;

    32 

    33 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 

    34 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;

    35 

    36 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 

    37 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;

    38 

    39 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

    40 "----------- mathengine with usecase1 -------------------";

    41 "----------- mathengine with usecase1 -------------------";

    42 "----------- mathengine with usecase1 -------------------";

    43 val p = e_pos'; val c = []; 

    44 val (p,_,f,nxt,_,pt) = 

    45     CalcTreeTEST 

    46         [(["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven (xxx::int)", "boolTestFind sss"],

    47           (Context.theory_name thy, 

    48   ["diophantine","equation"], ["Test","solve_diophant"]))];

    49 "----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";

    50 val (p,_,f,nxt,_,pt) = me nxt p c pt; 

    51 val (p,_,f,nxt,_,pt) = me nxt p c pt; 

    52 val (p,_,f,nxt,_,pt) = me nxt p c pt; 

    53 val (p,_,f,nxt,_,pt) = me nxt p c pt; 

    54 val (p,_,f,nxt,_,pt) = me nxt p c pt; 

    55 val (p,_,f,nxt,_,pt) = me nxt p c pt; 

    56 val (p,_,f,nxt,_,pt) = me nxt p c pt; 

    57 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
wneuper/isa