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 Diophant'_equation :: "[bool, int, bool ]
14 ("((Script Diophant'_equation (_ _ =))//(_))" 9)
17 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
19 ML \<open>val thy = @{theory}\<close>
21 text \<open>problemclass for the usecase\<close>
22 setup \<open>KEStore_Elems.add_pbts
23 [(Specify.prep_pbt thy "pbl_equ_dio" [] Celem.e_pblID
24 (["diophantine","equation"],
25 [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
28 ("#Find" ,["boolTestFind s_s"])],
29 Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close>
31 text \<open>method solving the usecase\<close>
32 partial_function (tailrec) diophant_equation :: "bool => int => bool"
34 "diophant_equation e_e v_v =
36 ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@
37 (Try (Calculate ''PLUS'')) @@
38 (Try (Calculate ''TIMES''))) e_e)"
39 setup \<open>KEStore_Elems.add_mets
40 [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
41 (["Test","solve_diophant"],
42 [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
45 ("#Find" ,["boolTestFind s_s"])],
46 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [],
47 crls = tval_rls, errpats = [], nrls = Test_simplify},
48 "Script Diophant_equation (e_e::bool) (v_v::int)= " ^
50 " ((Try (Rewrite_Inst [(''bdv'',v_v::int)] ''int_isolate_add'' False)) @@" ^
51 " (Try (Calculate ''PLUS'')) @@ " ^
52 " (Try (Calculate ''TIMES''))) e_e::bool)")]