neuper@38036: (* Title: tests for ProgLang/rewrite.sml
neuper@37906:    TODO.WN0509 collect typical tests from systest here !!!!!
neuper@38036:    Author: Walther Neuper 050908
neuper@37906:    (c) copyright due to lincense terms.
neuper@37906: 
neuper@38022: 12345678901234567890123456789012345678901234567890123456789012345678901234567890
neuper@38022:         10        20        30        40        50        60        70        80
neuper@37906: *)
neuper@37906: 
neuper@38022: "--------------------------------------------------------";
neuper@38022: "table of contents --------------------------------------";
neuper@38022: "--------------------------------------------------------";
neuper@38022: "----------- assemble rewrite ---------------------------";
neuper@38022: "----------- test rewriting without Isac's thys ---------";
neuper@38022: "----------- conditional rewriting without Isac's thys --";
neuper@38022: "----------- step through 'and rew_sub': ----------------";
neuper@38025: "----------- step through 'fun rewrite_terms_'  ---------";
neuper@38022: "----------- rewrite_inst_ bdvs -------------------------";
neuper@38022: "----------- check diff 2002--2009-3 --------------------";
neuper@38036: "----------- fun app_rev, Rrls, prepat ------------------";
neuper@38022: "--------------------------------------------------------";
neuper@38022: "--------------------------------------------------------";
neuper@38022: "--------------------------------------------------------";
neuper@37906: 
neuper@38036: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
neuper@38036: 
neuper@38022: "----------- assemble rewrite ---------------------------";
neuper@38022: "----------- assemble rewrite ---------------------------";
neuper@38022: "----------- assemble rewrite ---------------------------";
neuper@37906: "===== rewriting by thm with 'a";
neuper@37906: show_types := true;
neuper@37906: val thy = @{theory Complex_Main};
neuper@37906: val ctxt = @{context};
neuper@37906: val thm = @{thm add_commute};
neuper@37906: val t = (term_of o the) (parse thy "((r + u) + t) + s");
neuper@37906: "----- from old: fun rewrite__";
neuper@37906: val bdv = [];
neuper@37906: val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
neuper@37906: "----- from old: and rew_sub";
neuper@37906: val (lhs,rhs) = (dest_equals' o strip_trueprop 
neuper@37906:    	      o Logic.strip_imp_concl) r;
neuper@37906: (* old
neuper@37906: val insts = Pattern.match thy (lhs,t) (Vartab.empty, Vartab.empty);*)
neuper@37906: "----- fun match_rew in Pure/pattern.ML";
neuper@37906: val rtm = the_default rhs (Term.rename_abs lhs t rhs);
neuper@37906: 
neuper@38022: writeln(Syntax.string_of_term ctxt rtm);
neuper@38022: writeln(Syntax.string_of_term ctxt lhs);
neuper@38022: writeln(Syntax.string_of_term ctxt t);
neuper@37906: 
neuper@37906: (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
neuper@37906: val (rew, rhs) = (Envir.subst_term 
neuper@37906:   (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
neuper@37906: (*lookup in isabelle?trace?response...*)
neuper@37906: writeln(Syntax.string_of_term ctxt rew);
neuper@37906: writeln(Syntax.string_of_term ctxt rhs);
neuper@38022: 
neuper@37906: "===== rewriting: prep insertion into rew_sub";
neuper@37906: val thy = @{theory Complex_Main};
neuper@37906: val ctxt = @{context};
neuper@37906: val thm =  @{thm nonzero_mult_divide_cancel_right};
neuper@37906: val r = Thm.prop_of thm;
neuper@37906: val tm = @{term "x*2 / 2::real"};
neuper@37906: "----- and rew_sub";
neuper@37906: val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
neuper@37906:                   o Logic.strip_imp_concl) r;
neuper@37906: val r' = Envir.subst_term (Pattern.match thy (lhs, tm) 
neuper@37906:                                 (Vartab.empty, Vartab.empty)) r;
neuper@37906: val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
neuper@37906: val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
neuper@37906:             o Logic.strip_imp_concl) r';
neuper@37906: 
neuper@37906: (*is displayed on top of <response> buffer...*)
neuper@37906: Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
neuper@37906: Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
neuper@37906: (*}*)
neuper@37906: 
neuper@38022: "----------- test rewriting without Isac's thys ---------";
neuper@38022: "----------- test rewriting without Isac's thys ---------";
neuper@38022: "----------- test rewriting without Isac's thys ---------";
neuper@38022: 
neuper@37906: "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
neuper@37906: val thy = @{theory Complex_Main};
neuper@37906: val ctxt = @{context};
neuper@37906: val thm =  @{thm add_commute};
neuper@37906: val tm = @{term "x + y*z::real"};
neuper@37906: 
neuper@37906: val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
neuper@38022:   handle _ => error "rewrite.sml diff.behav. in rewriting";
neuper@37906: (*is displayed on _TOP_ of <response> buffer...*)
neuper@37906: Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
neuper@38022: if r = @{term "y*z + x::real"}
neuper@38022: then () else error "rewrite.sml diff.result in rewriting";
neuper@37906: 
neuper@37906: "----- rewriting a subterm";
neuper@37906: val tm = @{term "w*(x + y*z)::real"};
neuper@37906: 
neuper@37906: val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
neuper@38022:   handle _ => error "rewrite.sml diff.behav. in rew_sub";
neuper@37906: 
neuper@37906: "----- ordered rewriting";
neuper@38022: fun tord (_:subst) pp = Term_Ord.termless pp;
neuper@37906: if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
neuper@38022: else error "rewrite.sml diff.behav. in ord.rewr.";
neuper@37906: 
neuper@37906: val NONE = (rewrite_ thy tord e_rls false thm tm)
neuper@38022:   handle _ => error "rewrite.sml diff.behav. in rewriting";
neuper@37906: (*is displayed on _TOP_ of <response> buffer...*)
neuper@37906: Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
neuper@37906: 
neuper@37906: val tm = @{term "x*y + z::real"};
neuper@37906: val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
neuper@38022:   handle _ => error "rewrite.sml diff.behav. in rewriting";
neuper@37906: 
neuper@37906: 
neuper@38022: "----------- conditional rewriting without Isac's thys --";
neuper@38022: "----------- conditional rewriting without Isac's thys --";
neuper@38022: "----------- conditional rewriting without Isac's thys --";
neuper@37906: (*ML {*)
neuper@37906: "===== prepr cond.rew. with Pattern.match";
neuper@37906: val thy = @{theory Complex_Main};
neuper@37906: val ctxt = @{context};
neuper@37906: val thm =  @{thm nonzero_mult_divide_cancel_right};
neuper@37906: val rule = Thm.prop_of thm;
neuper@37906: val tm = @{term "x*2 / 2::real"};
neuper@37906: 
neuper@37906: val prem = Logic.strip_imp_prems rule;
neuper@37906: val nps = Logic.count_prems rule;
neuper@37906: val prems = Logic.strip_prems (nps, [], rule);
neuper@37906: 
neuper@37906: val eq = Logic.strip_imp_concl rule;
neuper@37906: val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
neuper@37906: 
neuper@37906: val mtcs = Pattern.match thy (lhs, tm) (Vartab.empty, Vartab.empty);
neuper@37906: val rule' = Envir.subst_term mtcs rule;
neuper@37906: 
neuper@37906: val prems' = (fst o Logic.strip_prems) 
neuper@37906:               (Logic.count_prems rule', [], rule');
neuper@37906: val rhs' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
neuper@37906:             o Logic.strip_imp_concl) rule';
neuper@37906: 
neuper@37906: "----- conditional rewriting creating an assumption";
neuper@37906: "----- conditional rewriting creating an assumption";
neuper@37906: val tm = @{term "x*y / y::real"};
neuper@38022: val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
neuper@38022:   handle _ => error "rewrite.sml diff.behav. in cond.rew.";
neuper@37906: 
neuper@38022: if rew = @{term "x::real"} then () (* the rewrite is _NO_ Trueprop *)
neuper@38022: else error "rewrite.sml diff.result in cond.rew.";
neuper@37906: 
neuper@38022: if hd asm = @{term "~ y = (0::real)"} (* dropped Trueprop $ ...*)
neuper@38022: then () else error "rewrite.sml diff.asm in cond.rew.";
neuper@38022: "----- conditional rewriting immediately: can only be done with ";
neuper@38022: "------Isabelle numerals, because erls cannot handle them yet.";
neuper@37906: 
neuper@37906: 
neuper@38022: "----------- step through 'and rew_sub': ----------------";
neuper@38022: "----------- step through 'and rew_sub': ----------------";
neuper@38022: "----------- step through 'and rew_sub': ----------------";
neuper@38022: (*and make asms without Trueprop, beginning with the result:*)
neuper@38025: val tm = @{term "x*y / y::real"};
neuper@38022: val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
neuper@38022: show_types := false;
neuper@38022: "----- evaluate arguments";
neuper@38022: val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 
neuper@38022:     (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
neuper@38022: "----- step 1: lhs, rhs of rule";
neuper@38022:      val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
neuper@38022:                        o Logic.strip_imp_concl) r;
neuper@38025: term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
neuper@38022: term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a";
neuper@38022: "----- step 2: the rule instantiated";
neuper@38025:      val r' = Envir.subst_term 
neuper@38025:                   (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
neuper@38022: term2str r' = "y ~= 0 ==> x * y / y = x";
neuper@38022: "----- step 3: get the (instantiated) assumption(s)";
neuper@38022:      val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
neuper@38022: term2str (hd p') = "y ~= 0";
neuper@38022: "=====vvv make asms without Trueprop ---vvv";
neuper@38022:      val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) 
neuper@38022:                                              (Logic.count_prems r', [], r'));
neuper@38022: case p' of
neuper@38022:     [Const ("Not", _) $ (Const ("op =", _) $ Free ("y", _) $
neuper@38022:                                Const ("Groups.zero_class.zero", _))] => ()
neuper@38022:   | _ => error "rewrite.sml assumption changed";
neuper@38022: "=====^^^ make asms without Trueprop ---^^^";
neuper@38022: "----- step 4: get the (instantiated) rhs";
neuper@38022:      val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
neuper@38022:                o Logic.strip_imp_concl) r';
neuper@38022: term2str t' = "x";
neuper@37906: 
neuper@38025: "----------- step through 'fun rewrite_terms_'  ---------";
neuper@38025: "----------- step through 'fun rewrite_terms_'  ---------";
neuper@38025: "----------- step through 'fun rewrite_terms_'  ---------";
neuper@38025: "----- step 0: args for rewrite_terms_, local fun";
neuper@38025: val (thy, ord, erls, equs, t) =
neuper@38025:     (theory "Biegelinie", dummy_ord, Erls, [str2term "x = 0"],
neuper@38025:      str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
neuper@38025: "----- step 1: args for rew_";
neuper@38025: val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
neuper@38025: "----- step 2: rew_sub";
neuper@38025: rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t;
neuper@38025: "----- step 3: step through rew_sub -- inefficient: goes into subterms";
neuper@38025: 
neuper@38025: 
neuper@38025: val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
neuper@38025: writeln "----------- rewrite_terms_  1---------------------------";
neuper@37906: if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
neuper@38031: else error "rewrite.sml rewrite_terms_ [x = 0]";
neuper@37906: 
neuper@38025: val equs = [str2term "M_b 0 = 0"];
neuper@38025: val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
neuper@38025: val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
neuper@38025: writeln "----------- rewrite_terms_  2---------------------------";
neuper@37906: if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
neuper@38031: else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
neuper@37906: 
neuper@38025: val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
neuper@38025: val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
neuper@38025: val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
neuper@38025: writeln "----------- rewrite_terms_  3---------------------------";
neuper@37906: if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
neuper@38031: else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
neuper@37906: 
neuper@37906: 
neuper@38022: "----------- rewrite_inst_ bdvs -------------------------";
neuper@38022: "----------- rewrite_inst_ bdvs -------------------------";
neuper@38022: "----------- rewrite_inst_ bdvs -------------------------";
neuper@37906: (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
neuper@37906: val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
neuper@37906: val bdvs = [(str2term"bdv_1",str2term"c"),
neuper@37906: 	    (str2term"bdv_2",str2term"c_2"),
neuper@37906: 	    (str2term"bdv_3",str2term"c_3"),
neuper@37906: 	    (str2term"bdv_4",str2term"c_4")];
neuper@37906: (*------------ outcommented WN071210, after inclusion into ROOT.ML 
neuper@37926: val SOME (t,_) = 
neuper@37906:     rewrite_inst_ thy e_rew_ord 
neuper@37906: 		  (append_rls "erls_isolate_bdvs" e_rls 
neuper@37906: 			      [(Calc ("EqSystem.occur'_exactly'_in", 
neuper@37906: 				      eval_occur_exactly_in 
neuper@37906: 					  "#eval_occur_exactly_in_"))
neuper@37906: 			       ]) 
neuper@37967: 		  false bdvs (num_str @{separate_bdvs_add) t;
neuper@37906: (writeln o term2str) t;
neuper@37906: if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
neuper@38031: then () else error "rewrite.sml rewrite_inst_ bdvs";
neuper@37906: trace_rewrite:=true;
neuper@37906: trace_rewrite:=false;--------------------------------------------*)
neuper@37906: 
neuper@38025: 
neuper@38022: "----------- check diff 2002--2009-3 --------------------";
neuper@38022: "----------- check diff 2002--2009-3 --------------------";
neuper@38022: "----------- check diff 2002--2009-3 --------------------";
neuper@38022: (*----- 2002 -------------------------------------------------------------------
neuper@38022: #  rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
neuper@38022: q_0 * x ^^^ 2 / 2)
neuper@38022: ##  rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
neuper@38022: / 2)
neuper@38022: ###  try thm: real_diff_minus
neuper@38022: ###  try thm: sym_real_mult_minus1
neuper@38022: ##  rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
neuper@38022: / 2)
neuper@38022: ###  try thm: rat_mult_poly_l
neuper@38022: ###  try thm: rat_mult_poly_r
neuper@38022: ####  eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
neuper@38022: ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
neuper@38022:     1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
neuper@38022: #####  rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
neuper@38022: is_polyexp
neuper@38022: ######  try calc: Poly.is'_polyexp'
neuper@38022: ======  calc. to: False
neuper@38022: ######  try calc: Poly.is'_polyexp'
neuper@38022: ######  try calc: Poly.is'_polyexp'
neuper@38022: ####  asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
neuper@38022: ----- 2002 NONE rewrite --------------------------------------------------------
neuper@38022: ----- 2009 should maintain this behaviour, but: --------------------------------
neuper@38022: #  rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
neuper@38022: ##  rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
neuper@38022: ###  try thm: real_diff_minus
neuper@38022: ###  try thm: sym_real_mult_minus1
neuper@38022: ##  rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
neuper@38022: ###  try thm: rat_mult_poly_l
neuper@38022: ###  try thm: rat_mult_poly_r
neuper@38022: ####  eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
neuper@38022: ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
neuper@38022:     1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
neuper@38022: #####  rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
neuper@38022: ######  try calc: Poly.is'_polyexp'
neuper@38022: ======  calc. to: False
neuper@38022: ######  try calc: Poly.is'_polyexp'
neuper@38022: ######  try calc: Poly.is'_polyexp'
neuper@38022: ####  asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]   stored: ["False"]
neuper@38022: ===  rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
neuper@38022: ----- 2009 -------------------------------------------------------------------*)
neuper@38022: 
neuper@38022: (*the situation as was before repair (asm without Trueprop) is outcommented*)
neuper@38022: val thy = theory "Isac";
neuper@38022: "===== example which raised the problem =================";
neuper@38022: val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
neuper@38022: "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
neuper@38022: val subs = [(str2term "bdv", str2term "x")];
neuper@38022: val rls = norm_Rational_noadd_fractions;
neuper@38022: val NONE (*SOME (t', _)*) = rewrite_set_inst_ thy true subs rls t;
neuper@38022: "----- rewrite_ rat_mult_poly_r--------------------------";
neuper@38022: val thm = @{thm rat_mult_poly_r};
neuper@38022:          "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
neuper@38022: val erls = append_rls "e_rls-is_polyexp" e_rls 
neuper@38022:                       [Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
neuper@38022: val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
neuper@38022: (*t' = t''; (*false because of further rewrites in t'*)*)
neuper@38022: "----- rew_sub  --------------------------------";
neuper@38022: val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
neuper@38022: (*t'' = t'''; (*true*)*)
neuper@38022: "----- rewrite_set_ erls --------------------------------";
neuper@38022: val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
neuper@38022: val NONE = rewrite_set_ thy true erls cond; 
neuper@38022: (* ^^^^^ goes with '======  calc. to: False' above from beginning*)
neuper@38022: 
neuper@38022: writeln "===== maximally simplified example =====================";
neuper@38022: val t = @{term "a / b * (x / x ^^^ 2)"};
neuper@38022:          "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
neuper@38022: writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
neuper@38022: val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
neuper@38022: term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
neuper@38022: (*checked visually: trace_rewrite looks like above for 2009*)
neuper@38022: 
neuper@38022: trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
neuper@38022: show_types := false;
neuper@38022: writeln "----- rewrite_ rat_mult_poly_r--------------------------";
neuper@38022: val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
neuper@38022: (*t' = t''; (*false because of further rewrites in t'*)*)
neuper@38022: writeln "----- rew_sub  --------------------------------";
neuper@38022: val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
neuper@38022: (*t'' = t'''; (*true*)*)
neuper@38022: writeln "----- rewrite_set_ erls --------------------------------";
neuper@38022: val cond = @{term "(x / x ^^^ 2)"};
neuper@38022: val NONE = rewrite_set_ thy true erls cond; 
neuper@38022: (* ^^^^^ goes with '======  calc. to: False' above from beginning*)
neuper@38022: trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
neuper@38022: "--------------------------------------------------------";
neuper@38025: 
neuper@38036: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
neuper@38025: 
neuper@38036: "----------- fun app_rev, Rrls, prepat ------------------";
neuper@38036: "----------- fun app_rev, Rrls, prepat ------------------";
neuper@38036: "----------- fun app_rev, Rrls, prepat ------------------";
neuper@38036: (* Christian Urban, 101001 
neuper@38036: theory Test
neuper@38036: imports Main Complex
neuper@38036: begin
neuper@38036: 
neuper@38036: ML {*
neuper@38036: let
neuper@38036:   val parser = Args.context -- Scan.lift Args.name_source
neuper@38036:   fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
neuper@38036:   |> ML_Syntax.print_term |> ML_Syntax.atomic
neuper@38036: in
neuper@38036:   ML_Antiquote.inline "term_pat" (parser >> term_pat)
neuper@38036: end
neuper@38036: *}
neuper@38036: 
neuper@38036: ML {*
neuper@38036:   val t = @{term "a + b * x = (0 ::real)"};
neuper@38036:   val pat = @{term_pat "?l = (?r ::real)"};
neuper@38036:   val precond = @{term_pat "is_polynomial (?l::real)"};
neuper@38036:   val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
neuper@38036: *}
neuper@38036: 
neuper@38036: ML {*
neuper@38036:   Envir.subst_term inst precond
neuper@38036:   |> Syntax.string_of_term @{context}
neuper@38036:   |> writeln
neuper@38036: *}
neuper@38036: end *)
neuper@38036: val t = @{term "a + b * x = (0 ::real)"};
neuper@38036: val pat = parse_patt thy "?l = (?r ::real)";
neuper@38036: val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
neuper@38036: val precond = parse_patt thy " (?l::real) is_expanded"; 
neuper@38036: 
neuper@38036: val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
neuper@38036: val preinst = Envir.subst_term inst precond;
neuper@38036: term2str preinst;
neuper@38036: 
neuper@38036: "===== Rational.thy: cancel ===";
neuper@38036: (* pat matched with the current term gives an environment 
neuper@38036:    (or not: hen the Rrls not applied);
neuper@38036:    if pre1 and pre2 evaluate to HOLogic.true_const in this environment,
neuper@38036:    then the Rrls is applied. *)
neuper@38036: val t = str2term "(a + b) / c ::real";
neuper@38036: val pat = parse_patt thy "?r / ?s ::real";
neuper@38036: val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
neuper@38036: val prepat = [(pres, pat)];
neuper@38036: val erls = rational_erls;
neuper@38036: (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
neuper@38036: 
neuper@38036: val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
neuper@38036: val asms = map (Envir.subst_term subst) pres;
neuper@38036: if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
neuper@38036: then () else error "rewrite.sml: prepat cancel subst";
neuper@38036: if ([], true) = eval__true thy 0 asms [] erls
neuper@38036: then () else error "rewrite.sml: prepat cancel eval__true";
neuper@38036: 
neuper@38036: "===== Rational.thy: common_nominator_p ===";
neuper@38036: (* if each pat* matches with the current term, the Rrls is applied
neuper@38036:    (there are no preconditions to be checked, they are HOLogic.true_const) *)
neuper@38036: val t = str2term "a / b + 1 / 2";
neuper@38036: val pat = parse_patt thy "?r / ?s + ?u / ?v";
neuper@38036: val pres = [HOLogic.true_const];
neuper@38036: val prepat = [(pres, pat)];
neuper@38036: val erls = rational_erls;
neuper@38036: (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
neuper@38036: 
neuper@38036: val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
neuper@38036: if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
neuper@38036: then () else error "rewrite.sml: prepat common_nominator_p";
neuper@38036: 
neuper@38036: "===== Poly.thy: order_mult_ ===";
neuper@38036:           (* ?p matched with the current term gives an environment,
neuper@38036:              which evaluates (the instantiated) "p is_multUnordered" to true*)
neuper@38036: val t = str2term "x^^^2 * x";
neuper@38036: val pat = parse_patt thy "?p :: real"
neuper@38036: val pres = [parse_patt thy "?p is_multUnordered"];
neuper@38036: val prepat = [(pres, pat)];
neuper@38036: val erls = append_rls "e_rls-is_multUnordered" e_rls
neuper@38036: 		      [Calc ("Poly.is'_multUnordered", 
neuper@38036:                              eval_is_multUnordered "")];
neuper@38036: 
neuper@38036: val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
neuper@38036: val asms = map (Envir.subst_term subst) pres;
neuper@38036: if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
neuper@38036: then () else error "rewrite.sml: prepat order_mult_ subst";
neuper@38036: if ([], true) = eval__true thy 0 asms [] erls
neuper@38036: then () else error "rewrite.sml: prepat order_mult_ eval__true";
neuper@38036: 
neuper@38036: 
neuper@38036: (*========== inhibit exn =======================================================
neuper@38036: ============ inhibit exn =====================================================*)
neuper@38025: 
neuper@38030: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
neuper@38030: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)