(* tests for ME/rewrite.sml

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

   author: Walther Neuper 050908

   (c) copyright due to lincense terms.

use"../smltest/Scripts/rewrite.sml";

use"rewrite.sml";

*)

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

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

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

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

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

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

"----------- rewrite_terms_  -------------------------------------";

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

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

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

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

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

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

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

(*ML {**)

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

show_types := true;

val thy = @{theory Complex_Main};

val ctxt = @{context};

val thm = @{thm add_commute};

val t = (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 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);

tracing(Syntax.string_of_term ctxt rtm);

tracing(Syntax.string_of_term ctxt lhs);

tracing(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);

(*}

ML {*)

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

val thy = @{theory Complex_Main};

val ctxt = @{context};

val thm =  @{thm nonzero_mult_divide_cancel_right};

val r = Thm.prop_of thm;

val tm = @{term "x*2 / 2::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 (ProofContext.pretty_term_abbrev @{context} r');

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

(*}*)

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

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

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

(*ML {*)

"===== 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 with Isabelle2009-1 only";

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

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

"----- 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 with Isabelle2009-1 only";

"----- ordered rewriting";

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

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

else error "rewrite.sml diff.behav. in ord.rewr. with Isabelle2009-1 only";

val NONE = (rewrite_ thy tord e_rls false thm tm)

  handle _ => error "rewrite.sml diff.behav. in rewriting with Isabelle2009-1 only";

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

Pretty.writeln (ProofContext.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 with Isabelle2009-1 only";

(*}*)

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

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

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

(*ML {*)

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

val thy = @{theory Complex_Main};

val ctxt = @{context};

val thm =  @{thm nonzero_mult_divide_cancel_right};

val rule = Thm.prop_of thm;

val tm = @{term "x*2 / 2::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 tm = @{term "x*y / y::real"};

val SOME (rew,asm) = (rewrite_ thy dummy_ord e_rls false thm tm)

  handle _ => error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only a";

if rew = @{term "x::real"} then ()

else error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only b";

if HOLogic.dest_Trueprop (hd asm) = @{term "~ y = (0::real)"} then ()

else error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only c";

"----- conditional rewriting immediately: can only be done with Isabelle numerals\

\because erls cannot handle them yet.";

(*}*)

"----------- rewrite_terms_  -------------------------------------";

"----------- rewrite_terms_  -------------------------------------";

"----------- rewrite_terms_  -------------------------------------";

val subte = [str2term"x = 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 subte t;

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

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

val subte = [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 subte t;

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

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

val subte = [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 subte t;

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

else raise 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 raise error "rewrite.sml rewrite_inst_ bdvs";

trace_rewrite:=true;

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