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

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

  by auto

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

problem pbl_equ_dio : "diophantine/equation" =

  \<open>Rule_Set.empty\<close>

  Method_Ref: "LinEq/solve_lineq_equation"

  CAS: "solve (e_e::bool, v_v::int)"

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

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

  Where:

  Find: "boolTestFind s_s"

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' = "Rewrite_Ord.id_empty", 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