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