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*}
neuper@41921: ML {*
neuper@41921: store_pbt
neuper@41921:  (prep_pbt thy "pbl_equ_dio" [] e_pblID
neuper@41921:  (["diophantine","equation"],
neuper@41921:   [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
neuper@41921:   (*                                      TODO: drop ^^^^^*)
neuper@41921:    ("#Where" ,[]),
neuper@41921:    ("#Find"  ,["boolTestFind s_s"]) 
neuper@41921:   ],
neuper@41921:   e_rls, SOME "solve (e_e::bool, v_v::int)",
neuper@41921:   [["LinEq","solve_lineq_equation"]])); (*-----TODO*)
neuper@41921: *}
s1210629013@55339: setup {* KEStore_Elems.store_pbts
s1210629013@55339:   [(prep_pbt thy "pbl_equ_dio" [] 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"])],
s1210629013@55339:         e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
neuper@41921: 
neuper@41931: text {*method solving the usecase*}
neuper@41921: ML {*
neuper@41931: store_met
neuper@41931: (prep_met thy "met_test_diophant" [] e_metID
neuper@41931:  (["Test","solve_diophant"]:metID,
neuper@41931:   [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
neuper@41931:   (*                                      TODO: drop ^^^^^*)
neuper@41931:    ("#Where" ,[]),
neuper@41931:    ("#Find"  ,["boolTestFind s_s"]) 
neuper@41931:   ],
neuper@41931:    {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
neuper@42425:     prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},
neuper@41931:  "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
neuper@41931:  "(Repeat                                                          " ^
neuper@41931:  "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
neuper@41931:  "     (Try (Calculate PLUS)) @@  " ^
neuper@41931:  "     (Try (Calculate TIMES))) e_e::bool)"
neuper@41931:  ))
neuper@41921: *}
neuper@41921: 
neuper@41921: end