(*

 cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/course/

 /usr/local/Isabelle/bin/isabelle jedit -l Isac T2_Rewriting.thy &

 *)

 theory T3_MathEngine imports Isac begin

 chapter {* ISACs mathematics engine *}

 text {* This is a brief introduction to ISACs mathematics engine (ME). The

   goal of the introduction is enabling authors to test new developments of

   knowledge.

   As an example we continue the previous one on rewriting. The previous

   chapter raised questions about didactics and stated open developments problems.

   So, let us assume, some additional knowledge has been added to solve some of

   the open problems with '-' in simplification.

   Now we want to test, if 

       Vereinfache (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)

   really simplifies to

       3 - 2 * e + 2 * f + 2 * g

 *}

 section {* Knowledge for automated solving the example problem *}

 text {* ISAC wants to show possibilities for next steps, if learners get stuck.

   So, at least ISAC needs to be able to solve a problem automatically. For this

   purpose, ISAC requires three kinds of knowledge, (1) rules to apply (2) a 

   specification of the problem and (3) a method solving the problem.

   ad (1) The rules required for simplifying our example are found in theory

   ~~/Tools/isac/Knowledge/PolyMinus.thy. 

   ad (2) The problem of 'vereinfachen' is one of many other problems;

   the function 'get_pbt' gets the one we need:  

 *}

 ML {* show_ptyps ();

   get_pbt ["plus_minus", "polynom", "vereinfachen"];

 *}

 text {* However, 'get_pbt' shows an internal format; for a human readable format

   see http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html

   Note, that in this tree you first lookup "vereinfachen", then "polynom" and

   finally "plus_minus", the same as you see from 'show_ptyps ()'.

   However, we call the problem "plus_minus - polynom - vereinfachen".

   ad (3) The method solving the problem is also one of many others; the function

   'get_met' gets the one we need:

 *}

 ML {*

 show_mets ();

 get_met ["simplification","for_polynomials","with_minus"];

 *}

 text {* For a readable format of the method look up the definition in

   ~~/Tools/isac/Knowledge/PolyMinus.thy or 

   http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html

   The path to the method "simplification - for_polynomials - with_minus" is

   not reversed like the one to the problem, because the structure of the

   methods' container is not yet clarified.

 *}

 section {* Testing the example problem *}

 text {* Now we have all the knowledge ISAC requires for guiding the learner:

   (1) the theory "PolyMinus", (2) the problem ["plus_minus","polynom","vereinfachen"]

   and (3) the method ["simplification","for_polynomials","with_minus"].

   So we can start testing the example by calling 'CalcTreeTEST':

 *}

 ML {* val (p,_,f,nxt,_,pt) = 

       CalcTreeTEST 

         [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",

            "normalform N"],

 	          ("PolyMinus",["plus_minus","polynom","vereinfachen"],

 	           ["simplification","for_polynomials","with_minus"]))];

 *}

 text {* The function 'CalcTreeTEST' returns the following values:

   p:    the position in the calculation

   f:    the formula produced by this step of calculation.

         In this case 'f' is an incomplete model of the problem.

   nxt:  the tactic suggested to do the next step

   pt:   the _whole_ calculation in an internal format; the calculation 'pt'

         will be fed back into the mathematics engine, the function 'me' below,

         'me' is purely functional, no further data remains in the memory.

         'me' returns the same data as 'CalcTreeTEST'.

   The first tactic suggested by ISAC is 'Model_Problem', we use this tactic

   (stored in 'nxt') and enter the 'specification phase'.

 *}

 section {* Specifying the example problem *}

 text {* Often the specification phase is hidden from the learner by the dialog 

   module; here we see the mathematics engine at work directly.

   Only note the tactic 'nxt' suggested for the next step:

 *}

 ML {* val c = [(*this is an unimportant, but necessary detail*)];

   val (p,_,f,nxt,_,pt) = me nxt p c pt;

   val (p,_,f,nxt,_,pt) = me nxt p c pt;

 *}

 text{* The tactics 'Add_Given' and 'Add_Find' inserted the respective values

   into the model. Then 'Specify_Theory' determines the knowledge item no.1 from

   above, 'Specify_Problem' item 2 and 'Specify_Method' item 3.

 *}

 ML {* 

   val (p,_,f,nxt,_,pt) = me nxt p c pt;

   val (p,_,f,nxt,_,pt) = me nxt p c pt;

   val (p,_,f,nxt,_,pt) = me nxt p c pt;

   val (p,_,f,nxt,_,pt) = me nxt p c pt;

 *}

 text{* The final suggestion 'Apply_Method' completes the specification phase

   and starts the 'solving phase', which is guided by the method determined.

 *}

 section {* Solving the example problem *}

 text {* Now let us observe, how the method ["simplification","for_polynomials",

   "with_minus"] guides through simplification by rewriting. For that purpose

   we increase the 'print_depth' (with the disadvantage of extending the output)

   and print out the results by use of 'f2str'.

   Please, note only 'nxt' close to the beginning of the output and the resulting

   term at the end:

 *}

 ML {* print_depth 40; *}

 ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}

 ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}

 ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}

 ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}

 ML {* print_depth 3; *}

 text{* And, please, note that the result of applying the 'nxt' ruleset is to be

   found in the output of the next step !

 *}

 section {* Completing the example problem *}

 text {* The 'nxt' tactic suggested above was 'Check_Postcond'. That means, a

   perfect mathematics engine has to prove the socalled 'postcondition' of the

   current problem; this is not yet implemented in the current version of ISAC.

 *}

 ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}

 text{* Now the mathematics engine has found the end of the calculation.

   With 'show_pt' the calculation can be inspected (in a more or less readable

   format) by clicking the checkbox <Tracing> on top of the <Output> window:

 *}

 ML {* show_pt pt *}

 section {* Test further examples *}

 text{* Now it is easy to do further examples: just put another calculation into

   the formalisation:

 *}

 ML {* val (p,_,f,nxt,_,pt) = 

       CalcTreeTEST 

         [(["Term (1 + 2 + 3)", "normalform N"],

 	          ("PolyMinus",["plus_minus","polynom","vereinfachen"],

 	           ["simplification","for_polynomials","with_minus"]))];

 *}

 ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; *}

 text{* and repeat this ML line as often as required ...*}

 end