neuper@38079
|
1 |
(*
|
neuper@38079
|
2 |
cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/course/
|
neuper@38079
|
3 |
/usr/local/Isabelle/bin/isabelle jedit -l Isac T2_Rewriting.thy &
|
neuper@38079
|
4 |
*)
|
neuper@38079
|
5 |
|
neuper@38079
|
6 |
theory T3_MathEngine imports Isac begin
|
neuper@38079
|
7 |
|
neuper@38079
|
8 |
chapter {* ISACs mathematics engine *}
|
neuper@38079
|
9 |
text {* This is a brief introduction to ISACs mathematics engine (ME). The
|
neuper@38079
|
10 |
goal of the introduction is enabling authors to test new developments of
|
neuper@38080
|
11 |
knowledge.
|
neuper@38080
|
12 |
As an example we continue the previous one on rewriting. The previous
|
neuper@38080
|
13 |
chapter raised questions about didactics and stated open developments problems.
|
neuper@38080
|
14 |
So, let us assume, some additional knowledge has been added to solve some of
|
neuper@38080
|
15 |
the open problems with '-' in simplification.
|
neuper@38080
|
16 |
Now we want to test, if
|
neuper@38086
|
17 |
Vereinfache (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)
|
neuper@38080
|
18 |
really simplifies to
|
neuper@38086
|
19 |
3 - 2 * e + 2 * f + 2 * g
|
neuper@38079
|
20 |
*}
|
neuper@38079
|
21 |
|
neuper@38080
|
22 |
section {* Knowledge for automated solving the example problem *}
|
neuper@38080
|
23 |
text {* ISAC wants to show possibilities for next steps, if learners get stuck.
|
neuper@38080
|
24 |
So, at least ISAC needs to be able to solve a problem automatically. For this
|
neuper@38080
|
25 |
purpose, ISAC requires three kinds of knowledge, (1) rules to apply (2) a
|
neuper@38080
|
26 |
specification of the problem and (3) a method solving the problem.
|
neuper@38080
|
27 |
|
neuper@38080
|
28 |
ad (1) The rules required for simplifying our example are found in theory
|
neuper@38080
|
29 |
~~/Tools/isac/Knowledge/PolyMinus.thy.
|
neuper@38080
|
30 |
|
neuper@38086
|
31 |
ad (2) The problem of 'vereinfachen' is one of many other problems;
|
neuper@38080
|
32 |
the function 'get_pbt' gets the one we need:
|
neuper@38080
|
33 |
*}
|
neuper@38080
|
34 |
ML {* show_ptyps ();
|
neuper@38080
|
35 |
get_pbt ["plus_minus", "polynom", "vereinfachen"];
|
neuper@38080
|
36 |
*}
|
neuper@38080
|
37 |
text {* However, 'get_pbt' shows an internal format; for a human readable format
|
neuper@38087
|
38 |
see http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html
|
neuper@38080
|
39 |
Note, that in this tree you first lookup "vereinfachen", then "polynom" and
|
neuper@38080
|
40 |
finally "plus_minus", the same as you see from 'show_ptyps ()'.
|
neuper@38080
|
41 |
However, we call the problem "plus_minus - polynom - vereinfachen".
|
neuper@38080
|
42 |
|
neuper@38080
|
43 |
ad (3) The method solving the problem is also one of many others; the function
|
neuper@38080
|
44 |
'get_met' gets the one we need:
|
neuper@38080
|
45 |
*}
|
neuper@38080
|
46 |
ML {*
|
neuper@38080
|
47 |
show_mets ();
|
neuper@38080
|
48 |
get_met ["simplification","for_polynomials","with_minus"];
|
neuper@38080
|
49 |
*}
|
neuper@38080
|
50 |
text {* For a readable format of the method look up the definition in
|
neuper@38080
|
51 |
~~/Tools/isac/Knowledge/PolyMinus.thy or
|
neuper@38087
|
52 |
http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html
|
neuper@38080
|
53 |
The path to the method "simplification - for_polynomials - with_minus" is
|
neuper@38080
|
54 |
not reversed like the one to the problem, because the structure of the
|
neuper@38080
|
55 |
methods' container is not yet clarified.
|
neuper@38080
|
56 |
*}
|
neuper@38080
|
57 |
|
neuper@38080
|
58 |
section {* Testing the example problem *}
|
neuper@38080
|
59 |
text {* Now we have all the knowledge ISAC requires for guiding the learner:
|
neuper@38080
|
60 |
(1) the theory "PolyMinus", (2) the problem ["plus_minus","polynom","vereinfachen"]
|
neuper@38080
|
61 |
and (3) the method ["simplification","for_polynomials","with_minus"].
|
neuper@38080
|
62 |
|
neuper@38080
|
63 |
So we can start testing the example by calling 'CalcTreeTEST':
|
neuper@38080
|
64 |
*}
|
neuper@38080
|
65 |
ML {* val (p,_,f,nxt,_,pt) =
|
neuper@38080
|
66 |
CalcTreeTEST
|
neuper@38083
|
67 |
[(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
|
neuper@38080
|
68 |
"normalform N"],
|
neuper@38080
|
69 |
("PolyMinus",["plus_minus","polynom","vereinfachen"],
|
neuper@38080
|
70 |
["simplification","for_polynomials","with_minus"]))];
|
neuper@38080
|
71 |
*}
|
neuper@38080
|
72 |
text {* The function 'CalcTreeTEST' returns the following values:
|
neuper@38080
|
73 |
p: the position in the calculation
|
neuper@38080
|
74 |
f: the formula produced by this step of calculation.
|
neuper@38086
|
75 |
In this case 'f' is an incomplete model of the problem.
|
neuper@38080
|
76 |
nxt: the tactic suggested to do the next step
|
neuper@38080
|
77 |
pt: the _whole_ calculation in an internal format; the calculation 'pt'
|
neuper@38080
|
78 |
will be fed back into the mathematics engine, the function 'me' below,
|
neuper@38080
|
79 |
'me' is purely functional, no further data remains in the memory.
|
neuper@38080
|
80 |
'me' returns the same data as 'CalcTreeTEST'.
|
neuper@38080
|
81 |
|
neuper@38080
|
82 |
The first tactic suggested by ISAC is 'Model_Problem', we use this tactic
|
neuper@38086
|
83 |
(stored in 'nxt') and enter the 'specification phase'.
|
neuper@38080
|
84 |
*}
|
neuper@38080
|
85 |
|
neuper@38080
|
86 |
section {* Specifying the example problem *}
|
neuper@38080
|
87 |
text {* Often the specification phase is hidden from the learner by the dialog
|
neuper@38080
|
88 |
module; here we see the mathematics engine at work directly.
|
neuper@38086
|
89 |
|
neuper@38086
|
90 |
Only note the tactic 'nxt' suggested for the next step:
|
neuper@38080
|
91 |
*}
|
neuper@38086
|
92 |
ML {* val c = [(*this is an unimportant, but necessary detail*)];
|
neuper@38086
|
93 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@38080
|
94 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@38080
|
95 |
*}
|
neuper@38086
|
96 |
text{* The tactics 'Add_Given' and 'Add_Find' inserted the respective values
|
neuper@38086
|
97 |
into the model. Then 'Specify_Theory' determines the knowledge item no.1 from
|
neuper@38086
|
98 |
above, 'Specify_Problem' item 2 and 'Specify_Method' item 3.
|
neuper@38086
|
99 |
*}
|
neuper@38086
|
100 |
ML {*
|
neuper@38086
|
101 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@38086
|
102 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@38086
|
103 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@38086
|
104 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@38086
|
105 |
*}
|
neuper@38086
|
106 |
text{* The final suggestion 'Apply_Method' completes the specification phase
|
neuper@38086
|
107 |
and starts the 'solving phase', which is guided by the method determined.
|
neuper@38086
|
108 |
*}
|
neuper@38080
|
109 |
|
neuper@38080
|
110 |
section {* Solving the example problem *}
|
neuper@38086
|
111 |
text {* Now let us observe, how the method ["simplification","for_polynomials",
|
neuper@38086
|
112 |
"with_minus"] guides through simplification by rewriting. For that purpose
|
neuper@38086
|
113 |
we increase the 'print_depth' (with the disadvantage of extending the output)
|
neuper@38086
|
114 |
and print out the results by use of 'f2str'.
|
neuper@38086
|
115 |
Please, note only 'nxt' close to the beginning of the output and the resulting
|
neuper@38086
|
116 |
term at the end:
|
neuper@38080
|
117 |
*}
|
neuper@38086
|
118 |
ML {* print_depth 40; *}
|
neuper@38086
|
119 |
ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
|
neuper@38086
|
120 |
ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
|
neuper@38086
|
121 |
ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
|
neuper@38086
|
122 |
ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
|
neuper@52101
|
123 |
ML {* print_depth 3; *}
|
neuper@38086
|
124 |
text{* And, please, note that the result of applying the 'nxt' ruleset is to be
|
neuper@38086
|
125 |
found in the output of the next step !
|
neuper@38086
|
126 |
*}
|
neuper@38080
|
127 |
|
neuper@38080
|
128 |
section {* Completing the example problem *}
|
neuper@38086
|
129 |
text {* The 'nxt' tactic suggested above was 'Check_Postcond'. That means, a
|
neuper@38086
|
130 |
perfect mathematics engine has to prove the socalled 'postcondition' of the
|
neuper@38086
|
131 |
current problem; this is not yet implemented in the current version of ISAC.
|
neuper@38080
|
132 |
*}
|
neuper@38086
|
133 |
ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
|
neuper@38086
|
134 |
text{* Now the mathematics engine has found the end of the calculation.
|
neuper@38086
|
135 |
|
neuper@38086
|
136 |
With 'show_pt' the calculation can be inspected (in a more or less readable
|
neuper@38086
|
137 |
format) by clicking the checkbox <Tracing> on top of the <Output> window:
|
neuper@38080
|
138 |
*}
|
neuper@38086
|
139 |
ML {* show_pt pt *}
|
neuper@38080
|
140 |
|
neuper@38087
|
141 |
|
neuper@38087
|
142 |
section {* Test further examples *}
|
neuper@38087
|
143 |
text{* Now it is easy to do further examples: just put another calculation into
|
neuper@38087
|
144 |
the formalisation:
|
neuper@38087
|
145 |
*}
|
neuper@38087
|
146 |
ML {* val (p,_,f,nxt,_,pt) =
|
neuper@38087
|
147 |
CalcTreeTEST
|
neuper@38087
|
148 |
[(["Term (1 + 2 + 3)", "normalform N"],
|
neuper@38087
|
149 |
("PolyMinus",["plus_minus","polynom","vereinfachen"],
|
neuper@38087
|
150 |
["simplification","for_polynomials","with_minus"]))];
|
neuper@38087
|
151 |
*}
|
neuper@38087
|
152 |
ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; *}
|
neuper@38087
|
153 |
text{* and repeat this ML line as often as required ...*}
|
neuper@38087
|
154 |
|
neuper@38079
|
155 |
end
|