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

 axioms

   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*)

 show_ptyps();

 get_pbt ["diophantine","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, 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