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

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

setup \<open>KEStore_Elems.add_pbts

  [(Problem.prep_input @{theory} "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)"

method met_test_diophant : "Test/solve_diophant" =

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

    crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>

  Program: diophant_equation.simps

  Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"

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

  Where:

  Find: "boolTestFind s_s"

ML \<open>

\<close> ML \<open>

\<close>

end