(* Title:  Knowledge/DiophantEq.thy

    Author: Mathias Lehnfeld 2011

    (c) due to copyright terms

 12345678901234567890123456789012345678901234567890123456789012345678901234567890

         10        20        30        40        50        60        70        80

 *)

 theory DiophantEq imports Base_Tools Equation Test

 begin

 axiomatization where

   int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"

 ML \<open>val thy = @{theory}\<close>

 text \<open>problemclass for the usecase\<close>

 setup \<open>KEStore_Elems.add_pbts

   [(Problem.prep_input thy "pbl_equ_dio" [] Problem.id_empty

       (["diophantine", "equation"],

         [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),

           (*                                      TODO: drop ^^^^^*)

           ("#Where" ,[]),

           ("#Find"  ,["boolTestFind s_s"])],

         Rule_Set.empty, SOME "solve (e_e::bool, v_v::int)", [["LinEq", "solve_lineq_equation"]]))]\<close>

 text \<open>method solving the usecase\<close>

 partial_function (tailrec) diophant_equation :: "bool => int => bool"

   where

 "diophant_equation e_e v_v = (

   Repeat (

     (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>

     (Try (Calculate ''PLUS'')) #>

     (Try (Calculate ''TIMES''))) e_e)"

 setup \<open>KEStore_Elems.add_mets

     [MethodC.prep_input thy "met_test_diophant" [] MethodC.id_empty

       (["Test", "solve_diophant"],

         [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),

           (*                                      TODO: drop ^^^^^*)

           ("#Where" ,[]),

           ("#Find"  ,["boolTestFind s_s"])],

         {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],

           crls = tval_rls, errpats = [], nrls = Test_simplify},

         @{thm diophant_equation.simps})]

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end