27 ("#Where" ,[]), |
27 ("#Where" ,[]), |
28 ("#Find" ,["boolTestFind s_s"])], |
28 ("#Find" ,["boolTestFind s_s"])], |
29 Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close> |
29 Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close> |
30 |
30 |
31 text \<open>method solving the usecase\<close> |
31 text \<open>method solving the usecase\<close> |
32 (*ok |
32 |
33 partial_function (tailrec) diophant_equation :: "bool => int => bool" |
33 partial_function (tailrec) diophant_equation :: "bool => int => bool" |
34 where |
34 where |
35 "diophant_equation e_e v_v = |
35 "diophant_equation e_e v_v = |
36 (Repeat |
36 (Repeat |
37 ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@ |
37 ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@ |
38 (Try (Calculate ''PLUS'')) @@ |
38 (Try (Calculate ''PLUS'')) @@ |
39 (Try (Calculate ''TIMES''))) e_e)" |
39 (Try (Calculate ''TIMES''))) e_e)" |
40 *) |
|
41 setup \<open>KEStore_Elems.add_mets |
40 setup \<open>KEStore_Elems.add_mets |
42 [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID |
41 [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID |
43 (["Test","solve_diophant"], |
42 (["Test","solve_diophant"], |
44 [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]), |
43 [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]), |
45 (* TODO: drop ^^^^^*) |
44 (* TODO: drop ^^^^^*) |
46 ("#Where" ,[]), |
45 ("#Where" ,[]), |
47 ("#Find" ,["boolTestFind s_s"])], |
46 ("#Find" ,["boolTestFind s_s"])], |
48 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], |
47 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], |
49 crls = tval_rls, errpats = [], nrls = Test_simplify}, |
48 crls = tval_rls, errpats = [], nrls = Test_simplify}, |
50 "Script Diophant_equation (e_e::bool) (v_v::int)= " ^ |
49 @{thm diophant_equation.simps} |
|
50 (*"Script Diophant_equation (e_e::bool) (v_v::int)= " ^ |
51 "(Repeat " ^ |
51 "(Repeat " ^ |
52 " ((Try (Rewrite_Inst [(''bdv'',v_v::int)] ''int_isolate_add'' False)) @@" ^ |
52 " ((Try (Rewrite_Inst [(''bdv'',v_v::int)] ''int_isolate_add'' False)) @@" ^ |
53 " (Try (Calculate ''PLUS'')) @@ " ^ |
53 " (Try (Calculate ''PLUS'')) @@ " ^ |
54 " (Try (Calculate ''TIMES''))) e_e::bool)")] |
54 " (Try (Calculate ''TIMES''))) e_e::bool)"*))] |
55 \<close> |
55 \<close> |
56 |
56 |
57 end |
57 end |