(*

/usr/local/isabisac/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/

section {* 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 

Just to show, how simple rewriting is

=======================================================================================

???????????????????? star with diff --- this allows trial and error from the beginning,

!!!!!!!!!!!!!!!!!!!! if all the thems are given: here +?+ .thy (code or html?)

=======================================================================================

The following

Please, skip the following ML-section in the first go ...*}

ML {*

print_depth 5;

val (thy, ro, er, inst) = (theory "Isac", tless_true, eval_rls, [("bdv", "x::real")]);

*}

ML {*

val t = (term_of o the o (parse thy)) "2 * a + 3 * (a - b)";

*}

ML {* 

val SOME (t, _) = rewrite_ thy ro er true (@{thm "klammer_mult_minus"}) t; term2str t;

val SOME (t, _) = rewrite_ thy ro er true (@{thm "klammer_plus_minus"}) t; term2str t;

val SOME (t, _) = rewrite_ thy ro er true (@{thm "real_num_collect"}) t; term2str t;

*}

ML {*

("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_"));

get_calculation_ thy ;

calculate_ thy ;

*}

ML {* 

111

*}

text {* ... and let's start with an example:

*}

ML {* val t = parse (theory "PolyMinus") "2 * a + 3 * a + 4 * b";

*}

end