neuper@41931: (* Title:  Knowledge/DiophantEq.thy
neuper@41931:    Author: Mathias Lehnfeld 2011
neuper@41931:    (c) due to copyright terms
neuper@41931: 12345678901234567890123456789012345678901234567890123456789012345678901234567890
neuper@41931:         10        20        30        40        50        60        70        80
neuper@41931: *)
neuper@41931: 
wneuper@59424: theory DiophantEq imports Base_Tools Equation Test
neuper@41931: begin
neuper@41921: 
walther@60377: lemma int_isolate_add : "(bdv + a = b) = (bdv = b +  -1 * (a::int))"
walther@60377:   by auto
neuper@41921: 
wneuper@59472: text \<open>problemclass for the usecase\<close>
wenzelm@60306: 
wenzelm@60306: problem pbl_equ_dio : "diophantine/equation" =
wenzelm@60306:   \<open>Rule_Set.empty\<close>
Walther@60449:   Method_Ref: "LinEq/solve_lineq_equation"
wenzelm@60306:   CAS: "solve (e_e::bool, v_v::int)"
wenzelm@60306:   Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
wenzelm@60306:   (*                                TODO: drop ^^^^^*)
wenzelm@60306:   Where:
wenzelm@60306:   Find: "boolTestFind s_s"
neuper@41921: 
wneuper@59472: text \<open>method solving the usecase\<close>
wneuper@59545: 
wneuper@59504: partial_function (tailrec) diophant_equation :: "bool => int => bool"
wneuper@59504:   where
walther@59635: "diophant_equation e_e v_v = (
walther@59635:   Repeat (
walther@59637:     (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
walther@59637:     (Try (Calculate ''PLUS'')) #>
walther@59635:     (Try (Calculate ''TIMES''))) e_e)"
wenzelm@60303: 
wenzelm@60303: method met_test_diophant : "Test/solve_diophant" =
Walther@60509:   \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
wenzelm@60303:     crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
wenzelm@60303:   Program: diophant_equation.simps
wenzelm@60303:   Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
wenzelm@60303: (*                                  TODO: drop ^^^^^*)
wenzelm@60303:   Where:
wenzelm@60303:   Find: "boolTestFind s_s"
wenzelm@60303: ML \<open>
walther@60278: \<close> ML \<open>
wneuper@59472: \<close>
neuper@41921: 
walther@60278: end