1 (* Title: example_1 |
1 |
2 Author: Jan Rocnik |
|
3 Description: The following Example can be used as an HOWTO on applying |
|
4 already implemented Subproblems. In example solving a |
|
5 linear equation. |
|
6 (c) copyright due to license terms. |
|
7 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
|
8 10 20 30 40 50 60 70 80 |
|
9 *) |
|
10 |
2 |
11 theory example_1 imports Isac |
3 theory example_1 imports Isac |
12 begin |
4 begin |
13 |
5 |
14 section{*Equation Solving*} |
6 section{*Equation Solving*} |
15 text{*Setup equation, Calc Tree,\ldots*} |
7 text{*Setup equation, Calc Tree,\ldots*} |
16 |
8 |
17 ML {* |
9 ML {* |
18 val equation = "equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))"; |
10 val expr = ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))", |
19 val expr = [ equation, "solveFor z", "solutions L"]; (*specification*) |
11 "solveFor z", "solutions L"]; |
20 (*equality, bound variable, identifier for solution*) |
|
21 |
|
22 val (dI',pI',mI') = |
12 val (dI',pI',mI') = |
23 ("Isac", |
13 ("Isac", |
24 ["abcFormula","degree_2","polynomial","univariate","equation"], |
14 ["abcFormula","degree_2","polynomial","univariate","equation"], |
25 ["no_met"]); |
15 ["no_met"]); |
26 |
|
27 *} |
16 *} |
28 |
17 |
29 text{*Possible Check if the equation matches the designated Method*} |
18 text{*Step through the Calculation*} |
30 |
|
31 ML {* |
|
32 match_pbl expr (get_pbt |
|
33 ["abcFormula","degree_2","polynomial","univariate","equation"]); |
|
34 *} |
|
35 |
|
36 text{*Step throuh the Calculation Tree*} |
|
37 |
19 |
38 ML {* |
20 ML {* |
39 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(expr, (dI',pI',mI'))]; |
21 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(expr, (dI',pI',mI'))]; |
40 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
22 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
41 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
23 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |