author | wneuper <Walther.Neuper@jku.at> |
Mon, 07 Nov 2022 17:37:20 +0100 | |
changeset 60586 | 007ef64dbb08 |
parent 60509 | 2e0b7ca391dc |
child 60587 | 8af797c555a8 |
permissions | -rw-r--r-- |
neuper@41931 | 1 |
(* Title: Knowledge/DiophantEq.thy |
neuper@41931 | 2 |
Author: Mathias Lehnfeld 2011 |
neuper@41931 | 3 |
(c) due to copyright terms |
neuper@41931 | 4 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
neuper@41931 | 5 |
10 20 30 40 50 60 70 80 |
neuper@41931 | 6 |
*) |
neuper@41931 | 7 |
|
wneuper@59424 | 8 |
theory DiophantEq imports Base_Tools Equation Test |
neuper@41931 | 9 |
begin |
neuper@41921 | 10 |
|
walther@60377 | 11 |
lemma int_isolate_add : "(bdv + a = b) = (bdv = b + -1 * (a::int))" |
walther@60377 | 12 |
by auto |
neuper@41921 | 13 |
|
wneuper@59472 | 14 |
text \<open>problemclass for the usecase\<close> |
wenzelm@60306 | 15 |
|
wenzelm@60306 | 16 |
problem pbl_equ_dio : "diophantine/equation" = |
wenzelm@60306 | 17 |
\<open>Rule_Set.empty\<close> |
Walther@60449 | 18 |
Method_Ref: "LinEq/solve_lineq_equation" |
wenzelm@60306 | 19 |
CAS: "solve (e_e::bool, v_v::int)" |
wenzelm@60306 | 20 |
Given: "boolTestGiven e_e" "intTestGiven (v_v::int)" |
wenzelm@60306 | 21 |
(* TODO: drop ^^^^^*) |
wenzelm@60306 | 22 |
Where: |
wenzelm@60306 | 23 |
Find: "boolTestFind s_s" |
neuper@41921 | 24 |
|
wneuper@59472 | 25 |
text \<open>method solving the usecase\<close> |
wneuper@59545 | 26 |
|
wneuper@59504 | 27 |
partial_function (tailrec) diophant_equation :: "bool => int => bool" |
wneuper@59504 | 28 |
where |
walther@59635 | 29 |
"diophant_equation e_e v_v = ( |
walther@59635 | 30 |
Repeat ( |
walther@59637 | 31 |
(Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #> |
walther@59637 | 32 |
(Try (Calculate ''PLUS'')) #> |
walther@59635 | 33 |
(Try (Calculate ''TIMES''))) e_e)" |
wenzelm@60303 | 34 |
|
wenzelm@60303 | 35 |
method met_test_diophant : "Test/solve_diophant" = |
Walther@60586 | 36 |
\<open>{rew_ord = "Rewrite_Ord.id_empty", rls' = tval_rls, prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, calc = [], |
Walther@60586 | 37 |
crls = tval_rls, errpats = [], rew_rls = Test_simplify}\<close> |
wenzelm@60303 | 38 |
Program: diophant_equation.simps |
wenzelm@60303 | 39 |
Given: "boolTestGiven e_e" "intTestGiven (v_v::int)" |
wenzelm@60303 | 40 |
(* TODO: drop ^^^^^*) |
wenzelm@60303 | 41 |
Where: |
wenzelm@60303 | 42 |
Find: "boolTestFind s_s" |
wenzelm@60303 | 43 |
ML \<open> |
walther@60278 | 44 |
\<close> ML \<open> |
wneuper@59472 | 45 |
\<close> |
neuper@41921 | 46 |
|
walther@60278 | 47 |
end |