|
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 |
|
|
wneuper@59424
|
8 |
theory DiophantEq imports Base_Tools 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 |
|
|
wneuper@59472
|
19 |
ML \<open>val thy = @{theory}\<close>
|
|
neuper@41921
|
20 |
|
|
wneuper@59472
|
21 |
text \<open>problemclass for the usecase\<close>
|
|
wneuper@59472
|
22 |
setup \<open>KEStore_Elems.add_pbts
|
|
wneuper@59406
|
23 |
[(Specify.prep_pbt thy "pbl_equ_dio" [] Celem.e_pblID
|
|
s1210629013@55339
|
24 |
(["diophantine","equation"],
|
|
s1210629013@55339
|
25 |
[("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
|
|
s1210629013@55339
|
26 |
(* TODO: drop ^^^^^*)
|
|
s1210629013@55339
|
27 |
("#Where" ,[]),
|
|
s1210629013@55339
|
28 |
("#Find" ,["boolTestFind s_s"])],
|
|
wneuper@59472
|
29 |
Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close>
|
|
neuper@41921
|
30 |
|
|
wneuper@59472
|
31 |
text \<open>method solving the usecase\<close>
|
|
wneuper@59505
|
32 |
(*ok
|
|
wneuper@59504
|
33 |
partial_function (tailrec) diophant_equation :: "bool => int => bool"
|
|
wneuper@59504
|
34 |
where
|
|
wneuper@59504
|
35 |
"diophant_equation e_e v_v =
|
|
wneuper@59504
|
36 |
(Repeat
|
|
wneuper@59504
|
37 |
((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@
|
|
wneuper@59504
|
38 |
(Try (Calculate ''PLUS'')) @@
|
|
wneuper@59504
|
39 |
(Try (Calculate ''TIMES''))) e_e)"
|
|
wneuper@59505
|
40 |
*)
|
|
wneuper@59472
|
41 |
setup \<open>KEStore_Elems.add_mets
|
|
wneuper@59473
|
42 |
[Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
|
|
wneuper@59406
|
43 |
(["Test","solve_diophant"],
|
|
s1210629013@55373
|
44 |
[("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
|
|
s1210629013@55373
|
45 |
(* TODO: drop ^^^^^*)
|
|
s1210629013@55373
|
46 |
("#Where" ,[]),
|
|
s1210629013@55373
|
47 |
("#Find" ,["boolTestFind s_s"])],
|
|
wneuper@59416
|
48 |
{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [],
|
|
s1210629013@55373
|
49 |
crls = tval_rls, errpats = [], nrls = Test_simplify},
|
|
s1210629013@55373
|
50 |
"Script Diophant_equation (e_e::bool) (v_v::int)= " ^
|
|
s1210629013@55373
|
51 |
"(Repeat " ^
|
|
wneuper@59488
|
52 |
" ((Try (Rewrite_Inst [(''bdv'',v_v::int)] ''int_isolate_add'' False)) @@" ^
|
|
wneuper@59488
|
53 |
" (Try (Calculate ''PLUS'')) @@ " ^
|
|
wneuper@59488
|
54 |
" (Try (Calculate ''TIMES''))) e_e::bool)")]
|
|
wneuper@59472
|
55 |
\<close>
|
|
neuper@41921
|
56 |
|
|
neuper@41921
|
57 |
end |