1.1 --- a/src/Tools/isac/Test_Isac.thy	Mon Dec 27 10:38:49 2010 +0100
     1.2 +++ b/src/Tools/isac/Test_Isac.thy	Wed Dec 29 20:07:52 2010 +0100
     1.3 @@ -127,8 +127,8 @@
     1.4  theory "Isac"
     1.5  *}
     1.6  use "../../../test/Tools/isac/Knowledge/isac.sml"; (**)
     1.7 +
     1.8  ML {*print_depth 3*}
     1.9 -
    1.10  ML {*111*}
    1.11  
    1.12  (*
    1.13 @@ -141,7 +141,8 @@
    1.14  *** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
    1.15  
    1.16  use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
    1.17 -*)use "../../../test/Pure/library.sml" (**)
    1.18 +*)
    1.19 +use "../../../test/Pure/library.sml" (**)
    1.20  use_thy "../../../test/Pure/General/Basics"
    1.21  
    1.22  use_thy "../../../test/Pure/Isar/Test_Parse_Term"

     2.1 --- a/test/Tools/isac/ADDTESTS/course/T2_Rewriting.thy	Mon Dec 27 10:38:49 2010 +0100
     2.2 +++ b/test/Tools/isac/ADDTESTS/course/T2_Rewriting.thy	Wed Dec 29 20:07:52 2010 +0100
     2.3 @@ -186,7 +186,7 @@
     2.4  subsection {* What already works *}
     2.5  ML {*
     2.6  val t2 = (term_of o the o (parse thy)) 
     2.7 -  "- r - 2 * s - 3 * t + 5 + 4 * r + 8 * s - 5 * t - 2";
     2.8 +  "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
     2.9  val SOME (t, _) = rewrite_set_ thy true rls_p_33 t2; term2str t;
    2.10  *}
    2.11  text {* Try your own examples ! *}

     3.1 --- a/test/Tools/isac/ADDTESTS/course/T3_MathEngine.thy	Mon Dec 27 10:38:49 2010 +0100
     3.2 +++ b/test/Tools/isac/ADDTESTS/course/T3_MathEngine.thy	Wed Dec 29 20:07:52 2010 +0100
     3.3 @@ -8,7 +8,104 @@
     3.4  chapter {* ISACs mathematics engine *}
     3.5  text {* This is a brief introduction to ISACs mathematics engine (ME). The
     3.6    goal of the introduction is enabling authors to test new developments of
     3.7 -  knowledge 
     3.8 +  knowledge.
     3.9 +  As an example we continue the previous one on rewriting. The previous
    3.10 +  chapter raised questions about didactics and stated open developments problems.
    3.11 +  So, let us assume, some additional knowledge has been added to solve some of
    3.12 +  the open problems with '-' in simplification.
    3.13 +  Now we want to test, if 
    3.14 +      Vereinfache (- r - 2 * s - 3 * t + 5 + 4 * r + 8 * s - 5 * t - 2)
    3.15 +  really simplifies to
    3.16 +      3 + 3*r + 6*s - 8*t
    3.17  *}
    3.18  
    3.19 +section {* Knowledge for automated solving the example problem *}
    3.20 +text {* ISAC wants to show possibilities for next steps, if learners get stuck.
    3.21 +  So, at least ISAC needs to be able to solve a problem automatically. For this
    3.22 +  purpose, ISAC requires three kinds of knowledge, (1) rules to apply (2) a 
    3.23 +  specification of the problem and (3) a method solving the problem.
    3.24 +
    3.25 +  ad (1) The rules required for simplifying our example are found in theory
    3.26 +  ~~/Tools/isac/Knowledge/PolyMinus.thy. 
    3.27 +
    3.28 +  ad (2) The specification of the problem 'vereinfachen' is one of many others;
    3.29 +  the function 'get_pbt' gets the one we need:  
    3.30 +*}
    3.31 +ML {* show_ptyps ();
    3.32 +  get_pbt ["plus_minus", "polynom", "vereinfachen"];
    3.33 +*}
    3.34 +text {* However, 'get_pbt' shows an internal format; for a human readable format
    3.35 +  see http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html.
    3.36 +  Note, that in this tree you first lookup "vereinfachen", then "polynom" and
    3.37 +  finally "plus_minus", the same as you see from 'show_ptyps ()'.
    3.38 +  However, we call the problem "plus_minus - polynom - vereinfachen".
    3.39 +
    3.40 +  ad (3) The method solving the problem is also one of many others; the function
    3.41 +  'get_met' gets the one we need:
    3.42 +*}
    3.43 +ML {*
    3.44 +show_mets ();
    3.45 +get_met ["simplification","for_polynomials","with_minus"];
    3.46 +*}
    3.47 +text {* For a readable format of the method look up the definition in
    3.48 +  ~~/Tools/isac/Knowledge/PolyMinus.thy or 
    3.49 +  http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html.
    3.50 +  The path to the method "simplification - for_polynomials - with_minus" is
    3.51 +  not reversed like the one to the problem, because the structure of the
    3.52 +  methods' container is not yet clarified.
    3.53 +*}
    3.54 +
    3.55 +section {* Testing the example problem *}
    3.56 +text {* Now we have all the knowledge ISAC requires for guiding the learner:
    3.57 +  (1) the theory "PolyMinus", (2) the problem ["plus_minus","polynom","vereinfachen"]
    3.58 +  and (3) the method ["simplification","for_polynomials","with_minus"].
    3.59 +
    3.60 +  So we can start testing the example by calling 'CalcTreeTEST':
    3.61 +*}
    3.62 +ML {* val (p,_,f,nxt,_,pt) = 
    3.63 +      CalcTreeTEST 
    3.64 +        [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
    3.65 +           "normalform N"],
    3.66 +	          ("PolyMinus",["plus_minus","polynom","vereinfachen"],
    3.67 +	           ["simplification","for_polynomials","with_minus"]))];
    3.68 +*}
    3.69 +text {* The function 'CalcTreeTEST' returns the following values:
    3.70 +  p:    the position in the calculation
    3.71 +  f:    the formula produced by this step of calculation.
    3.72 +        In this case 'f' is an incomplete model of the problem, so we skip it.
    3.73 +  nxt:  the tactic suggested to do the next step
    3.74 +  pt:   the _whole_ calculation in an internal format; the calculation 'pt'
    3.75 +        will be fed back into the mathematics engine, the function 'me' below,
    3.76 +        'me' is purely functional, no further data remains in the memory.
    3.77 +        'me' returns the same data as 'CalcTreeTEST'.
    3.78 +
    3.79 +  The first tactic suggested by ISAC is 'Model_Problem', we use this tactic
    3.80 +  (stored in 'nxt') and enter the specification phase.
    3.81 +*}
    3.82 +
    3.83 +section {* Specifying the example problem *}
    3.84 +text {* Often the specification phase is hidden from the learner by the dialog 
    3.85 +  module; here we see the mathematics engine at work directly.
    3.86 +*}
    3.87 +ML {* val c = [];
    3.88 +  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    3.89 +*}
    3.90 +
    3.91 +
    3.92 +
    3.93 +
    3.94 +
    3.95 +section {* Solving the example problem *}
    3.96 +text {*
    3.97 +*}
    3.98 +ML {*  val (p,_,f,nxt,_,pt) = me nxt p c pt; *}
    3.99 +
   3.100 +section {* Completing the example problem *}
   3.101 +text {*
   3.102 +*}
   3.103 +ML {*
   3.104 +*}
   3.105 +
   3.106 +
   3.107 +
   3.108  end

     4.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon Dec 27 10:38:49 2010 +0100
     4.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Wed Dec 29 20:07:52 2010 +0100
     4.3 @@ -6,7 +6,6 @@
     4.4  use"../smltest/IsacKnowledge/polyminus.sml";
     4.5  use"polyminus.sml";
     4.6  *)
     4.7 -(*========== inhibit exn ?======================================================
     4.8  "--------------------------------------------------------";
     4.9  "--------------------------------------------------------";
    4.10  "table of contents --------------------------------------";
    4.11 @@ -17,6 +16,7 @@
    4.12  "----------- build fasse_zusammen -----------------------";
    4.13  "----------- build verschoenere -------------------------";
    4.14  "----------- met simplification for_polynomials with_minu";
    4.15 +"----------- me simplification.for_polynomials.with_minus";
    4.16  "----------- pbl polynom vereinfachen p.33 --------------";
    4.17  "----------- met probe fuer_polynom ---------------------";
    4.18  "----------- pbl polynom probe --------------------------";
    4.19 @@ -30,12 +30,13 @@
    4.20  "--------------------------------------------------------";
    4.21  "--------------------------------------------------------";
    4.22  
    4.23 -val thy = PolyMinus.thy;
    4.24 +val thy = theory "PolyMinus";
    4.25  
    4.26  "----------- fun eval_ist_monom ----------------------------------";
    4.27  "----------- fun eval_ist_monom ----------------------------------";
    4.28  "----------- fun eval_ist_monom ----------------------------------";
    4.29  ist_monom (str2term "12");
    4.30 +(*========== inhibit exn =======================================================
    4.31  case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of
    4.32      SOME ("12 ist_monom = True", _) => ()
    4.33    | _ => error "polyminus.sml: 12 ist_monom = True";
    4.34 @@ -64,6 +65,7 @@
    4.35      SOME ("3 * a * b ist_monom = True", _) => ()
    4.36    | _ => error "polyminus.sml: 3*a*b ist_monom = True";
    4.37  
    4.38 +============ inhibit exn =====================================================*)
    4.39  
    4.40  "----------- watch order_add_mult  -------------------------------";
    4.41  "----------- watch order_add_mult  -------------------------------";
    4.42 @@ -78,16 +80,16 @@
    4.43  trace_rewrite:=false;
    4.44  
    4.45  "----- the same stepwise...";
    4.46 -val od = ord_make_polynomial true Poly.thy;
    4.47 +val od = ord_make_polynomial true (theory "Poly");
    4.48  val t = str2term "((a + d) + c) + b";
    4.49  "((a + d) + c) + b"; 
    4.50 -val SOME (t,_) = rewrite_ thy od e_rls true add_commute t; term2str t;
    4.51 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t;
    4.52  "b + ((a + d) + c)";
    4.53 -val SOME (t,_) = rewrite_ thy od e_rls true add_commute t; term2str t;
    4.54 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t;
    4.55  "b + (c + (a + d))";
    4.56 -val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t;
    4.57 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    4.58  "b + (a + (c + d))";
    4.59 -val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t;
    4.60 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    4.61  "a + (b + (c + d))";
    4.62  if term2str t = "a + (b + (c + d))" then ()
    4.63  else error "polyminus.sml 2 watch order_add_mult";
    4.64 @@ -95,11 +97,11 @@
    4.65  "----- if parentheses are right, left_commute is (almost) sufficient...";
    4.66  val t = str2term "a + (d + (c + b))";
    4.67  "a + (d + (c + b))";
    4.68 -val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t;
    4.69 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    4.70  "a + (c + (d + b))";
    4.71 -val SOME (t,_) = rewrite_ thy od e_rls true add_commute t;term2str t;
    4.72 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t;term2str t;
    4.73  "a + (c + (b + d))";
    4.74 -val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t;
    4.75 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    4.76  "a + (b + (c + d))";
    4.77  
    4.78  "----- but we do not want the parentheses at right; thus: cond.rew.";
    4.79 @@ -110,10 +112,10 @@
    4.80  else error "polyminus.sml: order_add_mult changed";
    4.81  
    4.82  "----- here we see rew_sub going into subterm with ord.rew....";
    4.83 -val od = ord_make_polynomial false Poly.thy;
    4.84 +val od = ord_make_polynomial false (theory "Poly");
    4.85  val t = str2term "b + a + c + d";
    4.86 -val SOME (t,_) = rewrite_ thy od e_rls false add_commute t; term2str t;
    4.87 -val SOME (t,_) = rewrite_ thy od e_rls false add_commute t; term2str t;
    4.88 +val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t;
    4.89 +val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t;
    4.90  (*@@@ rew_sub gosub: t = d + (b + a + c)
    4.91    @@@ rew_sub begin: t = b + a + c*)
    4.92  
    4.93 @@ -134,6 +136,7 @@
    4.94      SOME ("12 kleiner 9 = False", _) => ()
    4.95    | _ => error "polyminus.sml: 12 kleiner 9 = False";
    4.96  *)
    4.97 +(*========== inhibit exn =======================================================
    4.98  case eval_kleiner 0 0 (str2term "a kleiner b") 0 of
    4.99      SOME ("a kleiner b = True", _) => ()
   4.100    | _ => error "polyminus.sml: a kleiner b = True";
   4.101 @@ -158,6 +161,7 @@
   4.102      SOME ("3 * a * b kleiner c = True", _) => ()
   4.103    | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
   4.104  
   4.105 +============ inhibit exn =====================================================*)
   4.106  
   4.107  
   4.108  "----- compare tausche_plus with real_num_collect";
   4.109 @@ -165,13 +169,13 @@
   4.110  
   4.111  val erls = erls_ordne_alphabetisch;
   4.112  val t = str2term "b + a";
   4.113 -val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t;
   4.114 +val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; term2str t;
   4.115  if term2str t = "a + b" then ()
   4.116  else error "polyminus.sml: ordne_alphabetisch1 b + a";
   4.117  
   4.118  val erls = Atools_erls;
   4.119  val t = str2term "2*a + 3*a";
   4.120 -val SOME (t,_) = rewrite_ thy od erls false real_num_collect t; term2str t;
   4.121 +val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; term2str t;
   4.122  
   4.123  "----- test rewrite_, rewrite_set_";
   4.124  trace_rewrite:=true;
   4.125 @@ -193,7 +197,7 @@
   4.126  
   4.127  "----- rewrite goes into subterms";
   4.128  val t = str2term "a + c + b + d";
   4.129 -val SOME (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t;
   4.130 +val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; term2str t;
   4.131  if term2str t = "a + b + c + d" then ()
   4.132  else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
   4.133  
   4.134 @@ -204,7 +208,7 @@
   4.135  
   4.136  "----- here we see rew_sub going into subterm with cond.rew....";
   4.137  val t = str2term "b + a + c + d";
   4.138 -val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t;
   4.139 +val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; term2str t;
   4.140  if term2str t = "a + b + c + d" then ()
   4.141  else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
   4.142  
   4.143 @@ -239,14 +243,28 @@
   4.144  "----------- met simplification for_polynomials with_minus -------";
   4.145  "----------- met simplification for_polynomials with_minus -------";
   4.146  val str = 
   4.147 -"Script SimplifyScript (t_::real) =                \
   4.148 +"Script SimplifyScript (t_t::real) =                \
   4.149  \  (((Try (Rewrite_Set ordne_alphabetisch False)) @@     \
   4.150  \    (Try (Rewrite_Set fasse_zusammen False)) @@     \
   4.151 -\    (Try (Rewrite_Set verschoenere False))) t_)"
   4.152 +\    (Try (Rewrite_Set verschoenere False))) t_t)"
   4.153  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
   4.154  atomty sc;
   4.155  
   4.156 +"----------- me simplification.for_polynomials.with_minus";
   4.157 +"----------- me simplification.for_polynomials.with_minus";
   4.158 +"----------- me simplification.for_polynomials.with_minus";
   4.159 +val c = [];
   4.160 +val (p,_,f,nxt,_,pt) = 
   4.161 +      CalcTreeTEST 
   4.162 +        [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
   4.163 +           "normalform N"],
   4.164 +	          ("PolyMinus",["plus_minus","polynom","vereinfachen"],
   4.165 +	           ["simplification","for_polynomials","with_minus"]))];
   4.166 +(*========== inhibit exn =======================================================
   4.167 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
   4.168 +============ inhibit exn =====================================================*)
   4.169  
   4.170 +(*========== inhibit exn ?======================================================
   4.171  "----------- pbl polynom vereinfachen p.33 -----------------------";
   4.172  "----------- pbl polynom vereinfachen p.33 -----------------------";
   4.173  "----------- pbl polynom vereinfachen p.33 -----------------------";
   4.174 @@ -530,8 +548,7 @@
   4.175  "----------- pbl binom polynom vereinfachen: cube ----------------";
   4.176  "----------- pbl binom polynom vereinfachen: cube ----------------";
   4.177  states:=[];
   4.178 -CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))",
   4.179 -	    "normalform N"],
   4.180 +CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"],
   4.181  	   ("PolyMinus",["binom_klammer","polynom","vereinfachen"],
   4.182  	    ["simplification","for_polynomials","with_parentheses_mult"]))];
   4.183  moveActiveRoot 1;
   4.184 @@ -604,8 +621,6 @@
   4.185  then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
   4.186  show_types := false;
   4.187  
   4.188 -(*========== inhibit exn =======================================================
   4.189 -============ inhibit exn =====================================================*)
   4.190 -
   4.191  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
   4.192  -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
   4.193 +

     5.1 --- a/test/Tools/isac/Knowledge/rational.sml	Mon Dec 27 10:38:49 2010 +0100
     5.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Wed Dec 29 20:07:52 2010 +0100
     5.3 @@ -3,6 +3,9 @@
     5.4     Copyright (c) Stefan Karnel 2002
     5.5     Use is subject to license terms.
     5.6  
     5.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
     5.8 +        10        20        30        40        50        60        70        80
     5.9 +
    5.10  LEGEND WN070906
    5.11     nonterm.SK   marks non-terminating examples
    5.12     ord.SK       PARTIALLY marks crucial ordering examples
    5.13 @@ -2079,3 +2082,6 @@
    5.14  
    5.15  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    5.16  -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    5.17 +
    5.18 +
    5.19 +