neuper@37906
|
1 |
(* equations and functions; functions NOT as lambda-terms
|
neuper@37906
|
2 |
author: Walther Neuper 2005, 2006
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
*)
|
neuper@37906
|
5 |
|
wneuper@59424
|
6 |
theory Equation imports Base_Tools begin
|
neuper@37906
|
7 |
|
wneuper@59472
|
8 |
text \<open>univariate equations over terms :
|
neuper@42398
|
9 |
In 2003 Richard Lang prototyped ISAC's equation solver while also alpha-testing
|
neuper@42398
|
10 |
the Lucas-Interpreter's Subproblem mechanism.
|
neuper@42398
|
11 |
This prototype suffers from the drop-out of Matthias Goldgruber for a year,
|
neuper@42398
|
12 |
who had started to work on simplification in parallel. So this implementation
|
neuper@42398
|
13 |
replaced simplifiers by many specific theorems for specific terms in specific
|
neuper@42398
|
14 |
phases of equation solving; these specific solutions wait for generalisation
|
neuper@42398
|
15 |
in future improvements of ISAC's equation solver.
|
wneuper@59472
|
16 |
\<close>
|
neuper@42398
|
17 |
|
neuper@37906
|
18 |
consts
|
neuper@37906
|
19 |
|
neuper@37906
|
20 |
(*descriptions in the related problems TODOshift here from Descriptions.thy*)
|
neuper@37950
|
21 |
substitution :: "bool => una"
|
neuper@37906
|
22 |
|
neuper@37906
|
23 |
(*the CAS-commands*)
|
neuper@37950
|
24 |
solve :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
|
neuper@37950
|
25 |
solveTest :: "[bool * 'a] => bool list" (* for test collection *)
|
neuper@37906
|
26 |
|
wneuper@59472
|
27 |
text \<open>defines equation and univariate-equation
|
neuper@37950
|
28 |
created by: rlang
|
neuper@37950
|
29 |
date: 02.09
|
neuper@37950
|
30 |
changed by: rlang
|
neuper@37950
|
31 |
last change by: rlang
|
neuper@37950
|
32 |
date: 02.11.29
|
wneuper@59472
|
33 |
(c) by Richard Lang, 2003\<close>
|
neuper@37950
|
34 |
|
wneuper@59472
|
35 |
ML \<open>
|
neuper@37972
|
36 |
val thy = @{theory};
|
wneuper@59416
|
37 |
val ctxt = Rule.thy2ctxt thy;
|
neuper@37972
|
38 |
|
neuper@37950
|
39 |
val univariate_equation_prls =
|
wneuper@59416
|
40 |
Rule.append_rls "univariate_equation_prls" Rule.e_rls
|
wneuper@59491
|
41 |
[Rule.Calc ("Tools.matches", Tools.eval_matches "")];
|
wneuper@59472
|
42 |
\<close>
|
wneuper@59472
|
43 |
setup \<open>KEStore_Elems.add_rlss [("univariate_equation_prls",
|
wneuper@59472
|
44 |
(Context.theory_name @{theory}, LTool.prep_rls @{theory} univariate_equation_prls))]\<close>
|
wneuper@59472
|
45 |
setup \<open>KEStore_Elems.add_pbts
|
wneuper@59406
|
46 |
[(Specify.prep_pbt thy "pbl_equ" [] Celem.e_pblID
|
s1210629013@55339
|
47 |
(["equation"],
|
s1210629013@55339
|
48 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
s1210629013@55339
|
49 |
("#Where" ,["matches (?a = ?b) e_e"]),
|
s1210629013@55339
|
50 |
("#Find" ,["solutions v_v'i'"])],
|
wneuper@59491
|
51 |
Rule.append_rls "equation_prls" Rule.e_rls [Rule.Calc ("Tools.matches", Tools.eval_matches "")],
|
s1210629013@55339
|
52 |
SOME "solve (e_e::bool, v_v)", [])),
|
wneuper@59406
|
53 |
(Specify.prep_pbt thy "pbl_equ_univ" [] Celem.e_pblID
|
s1210629013@55339
|
54 |
(["univariate","equation"],
|
s1210629013@55339
|
55 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
s1210629013@55339
|
56 |
("#Where" ,["matches (?a = ?b) e_e"]),
|
s1210629013@55339
|
57 |
("#Find" ,["solutions v_v'i'"])],
|
wneuper@59472
|
58 |
univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))]\<close>
|
neuper@37950
|
59 |
|
neuper@37950
|
60 |
|
wneuper@59472
|
61 |
ML\<open>
|
neuper@37950
|
62 |
(*.function for handling the cas-input "solve (x+1=2, x)":
|
wneuper@59279
|
63 |
make a model which is already in ctree-internal format.*)
|
neuper@37950
|
64 |
(* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
|
wneuper@59186
|
65 |
val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy))
|
neuper@37950
|
66 |
"solveTest (x+1=2, x)");
|
neuper@37950
|
67 |
*)
|
neuper@41972
|
68 |
fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =
|
wneuper@59389
|
69 |
[((the o (TermC.parseNEW ctxt)) "equality", [eq]),
|
wneuper@59389
|
70 |
((the o (TermC.parseNEW ctxt)) "solveFor", [bdv]),
|
wneuper@59389
|
71 |
((the o (TermC.parseNEW ctxt)) "solutions",
|
wneuper@59389
|
72 |
[(the o (TermC.parseNEW ctxt)) "L"])
|
neuper@37950
|
73 |
]
|
neuper@38031
|
74 |
| argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
|
wneuper@59472
|
75 |
\<close>
|
wneuper@59472
|
76 |
setup \<open>KEStore_Elems.add_cas
|
wneuper@59389
|
77 |
[((Thm.term_of o the o (TermC.parse thy)) "solveTest",
|
s1210629013@52170
|
78 |
(("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)),
|
wneuper@59389
|
79 |
((Thm.term_of o the o (TermC.parse thy)) "solve",
|
wneuper@59592
|
80 |
(("Isac_Knowledge", ["univariate","equation"], ["no_met"]), argl2dtss))]\<close>
|
neuper@37950
|
81 |
|
neuper@37950
|
82 |
|
wneuper@59472
|
83 |
setup \<open>KEStore_Elems.add_mets
|
wneuper@59473
|
84 |
[Specify.prep_met thy "met_equ" [] Celem.e_metID
|
s1210629013@55373
|
85 |
(["Equation"], [],
|
wneuper@59416
|
86 |
{rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
|
wneuper@59416
|
87 |
errpats = [], nrls = Rule.e_rls},
|
wneuper@59545
|
88 |
@{thm refl})]
|
wneuper@59472
|
89 |
\<close>
|
neuper@37950
|
90 |
|
neuper@37906
|
91 |
end |