(* Title: "MathEngBasic/rewrite.sml"

   Author: Walther Neuper 050908

   (c) copyright due to lincense terms.

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- assemble rewrite ------------------------------------------------------------------";

"----------- test rewriting without Isac's thys ------------------------------------------------";

"----------- test rewriting without Isac's thys, ~~~~~ fun rewrite_ ----------------------------";

"----------- conditional rewriting without Isac's thys -----------------------------------------";

"----------- conditional rewriting without Isac's thys, ~~~~~ fun ------------------------------";

"----------- conditional rewriting creating an assumption---------------------------------------";

"----------- step through 'and rew_sub': -------------------------------------------------------";

"----------- step through 'fun rewrite_terms_'  ------------------------------------------------";

"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";

"----------- check diff 2002--2009-3 -----------------------------------------------------------";

"----------- compare all prepat's existing 2010 ------------------------------------------------";

"----------- fun app_rev, Rrls, ----------------------------------------------------------------";

"----------- 2011 thms with axclasses ----------------------------------------------------------";

"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";

"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";

"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- assemble rewrite ------------------------------------------------------------------";

"----------- assemble rewrite ------------------------------------------------------------------";

"----------- assemble rewrite ------------------------------------------------------------------";

"===== rewriting by thm with 'a";

(*show_types := true;*)

val thy = @{theory Complex_Main};

val ctxt = @{context};

val thm = @{thm add.commute};

val t = TermC.parseNEW' ctxt "((r + u) + t) + (s::real)";

"----- from old: fun rewrite__";

val bdv = [];

val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));

"----- from old: and rew_sub";

val (LHS,RHS) = (dest_equals o strip_trueprop 

   	      o Logic.strip_imp_concl) r;

(* old

val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)

"----- fun match_rew in Pure/pattern.ML";

val rtm = the_default RHS (Term.rename_abs LHS t RHS);

writeln(Syntax.string_of_term ctxt rtm);

writeln(Syntax.string_of_term ctxt LHS);

writeln(Syntax.string_of_term ctxt t);

(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));

val (rew, RHS) = (Envir.subst_term 

  (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);

(*lookup in isabelle?trace?response...*)

writeln(Syntax.string_of_term ctxt rew);

writeln(Syntax.string_of_term ctxt RHS);

"===== rewriting: prep insertion into rew_sub";

val thy = @{theory Complex_Main};

val ctxt = @{context};

val thm =  @{thm nonzero_divide_mult_cancel_right};

val r = Thm.prop_of thm;

val tm = @{term "x / (2 * x)::real"};

"----- and rew_sub";

val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop

                  o Logic.strip_imp_concl) r;

val r' = Envir.subst_term (Pattern.match thy (LHS, tm) 

                                (Vartab.empty, Vartab.empty)) r;

val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');

val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 

            o Logic.strip_imp_concl) r';

(*is displayed on top of <response> buffer...*)

Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');

Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');

(**)

"----------- test rewriting without Isac's thys ------------------------------------------------";

"----------- test rewriting without Isac's thys ------------------------------------------------";

"----------- test rewriting without Isac's thys ------------------------------------------------";

"===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";

val thy = @{theory Complex_Main};

val ctxt = @{context};

val thm =  @{thm add.commute};

val tm = @{term "x + y*z::real"};

val SOME (r,_) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);

(*is displayed on _TOP_ of <response> buffer...*)

Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);

if r = @{term "y*z + x::real"}

then () else error "rewrite.sml diff.result in rewriting";

"----- rewriting a subterm";

val tm = @{term "w*(x + y*z)::real"};

val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);

"----- ordered rewriting";

fun tord (_:subst) pp = LibraryC.termless pp;

if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()

else error "rewrite.sml diff.behav. in ord.rewr.";

val NONE = (rewrite_ ctxt tord Rule_Set.empty false thm tm);

(*is displayed on _TOP_ of <response> buffer...*)

Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);

val tm = @{term "x*y + z::real"};

val SOME (r, _) = (rewrite_ ctxt tord Rule_Set.empty false thm tm);

