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