# HG changeset patch # User Walther Neuper # Date 1293649672 -3600 # Node ID 53ee777684caa8f777a1583b63d4ed64e25bb1a1 # Parent 431344850e4082a9d705848fec040c3abb575543 intermed. in course/T3_MathEngine.thy two problems encountered (1) isabelle jedit does NOT accept syntax in Test_Isac.thy, which is accepted by isabelle emacs Thus unnecessarily edited test/../rational.sml (2) There is an error at Model_Problem in me poly_minus. This will be fixed before continuing T3_MathEngine.thy Tests are running again under isabelle emacs. diff -r 431344850e40 -r 53ee777684ca src/Tools/isac/Test_Isac.thy --- a/src/Tools/isac/Test_Isac.thy Mon Dec 27 10:38:49 2010 +0100 +++ b/src/Tools/isac/Test_Isac.thy Wed Dec 29 20:07:52 2010 +0100 @@ -127,8 +127,8 @@ theory "Isac" *} use "../../../test/Tools/isac/Knowledge/isac.sml"; (**) + ML {*print_depth 3*} - ML {*111*} (* @@ -141,7 +141,8 @@ *** Theory loader: the error(s) above occurred while examining theory "Foo_Language" use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test" -*)use "../../../test/Pure/library.sml" (**) +*) +use "../../../test/Pure/library.sml" (**) use_thy "../../../test/Pure/General/Basics" use_thy "../../../test/Pure/Isar/Test_Parse_Term" diff -r 431344850e40 -r 53ee777684ca test/Tools/isac/ADDTESTS/course/T2_Rewriting.thy --- a/test/Tools/isac/ADDTESTS/course/T2_Rewriting.thy Mon Dec 27 10:38:49 2010 +0100 +++ b/test/Tools/isac/ADDTESTS/course/T2_Rewriting.thy Wed Dec 29 20:07:52 2010 +0100 @@ -186,7 +186,7 @@ subsection {* What already works *} ML {* val t2 = (term_of o the o (parse thy)) - "- r - 2 * s - 3 * t + 5 + 4 * r + 8 * s - 5 * t - 2"; + "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; val SOME (t, _) = rewrite_set_ thy true rls_p_33 t2; term2str t; *} text {* Try your own examples ! *} diff -r 431344850e40 -r 53ee777684ca test/Tools/isac/ADDTESTS/course/T3_MathEngine.thy --- a/test/Tools/isac/ADDTESTS/course/T3_MathEngine.thy Mon Dec 27 10:38:49 2010 +0100 +++ b/test/Tools/isac/ADDTESTS/course/T3_MathEngine.thy Wed Dec 29 20:07:52 2010 +0100 @@ -8,7 +8,104 @@ 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 + 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 (- r - 2 * s - 3 * t + 5 + 4 * r + 8 * s - 5 * t - 2) + really simplifies to + 3 + 3*r + 6*s - 8*t *} +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 specification of the problem 'vereinfachen' is one of many others; + 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, so we skip it. + 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. +*} +ML {* val c = []; + val (p,_,f,nxt,_,pt) = me nxt p c pt; +*} + + + + + +section {* Solving the example problem *} +text {* +*} +ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; *} + +section {* Completing the example problem *} +text {* +*} +ML {* +*} + + + end diff -r 431344850e40 -r 53ee777684ca test/Tools/isac/Knowledge/polyminus.sml --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Dec 27 10:38:49 2010 +0100 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Dec 29 20:07:52 2010 +0100 @@ -6,7 +6,6 @@ use"../smltest/IsacKnowledge/polyminus.sml"; use"polyminus.sml"; *) -(*========== inhibit exn ?====================================================== "--------------------------------------------------------"; "--------------------------------------------------------"; "table of contents --------------------------------------"; @@ -17,6 +16,7 @@ "----------- build fasse_zusammen -----------------------"; "----------- build verschoenere -------------------------"; "----------- met simplification for_polynomials with_minu"; +"----------- me simplification.for_polynomials.with_minus"; "----------- pbl polynom vereinfachen p.33 --------------"; "----------- met probe fuer_polynom ---------------------"; "----------- pbl polynom probe --------------------------"; @@ -30,12 +30,13 @@ "--------------------------------------------------------"; "--------------------------------------------------------"; -val thy = PolyMinus.thy; +val thy = theory "PolyMinus"; "----------- fun eval_ist_monom ----------------------------------"; "----------- fun eval_ist_monom ----------------------------------"; "----------- fun eval_ist_monom ----------------------------------"; ist_monom (str2term "12"); +(*========== inhibit exn ======================================================= case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of SOME ("12 ist_monom = True", _) => () | _ => error "polyminus.sml: 12 ist_monom = True"; @@ -64,6 +65,7 @@ SOME ("3 * a * b ist_monom = True", _) => () | _ => error "polyminus.sml: 3*a*b ist_monom = True"; +============ inhibit exn =====================================================*) "----------- watch order_add_mult -------------------------------"; "----------- watch order_add_mult -------------------------------"; @@ -78,16 +80,16 @@ trace_rewrite:=false; "----- the same stepwise..."; -val od = ord_make_polynomial true Poly.thy; +val od = ord_make_polynomial true (theory "Poly"); val t = str2term "((a + d) + c) + b"; "((a + d) + c) + b"; -val SOME (t,_) = rewrite_ thy od e_rls true add_commute t; term2str t; +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t; "b + ((a + d) + c)"; -val SOME (t,_) = rewrite_ thy od e_rls true add_commute t; term2str t; +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t; "b + (c + (a + d))"; -val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t; +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t; "b + (a + (c + d))"; -val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t; +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t; "a + (b + (c + d))"; if term2str t = "a + (b + (c + d))" then () else error "polyminus.sml 2 watch order_add_mult"; @@ -95,11 +97,11 @@ "----- if parentheses are right, left_commute is (almost) sufficient..."; val t = str2term "a + (d + (c + b))"; "a + (d + (c + b))"; -val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t; +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t; "a + (c + (d + b))"; -val SOME (t,_) = rewrite_ thy od e_rls true add_commute t;term2str t; +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t;term2str t; "a + (c + (b + d))"; -val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t; +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t; "a + (b + (c + d))"; "----- but we do not want the parentheses at right; thus: cond.rew."; @@ -110,10 +112,10 @@ else error "polyminus.sml: order_add_mult changed"; "----- here we see rew_sub going into subterm with ord.rew...."; -val od = ord_make_polynomial false Poly.thy; +val od = ord_make_polynomial false (theory "Poly"); val t = str2term "b + a + c + d"; -val SOME (t,_) = rewrite_ thy od e_rls false add_commute t; term2str t; -val SOME (t,_) = rewrite_ thy od e_rls false add_commute t; term2str t; +val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t; +val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t; (*@@@ rew_sub gosub: t = d + (b + a + c) @@@ rew_sub begin: t = b + a + c*) @@ -134,6 +136,7 @@ SOME ("12 kleiner 9 = False", _) => () | _ => error "polyminus.sml: 12 kleiner 9 = False"; *) +(*========== inhibit exn ======================================================= case eval_kleiner 0 0 (str2term "a kleiner b") 0 of SOME ("a kleiner b = True", _) => () | _ => error "polyminus.sml: a kleiner b = True"; @@ -158,6 +161,7 @@ SOME ("3 * a * b kleiner c = True", _) => () | _ => error "polyminus.sml: 3 * a * b kleiner b = True"; +============ inhibit exn =====================================================*) "----- compare tausche_plus with real_num_collect"; @@ -165,13 +169,13 @@ val erls = erls_ordne_alphabetisch; val t = str2term "b + a"; -val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; +val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; term2str t; if term2str t = "a + b" then () else error "polyminus.sml: ordne_alphabetisch1 b + a"; val erls = Atools_erls; val t = str2term "2*a + 3*a"; -val SOME (t,_) = rewrite_ thy od erls false real_num_collect t; term2str t; +val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; term2str t; "----- test rewrite_, rewrite_set_"; trace_rewrite:=true; @@ -193,7 +197,7 @@ "----- rewrite goes into subterms"; val t = str2term "a + c + b + d"; -val SOME (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t; +val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; term2str t; if term2str t = "a + b + c + d" then () else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d"; @@ -204,7 +208,7 @@ "----- here we see rew_sub going into subterm with cond.rew...."; val t = str2term "b + a + c + d"; -val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; +val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; term2str t; if term2str t = "a + b + c + d" then () else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d"; @@ -239,14 +243,28 @@ "----------- met simplification for_polynomials with_minus -------"; "----------- met simplification for_polynomials with_minus -------"; val str = -"Script SimplifyScript (t_::real) = \ +"Script SimplifyScript (t_t::real) = \ \ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \ \ (Try (Rewrite_Set fasse_zusammen False)) @@ \ -\ (Try (Rewrite_Set verschoenere False))) t_)" +\ (Try (Rewrite_Set verschoenere False))) t_t)" val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; atomty sc; +"----------- me simplification.for_polynomials.with_minus"; +"----------- me simplification.for_polynomials.with_minus"; +"----------- me simplification.for_polynomials.with_minus"; +val c = []; +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"]))]; +(*========== inhibit exn ======================================================= +val (p,_,f,nxt,_,pt) = me nxt p c pt; +============ inhibit exn =====================================================*) +(*========== inhibit exn ?====================================================== "----------- pbl polynom vereinfachen p.33 -----------------------"; "----------- pbl polynom vereinfachen p.33 -----------------------"; "----------- pbl polynom vereinfachen p.33 -----------------------"; @@ -530,8 +548,7 @@ "----------- pbl binom polynom vereinfachen: cube ----------------"; "----------- pbl binom polynom vereinfachen: cube ----------------"; states:=[]; -CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))", - "normalform N"], +CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"], ("PolyMinus",["binom_klammer","polynom","vereinfachen"], ["simplification","for_polynomials","with_parentheses_mult"]))]; moveActiveRoot 1; @@ -604,8 +621,6 @@ then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1"; show_types := false; -(*========== inhibit exn ======================================================= -============ inhibit exn =====================================================*) - (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) + diff -r 431344850e40 -r 53ee777684ca test/Tools/isac/Knowledge/rational.sml --- a/test/Tools/isac/Knowledge/rational.sml Mon Dec 27 10:38:49 2010 +0100 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Dec 29 20:07:52 2010 +0100 @@ -3,6 +3,9 @@ Copyright (c) Stefan Karnel 2002 Use is subject to license terms. +12345678901234567890123456789012345678901234567890123456789012345678901234567890 + 10 20 30 40 50 60 70 80 + LEGEND WN070906 nonterm.SK marks non-terminating examples ord.SK PARTIALLY marks crucial ordering examples @@ -2079,3 +2082,6 @@ (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) + + +