
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 \<open>Rewriting\<close>
neuper@38067: 
wneuper@59472: text \<open>\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\<close>
neuper@38067: 
wneuper@59472: text \<open>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: \<close>
wneuper@59472: ML \<open>
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: \<close>
wneuper@59472: text \<open>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 ...\<close>
wneuper@59472: ML \<open>
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: \<close>
wneuper@59472: text \<open>... and  let us differentiate the term t:\<close>
wneuper@59472: ML \<open>
Walther@60424: val t = TermC.parseNEW' ctxt "d_d x (x\<up>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: \<close>
wneuper@59472: text \<open>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 \<up> (2 - 1) + 1 + 0".
neuper@38067: 
neuper@38077:   ISAC has a set of rules called 'make_polynomial', which simplifies the result:
wneuper@59472: \<close>
wneuper@59472: ML \<open>
Walther@60501: val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t; UnparseC.term t;
wneuper@59472: \<close>
neuper@38067: 
wneuper@59472: section \<open>Note on bound variables\<close>
wneuper@59472: text \<open>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: \<close>
wneuper@59472: ML \<open>
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: \<close>
wneuper@59472: text \<open>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: \<close>
neuper@38067: 
wneuper@59472: section \<open>Conditional and ordered rewriting\<close>
wneuper@59472: text \<open>We have already seen conditional rewriting above when we used the rule
wneuper@59472:   diff_const; let us try:\<close>
wneuper@59472: ML \<open>
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: \<close>
wneuper@59472: text \<open>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: \<close>
neuper@38067: 
wneuper@59472: subsection \<open>ordered rewriting\<close>
wneuper@59472: text \<open>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: \<close>
wneuper@59472: ML \<open>
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: \<close>
wneuper@59472: text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a:
wneuper@59472: \<close>
wneuper@59472: ML \<open>
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: \<close>
wneuper@59472: text \<open>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: \<close>
Walther@60500: ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close>
Walther@60500: ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close>
Walther@60500: ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close>
Walther@60500: ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close>
wneuper@59472: text \<open>... 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: \<close>
neuper@38067: 
wneuper@59472: subsection \<open>Simplification in ISAC\<close>
wneuper@59472: text \<open>
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: \<close>
wneuper@59472: ML \<open>
neuper@42090: (*show_brackets := false; TODO*)
Walther@60424: val t1 = TermC.parseNEW' ctxt "(a - b) * (a\<up>2 + a*b + b\<up>2)";
Walther@60500: val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t1; UnparseC.term t;
wneuper@59472: \<close>
wneuper@59472: ML \<open>
Walther@60424: val t2 = TermC.parseNEW' ctxt 
walther@60242:   "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \<up> 2 - 9))";
Walther@60500: val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t;
wneuper@59472: \<close>
wneuper@59472: text \<open>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:\<close>
wneuper@59472: ML \<open>
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: \<close>
wneuper@59472: text \<open>You see what happend when you click the checkbox <Tracing> 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: \<close>
neuper@38067: 
neuper@38077: 
wneuper@59472: section \<open>Experiments with a simplifier conserving minus\<close>
neuper@38077: 
wneuper@59472: text \<open>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: \<close>
neuper@38067: 
wneuper@59472: subsection \<open>What already works\<close>
wneuper@59472: ML \<open>
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: \<close>
wneuper@59472: text \<open>Try your own examples !\<close>
neuper@38067: 
wneuper@59472: subsection \<open>This raises questions about didactics\<close>
wneuper@59472: text \<open>Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@38077: @{thm subtrahiere};
neuper@38077: @{thm subtrahiere_von_1};
neuper@38077: @{thm subtrahiere_1};
wneuper@59472: \<close>
wneuper@59472: text \<open>That would not be so bad. But it is only a little part of what else is
neuper@38077:   required:
wneuper@59472: \<close>
wneuper@59472: ML \<open>
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: \<close>
wneuper@59472: text \<open>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: \<close>
neuper@38077: 
wneuper@59472: subsection \<open>This does not yet work\<close>
wneuper@59472: ML \<open>
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: \<close>
neuper@38067: 
neuper@38067: end




