(* Title: tests for ProgLang/rewrite.sml

   TODO.WN0509 collect typical tests from systest here !!!!!

   Author: Walther Neuper 050908

   (c) copyright due to lincense terms.

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

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

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

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

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

"----------- test rewriting without Isac session --------";

"----------- conditional rewriting without Isac session -";

"----------- 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 -------------------";

"----------- repair NO asms from rls RatEq_eliminate ----";

"----------- fun assoc_thm' -----------------------------";

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

"----------- fun mk_thm ------------------------------------------------------------------------";

"----------- 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 = (Thm.term_of o the) (parse thy "((r + u) + t) + s");

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

val bdv = [];

val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) 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_ thy dummy_ord e_rls false thm tm)

  handle _ => error "rewrite.sml diff.behav. in rewriting";

(*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_ thy dummy_ord e_rls false thm tm)

  handle _ => error "rewrite.sml diff.behav. in rew_sub";

"----- ordered rewriting";

fun tord (_:subst) pp = Term_Ord.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_ thy tord e_rls false thm tm)

  handle _ => error "rewrite.sml diff.behav. in rewriting";

(*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_ thy tord e_rls false thm tm)

  handle _ => error "rewrite.sml diff.behav. in rewriting";

"----------- 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};

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';

"----- 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_ thy dummy_ord e_rls false thm tm)

  handle _ => error "rewrite.sml diff.behav. in cond.rew.";

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.";

"----------- 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 thy 0 [] dummy_ord e_rls true [] (Thm.prop_of thm) tm;

(*show_types := false;*)

"----- evaluate arguments";

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

    (thy, 0, [], dummy_ord, e_rls, 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;

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

term2str LHS = "?b / (?a * ?b)"; term2str RHS = "(1::?'a) / ?a";

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

     val r' = Envir.subst_term 

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

term2str 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');

term2str (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 ("HOL.Not", _) $ (Const ("HOL.eq", _) 

      $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()

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

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

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

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

               o Logic.strip_imp_concl) r';

term2str 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"}, dummy_ord, Erls, [str2term "x = 0"],

     str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");

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

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

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

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

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

val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;

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

if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()

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

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

val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";

val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;

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

if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()

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

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

val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";

val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;

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

if term2str t' = "0 = -1 * q_0 * 0 ^^^ 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 = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";

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

	    (str2term"bdv_2",str2term"c_2"),

	    (str2term"bdv_3",str2term"c_3"),

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

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

val SOME (t,_) = 

    rewrite_inst_ thy e_rew_ord 

		  (append_rls "erls_isolate_bdvs" e_rls 

			      [(Calc ("EqSystem.occur'_exactly'_in", 

				      eval_occur_exactly_in 

					  "#eval_occur_exactly_in_"))

			       ]) 

		  false bdvs (num_str @{separate_bdvs_add) t;

(writeln o term2str) t;

if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"

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

trace_rewrite:=true;

trace_rewrite:=false;--------------------------------------------*)

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

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

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

(*----- 2002 -------------------------------------------------------------------

#  rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *

q_0 * x ^^^ 2 / 2)

##  rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2

/ 2)

###  try thm: real_diff_minus

###  try thm: sym_real_mult_minus1

##  rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2

/ 2)

###  try thm: rat_mult_poly_l

###  try thm: rat_mult_poly_r

####  eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp

==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =

    1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI

#####  rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2

is_polyexp

######  try calc: Poly.is'_polyexp'

======  calc. to: False

######  try calc: Poly.is'_polyexp'

######  try calc: Poly.is'_polyexp'

####  asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]

----- 2002 NONE rewrite --------------------------------------------------------

----- 2009 should maintain this behaviour, but: --------------------------------

#  rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)

##  rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)

###  try thm: real_diff_minus

###  try thm: sym_real_mult_minus1

##  rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)

###  try thm: rat_mult_poly_l

###  try thm: rat_mult_poly_r

####  eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp

==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =

    1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI

#####  rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp

######  try calc: Poly.is'_polyexp'

