neuper@38067: (* neuper@38077: cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/course/ neuper@38077: /usr/local/Isabelle/bin/isabelle jedit -l Isac T2_Rewriting.thy & neuper@38067: *) neuper@38067: wneuper@59592: theory T2_Rewriting imports Isac.Isac_Knowledge wneuper@59460: begin neuper@38067: wneuper@59472: chapter \Rewriting\ neuper@38067: wneuper@59472: text \\emph{Rewriting} is a technique of Symbolic Computation, which is neuper@38077: appropriate to make a 'transparent system', because it is intuitively neuper@38077: comprehensible. For a thourogh introduction see the book of Tobias Nipkow, neuper@38067: http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/ neuper@38067: wneuper@59472: section {* Introduction to rewriting\ neuper@38067: wneuper@59472: text \Rewriting creates calculations which look like written by hand; see the neuper@38067: ISAC tutoring system ! ISAC finds the rules automatically. Here we start by neuper@38077: telling the rules ourselves. neuper@38077: Let's differentiate after we have identified the rules for differentiation, as wenzelm@60192: found in $ISABELLE_ISAC/Knowledge/Diff.thy: wneuper@59472: \ wneuper@59472: ML \ Walther@60424: val diff_sum = @{thm diff_sum}; Walther@60424: val diff_pow = @{thm diff_pow}; Walther@60424: val diff_var = @{thm diff_var}; Walther@60424: val diff_const = @{thm diff_const}; wneuper@59472: \ wneuper@59472: text \Looking at the rules (abbreviated by 'thm' above), we see the neuper@38077: differential operator abbreviated by 'd_d ?bdv', where '?bdv' is the bound neuper@38077: variable. neuper@38077: Can you read diff_const in the Ouput window ? neuper@38067: wneuper@59472: Please, skip this introductory ML-section in the first go ...\ wneuper@59472: ML \ wneuper@59348: (*default_print_depth 1;*) neuper@38077: val (thy, ro, er, inst) = wneuper@59592: (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); Walther@60424: val ctxt = Proof_Context.init_global thy; (*required for parsing*) wneuper@59472: \ wneuper@59472: text \... and let us differentiate the term t:\ wneuper@59472: ML \ Walther@60424: val t = TermC.parseNEW' ctxt "d_d x (x\2 + x + y)"; neuper@38067: Walther@60501: val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t; Walther@60501: val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t; Walther@60501: val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_pow t; UnparseC.term t; Walther@60501: val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_var t; UnparseC.term t; Walther@60501: val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t; UnparseC.term t; wneuper@59472: \ wneuper@59472: text \Please, scoll up the Output-window to check the 5 steps of rewriting ! walther@60242: You might not be satisfied by the result "2 * x \ (2 - 1) + 1 + 0". neuper@38067: neuper@38077: ISAC has a set of rules called 'make_polynomial', which simplifies the result: wneuper@59472: \ wneuper@59472: ML \ Walther@60501: val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t; UnparseC.term t; wneuper@59472: \ neuper@38067: wneuper@59472: section \Note on bound variables\ wneuper@59472: text \You may have noticed that rewrite_ above could distinguish between x neuper@38077: (d_d x x = 1) and y (d_d x y = 0). ISAC does this by instantiating theorems neuper@38077: before application: given [(@{term "bdv::real"}, @{term "x::real"})] the neuper@38077: theorem diff_sum becomes "d_d x (?u + ?v) = d_d x ?u + d_d x ?v". neuper@38077: neuper@38077: Isabelle does this differently by variables bound by a 'lambda' %, see neuper@38077: http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html wneuper@59472: \ wneuper@59472: ML \ Walther@60650: val t = @{term "%x. x^2 + x + y"}; Walther@60650: TermC.atom_write_detail @{context} t; UnparseC.term_in_ctxt @{context} t; wneuper@59472: \ wneuper@59472: text \Since this notation does not conform to present high-school matheatics neuper@38077: ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation neuper@38077: solving in ISAC. wneuper@59472: \ neuper@38067: wneuper@59472: section \Conditional and ordered rewriting\ wneuper@59472: text \We have already seen conditional rewriting above when we used the rule wneuper@59472: diff_const; let us try:\ wneuper@59472: ML \ Walther@60424: val t1 = TermC.parseNEW' ctxt "d_d x (a*BC*x*z)"; Walther@60500: Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t1; neuper@38077: Walther@60424: val t2 = TermC.parseNEW' ctxt "d_d x (a*BC*y*z)"; Walther@60500: Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t2; wneuper@59472: \ wneuper@59472: text \For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false, neuper@38077: since x occurs in t1 actually; thus the rule following implication '==>' is neuper@38077: not applied and rewrite_inst_ returns NONE. neuper@38077: For term t2 is 'not (x occurs_in "a*BC*y*z")' true, thus the rule is applied. wneuper@59472: \ neuper@38067: wneuper@59472: subsection \ordered rewriting\ wneuper@59472: text \Let us start with an example; in order to see what is going on we tell neuper@38077: Isabelle to show all brackets: wneuper@59472: \ wneuper@59472: ML \ neuper@42090: (*show_brackets := true; TODO*) Walther@60424: val t0 = TermC.parseNEW' ctxt "2*a + 3*b + 4*a::real"; UnparseC.term t0; neuper@38077: (*show_brackets := false;*) wneuper@59472: \ wneuper@59472: text \Now we want to bring 4*a close to 2*a in order to get 6*a: wneuper@59472: \ wneuper@59472: ML \ Walther@60500: val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.assoc} t0; UnparseC.term t; Walther@60500: val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.left_commute} t; UnparseC.term t; Walther@60500: val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t; Walther@60500: val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm real_num_collect} t; UnparseC.term t; wneuper@59472: \ wneuper@59472: text \That is fine, we just need to add 2+4 !!!!! See the next section below. neuper@38077: neuper@38077: But we cannot automate such ordering with what we know so far: If we put wneuper@59118: add.assoc, add.left_commute and add.commute into one ruleset (your have used neuper@38077: ruleset 'make_polynomial' already), then all the rules are applied as long neuper@38077: as one rule is applicable (that is the way such rulesets work). neuper@38077: Try to step through the ML-sections without skipping one of them ... wneuper@59472: \ Walther@60500: ML \val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\ Walther@60500: ML \val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\ Walther@60500: ML \val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\ Walther@60500: ML \val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\ wneuper@59472: text \... you can go forever, the ruleset is 'not terminating'. neuper@38077: The theory of rewriting makes this kind of rulesets terminate by the use of neuper@38077: 'rewrite orders': neuper@38077: Given two terms t1 and t2 we describe rewriting by: t1 ~~> t2. Then neuper@38077: 'ordered rewriting' is: t2 < t1 ==> t1 ~~> t2. That means, a rule is only neuper@38077: applied, when the result t2 is 'smaller', '<', than the one to be rewritten. neuper@38077: Defining such a '<' is not trivial, see ~~/src/Tools/isacKnowledge/Poly.thy neuper@38077: for 'fun has_degree_in' etc. wneuper@59472: \ neuper@38067: wneuper@59472: subsection \Simplification in ISAC\ wneuper@59472: text \ neuper@38077: With the introduction into rewriting, ordered rewriting and conditional neuper@38077: rewriting we have seen all what is necessary for the practice of rewriting. neuper@38077: neuper@38077: One basic technique of 'symbolic computation' which uses rewriting is neuper@38077: simplification, that means: transform terms into an equivalent form which is neuper@38077: as simple as possible. neuper@38077: Isabelle has powerful and efficient simplifiers. Nevertheless, ISAC has another neuper@38077: kind of simplifiers, which groups rulesets such that the trace of rewrites is neuper@38077: more readable in ISAC's worksheets. neuper@38077: neuper@38077: Here are examples of of how ISAC's simplifier work: wneuper@59472: \ wneuper@59472: ML \ neuper@42090: (*show_brackets := false; TODO*) Walther@60424: val t1 = TermC.parseNEW' ctxt "(a - b) * (a\2 + a*b + b\2)"; Walther@60500: val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t1; UnparseC.term t; wneuper@59472: \ wneuper@59472: ML \ Walther@60424: val t2 = TermC.parseNEW' ctxt walther@60242: "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \ 2 - 9))"; Walther@60500: val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t; wneuper@59472: \ wneuper@59472: text \The simplifiers are quite busy when finding the above results. you can walther@59901: watch them at work by setting the switch 'Rewrite.trace_on:\ wneuper@59472: ML \ neuper@38077: tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; Walther@60500: val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t; neuper@38077: tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; wneuper@59472: \ wneuper@59472: text \You see what happend when you click the checkbox on the bar neuper@38077: separating this window from the Output-window. neuper@38077: neuper@38077: So, it might be better to take simpler examples for watching the simplifiers. wneuper@59472: \ neuper@38067: neuper@38077: wneuper@59472: section \Experiments with a simplifier conserving minus\ neuper@38077: wneuper@59472: text \We conclude the section on rewriting with starting into an experimental neuper@38077: development. This development has been urged by teachers using ISAC for neuper@38077: introduction to algebra with students at the age of 12-14. neuper@38077: neuper@38077: The teachers requested ISAC to keep the minus, for instance in the above neuper@38077: result "a^3 + -1 * b^3" (here ISAC should write "a^3 - * b^3") and also neuper@38077: in all intermediate steps. neuper@38077: neuper@38077: So we started to develop (in German !) such a simplifier in wenzelm@60192: $ISABELLE_ISAC/Knowledge/PolyMinus.thy wneuper@59472: \ neuper@38067: wneuper@59472: subsection \What already works\ wneuper@59472: ML \ Walther@60424: val t2 = TermC.parseNEW' ctxt Walther@60424: "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12::real"; Walther@60500: val SOME (t, _) = Rewrite.rewrite_set_ ctxt true rls_p_33 t2; UnparseC.term t; wneuper@59472: \ wneuper@59472: text \Try your own examples !\ neuper@38067: wneuper@59472: subsection \This raises questions about didactics\ wneuper@59472: text \Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy wneuper@59472: \ wneuper@59472: ML \ neuper@38077: @{thm subtrahiere}; neuper@38077: @{thm subtrahiere_von_1}; neuper@38077: @{thm subtrahiere_1}; wneuper@59472: \ wneuper@59472: text \That would not be so bad. But it is only a little part of what else is neuper@38077: required: wneuper@59472: \ wneuper@59472: ML \ neuper@38077: @{thm subtrahiere_x_plus_minus}; neuper@38077: @{thm subtrahiere_x_plus1_minus}; neuper@38077: @{thm subtrahiere_x_plus_minus1}; neuper@38077: @{thm subtrahiere_x_minus_plus}; neuper@38077: @{thm subtrahiere_x_minus1_plus}; neuper@38077: @{thm subtrahiere_x_minus_plus1}; neuper@38077: @{thm subtrahiere_x_minus_minus}; neuper@38077: @{thm subtrahiere_x_minus1_minus}; neuper@38077: @{thm subtrahiere_x_minus_minus1}; wneuper@59472: \ wneuper@59472: text \So, learning so many rules, and learning to apply these rules, is futile. neuper@38077: Actually, most of our students are unable to apply theorems. neuper@38077: neuper@38077: But if you look at 'make_polynomial' or even 'norm_Rational' you see, neuper@38077: that these general simplifiers require about 10% than rulesets for '-'. neuper@38077: neuper@38077: So, we might have better chances to teach our student to apply theorems neuper@38077: without '-' ? wneuper@59472: \ neuper@38077: wneuper@59472: subsection \This does not yet work\ wneuper@59472: ML \ Walther@60424: val t = TermC.parseNEW' ctxt neuper@38077: "(2*a - 5*b) * (2*a + 5*b)"; Walther@60500: Rewrite.rewrite_set_ ctxt true rls_p_33 t; UnparseC.term t; wneuper@59472: \ neuper@38067: neuper@38067: end