neuper@41931: (* Title:  Knowledge/DiophantEq.thy
neuper@41931:    Author: Mathias Lehnfeld 2011
neuper@41931:    (c) due to copyright terms
neuper@41931: 12345678901234567890123456789012345678901234567890123456789012345678901234567890
neuper@41931:         10        20        30        40        50        60        70        80
neuper@41931: *)
neuper@41931: 
neuper@41931: theory DiophantEq imports Atools Equation Test
neuper@41931: begin
neuper@41921: 
neuper@41921: consts
neuper@41931:   Diophant'_equation :: "[bool, int, bool ] 
neuper@41921:                                        => bool "
neuper@41921:                     ("((Script Diophant'_equation (_ _ =))//(_))" 9)
neuper@41921: 
neuper@52148: axiomatization where
neuper@41931:   int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
neuper@41921: 
neuper@41931: ML {*val thy = @{theory}*}
neuper@41921: 
neuper@41931: text {*problemclass for the usecase*}
s1210629013@55359: setup {* KEStore_Elems.add_pbts
wneuper@59406:   [(Specify.prep_pbt thy "pbl_equ_dio" [] Celem.e_pblID
s1210629013@55339:       (["diophantine","equation"],
s1210629013@55339:         [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
s1210629013@55339:           (*                                      TODO: drop ^^^^^*)
s1210629013@55339:           ("#Where" ,[]),
s1210629013@55339:           ("#Find"  ,["boolTestFind s_s"])],
wneuper@59406:         Celem.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
neuper@41921: 
neuper@41931: text {*method solving the usecase*}
s1210629013@55373: setup {* KEStore_Elems.add_mets
wneuper@59406:   [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
wneuper@59406:       (["Test","solve_diophant"],
s1210629013@55373:         [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
s1210629013@55373:           (*                                      TODO: drop ^^^^^*)
s1210629013@55373:           ("#Where" ,[]),
s1210629013@55373:           ("#Find"  ,["boolTestFind s_s"])],
wneuper@59406:         {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls, prls = Celem.e_rls, calc = [],
s1210629013@55373:           crls = tval_rls, errpats = [], nrls = Test_simplify},
s1210629013@55373:         "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
s1210629013@55373:           "(Repeat                                                          " ^
s1210629013@55373:           "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
s1210629013@55373:           "     (Try (Calculate PLUS)) @@  " ^
s1210629013@55373:           "     (Try (Calculate TIMES))) e_e::bool)")]
s1210629013@55373: *}
neuper@41921: 
neuper@41921: end