======  calc. to: False

######  try calc: Poly.is'_polyexp'

######  try calc: Poly.is'_polyexp'

####  asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]   stored: ["False"]

===  rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI

----- 2009 -------------------------------------------------------------------*)

(*the situation as was before repair (asm without Trueprop) is outcommented*)

val thy = @{theory "Isac"};

"===== example which raised the problem =================";

val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};

"----- rewrite_set_inst_ norm_Rational_noadd_fractions--";

val subs = [(@{term "bdv"}, @{term  "x"})];

val rls = norm_Rational_noadd_fractions;

val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;

if term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * 1 * q_0 * x ^^^ 2 / 2)" andalso

  terms2str asms = "[]" then {}

else error "this was NONE with Isabelle2013-2 ?!?"

"----- rewrite_ rat_mult_poly_r--------------------------";

val thm = @{thm rat_mult_poly_r};

         "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";

val erls = append_rls "e_rls-is_polyexp" e_rls 

                      [Calc ("Poly.is'_polyexp", eval_is_polyexp "")];

val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;

(*t' = t''; (*false because of further rewrites in t'*)*)

"----- rew_sub  --------------------------------";

val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;

(*t'' = t'''; (*true*)*)

"----- rewrite_set_ erls --------------------------------";

val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};

val NONE = rewrite_set_ thy true erls cond; 

(* ^^^^^ goes with '======  calc. to: False' above from beginning*)

writeln "===== maximally simplified example =====================";

val t = @{term "a / b * (x / x ^^^ 2)"};

         "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";

writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";

val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;

term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)

(*checked visually: trace_rewrite looks like above for 2009*)

writeln "----- rewrite_ rat_mult_poly_r--------------------------";

val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;

(*t' = t''; (*false because of further rewrites in t'*)*)

writeln "----- rew_sub  --------------------------------";

val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;

(*t'' = t'''; (*true*)*)

writeln "----- rewrite_set_ erls --------------------------------";

val cond = @{term "(x / x ^^^ 2)"};

val NONE = rewrite_set_ thy true erls cond; 

(* ^^^^^ goes with '======  calc. to: False' above from beginning*)

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

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

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

val thy = @{theory "Isac"};

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 @{term True} 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: add_fractions_p ===";

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

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

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

val pat = 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 thy 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 = 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";

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

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

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

val t = str2term "x^^^2 * x";

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

val tm = str2term "(x^^^2 * x) is_multUnordered";

eval_is_multUnordered "testid" "" tm thy;

case eval_is_multUnordered "testid" "" tm thy of

    SOME (_, Const ("HOL.Trueprop", _) $ 

                   (Const ("HOL.eq", _) $

                          (Const ("Poly.is'_multUnordered", _) $ _) $ 

                          Const ("HOL.True", _))) => ()

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

tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := true;

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

tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;

if term2str t' = "x * x ^^^ 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 thy (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 thy (i+1) 

					(map (Envir.subst_term subst) pres)

					[] erls)

		     end)

		    handle _ => 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 = "^(term2str 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 thy (i+1) 

					(map (Envir.subst_term subst) pres)

					[] erls)

		     end)

		    handle _ => false;

		fun scan_ f [] = 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 = str2term "x ^^^ 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 terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()

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

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

    (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"], 

     [] : (term * term) list, erls);

case eval__true thy 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 = num_str @{thm div_by_1};

val prop = Thm.prop_of thm;

