1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Thu Mar 17 10:11:18 2011 +0100
1.3 @@ -0,0 +1,57 @@
1.4 +(* Title: tests on DiophantEq.thy
1.5 + Author: Mathias Lehnfeld 2011
1.6 + (c) due to copyright terms
1.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.8 + 10 20 30 40 50 60 70 80
1.9 +*)
1.10 +"--------------------------------------------------------";
1.11 +"table of contents --------------------------------------";
1.12 +"--------------------------------------------------------";
1.13 +"----------- rewriting for usecase1 ---------------------";
1.14 +"----------- mathengine with usecase1 -------------------";
1.15 +"--------------------------------------------------------";
1.16 +"--------------------------------------------------------";
1.17 +"--------------------------------------------------------";
1.18 +
1.19 +(*apparently no way to do these tests within DiophantEq.thy:
1.20 +val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
1.21 + from CalcTreeTest*)
1.22 +(*(*val thy = @{theory "Isac"};toplevel error from store_met?!?*)*)
1.23 +*)
1.24 +val thy = @{theory "DiophantEq"};
1.25 +val ctxt = ProofContext.init_global thy;
1.26 +
1.27 +"----------- rewriting for usecase1 ---------------------";
1.28 +"----------- rewriting for usecase1 ---------------------";
1.29 +"----------- rewriting for usecase1 ---------------------";
1.30 +val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int")];
1.31 +val t = parseNEW ctxt "xxx + 111 = abc + (123::int)";
1.32 +
1.33 +val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst
1.34 + (num_str @{thm "int_isolate_add"}) t; term2str t;
1.35 +
1.36 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
1.37 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
1.38 +
1.39 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
1.40 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
1.41 +
1.42 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.43 +"----------- mathengine with usecase1 -------------------";
1.44 +"----------- mathengine with usecase1 -------------------";
1.45 +"----------- mathengine with usecase1 -------------------";
1.46 +val p = e_pos'; val c = [];
1.47 +val (p,_,f,nxt,_,pt) =
1.48 + CalcTreeTEST
1.49 + [(["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven (xxx::int)", "boolTestFind sss"],
1.50 + (Context.theory_name thy,
1.51 + ["diophantine","equation"], ["Test","solve_diophant"]))];
1.52 +"----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
1.53 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.54 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.55 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.56 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.58 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.59 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.60 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)