*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Cygwin/jEdit works*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Mon, 06 Dec 2010 17:35:17 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.1.10.1012061550370.7059@atbroy100.informatik.tu-muenchen.de>*References*: <4CF8FB00.9010604@ist.tugraz.at> <alpine.LNX.1.10.1012061550370.7059@atbroy100.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.1.15) Gecko/20101027 Thunderbird/3.0.10

On 12/06/2010 03:55 PM, Makarius wrote:

I suppose you have copied an actual x86-cygwin image here, not x86-linux?

Right.

starts jedit as well, but Plugin/Isabelle gives error 'Failed tostart Isabelle process' together with a window just containing '>'.PS: These 2 notebooks only have 1 GB of memory.This could well be the startup timeout, which is 10s by default. Seeoptions.isabelle.startup-timeout in Isabelle.props of the plugin,although I can't say on the spot how to change that in the publishedversion without rebuilding the plugin.

Thank you very much for that hint !

Running Isabelle/jEdit with as little as 1 GB is a bit ambitiousanyway. In the local course that we had 2 weeks ago, we required 2 GBas minimum and that was already tight.

Makarius

Walther

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

**References**:**[isabelle] Cygwin/jEdit works***From:*Walther Neuper

**Re: [isabelle] Cygwin/jEdit works***From:*Makarius

- Previous by Date: [isabelle] Suppressing warnings
- Next by Date: Re: [isabelle] Suppressing warnings
- Previous by Thread: Re: [isabelle] Cygwin/jEdit works
- Next by Thread: [isabelle] Announcement: New Isabelle IRC channel on Freenode
- Cl-isabelle-users December 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list