neuper@41931
|
1 |
(* Title: Knowledge/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@41931
|
7 |
|
neuper@41931
|
8 |
theory DiophantEq imports Atools Equation Test
|
neuper@41931
|
9 |
begin
|
neuper@41921
|
10 |
|
neuper@41921
|
11 |
consts
|
neuper@41931
|
12 |
Diophant'_equation :: "[bool, int, bool ]
|
neuper@41921
|
13 |
=> bool "
|
neuper@41921
|
14 |
("((Script Diophant'_equation (_ _ =))//(_))" 9)
|
neuper@41921
|
15 |
|
neuper@52148
|
16 |
axiomatization where
|
neuper@41931
|
17 |
int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
|
neuper@41921
|
18 |
|
neuper@41931
|
19 |
ML {*val thy = @{theory}*}
|
neuper@41921
|
20 |
|
neuper@41931
|
21 |
text {*problemclass for the usecase*}
|
neuper@41921
|
22 |
ML {*
|
neuper@41921
|
23 |
store_pbt
|
neuper@41921
|
24 |
(prep_pbt thy "pbl_equ_dio" [] e_pblID
|
neuper@41921
|
25 |
(["diophantine","equation"],
|
neuper@41921
|
26 |
[("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
|
neuper@41921
|
27 |
(* TODO: drop ^^^^^*)
|
neuper@41921
|
28 |
("#Where" ,[]),
|
neuper@41921
|
29 |
("#Find" ,["boolTestFind s_s"])
|
neuper@41921
|
30 |
],
|
neuper@41921
|
31 |
e_rls, SOME "solve (e_e::bool, v_v::int)",
|
neuper@41921
|
32 |
[["LinEq","solve_lineq_equation"]])); (*-----TODO*)
|
neuper@41921
|
33 |
show_ptyps();
|
neuper@41921
|
34 |
get_pbt ["diophantine","equation"];
|
neuper@41921
|
35 |
*}
|
neuper@41921
|
36 |
|
neuper@41931
|
37 |
text {*method solving the usecase*}
|
neuper@41921
|
38 |
ML {*
|
neuper@41931
|
39 |
store_met
|
neuper@41931
|
40 |
(prep_met thy "met_test_diophant" [] e_metID
|
neuper@41931
|
41 |
(["Test","solve_diophant"]:metID,
|
neuper@41931
|
42 |
[("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
|
neuper@41931
|
43 |
(* TODO: drop ^^^^^*)
|
neuper@41931
|
44 |
("#Where" ,[]),
|
neuper@41931
|
45 |
("#Find" ,["boolTestFind s_s"])
|
neuper@41931
|
46 |
],
|
neuper@41931
|
47 |
{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
|
neuper@42425
|
48 |
prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},
|
neuper@41931
|
49 |
"Script Diophant_equation (e_e::bool) (v_v::int)= " ^
|
neuper@41931
|
50 |
"(Repeat " ^
|
neuper@41931
|
51 |
" ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
|
neuper@41931
|
52 |
" (Try (Calculate PLUS)) @@ " ^
|
neuper@41931
|
53 |
" (Try (Calculate TIMES))) e_e::bool)"
|
neuper@41931
|
54 |
))
|
neuper@41921
|
55 |
*}
|
neuper@41921
|
56 |
|
neuper@41921
|
57 |
end |