(* 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 Atools Equation Test

 begin

 consts

   Diophant'_equation :: "[bool, int, bool ] 

                                        => bool "

                     ("((Script Diophant'_equation (_ _ =))//(_))" 9)

 axiomatization where

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

 ML {*val thy = @{theory}*}

 text {*problemclass for the usecase*}

 setup {* KEStore_Elems.add_pbts

   [(Specify.prep_pbt thy "pbl_equ_dio" [] Celem.e_pblID

       (["diophantine","equation"],

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

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

           ("#Where" ,[]),

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

         Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}

 text {*method solving the usecase*}

 setup {* KEStore_Elems.add_mets

   [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID

       (["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.e_rls, prls = Rule.e_rls, calc = [],

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

         "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^

           "(Repeat                                                          " ^

           "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^

           "     (Try (Calculate PLUS)) @@  " ^

           "     (Try (Calculate TIMES))) e_e::bool)")]

 *}

 end