"----------- conditional rewriting without Isac's thys -----------------------------------------";

"----------- conditional rewriting without Isac's thys -----------------------------------------";

"----------- conditional rewriting without Isac's thys -----------------------------------------";

"===== prepr cond.rew. with Pattern.match";

val thy = @{theory Complex_Main};

val ctxt = @{context};

val thm =  @{thm nonzero_divide_mult_cancel_right}; (* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a":*)

val rule = Thm.prop_of thm;

val tm = @{term "x / (2 * x)::real"};

val prem = Logic.strip_imp_prems rule;

val nps = Logic.count_prems rule;

val prems = Logic.strip_prems (nps, [], rule);

val eq = Logic.strip_imp_concl rule;

val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;

val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);

val rule' = Envir.subst_term mtcs rule;

val prems' = (fst o Logic.strip_prems) (Logic.count_prems rule', [], rule');

val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) rule';

(rule' |> UnparseC.term) = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";

 rule';

(rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";

 rule' |> Logic.strip_imp_concl;

(rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";

 rule' |> Logic.strip_imp_concl;

"----------- conditional rewriting creating an assumption---------------------------------------";

"----------- conditional rewriting creating an assumption---------------------------------------";

"----------- conditional rewriting creating an assumption---------------------------------------";

val thm =  @{thm nonzero_divide_mult_cancel_right};

val tm = @{term "x / (2 * x)::real"};

val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;

if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)

else error "rewrite.sml diff.result in cond.rew.";

if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)

then () else error "rewrite.sml diff.asm in cond.rew.";

"----- conditional rewriting immediately: can only be done with ";

"------Isabelle numerals, because erls cannot handle them yet.";

"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";

"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";

"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";

val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a"*)

val tm = @{term "x / (2 * x)::real"};

val erls = eval_rls;

(**)val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;

(** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):

  dest_Trueprop

  ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)

"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =

  (thy, Rewrite_Ord.function_empty, erls, false, thm, tm);

"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =

  (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);

(**) val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)

		  (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;

(** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):

  dest_Trueprop

  ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)

"~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =

  (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),

		  (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);

(*+*)UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";

    val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r;

(*+*)(UnparseC.term lhs, UnparseC.term rhs) = ("?b / (?a * ?b)", "(1::?'a) / ?a");

    val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)

      handle Pattern.MATCH => raise NO_REWRITE;

    val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'));

(*+*)UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";

(*+*)r';

    val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'

    val _ = trace_in2 ctxt i "eval asms" r';

        val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls;

	      (*if*) nofalse (*then*);

      val (t'', p'') = (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t',simpl_p'));

(*##  asms accepted: [x \<noteq> 0]   stored: [x \<noteq> 0] *)

(*+*)if (UnparseC.term t'', map UnparseC.term p'') = ("1 / 2", ["x \<noteq> 0"]) then ()

(*+*)else error "conditional rewriting x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2 CHANGED";

"----------- step through 'and rew_sub': ----------------";

"----------- step through 'and rew_sub': ----------------";

"----------- step through 'and rew_sub': ----------------";

(*and make asms without Trueprop, beginning with the result:*)

val tm = @{term "x / (2 * x)::real"};

val (t', asm, _, _) = rew_sub ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true [] (Thm.prop_of thm) tm;

(*show_types := false;*)

"----- evaluate arguments";

val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 

    (thy, 0, [], Rewrite_Ord.function_empty, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);

"----- step 1: LHS, RHS of rule";

     val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop

                       o Logic.strip_imp_concl) r;

UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";

UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?a";

"----- step 2: the rule instantiated";

     val r' = Envir.subst_term 

                  (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;

UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";

"----- step 3: get the (instantiated) assumption(s)";

     val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');

UnparseC.term (hd p') = "x \<noteq> 0";

"=====vvv make asms without Trueprop ---vvv";

     val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) 

                                             (Logic.count_prems r', [], r'));

case p' of

    [Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) 

      $ Free ("x", _) $ Const (\<^const_name>\<open>zero_class.zero\<close>, _))] => ()

  | _ => error "rewrite.sml assumption changed";

