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 ---------------------------"; wneuper@59382: "----------- test rewriting without Isac session --------"; wneuper@59382: "----------- conditional rewriting without Isac session -"; 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@38039: "----------- compare all prepat's existing 2010 ---------"; neuper@38039: "----------- fun app_rev, Rrls, -------------------------"; neuper@42223: "----------- 2011 thms with axclasses -------------------"; neuper@42394: "----------- repair NO asms from rls RatEq_eliminate ----"; wneuper@59110: "----------- fun assoc_thm' -----------------------------"; wneuper@59252: "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; wneuper@59381: "----------- fun mk_thm ------------------------------------------------------------------------"; neuper@38022: "--------------------------------------------------------"; neuper@38022: "--------------------------------------------------------"; neuper@38022: "--------------------------------------------------------"; neuper@37906: neuper@38036: neuper@38022: "----------- assemble rewrite ---------------------------"; neuper@38022: "----------- assemble rewrite ---------------------------"; neuper@38022: "----------- assemble rewrite ---------------------------"; neuper@37906: "===== rewriting by thm with 'a"; neuper@41924: (*show_types := true;*) akargl@42188: neuper@37906: val thy = @{theory Complex_Main}; neuper@37906: val ctxt = @{context}; wneuper@59112: val thm = @{thm add.commute}; wneuper@59188: val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s"); neuper@37906: "----- from old: fun rewrite__"; neuper@37906: val bdv = []; wneuper@59188: val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm); neuper@37906: "----- from old: and rew_sub"; wneuper@59395: val (LHS,RHS) = (dest_equals o strip_trueprop neuper@37906: o Logic.strip_imp_concl) r; neuper@37906: (* old neuper@41942: val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*) neuper@37906: "----- fun match_rew in Pure/pattern.ML"; neuper@41942: val rtm = the_default RHS (Term.rename_abs LHS t RHS); neuper@37906: neuper@38022: writeln(Syntax.string_of_term ctxt rtm); neuper@41942: writeln(Syntax.string_of_term ctxt LHS); neuper@38022: writeln(Syntax.string_of_term ctxt t); neuper@37906: neuper@41942: (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)); neuper@41942: val (rew, RHS) = (Envir.subst_term neuper@41942: (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@41942: writeln(Syntax.string_of_term ctxt RHS); neuper@37906: "===== rewriting: prep insertion into rew_sub"; neuper@37906: val thy = @{theory Complex_Main}; neuper@37906: val ctxt = @{context}; wneuper@59358: val thm = @{thm nonzero_divide_mult_cancel_right}; neuper@37906: val r = Thm.prop_of thm; wneuper@59358: val tm = @{term "x / (2 * x)::real"}; neuper@37906: "----- and rew_sub"; neuper@41942: val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop neuper@37906: o Logic.strip_imp_concl) r; neuper@41942: 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 buffer...*) neuper@48761: Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r'); neuper@48761: Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t'); akargl@42188: (**) 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}; wneuper@59112: 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 buffer...*) neuper@48761: Pretty.writeln (Proof_Context.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 buffer...*) neuper@48761: Pretty.writeln (Proof_Context.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 --"; akargl@42224: neuper@37906: "===== prepr cond.rew. with Pattern.match"; neuper@37906: val thy = @{theory Complex_Main}; neuper@37906: val ctxt = @{context}; wneuper@59358: val thm = @{thm nonzero_divide_mult_cancel_right}; neuper@37906: val rule = Thm.prop_of thm; wneuper@59358: val tm = @{term "x / (2 * x)::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@41942: val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; neuper@37906: neuper@41942: 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@41942: 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"; wneuper@59358: val thm = @{thm nonzero_divide_mult_cancel_right}; wneuper@59358: val tm = @{term "x / (2 * x)::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: wneuper@59358: if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *) neuper@38022: else error "rewrite.sml diff.result in cond.rew."; neuper@37906: wneuper@59358: if hd asm = @{term "x \ (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:*) wneuper@59358: val tm = @{term "x / (2 * x)::real"}; wneuper@59188: val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (Thm.prop_of thm) tm; neuper@41924: (*show_types := false;*) neuper@38022: "----- evaluate arguments"; neuper@38022: val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = wneuper@59188: (thy, 0, [], dummy_ord, e_rls, true, [], (Thm.prop_of thm), tm); neuper@41942: "----- step 1: LHS, RHS of rule"; neuper@41942: val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop neuper@38022: o Logic.strip_imp_concl) r; wneuper@59358: term2str r = "?b \ (0::?'a) \ ?b / (?a * ?b) = (1::?'a) / ?a"; wneuper@59358: term2str LHS = "?b / (?a * ?b)"; term2str RHS = "(1::?'a) / ?a"; neuper@38022: "----- step 2: the rule instantiated"; neuper@38025: val r' = Envir.subst_term neuper@41942: (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r; wneuper@59358: term2str r' = "x \ 0 \ x / (2 * x) = 1 / 2"; neuper@38022: "----- step 3: get the (instantiated) assumption(s)"; neuper@38022: val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r'); wneuper@59358: term2str (hd p') = "x \ 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 wneuper@59358: [Const ("HOL.Not", _) $ (Const ("HOL.eq", _) wneuper@59358: $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => () neuper@38022: | _ => error "rewrite.sml assumption changed"; neuper@38022: "=====^^^ make asms without Trueprop ---^^^"; neuper@41942: "----- 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'; wneuper@59358: term2str t' = "1 / 2"; 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@41928: (@{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"; wneuper@59395: rew_sub thy 1 [] ord erls false [] (HOLogic.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@41928: 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--"; wneuper@59382: val subs = [(@{term "bdv"}, @{term "x"})]; neuper@38022: val rls = norm_Rational_noadd_fractions; wneuper@59112: val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t; wneuper@59112: if term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * 1 * q_0 * x ^^^ 2 / 2)" andalso wneuper@59112: terms2str asms = "[]" then {} wneuper@59112: else error "this was NONE with Isabelle2013-2 ?!?" 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 --------------------------------"; wneuper@59188: val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.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: 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 --------------------------------"; wneuper@59188: val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.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@42201: neuper@38025: neuper@38039: "----------- compare all prepat's existing 2010 ---------"; neuper@38039: "----------- compare all prepat's existing 2010 ---------"; neuper@38039: "----------- compare all prepat's existing 2010 ---------"; neuper@41928: val thy = @{theory "Isac"}; 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@38039: 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@48760: if pre1 and pre2 evaluate to @{term True} 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@52105: "===== Rational.thy: add_fractions_p ==="; neuper@38036: (* if each pat* matches with the current term, the Rrls is applied neuper@48760: (there are no preconditions to be checked, they are @{term True}) *) neuper@38036: val t = str2term "a / b + 1 / 2"; neuper@38036: val pat = parse_patt thy "?r / ?s + ?u / ?v"; neuper@48760: val pres = [@{term True}]; 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@52105: then () else error "rewrite.sml: prepat add_fractions_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@38039: "----------- fun app_rev, Rrls, -------------------------"; neuper@38039: "----------- fun app_rev, Rrls, -------------------------"; neuper@38039: "----------- fun app_rev, Rrls, -------------------------"; neuper@38039: val t = str2term "x^^^2 * x"; neuper@41928: neuper@38039: if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2"; neuper@38039: val tm = str2term "(x^^^2 * x) is_multUnordered"; neuper@41928: eval_is_multUnordered "testid" "" tm thy; neuper@41928: neuper@38039: case eval_is_multUnordered "testid" "" tm thy of neuper@41924: SOME (_, Const ("HOL.Trueprop", _) $ neuper@41922: (Const ("HOL.eq", _) $ neuper@38039: (Const ("Poly.is'_multUnordered", _) $ _) $ neuper@41928: Const ("HOL.True", _))) => () neuper@41928: | _ => error "rewrite.sml diff. eval_is_multUnordered 2b"; neuper@38039: neuper@38039: tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := true; neuper@38039: val SOME (t', _) = rewrite_set_ thy true order_mult_ t; neuper@38039: tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false; neuper@38039: if term2str t' = "x * x ^^^ 2" then () neuper@38039: else error "rewrite.sml Poly.is'_multUnordered doesn't work"; neuper@38039: neuper@38039: (* for achieving the previous result, the following code was taken apart *) neuper@38039: "----- rewrite__set_ ---"; neuper@38039: val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm); neuper@38039: val (t', asm, rew) = app_rev thy (i+1) rrls t; neuper@38039: "----- app_rev ---"; neuper@38039: val (thy, i, rrls, t) = (thy, (i+1), rrls, t); neuper@38039: fun chk_prepat thy erls [] t = true neuper@38039: | chk_prepat thy erls prepat t = neuper@38039: let fun chk (pres, pat) = neuper@38039: (let val subst: Type.tyenv * Envir.tenv = neuper@38039: Pattern.match thy (pat, t) neuper@38039: (Vartab.empty, Vartab.empty) neuper@38039: in snd (eval__true thy (i+1) neuper@38039: (map (Envir.subst_term subst) pres) neuper@38039: [] erls) neuper@38039: end) neuper@38039: handle _ => false neuper@38039: fun scan_ f [] = false (*scan_ NEVER called by []*) neuper@38039: | scan_ f (pp::pps) = if f pp then true neuper@38039: else scan_ f pps; neuper@38039: in scan_ chk prepat end; neuper@38039: neuper@38039: (*.apply the normal_form of a rev-set.*) neuper@38039: fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t = neuper@38039: if chk_prepat thy erls prepat t neuper@38039: then ((*tracing("### app_rev': t = "^(term2str t));*) neuper@38039: normal_form t) neuper@38039: else NONE; neuper@38039: (*fixme val NONE = app_rev' thy rrls t;*) neuper@38039: "----- app_rev' ---"; neuper@38039: val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t); neuper@38039: (*fixme false*) chk_prepat thy erls prepat t; neuper@38039: "----- chk_prepat ---"; neuper@38039: val (thy, erls, prepat, t) = (thy, erls, prepat, t); neuper@38039: fun chk (pres, pat) = neuper@38039: (let val subst: Type.tyenv * Envir.tenv = neuper@38039: Pattern.match thy (pat, t) neuper@38039: (Vartab.empty, Vartab.empty) neuper@38039: in snd (eval__true thy (i+1) neuper@38039: (map (Envir.subst_term subst) pres) neuper@38039: [] erls) neuper@38039: end) neuper@38039: handle _ => false; neuper@38039: fun scan_ f [] = false (*scan_ NEVER called by []*) neuper@38039: | scan_ f (pp::pps) = if f pp then true neuper@38039: else scan_ f pps; neuper@38039: tracing "=== poly.sml: scan_ chk prepat begin"; neuper@38039: scan_ chk prepat; neuper@38039: tracing "=== poly.sml: scan_ chk prepat end"; neuper@38039: neuper@38039: "----- chk ---"; neuper@38039: (*reestablish...*) val t = str2term "x ^^^ 2 * x"; neuper@38039: val [(pres, pat)] = prepat; neuper@38039: val subst: Type.tyenv * Envir.tenv = neuper@38039: Pattern.match thy (pat, t) neuper@38039: (Vartab.empty, Vartab.empty); neuper@38039: neuper@38039: (*fixme: asms = ["p is_multUnordered"]...instantiate*) neuper@38039: "----- eval__true ---"; neuper@38039: val asms = (map (Envir.subst_term subst) pres); neuper@38039: if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then () neuper@38039: else error "rewrite.sml: diff. is_multUnordered, asms"; neuper@38039: val (thy, i, asms, bdv, rls) = neuper@38039: (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"], neuper@38039: [] : (term * term) list, erls); neuper@38039: case eval__true thy i asms bdv rls of neuper@38039: ([], true) => () neuper@38039: | _ => error "rewrite.sml: diff. is_multUnordered, eval__true"; neuper@42223: neuper@42223: "----------- 2011 thms with axclasses -------------------"; neuper@42223: "----------- 2011 thms with axclasses -------------------"; neuper@42223: "----------- 2011 thms with axclasses -------------------"; wneuper@59348: val thm = num_str @{thm div_by_1}; wneuper@59188: val prop = Thm.prop_of thm; neuper@42223: atomty prop; (*Type 'a*) neuper@42223: val t = str2term "(2*x)/1"; (*Type real*) neuper@42223: neuper@42223: val (thy, ro, er, inst) = neuper@42223: (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); neuper@42223: val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*) neuper@42223: neuper@42394: "----------- repair NO asms from rls RatEq_eliminate ----"; neuper@42394: "----------- repair NO asms from rls RatEq_eliminate ----"; neuper@42394: "----------- repair NO asms from rls RatEq_eliminate ----"; neuper@42394: val t = str2term "1 / x = 5"; neuper@42394: trace_rewrite := true; neuper@42394: val SOME (t', asm) = rewrite_ thy e_rew_ord e_rls true @{thm rat_mult_denominator_right} t; neuper@42394: term2str t' = "1 = 5 * x"; neuper@42394: terms2str asm = "[\"x ~= 0\"]"; neuper@42394: (* neuper@42394: ## eval asms: x ~= 0 ==> (1 / x = 5) = (1 = 5 * x) neuper@42394: ### rls: e_rls on: x ~= 0 neuper@42394: ## asms accepted: ["x ~= 0"] stored: ["x ~= 0"] neuper@42394: *) neuper@42394: trace_rewrite := false; neuper@42394: neuper@52101: trace_rewrite := false; neuper@42394: val SOME (t', []) = rewrite_set_ thy true RatEq_eliminate t; (*= [] must be = "x ~= 0"*) neuper@42394: term2str t' = "1 = 5 * x"; neuper@42394: (* neuper@42394: : neuper@42394: #### rls: rateq_erls on: x ~= 0 neuper@42394: : neuper@42394: ##### try calc: HOL.eq' <<<------------------------------- here the error comes from neuper@42394: ===== calc. to: ~ False neuper@42394: ##### try calc: HOL.eq' neuper@42394: ##### try thm: not_true neuper@42394: ##### try thm: not_false neuper@42394: ===== rewrites to: True neuper@42394: : neuper@42394: ### asms accepted: ["x ~= 0"] stored: [] neuper@42394: : neuper@42394: *) neuper@42394: trace_rewrite := false; neuper@42394: (* WN120317.TODO dropped rateq: the above error is the same in 2002 *) neuper@42394: wneuper@59110: "----------- fun assoc_thm' -----------------------------"; wneuper@59110: "----------- fun assoc_thm' -----------------------------"; wneuper@59110: "----------- fun assoc_thm' -----------------------------"; wneuper@59110: val thy = @{theory ProgLang} wneuper@59110: wneuper@59110: val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3"); wneuper@59110: if string_of_thm' thy tth = "6 = 2 * 3" then () wneuper@59110: else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed"; wneuper@59110: wneuper@59110: val tth = assoc_thm' thy ("add_0_left",""); wneuper@59110: if string_of_thm' thy tth = "0 + ?a = ?a" then () wneuper@59110: else error "assoc_thm' (add_0_left,\"\") changed"; wneuper@59110: wneuper@59110: val tth = assoc_thm' thy ("sym_add_0_left",""); wneuper@59110: if string_of_thm' thy tth = "?t = 0 + ?t" then () wneuper@59110: else error "assoc_thm' (sym_add_0_left,\"\") changed"; wneuper@59110: wneuper@59110: val tth = assoc_thm' thy ("add_commute",""); wneuper@59110: if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then () wneuper@59110: else error "assoc_thm' (add_commute,\"\") changed" wneuper@59110: wneuper@59252: "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; wneuper@59252: "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; wneuper@59252: "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; wneuper@59252: "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) = wneuper@59252: (@{theory}, dummy_ord, e_rls, false, @{thm distrib_left}, @{term "x * (y + z) :: int"}); wneuper@59252: "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) = wneuper@59252: (thy, 1, [], rew_ord, erls, bool, thm, term); wneuper@59252: "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = wneuper@59252: (thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct) wneuper@59252: val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r wneuper@59252: val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r wneuper@59252: val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r')) wneuper@59252: val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r' wneuper@59252: ; wneuper@59252: if term2str lhss = "?a * (?b + ?c)" andalso term2str t = "x * (y + z)" then () wneuper@59252: else error "ARGS FOR Pattern.match CHANGED"; wneuper@59252: val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty); wneuper@59252: if (Envir.subst_term match r |> term2str) = "x * (y + z) = x * y + x * z" then () wneuper@59252: else error "Pattern.match CHANGED"; wneuper@59381: wneuper@59381: "----------- fun mk_thm ------------------------------------------------------------------------"; wneuper@59381: "----------- fun mk_thm ------------------------------------------------------------------------"; wneuper@59381: "----------- fun mk_thm ------------------------------------------------------------------------"; wneuper@59385: val thy = @{theory Isac} wneuper@59381: wneuper@59385: (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*) wneuper@59385: val thm = @{thm realpow_twoI}; wneuper@59385: val patt_str = "?r ^^^ 2 = ?r * ?r"; wneuper@59385: val term_str = "r ^^^ 2 = r * r"; wneuper@59385: (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*) wneuper@59385: case parse_patt thy patt_str of wneuper@59385: Const ("HOL.eq", _) $ (Const ("Atools.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $ wneuper@59385: (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => () wneuper@59385: | _ => error "parse_patt ?r ^^^ 2 = ?r * ?r changed"; wneuper@59395: case parse thy term_str of wneuper@59385: NONE => () wneuper@59385: | _ => writeln "parse does NOT take patterns with '?'"; wneuper@59381: wneuper@59385: val t1 = (#prop o Thm.rep_thm) (num_str thm); wneuper@59385: if term2str t1 = patt_str then () else error "realpow_twoI (\ string) NOT equal to given string"; wneuper@59381: wneuper@59395: val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term; wneuper@59385: if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string"; wneuper@59385: wneuper@59385: (mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns"; wneuper@59385: (*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm wneuper@59385: gives a strange thm*); wneuper@59395: (*while this..*) wneuper@59385: val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm wneuper@59395: ..gives another strange thm; but it is used and works with rewriting: *); wneuper@59385: wneuper@59385: val t1' = (#prop o Thm.rep_thm) (num_str thm_made); wneuper@59385: if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string"; wneuper@59385: wneuper@59385: (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*) wneuper@59385: val thm = @{thm real_mult_div_cancel2}; wneuper@59385: val patt_str = "?k \ 0 \ ?m * ?k / (?n * ?k) = ?m / ?n"; wneuper@59385: val term_str = "k \ 0 \ m * k / (n * k) = m / n"; wneuper@59385: (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*) wneuper@59385: case parse_patt thy patt_str of wneuper@59385: Const ("Pure.imp", _) $ wneuper@59385: (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $ wneuper@59385: (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $ wneuper@59385: (Const ("HOL.Trueprop", _) $ wneuper@59385: (Const ("HOL.eq", _) $ _ $ _ )) => () wneuper@59385: | _ => error "parse_patt ?k \ 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n changed"; wneuper@59395: case parse thy term_str of wneuper@59385: NONE => () wneuper@59385: | _ => writeln "parse does NOT take patterns with '?'"; wneuper@59385: wneuper@59385: val t1 = (#prop o Thm.rep_thm) (num_str thm); wneuper@59385: if term2str t1 = patt_str then () else error "realpow_twoI (\ string) NOT equal to given string"; wneuper@59385: wneuper@59385: val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term; wneuper@59385: if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string"; wneuper@59385: wneuper@59385: (mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns"; wneuper@59385: (*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm wneuper@59385: gives a strange thm*); wneuper@59385: (*while this*) wneuper@59385: val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm wneuper@59385: gives another strange thm; but it is used and words with rewriting: *); wneuper@59385: wneuper@59385: val t1' = (#prop o Thm.rep_thm) (num_str thm_made); wneuper@59385: if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";