(* 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*}

ML {*

store_pbt

 (prep_pbt thy "pbl_equ_dio" [] e_pblID

 (["diophantine","equation"],

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

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

   ("#Where" ,[]),

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

  ],

  e_rls, SOME "solve (e_e::bool, v_v::int)",

  [["LinEq","solve_lineq_equation"]])); (*-----TODO*)

*}

setup {* KEStore_Elems.add_pbts

  [(prep_pbt thy "pbl_equ_dio" [] e_pblID

      (["diophantine","equation"],

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

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

          ("#Where" ,[]),

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

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

text {*method solving the usecase*}

ML {*

store_met

(prep_met thy "met_test_diophant" [] e_metID

 (["Test","solve_diophant"]:metID,

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

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

   ("#Where" ,[]),

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

  ],

   {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,

    prls = 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