atomty prop;                                     (*Type 'a*)

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

val (thy, ro, er, inst) = 

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

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

"----------- repair NO asms from rls RatEq_eliminate ----";

"----------- repair NO asms from rls RatEq_eliminate ----";

"----------- repair NO asms from rls RatEq_eliminate ----";

val t = str2term "1 / x = 5";

trace_rewrite := true;

val SOME (t', asm) = rewrite_ thy e_rew_ord e_rls true @{thm rat_mult_denominator_right} t;

term2str t' = "1 = 5 * x";

terms2str asm = "[\"x ~= 0\"]";

(*

 ##  eval asms: x ~= 0 ==> (1 / x = 5) = (1 = 5 * x) 

 ###  rls: e_rls on: x ~= 0 

 ##  asms accepted: ["x ~= 0"]   stored: ["x ~= 0"] 

*)

trace_rewrite := false;

trace_rewrite := false;

val SOME (t', []) = rewrite_set_ thy true RatEq_eliminate t; (*= [] must be = "x ~= 0"*)

term2str t' = "1 = 5 * x";

(*

 :

 ####  rls: rateq_erls on: x ~= 0 

 :

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

 =====  calc. to: ~ False 

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

 #####  try thm: not_true 

 #####  try thm: not_false 

 =====  rewrites to: True 

 :

 ###  asms accepted: ["x ~= 0"]   stored: []

 :

*)

trace_rewrite := false;

(* WN120317.TODO dropped rateq: the above error is the same in 2002 *)

"----------- fun assoc_thm' -----------------------------";

"----------- fun assoc_thm' -----------------------------";

"----------- fun assoc_thm' -----------------------------";

val thy = @{theory ProgLang}

val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");

if string_of_thm' thy tth = "6 = 2 * 3" then ()

else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";

val tth = assoc_thm' thy ("add_0_left","");

if string_of_thm' thy tth = "0 + ?a = ?a" then ()

else error "assoc_thm' (add_0_left,\"\") changed";

val tth = assoc_thm' thy ("sym_add_0_left","");

if string_of_thm' thy tth = "?t = 0 + ?t" then ()

else error "assoc_thm' (sym_add_0_left,\"\") changed";

val tth = assoc_thm' thy ("add_commute","");

if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()

else error "assoc_thm' (add_commute,\"\") changed"

"----------- 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}, dummy_ord, e_rls, 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, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)

     val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) 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 HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'

;

if term2str lhss = "?a * (?b + ?c)" andalso term2str 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 |> term2str) = "x * (y + z) = x * y + x * z" then ()

  else error "Pattern.match CHANGED";

"----------- fun mk_thm ------------------------------------------------------------------------";

"----------- fun mk_thm ------------------------------------------------------------------------";

"----------- fun mk_thm ------------------------------------------------------------------------";

val thy = @{theory Isac}

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

val thm = @{thm realpow_twoI};

val patt_str = "?r ^^^ 2 = ?r * ?r";

val term_str = "r ^^^ 2 = r * r";

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

case parse_patt thy patt_str of

  Const ("HOL.eq", _) $ (Const ("Atools.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $

      (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()

| _ => error "parse_patt  ?r ^^^ 2 = ?r * ?r  changed";

case parse thy term_str of

  NONE => ()

| _ => writeln "parse does NOT take patterns with '?'";

val t1 = (#prop o Thm.rep_thm) (num_str thm);

if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";

val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;

if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";

(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";

(*and   this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r"  [.]: thm

  gives a strange thm*);

(*while this..*) 

val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm

  ..gives another strange thm; but it is used and works with rewriting: *);

val t1' = (#prop o Thm.rep_thm) (num_str thm_made);

if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

val thm = @{thm real_mult_div_cancel2};

val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";

val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

case parse_patt thy patt_str of

  Const ("Pure.imp", _) $ 

    (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $

      (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $

        (Const ("HOL.Trueprop", _) $

          (Const ("HOL.eq", _) $ _ $ _ )) => ()

| _ => error "parse_patt  ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n  changed";

case parse thy term_str of

  NONE => ()

| _ => writeln "parse does NOT take patterns with '?'";

val t1 = (#prop o Thm.rep_thm) (num_str thm);

if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";

val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;

if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";

(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";

(*and   this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r"  [.]: thm

  gives a strange thm*);

(*while this*) 

val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm

  gives another strange thm; but it is used and words with rewriting: *);

val t1' = (#prop o Thm.rep_thm) (num_str thm_made);

if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";

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

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

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

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

val thy = @{theory};

val rls = norm_equation;

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

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

if term2str 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);

"~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);