author | wenzelm |
Sun, 20 Jun 2021 16:26:18 +0200 | |
changeset 60306 | 51ec2e101e9f |
parent 60303 | 815b0dc8b589 |
child 60377 | 4f5f29fd0af9 |
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 |
|
neuper@52148 | 11 |
axiomatization where |
neuper@41931 | 12 |
int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))" |
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> |
wenzelm@60306 | 18 |
Method: "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" = |
wenzelm@60303 | 36 |
\<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], |
wenzelm@60303 | 37 |
crls = tval_rls, errpats = [], nrls = 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 |