diff -r cd7854f2636d -r 02a9b2540eb7 test/Tools/isac/ProgLang/rewrite.sml
--- a/test/Tools/isac/ProgLang/rewrite.sml	Tue Sep 28 13:30:29 2010 +0200
+++ b/test/Tools/isac/ProgLang/rewrite.sml	Fri Oct 01 10:23:38 2010 +0200
@@ -1,6 +1,6 @@
-(* tests for ME/rewrite.sml
+(* Title: tests for ProgLang/rewrite.sml
    TODO.WN0509 collect typical tests from systest here !!!!!
-   author: Walther Neuper 050908
+   Author: Walther Neuper 050908
    (c) copyright due to lincense terms.
 
 12345678901234567890123456789012345678901234567890123456789012345678901234567890
@@ -17,10 +17,13 @@
 "----------- step through 'fun rewrite_terms_'  ---------";
 "----------- rewrite_inst_ bdvs -------------------------";
 "----------- check diff 2002--2009-3 --------------------";
+"----------- fun app_rev, Rrls, prepat ------------------";
 "--------------------------------------------------------";
 "--------------------------------------------------------";
 "--------------------------------------------------------";
 
+(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
+
 "----------- assemble rewrite ---------------------------";
 "----------- assemble rewrite ---------------------------";
 "----------- assemble rewrite ---------------------------";
@@ -336,9 +339,102 @@
 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
 "--------------------------------------------------------";
 
+-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
 
-(*===== inhibit exn ============================================================
-===== inhibit exn ============================================================*)
+"----------- fun app_rev, Rrls, prepat ------------------";
+"----------- fun app_rev, Rrls, prepat ------------------";
+"----------- fun app_rev, Rrls, prepat ------------------";
+(* Christian Urban, 101001 
+theory Test
+imports Main Complex
+begin
+
+ML {*
+let
+  val parser = Args.context -- Scan.lift Args.name_source
+  fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
+  |> ML_Syntax.print_term |> ML_Syntax.atomic
+in
+  ML_Antiquote.inline "term_pat" (parser >> term_pat)
+end
+*}
+
+ML {*
+  val t = @{term "a + b * x = (0 ::real)"};
+  val pat = @{term_pat "?l = (?r ::real)"};
+  val precond = @{term_pat "is_polynomial (?l::real)"};
+  val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
+*}
+
+ML {*
+  Envir.subst_term inst precond
+  |> Syntax.string_of_term @{context}
+  |> writeln
+*}
+end *)
+val t = @{term "a + b * x = (0 ::real)"};
+val pat = parse_patt thy "?l = (?r ::real)";
+val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
+val precond = parse_patt thy " (?l::real) is_expanded"; 
+
+val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
+val preinst = Envir.subst_term inst precond;
+term2str preinst;
+
+"===== Rational.thy: cancel ===";
+(* pat matched with the current term gives an environment 
+   (or not: hen the Rrls not applied);
+   if pre1 and pre2 evaluate to HOLogic.true_const in this environment,
+   then the Rrls is applied. *)
+val t = str2term "(a + b) / c ::real";
+val pat = parse_patt thy "?r / ?s ::real";
+val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
+val prepat = [(pres, pat)];
+val erls = rational_erls;
+(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
+
+val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
+val asms = map (Envir.subst_term subst) pres;
+if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
+then () else error "rewrite.sml: prepat cancel subst";
+if ([], true) = eval__true thy 0 asms [] erls
+then () else error "rewrite.sml: prepat cancel eval__true";
+
+"===== Rational.thy: common_nominator_p ===";
+(* if each pat* matches with the current term, the Rrls is applied
+   (there are no preconditions to be checked, they are HOLogic.true_const) *)
+val t = str2term "a / b + 1 / 2";
+val pat = parse_patt thy "?r / ?s + ?u / ?v";
+val pres = [HOLogic.true_const];
+val prepat = [(pres, pat)];
+val erls = rational_erls;
+(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
+
+val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
+if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
+then () else error "rewrite.sml: prepat common_nominator_p";
+
+"===== Poly.thy: order_mult_ ===";
+          (* ?p matched with the current term gives an environment,
+             which evaluates (the instantiated) "p is_multUnordered" to true*)
+val t = str2term "x^^^2 * x";
+val pat = parse_patt thy "?p :: real"
+val pres = [parse_patt thy "?p is_multUnordered"];
+val prepat = [(pres, pat)];
+val erls = append_rls "e_rls-is_multUnordered" e_rls
+		      [Calc ("Poly.is'_multUnordered", 
+                             eval_is_multUnordered "")];
+
+val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
+val asms = map (Envir.subst_term subst) pres;
+if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
+then () else error "rewrite.sml: prepat order_mult_ subst";
+if ([], true) = eval__true thy 0 asms [] erls
+then () else error "rewrite.sml: prepat order_mult_ eval__true";
+
+
+(*========== inhibit exn =======================================================
+============ inhibit exn =====================================================*)
 
 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)