neuper@37871: (* tests for ME/rewrite.sml
neuper@37871:    TODO.WN0509 collect typical tests from systest here !!!!!
neuper@37871:    author: Walther Neuper 050908
neuper@37871:    (c) copyright due to lincense terms.
neuper@37871: 
neuper@37871: use"../smltest/Scripts/rewrite.sml";
neuper@37871: use"rewrite.sml";
neuper@37871: *)
neuper@37871: 
neuper@37871: "-----------------------------------------------------------------";
neuper@37871: "table of contents -----------------------------------------------";
neuper@37871: "-----------------------------------------------------------------";
neuper@37871: "----------- assemble rewrite ------------------------------------";
neuper@37871: "----------- test rewriting without Isac's thys ------------------";
neuper@37871: "----------- conditional rewriting without Isac's thys -----------";
neuper@37871: "----------- rewrite_terms_  -------------------------------------";
neuper@37871: "----------- rewrite_inst_ bdvs ----------------------------------";
neuper@37871: "-----------------------------------------------------------------";
neuper@37871: "-----------------------------------------------------------------";
neuper@37871: "-----------------------------------------------------------------";
neuper@37871: 
neuper@37871: "----------- assemble rewrite ------------------------------------";
neuper@37871: "----------- assemble rewrite ------------------------------------";
neuper@37871: "----------- assemble rewrite ------------------------------------";
neuper@37871: (*ML {**)
neuper@37871: "===== rewriting by thm with 'a";
neuper@37871: show_types := true;
neuper@37871: val thy = @{theory Complex_Main};
neuper@37871: val ctxt = @{context};
neuper@37871: val thm = @{thm add_commute};
neuper@37871: val t = (term_of o the) (parse thy "((r + u) + t) + s");
neuper@37871: "----- from old: fun rewrite__";
neuper@37871: val bdv = [];
neuper@37871: val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
neuper@37871: "----- from old: and rew_sub";
neuper@37871: val (lhs,rhs) = (dest_equals' o strip_trueprop 
neuper@37871:    	      o Logic.strip_imp_concl) r;
neuper@37871: (* old
neuper@37871: val insts = Pattern.match thy (lhs,t) (Vartab.empty, Vartab.empty);*)
neuper@37871: "----- fun match_rew in Pure/pattern.ML";
neuper@37871: val rtm = the_default rhs (Term.rename_abs lhs t rhs);
neuper@37871: 
neuper@37871: tracing(Syntax.string_of_term ctxt rtm);
neuper@37871: tracing(Syntax.string_of_term ctxt lhs);
neuper@37871: tracing(Syntax.string_of_term ctxt t);
neuper@37871: 
neuper@37871: (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
neuper@37871: val (rew, rhs) = (Envir.subst_term 
neuper@37871:   (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
neuper@37871: (*lookup in isabelle?trace?response...*)
neuper@37871: writeln(Syntax.string_of_term ctxt rew);
neuper@37871: writeln(Syntax.string_of_term ctxt rhs);
neuper@37871: (*}
neuper@37871: ML {*)
neuper@37871: "===== rewriting: prep insertion into rew_sub";
neuper@37871: val thy = @{theory Complex_Main};
neuper@37871: val ctxt = @{context};
neuper@37871: val thm =  @{thm nonzero_mult_divide_cancel_right};
neuper@37871: val r = Thm.prop_of thm;
neuper@37871: val tm = @{term "x*2 / 2::real"};
neuper@37871: "----- and rew_sub";
neuper@37871: val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
neuper@37871:                   o Logic.strip_imp_concl) r;
neuper@37871: val r' = Envir.subst_term (Pattern.match thy (lhs, tm) 
neuper@37871:                                 (Vartab.empty, Vartab.empty)) r;
neuper@37871: val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
neuper@37871: val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
neuper@37871:             o Logic.strip_imp_concl) r';
neuper@37871: 
neuper@37871: (*is displayed on top of <response> buffer...*)
neuper@37871: Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
neuper@37871: Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
neuper@37871: (*}*)
neuper@37871: 
neuper@37871: "----------- test rewriting without Isac's thys ------------------";
neuper@37871: "----------- test rewriting without Isac's thys ------------------";
neuper@37871: "----------- test rewriting without Isac's thys ------------------";
neuper@37871: (*ML {*)
neuper@37871: "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
neuper@37871: val thy = @{theory Complex_Main};
neuper@37871: val ctxt = @{context};
neuper@37871: val thm =  @{thm add_commute};
neuper@37871: val tm = @{term "x + y*z::real"};
neuper@37871: 
neuper@37871: val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
neuper@37871:   handle _ => error "rewrite.sml diff.behav. in rewriting with Isabelle2009-1 only";
neuper@37871: (*is displayed on _TOP_ of <response> buffer...*)
neuper@37871: Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
neuper@37871: 
neuper@37871: "----- rewriting a subterm";
neuper@37871: val tm = @{term "w*(x + y*z)::real"};
neuper@37871: 
neuper@37871: val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
neuper@37871:   handle _ => error "rewrite.sml diff.behav. in rew_sub with Isabelle2009-1 only";
neuper@37871: 
neuper@37871: "----- ordered rewriting";
neuper@37871: fun tord (_:subst) pp = TermOrd.termless pp;
neuper@37871: if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
neuper@37871: else error "rewrite.sml diff.behav. in ord.rewr. with Isabelle2009-1 only";
neuper@37871: 
neuper@37871: val NONE = (rewrite_ thy tord e_rls false thm tm)
neuper@37871:   handle _ => error "rewrite.sml diff.behav. in rewriting with Isabelle2009-1 only";
neuper@37871: (*is displayed on _TOP_ of <response> buffer...*)
neuper@37871: Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
neuper@37871: 
neuper@37871: val tm = @{term "x*y + z::real"};
neuper@37871: val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
neuper@37871:   handle _ => error "rewrite.sml diff.behav. in rewriting with Isabelle2009-1 only";
neuper@37871: 
neuper@37871: 
neuper@37871: (*}*)
neuper@37871: 
neuper@37871: "----------- conditional rewriting without Isac's thys -----------";
neuper@37871: "----------- conditional rewriting without Isac's thys -----------";
neuper@37871: "----------- conditional rewriting without Isac's thys -----------";
neuper@37871: (*ML {*)
neuper@37871: "===== prepr cond.rew. with Pattern.match";
neuper@37871: val thy = @{theory Complex_Main};
neuper@37871: val ctxt = @{context};
neuper@37871: val thm =  @{thm nonzero_mult_divide_cancel_right};
neuper@37871: val rule = Thm.prop_of thm;
neuper@37871: val tm = @{term "x*2 / 2::real"};
neuper@37871: 
neuper@37871: val prem = Logic.strip_imp_prems rule;
neuper@37871: val nps = Logic.count_prems rule;
neuper@37871: val prems = Logic.strip_prems (nps, [], rule);
neuper@37871: 
neuper@37871: val eq = Logic.strip_imp_concl rule;
neuper@37871: val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
neuper@37871: 
neuper@37871: val mtcs = Pattern.match thy (lhs, tm) (Vartab.empty, Vartab.empty);
neuper@37871: val rule' = Envir.subst_term mtcs rule;
neuper@37871: 
neuper@37871: val prems' = (fst o Logic.strip_prems) 
neuper@37871:               (Logic.count_prems rule', [], rule');
neuper@37871: val rhs' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
neuper@37871:             o Logic.strip_imp_concl) rule';
neuper@37871: 
neuper@37871: "----- conditional rewriting creating an assumption";
neuper@37871: "----- conditional rewriting creating an assumption";
neuper@37871: val tm = @{term "x*y / y::real"};
neuper@37871: val SOME (rew,asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
neuper@37871:   handle _ => error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only a";
neuper@37871: 
neuper@37871: if rew = @{term "x::real"} then ()
neuper@37871: else error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only b";
neuper@37871: 
neuper@37871: if HOLogic.dest_Trueprop (hd asm) = @{term "~ y = (0::real)"} then ()
neuper@37871: else error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only c";
neuper@37871: 
neuper@37871: "----- conditional rewriting immediately: can only be done with Isabelle numerals\
neuper@37871: \because erls cannot handle them yet.";
neuper@37871: (*}*)
neuper@37871: 
neuper@37871: 
neuper@37871: "----------- rewrite_terms_  -------------------------------------";
neuper@37871: "----------- rewrite_terms_  -------------------------------------";
neuper@37871: "----------- rewrite_terms_  -------------------------------------";
neuper@37871: val subte = [str2term"x = 0"];
neuper@37871: val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
neuper@37871: val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
neuper@37871: if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
neuper@37871: else raise error "rewrite.sml rewrite_terms_ [x = 0]";
neuper@37871: 
neuper@37871: val subte = [str2term"M_b 0 = 0"];
neuper@37871: val t = str2term"M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
neuper@37871: val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
neuper@37871: if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
neuper@37871: else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
neuper@37871: 
neuper@37871: val subte = [str2term"x = 0", str2term"M_b 0 = 0"];
neuper@37871: val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
neuper@37871: val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
neuper@37871: if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
neuper@37871: else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
neuper@37871: 
neuper@37871: 
neuper@37871: "----------- rewrite_inst_ bdvs ----------------------------------";
neuper@37871: "----------- rewrite_inst_ bdvs ----------------------------------";
neuper@37871: "----------- rewrite_inst_ bdvs ----------------------------------";
neuper@37871: (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
neuper@37871: val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
neuper@37871: val bdvs = [(str2term"bdv_1",str2term"c"),
neuper@37871: 	    (str2term"bdv_2",str2term"c_2"),
neuper@37871: 	    (str2term"bdv_3",str2term"c_3"),
neuper@37871: 	    (str2term"bdv_4",str2term"c_4")];
neuper@37871: (*------------ outcommented WN071210, after inclusion into ROOT.ML 
neuper@37871: val Some (t,_) = 
neuper@37871:     rewrite_inst_ thy e_rew_ord 
neuper@37871: 		  (append_rls "erls_isolate_bdvs" e_rls 
neuper@37871: 			      [(Calc ("EqSystem.occur'_exactly'_in", 
neuper@37871: 				      eval_occur_exactly_in 
neuper@37871: 					  "#eval_occur_exactly_in_"))
neuper@37871: 			       ]) 
neuper@37871: 		  false bdvs (num_str separate_bdvs_add) t;
neuper@37871: (writeln o term2str) t;
neuper@37871: if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
neuper@37871: then () else raise error "rewrite.sml rewrite_inst_ bdvs";
neuper@37871: trace_rewrite:=true;
neuper@37871: trace_rewrite:=false;--------------------------------------------*)
neuper@37871: