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>
Fri, 18 Mar 2011 12:33:12 +0100
branchdecompose-isar
changeset 41934 95407f7fe14a
parent 41933 8d38adf87848
child 41936 c12d6f2a11aa
permissions -rw-r--r--
intermed. usecase Diophant: change usecase inttype

found only one working '= me' in test/../calculate.sml
and adjusted usecase to this test.

Test_Isac.thy worked !before! build 
     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 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

     8 "--------------------------------------------------------";

     9 "table of contents --------------------------------------";

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

    11 "----------- rewriting for usecase1 ---------------------";

    12 "----------- mathengine with usecase1 -------------------";

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

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

    15 "--------------------------------------------------------";

    16 

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

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

    19   from CalcTreeTest*)

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

    21 *)

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

    23 val ctxt = ProofContext.init_global thy;

    24 

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

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

    27 "----------- rewriting for usecase1 ---------------------";

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

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

    30 

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

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

    33 

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

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

    36 

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

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

    39 

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

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

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

    43 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

    44 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

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

    46 val (fmz, (thy, pbl, met)) = 

    47   (["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],

    48    (Context.theory_name thy, ["diophantine", "equation"], 

    49     ["Test", "solve_diophant"]));

    50 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];

    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 val (p,_,f,nxt,_,pt) = me nxt p c pt; 

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