1 (* Title: Knowledge/DiophantEq.thy
2 Author: Mathias Lehnfeld 2011
3 (c) due to copyright terms
4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80
8 theory DiophantEq imports Base_Tools Equation Test
11 lemma int_isolate_add : "(bdv + a = b) = (bdv = b + -1 * (a::int))"
14 text \<open>problemclass for the usecase\<close>
16 problem pbl_equ_dio : "diophantine/equation" =
17 \<open>Rule_Set.empty\<close>
18 Method_Ref: "LinEq/solve_lineq_equation"
19 CAS: "solve (e_e::bool, v_v::int)"
20 Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
23 Find: "boolTestFind s_s"
25 text \<open>method solving the usecase\<close>
27 partial_function (tailrec) diophant_equation :: "bool => int => bool"
29 "diophant_equation e_e v_v = (
31 (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
32 (Try (Calculate ''PLUS'')) #>
33 (Try (Calculate ''TIMES''))) e_e)"
35 method met_test_diophant : "Test/solve_diophant" =
36 \<open>{rew_ord = "Rewrite_Ord.id_empty", rls' = tval_rls, prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, calc = [],
37 crls = tval_rls, errpats = [], rew_rls = Test_simplify}\<close>
38 Program: diophant_equation.simps
39 Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
42 Find: "boolTestFind s_s"