"===== \<up>  make asms without Trueprop --- \<up> ";

"----- step 4: get the (instantiated) RHS";

     val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 

               o Logic.strip_imp_concl) r';

UnparseC.term t' = "1 / 2";

"----------- step through 'fun rewrite_terms_'  ------------------------------------------------";

"----------- step through 'fun rewrite_terms_'  ------------------------------------------------";

"----------- step through 'fun rewrite_terms_'  ------------------------------------------------";

"----- step 0: args for rewrite_terms_, local fun";

val (thy, ord, erls, equs, t) =

    (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.str2term "x = 0"],

     TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");

"----- step 1: args for rew_";

val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);

"----- step 2: rew_sub";

rew_sub ctxt 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;

"----- step 3: step through rew_sub -- inefficient: goes into subterms";

val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;

writeln "---------- rewrite_terms_  1---------------------------";

if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()

else error "rewrite.sml rewrite_terms_ [x = 0]";

val equs = [TermC.str2term "M_b 0 = 0"];

val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";

val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;

writeln "---------- rewrite_terms_  2---------------------------";

if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()

else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";

val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];

val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";

val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;

writeln "---------- rewrite_terms_  3---------------------------";

if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()

else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";

"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";

"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";

"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";

(*see smltest/Scripts/term_G.sml: inst_bdv 2*)

val t = TermC.str2term"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";

val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),

	    (TermC.str2term"bdv_2",TermC.str2term"c_2"),

	    (TermC.str2term"bdv_3",TermC.str2term"c_3"),

	    (TermC.str2term"bdv_4",TermC.str2term"c_4")];

(*------------ outcommented WN071210, after inclusion into ROOT.ML 

val SOME (t,_) = 

    rewrite_inst_ thy e_rew_ord 

		  (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty 

			      [(Eval ("EqSystem.occur_exactly_in", 

				      eval_occur_exactly_in 

					  "#eval_occur_exactly_in_"))

			       ]) 

		  false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t;

(writeln o UnparseC.term) t;

if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \<up> 2) / 2)"

then () else error "rewrite.sml rewrite_inst_ bdvs";

> Rewrite.trace_on:=true;false

Rewrite.trace_on:=false;--------------------------------------------*)

"----------- compare all prepat's existing 2010 ------------------------------------------------";

"----------- compare all prepat's existing 2010 ------------------------------------------------";

"----------- compare all prepat's existing 2010 ------------------------------------------------";

val thy = @{theory "Isac_Knowledge"};

val t = @{term "a + b * x = (0 ::real)"};

val pat = TermC.parse_patt thy "?l = (?r ::real)";

val precond = TermC.parse_patt thy "is_polynomial (?l::real)";(*no infix def*)

val precond = TermC.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;

UnparseC.term 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 @{term True} in this environment,

   then the Rrls is applied. *)

val t = TermC.str2term "(a + b) / c ::real";

val pat = TermC.parse_patt thy "?r / ?s ::real";

