clarified theory context: avoid global "val thy = ..." hanging around (left-over from Isabelle2005), which is apt to various pitfalls;
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
12 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
14 text \<open>problemclass for the usecase\<close>
15 setup \<open>KEStore_Elems.add_pbts
16 [(Problem.prep_input @{theory} "pbl_equ_dio" [] Problem.id_empty
17 (["diophantine", "equation"],
18 [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),
21 ("#Find" ,["boolTestFind s_s"])],
22 Rule_Set.empty, SOME "solve (e_e::bool, v_v::int)", [["LinEq", "solve_lineq_equation"]]))]\<close>
24 text \<open>method solving the usecase\<close>
26 partial_function (tailrec) diophant_equation :: "bool => int => bool"
28 "diophant_equation e_e v_v = (
30 (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
31 (Try (Calculate ''PLUS'')) #>
32 (Try (Calculate ''TIMES''))) e_e)"
33 setup \<open>KEStore_Elems.add_mets
34 [MethodC.prep_input @{theory} "met_test_diophant" [] MethodC.id_empty
35 (["Test", "solve_diophant"],
36 [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),
39 ("#Find" ,["boolTestFind s_s"])],
40 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
41 crls = tval_rls, errpats = [], nrls = Test_simplify},
42 @{thm diophant_equation.simps})]