intermed. usecase Diophant
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
7 "--------------------------------------------------------";
8 "table of contents --------------------------------------";
9 "--------------------------------------------------------";
10 "----------- rewriting for usecase1 ---------------------";
11 "----------- mathengine with usecase1 -------------------";
12 "----------- rewriting for usecase2 ---------------------";
13 "----------- mathengine with usecase2 -------------------";
14 "--------------------------------------------------------";
15 "--------------------------------------------------------";
16 "--------------------------------------------------------";
18 (*there seemed to be no way to do these tests within DiophantEq.thy:
19 val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
21 (*val thy = @{theory "Isac"};toplevel error from store_met?!?*)
23 val thy = @{theory "DiophantEq"};
24 val ctxt = ProofContext.init_global thy;
26 "----------- rewriting for usecase1 ---------------------";
27 "----------- rewriting for usecase1 ---------------------";
28 "----------- rewriting for usecase1 ---------------------";
29 val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int")];
30 val t = parseNEW ctxt "xxx + 111 = abc + (123::int)";
32 val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst
33 (num_str @{thm "int_isolate_add"}) t; term2str t;
35 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
36 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
38 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
39 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
41 "----------- mathengine with usecase1 -------------------";
42 "----------- mathengine with usecase1 -------------------";
43 "----------- mathengine with usecase1 -------------------";
44 val p = e_pos'; val c = [];
45 val (fmz, (thy, pbl, met)) =
46 (["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven xxx",
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 (*========== inhibit exn WN110318 ==============================================
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 val (p,_,f,nxt,_,pt) = me nxt p c pt;
59 ============ inhibit exn WN110318 ============================================*)
61 "----------- rewriting for usecase2 ---------------------";
62 "----------- rewriting for usecase2 ---------------------";
63 val thy = @{theory "Test"};
64 "----------- rewriting for usecase2 ---------------------";
66 val t = parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)";
68 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
69 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
71 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
72 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
75 "----------- mathengine with usecase2 -------------------";
76 "----------- mathengine with usecase2 -------------------";
77 "----------- mathengine with usecase2 -------------------";
78 val p = e_pos'; val c = [];
79 val (fmz, (thy, pbl, met)) =
80 (["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],
81 (Context.theory_name thy, ["inttype","test"], ["Test","intsimp"]));
82 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
83 (*nxt = ("Model_Problem", ...)*)
84 val (p,_,f,nxt,_,pt) = me nxt p c pt;
85 (*nxt = ("Add_Given", Add_Given "intTestGiven (xxx + abc + -1 * 111 + 123)")*)
86 val (p,_,f,nxt,_,pt) = me nxt p c pt;
87 (* Add_Find ###########################################*)
88 val (p,_,f,nxt,_,pt) = me nxt p c pt;
89 (*nxt = ("Specify_Theory", ...)*)
90 val (p,_,f,nxt,_,pt) = me nxt p c pt;
91 (*nxt = ("Specify_Problem", ...)*)
92 val (p,_,f,nxt,_,pt) = me nxt p c pt;
93 (*nxt = ("Specify_Method", ...)*)
94 val (p,_,f,nxt,_,pt) = me nxt p c pt;
95 (*nxt = ("Empty_Tac", ...) #############################*)
96 val (p,_,f,nxt,_,pt) = me nxt p c pt;
97 (*========== inhibit exn WN110318 ==============================================
98 ============ inhibit exn WN110318 ============================================*)