val pres = [TermC.parse_patt thy "?r is_expanded", TermC.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 UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"

then () else error "rewrite.sml: prepat cancel subst";

if ([], true) = eval__true ctxt 0 asms [] erls

then () else error "rewrite.sml: prepat cancel eval__true";

"===== Rational.thy: add_fractions_p ===";

(* if each pat* TermC.matches with the current term, the Rrls is applied

   (there are no preconditions to be checked, they are @{term True}) *)

val t = TermC.str2term "a / b + 1 / 2";

val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";

val pres = [@{term True}];

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 ctxt 0 (map (Envir.subst_term subst) pres) [] erls

then () else error "rewrite.sml: prepat add_fractions_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 = TermC.str2term "x \<up> 2 * x";

val pat = TermC.parse_patt thy "?p :: real"

val pres = [TermC.parse_patt thy "?p is_multUnordered"];

val prepat = [(pres, pat)];

val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty

		      [Eval ("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 UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"

then () else error "rewrite.sml: prepat order_mult_ subst";

if ([], true) = eval__true ctxt 0 asms [] erls

then () else error "rewrite.sml: prepat order_mult_ eval__true";

"----------- fun app_rev, Rrls, ----------------------------------------------------------------";

"----------- fun app_rev, Rrls, ----------------------------------------------------------------";

"----------- fun app_rev, Rrls, ----------------------------------------------------------------";

val t = TermC.str2term "x \<up> 2 * x";

if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";

val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";

(*+*)case eval_is_multUnordered "testid" "" tm ctxt of

(*+*)  SOME

(*+*)    ("testidx \<up> 2 * x_",

(*+*)     Const (\<^const_name>\<open>Trueprop\<close>, _) $

(*+*)       (Const (\<^const_name>\<open>HOL.eq\<close>, _) $

(*+*)         (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $

(*+*)           (Const (\<^const_name>\<open>times\<close>, _) $

(*+*)             (Const (\<^const_name>\<open>realpow\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $

(*+*)         Const (\<^const_name>\<open>True\<close>, _))) => ()

(*+*)(*                   ^^^^^^             compare ---vvv *)

(*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";

     eval_is_multUnordered "testid" "" tm ctxt;

case eval_is_multUnordered "testid" "" tm ctxt of

    SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ 

                   (Const (\<^const_name>\<open>HOL.eq\<close>, _) $

                          (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ 

                          Const (\<^const_name>\<open>True\<close>, _))) => ()

  | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";

tracing "----- begin rewrite x \<up> 2 * x ---";

val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t;

tracing "----- end rewrite x \<up> 2 * x ---";

if UnparseC.term t' = "x * x \<up> 2" then ()

else error "rewrite.sml Poly.is_multUnordered doesn't work";

(* for achieving the previous result, the following code was taken apart *)

"----- rewrite__set_ ---";

val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);

	val (t', asm, rew) = app_rev ctxt (i+1) rrls t;

"----- app_rev ---";

val (thy, i, rrls, t) = (thy, (i+1), rrls, t);

	fun chk_prepat thy erls [] t = true

	  | chk_prepat thy erls prepat t =

	    let fun chk (pres, pat) =

		    (let val subst: Type.tyenv * Envir.tenv = 

			     Pattern.match thy (pat, t)

					    (Vartab.empty, Vartab.empty)

		     in snd (eval__true ctxt (i+1) 

					(map (Envir.subst_term subst) pres)

					[] erls)

		     end)

		    handle Pattern.MATCH => false

		fun scan_ f [] = false (*scan_ NEVER called by []*)

		  | scan_ f (pp::pps) = if f pp then true

					else scan_ f pps;

	    in scan_ chk prepat end;

	(*.apply the normal_form of a rev-set.*)

	fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =

	    if chk_prepat thy erls prepat t

	    then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)

                  normal_form t)

	    else NONE;

(*fixme val NONE = app_rev' thy rrls t;*)

"----- app_rev' ---";

val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);

(*fixme false*)   chk_prepat thy erls prepat t;

"----- chk_prepat ---";

val (thy, erls, prepat, t) = (thy, erls, prepat, t);

                fun chk (pres, pat) =

		    (let val subst: Type.tyenv * Envir.tenv = 

			     Pattern.match thy (pat, t)

					    (Vartab.empty, Vartab.empty)

		     in snd (eval__true ctxt (i+1) 

					(map (Envir.subst_term subst) pres)

					[] erls)

		     end)

		    handle Pattern.MATCH => false;

		fun scan_ _ [] = false (*scan_ NEVER called by []*)

		  | scan_ f (pp::pps) = if f pp then true

					else scan_ f pps;

tracing "=== poly.sml: scan_ chk prepat begin";

scan_ chk prepat;

tracing "=== poly.sml: scan_ chk prepat end";

"----- chk ---";

(*reestablish...*) val t = TermC.str2term "x \<up> 2 * x";

val [(pres, pat)] = prepat;

                         val subst: Type.tyenv * Envir.tenv = 

			     Pattern.match thy (pat, t)

					    (Vartab.empty, Vartab.empty);

(*fixme: asms = ["p is_multUnordered"]...instantiate*)

"----- eval__true ---";

val asms = (map (Envir.subst_term subst) pres);

if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()

else error "rewrite.sml: diff. is_multUnordered, asms";

val (thy, i, asms, bdv, rls) = 

    (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"], 

     [] : Subst.T, erls);

case eval__true ctxt i asms bdv rls of 

    ([], true) => ()

  | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";

"----------- 2011 thms with axclasses ----------------------------------------------------------";

"----------- 2011 thms with axclasses ----------------------------------------------------------";

"----------- 2011 thms with axclasses ----------------------------------------------------------";

val thm = @{thm div_by_1};

val prop = Thm.prop_of thm;

TermC.atomty prop;                                     (*Type 'a*)

val t = TermC.str2term "(2*x)/1";                      (*Type real*)

val (thy, ro, er, inst) = 

    (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);

val SOME (t, _) = rewrite_ ctxt ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)

"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";

"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";

"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";

val thy = @{theory RatEq};

val ctxt = Proof_Context.init_global thy;

val SOME t = TermC.parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";

val rls = assoc_rls "RatEq_eliminate"

val SOME (t''''', asm''''') =

           rewrite_set_ ctxt true rls t;

"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);

           rewrite__set_ ctxt 1 bool [] rls term;

"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)

  = (thy, 1, bool, []:Subst.T, rls, term);

(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )

      datatype switch = Applicable.Yes | Noap;

      fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)

        | rew_once ruls asm ct Applicable.Yes [] = 

          (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls

          | Rule_Set.Sequence _ => (ct, asm)

          | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))

        | rew_once ruls asm ct apno (rul :: thms) =

          case rul of

            Rule.Thm (thmid, thm) =>

              (trace1 i (" try thm: " ^ thmid);

              case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)

                  ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of

                NONE => rew_once ruls asm ct apno thms

              | SOME (ct', asm') => 

                (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');

                rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))

                (* once again try the same rule, e.g. associativity against "()"*)

          | Rule.Eval (cc as (op_, _)) => 

            let val _= trace1 i (" try calc: " ^ op_ ^ "'")

              val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)

            in case Eval.adhoc_thm thy cc ct of

                NONE => rew_once ruls asm ct apno thms

              | SOME (_, thm') => 

                let 

                  val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)

                    ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;

                  val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ 

                    ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")

                  val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))

                in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end

            end

          | Rule.Cal1 (cc as (op_, _)) => 

            let val _= trace1 i (" try cal1: " ^ op_ ^ "'");

              val ct = TermC.uminus_to_string ct

            in case Eval.adhoc_thm1_ thy cc ct of

                NONE => (ct, asm)

              | SOME (_, thm') =>

                let 

                  val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)

                    ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;

                  val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^

                     ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")

                  val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))

                in the pairopt end

            end

          | Rule.Rls_ rls' => 

            (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of

              SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms

            | NONE => rew_once ruls asm ct apno thms)

          | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");

      val ruls = (#rules o Rule.Rule_Set.rep) rls;

(*    val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*)

      val (ct', asm') = rew_once ruls [] ct Noap ruls;

"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))

  = (ruls, []:term list, ct, Noap, ruls);

           val Rule.Thm (thmid, thm) = (*case*) rul (*of*);

    val SOME (ct', asm') = (*case*)

           rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)

                  ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);

