|
neuper@41931
|
1 |
(* Title: tests on DiophantEq.thy
|
|
neuper@41931
|
2 |
Author: Mathias Lehnfeld 2011
|
|
neuper@41931
|
3 |
(c) due to copyright terms
|
|
neuper@41931
|
4 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890
|
|
neuper@41931
|
5 |
10 20 30 40 50 60 70 80
|
|
neuper@41931
|
6 |
*)
|
|
neuper@41934
|
7 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
|
neuper@41931
|
8 |
"--------------------------------------------------------";
|
|
neuper@41931
|
9 |
"table of contents --------------------------------------";
|
|
neuper@41931
|
10 |
"--------------------------------------------------------";
|
|
neuper@41931
|
11 |
"----------- rewriting for usecase1 ---------------------";
|
|
neuper@41931
|
12 |
"----------- mathengine with usecase1 -------------------";
|
|
neuper@41931
|
13 |
"--------------------------------------------------------";
|
|
neuper@41931
|
14 |
"--------------------------------------------------------";
|
|
neuper@41931
|
15 |
"--------------------------------------------------------";
|
|
neuper@41931
|
16 |
|
|
neuper@41931
|
17 |
(*apparently no way to do these tests within DiophantEq.thy:
|
|
neuper@41931
|
18 |
val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
|
|
neuper@41931
|
19 |
from CalcTreeTest*)
|
|
neuper@41932
|
20 |
(*val thy = @{theory "Isac"};toplevel error from store_met?!?*)
|
|
neuper@41931
|
21 |
*)
|
|
neuper@41931
|
22 |
val thy = @{theory "DiophantEq"};
|
|
neuper@41931
|
23 |
val ctxt = ProofContext.init_global thy;
|
|
neuper@41931
|
24 |
|
|
neuper@41931
|
25 |
"----------- rewriting for usecase1 ---------------------";
|
|
neuper@41931
|
26 |
"----------- rewriting for usecase1 ---------------------";
|
|
neuper@41931
|
27 |
"----------- rewriting for usecase1 ---------------------";
|
|
neuper@41931
|
28 |
val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int")];
|
|
neuper@41931
|
29 |
val t = parseNEW ctxt "xxx + 111 = abc + (123::int)";
|
|
neuper@41931
|
30 |
|
|
neuper@41931
|
31 |
val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst
|
|
neuper@41931
|
32 |
(num_str @{thm "int_isolate_add"}) t; term2str t;
|
|
neuper@41931
|
33 |
|
|
neuper@41931
|
34 |
val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
|
|
neuper@41931
|
35 |
val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
|
|
neuper@41931
|
36 |
|
|
neuper@41931
|
37 |
val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
|
|
neuper@41931
|
38 |
val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
|
|
neuper@41931
|
39 |
|
|
neuper@41931
|
40 |
"----------- mathengine with usecase1 -------------------";
|
|
neuper@41931
|
41 |
"----------- mathengine with usecase1 -------------------";
|
|
neuper@41931
|
42 |
"----------- mathengine with usecase1 -------------------";
|
|
neuper@41934
|
43 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|
|
neuper@41934
|
44 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
|
neuper@41934
|
45 |
val p = e_pos'; val c = [];
|
|
neuper@41934
|
46 |
val (fmz, (thy, pbl, met)) =
|
|
neuper@41934
|
47 |
(["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],
|
|
neuper@41934
|
48 |
(Context.theory_name thy, ["diophantine", "equation"],
|
|
neuper@41934
|
49 |
["Test", "solve_diophant"]));
|
|
neuper@41934
|
50 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
|
|
neuper@41931
|
51 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@41931
|
52 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@41931
|
53 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@41931
|
54 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@41931
|
55 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@41931
|
56 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@41933
|
57 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@41931
|
58 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|