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: 
wneuper@59424: theory DiophantEq imports Base_Tools Equation Test
neuper@41931: begin
neuper@41921: 
neuper@52148: axiomatization where
neuper@41931:   int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
neuper@41921: 
wneuper@59472: ML \<open>val thy = @{theory}\<close>
neuper@41921: 
wneuper@59472: text \<open>problemclass for the usecase\<close>
wneuper@59472: setup \<open>KEStore_Elems.add_pbts
walther@59973:   [(Problem.prep_input thy "pbl_equ_dio" [] Problem.id_empty
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"])],
walther@59852:         Rule_Set.empty, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close>
neuper@41921: 
wneuper@59472: text \<open>method solving the usecase\<close>
wneuper@59545: 
wneuper@59504: partial_function (tailrec) diophant_equation :: "bool => int => bool"
wneuper@59504:   where
walther@59635: "diophant_equation e_e v_v = (
walther@59635:   Repeat (
walther@59637:     (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
walther@59637:     (Try (Calculate ''PLUS'')) #>
walther@59635:     (Try (Calculate ''TIMES''))) e_e)"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
walther@59973:     [Method.prep_input thy "met_test_diophant" [] Method.id_empty
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"])],
walther@59852:         {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
s1210629013@55373:           crls = tval_rls, errpats = [], nrls = Test_simplify},
wneuper@59551:         @{thm diophant_equation.simps})]
wneuper@59472: \<close>
neuper@41921: 
neuper@41921: end