"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)

  = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),

                  ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);

    val (t', asms, _ (*lrd*), rew) =

           rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)

		  (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct;

"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)

  = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),

		  (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);

    val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r

    val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r

;

(*+*)if UnparseC.term r' =

(*+*)  "\<lbrakk>9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^

(*+*)  "\<Longrightarrow> ((3 + -1 * x + x \<up> 2) /\n" ^

(*+*)  "                   (9 * x + -6 * x \<up> 2 + x \<up> 3) =\n" ^

(*+*)  "                   1 / x) =\n" ^

(*+*)  "                  ((3 + -1 * x + x \<up> 2) * x =\n" ^

(*+*)  "                   1 * (9 * x + -6 * x \<up> 2 + x \<up> 3))"

(*+*)then () else error "instantiated rule CHANGED";

    val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))

;

(*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]

(*+*)then () else error "stored assumptions CHANGED";

    val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'

;

(*+*)if UnparseC.term t' = "(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"

(*+*)then () else error "rewritten term (an equality) CHANGED";

        val (simpl_p', nofalse) =

           eval__true thy (i + 1) p' bdv rls;

"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);

  (*if*) asms = [@{term True}] orelse asms = [] (*else*); 

(*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]

(*+*)then () else error "asms before chk CHANGED";

        fun chk indets [] = (indets, true) (*return asms<>True until false*)

          | chk indets (a :: asms) =

            (case rewrite__set_ thy (i + 1) false bdv rls a of

              NONE => (chk (indets @ [a]) asms)

            | SOME (t, a') =>

              if t = @{term True} then (chk (indets @ a') asms) 

              else if t = @{term False} then ([], false)

            (*asm false .. thm not applied  \<up> ; continue until False vvv*)

            else chk (indets @ [t] @ a') asms);

    val (xxx, true) =

           chk [] asms;  (*return from eval__true*);

"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);

(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;

(*+*)(*val rules =

(*+*)   [Eval (\<^const_name>\<open>divide\<close>, fn),

(*+*)    Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),

(*+*)    :

(*+*)    Eval (\<^const_name>\<open>HOL.eq\<close>, fn),

(*+*)    Thm ("not_true", "(\<not> True) = False"),

(*+*)    Thm ("not_false", "(\<not> False) = True"),

(*+*)    :

(*+*)    Eval (\<^const_name>\<open>realpow\<close>, fn),

(*+*)    Eval ("RatEq.is_ratequation_in", fn)]:

(*+*)   rule list*)

(*+*)chk: term list -> term list -> term list * bool

           rewrite__set_ thy (i + 1) false bdv rls a (*of*);

(*+*)Rewrite.trace_on := false; (*true false*)

        (*this was False; vvvv--- means: indeterminate*)

    val (* SOME (t, a') *)NONE = (*case*)

           rewrite__set_ thy (i + 1) false bdv rls a (*of*);

(*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)

(*

 :

 ####  rls: rateq_erls on: x \<noteq> 0

 :

 #####  try calc: HOL.eq'    <<<------------------------------- here the error comes from

 =====  calc. to: ~ False    <<<------------------------------- \<not> x = 0 is NOT False

 #####  try calc: HOL.eq' 

 #####  try thm: not_true 

 #####  try thm: not_false 

 =====  rewrites to: True    <<<------------------------------- so x \<noteq> 0 is NOT True

                                                       and True, False are NOT stored ...

 :                             

 ###  asms accepted: [x \<noteq> 0]   stored: []

 : *)

Rewrite.trace_on := false; (*true false*)

( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)

"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";

"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";

"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";

"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =

  (@{theory}, Rewrite_Ord.function_empty, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});

"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =

  (thy, 1, [], rew_ord, erls, bool, thm, term);

"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =

  (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)

     val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r

     val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r

     val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))

     val t' = (snd o HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r'

;

if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()

else error "ARGS FOR Pattern.match CHANGED";

val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);

if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()

  else error "Pattern.match CHANGED";

"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";

"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";

"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";

(* norm_equation is defined in Test.thy, other rls see Knowledg/**)

val thy = @{theory};

val rls = norm_equation;

val term = TermC.str2term "x + 1 = 2";

(**)val SOME (t, asm) = rewrite_set_ ctxt false rls term;

(** )#####  try thm: "root_ge0" 

exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):

  dest_eq

  0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)

if UnparseC.term t = "x + 1 + - 1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";

"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);

"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =

  (thy, 1, bool, []: Subst.T, rls, term);

(*deleted after error detection*)