walther@60318: (* Title: "MathEngBasic/rewrite.sml" neuper@38036: Author: Walther Neuper 050908 neuper@37906: (c) copyright due to lincense terms. neuper@37906: *) neuper@37906: walther@60262: "-----------------------------------------------------------------------------------------------"; walther@60262: "table of contents -----------------------------------------------------------------------------"; walther@60262: "-----------------------------------------------------------------------------------------------"; walther@60262: "----------- assemble rewrite ------------------------------------------------------------------"; walther@60262: "----------- test rewriting without Isac's thys ------------------------------------------------"; walther@60262: "----------- test rewriting without Isac's thys, ~~~~~ fun rewrite_ ----------------------------"; walther@60262: "----------- conditional rewriting without Isac's thys -----------------------------------------"; walther@60262: "----------- conditional rewriting without Isac's thys, ~~~~~ fun ------------------------------"; walther@60262: "----------- conditional rewriting creating an assumption---------------------------------------"; walther@60262: "----------- step through 'and rew_sub': -------------------------------------------------------"; walther@60262: "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; walther@60262: "----------- rewrite_inst_ bdvs ----------------------------------------------------------------"; walther@60262: "----------- check diff 2002--2009-3 -----------------------------------------------------------"; walther@60262: "----------- compare all prepat's existing 2010 ------------------------------------------------"; walther@60262: "----------- fun app_rev, Rrls, ----------------------------------------------------------------"; walther@60262: "----------- 2011 thms with axclasses ----------------------------------------------------------"; walther@59841: "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------"; wneuper@59252: "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; wneuper@59411: "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------"; walther@60262: "-----------------------------------------------------------------------------------------------"; walther@60262: "-----------------------------------------------------------------------------------------------"; walther@60262: "-----------------------------------------------------------------------------------------------"; neuper@37906: neuper@38036: walther@60262: "----------- assemble rewrite ------------------------------------------------------------------"; walther@60262: "----------- assemble rewrite ------------------------------------------------------------------"; walther@60262: "----------- 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}; Walther@60424: val t = TermC.parseNEW' ctxt "((r + u) + t) + (s::real)"; neuper@37906: "----- from old: fun rewrite__"; neuper@37906: val bdv = []; walther@60230: val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of 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'); walther@60340: (**) neuper@37906: walther@60262: "----------- test rewriting without Isac's thys ------------------------------------------------"; walther@60262: "----------- test rewriting without Isac's thys ------------------------------------------------"; walther@60262: "----------- 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: Walther@60509: val SOME (r,_) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm); 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: Walther@60509: val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm); neuper@37906: neuper@37906: "----- ordered rewriting"; wneuper@59462: fun tord (_:subst) pp = LibraryC.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: Walther@60500: val NONE = (rewrite_ ctxt tord Rule_Set.empty false thm tm); 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"}; Walther@60500: val SOME (r, _) = (rewrite_ ctxt tord Rule_Set.empty false thm tm); neuper@37906: neuper@37906: walther@60262: "----------- conditional rewriting without Isac's thys -----------------------------------------"; walther@60262: "----------- conditional rewriting without Isac's thys -----------------------------------------"; walther@60262: "----------- conditional rewriting without Isac's thys -----------------------------------------"; neuper@37906: "===== prepr cond.rew. with Pattern.match"; neuper@37906: val thy = @{theory Complex_Main}; neuper@37906: val ctxt = @{context}; walther@60262: val thm = @{thm nonzero_divide_mult_cancel_right}; (* = "?b \ 0 \ ?b / (?a * ?b) = 1 / ?a":*) neuper@37906: val rule = Thm.prop_of thm; wneuper@59358: val tm = @{term "x / (2 * x)::real"}; 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: walther@60262: val prems' = (fst o Logic.strip_prems) (Logic.count_prems rule', [], rule'); walther@60262: val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) rule'; neuper@37906: walther@60262: (rule' |> UnparseC.term) = "x \ 0 \ x / (2 * x) = 1 / 2"; walther@60262: rule'; walther@60262: walther@60262: (rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2"; walther@60262: rule' |> Logic.strip_imp_concl; walther@60262: walther@60262: (rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2"; walther@60262: rule' |> Logic.strip_imp_concl; walther@60262: walther@60262: walther@60262: "----------- conditional rewriting creating an assumption---------------------------------------"; walther@60262: "----------- conditional rewriting creating an assumption---------------------------------------"; walther@60262: "----------- conditional rewriting creating an assumption---------------------------------------"; wneuper@59358: val thm = @{thm nonzero_divide_mult_cancel_right}; wneuper@59358: val tm = @{term "x / (2 * x)::real"}; walther@60262: Walther@60509: val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm; 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: walther@60262: "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------"; walther@60262: "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------"; walther@60262: "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------"; walther@60262: val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \ 0 \ ?b / (?a * ?b) = 1 / ?a"*) walther@60262: val tm = @{term "x / (2 * x)::real"}; walther@60262: val erls = eval_rls; walther@60262: Walther@60509: (**)val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm; walther@60262: (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"): walther@60262: dest_Trueprop walther@60262: ?b \ 0 \ ?b / (?a * ?b) = 1 / ?a( **) walther@60262: "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) = Walther@60509: (thy, Rewrite_Ord.function_empty, erls, false, thm, tm); walther@60262: "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) = Walther@60477: (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term); walther@60262: Walther@60500: (**) val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path) walther@60262: (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct; walther@60262: (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"): walther@60262: dest_Trueprop walther@60262: ?b \ 0 \ ?b / (?a * ?b) = 1 / ?a( **) walther@60262: "~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = walther@60262: (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path), walther@60262: (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct); walther@60262: (*+*)UnparseC.term r = "?b \ (0::?'a) \ ?b / (?a * ?b) = (1::?'a) / ?a"; walther@60262: walther@60262: val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r; walther@60262: (*+*)(UnparseC.term lhs, UnparseC.term rhs) = ("?b / (?a * ?b)", "(1::?'a) / ?a"); walther@60262: val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r) walther@60262: handle Pattern.MATCH => raise NO_REWRITE; walther@60262: val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r')); walther@60262: (*+*)UnparseC.term r' = "x \ 0 \ x / (2 * x) = 1 / 2"; walther@60262: (*+*)r'; walther@60262: val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r' Walther@60500: val _ = trace_in2 ctxt i "eval asms" r'; Walther@60500: val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls; walther@60262: (*if*) nofalse (*then*); Walther@60500: val (t'', p'') = (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t',simpl_p')); walther@60262: (*## asms accepted: [x \ 0] stored: [x \ 0] *) walther@60262: walther@60262: (*+*)if (UnparseC.term t'', map UnparseC.term p'') = ("1 / 2", ["x \ 0"]) then () walther@60262: (*+*)else error "conditional rewriting x \ 0 \ x / (2 * x) = 1 / 2 CHANGED"; walther@60262: walther@60262: 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"}; Walther@60509: val (t', asm, _, _) = rew_sub ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty 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) = Walther@60509: (thy, 0, [], Rewrite_Ord.function_empty, Rule_Set.empty, 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; walther@59868: UnparseC.term r = "?b \ (0::?'a) \ ?b / (?a * ?b) = (1::?'a) / ?a"; walther@59868: UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term 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; walther@59868: UnparseC.term 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'); walther@59868: UnparseC.term (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 wenzelm@60309: [Const (\<^const_name>\Not\, _) $ (Const (\<^const_name>\HOL.eq\, _) walther@60336: $ Free ("x", _) $ Const (\<^const_name>\zero_class.zero\, _))] => () neuper@38022: | _ => error "rewrite.sml assumption changed"; walther@60242: "===== \ 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'; walther@59868: UnparseC.term t' = "1 / 2"; neuper@37906: walther@60262: "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; walther@60262: "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; walther@60262: "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; neuper@38025: "----- step 0: args for rewrite_terms_, local fun"; neuper@38025: val (thy, ord, erls, equs, t) = Walther@60509: (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.str2term "x = 0"], walther@60242: TermC.str2term "M_b x = -1 * q_0 * x \ 2 / 2 + x * c + c_2"); neuper@38025: "----- step 1: args for rew_"; walther@59861: val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t); neuper@38025: "----- step 2: rew_sub"; Walther@60500: rew_sub ctxt 1 [] ord erls false [] (HOLogic.Trueprop $ r) t; neuper@38025: "----- step 3: step through rew_sub -- inefficient: goes into subterms"; neuper@38025: neuper@38025: Walther@60509: val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; walther@60262: writeln "---------- rewrite_terms_ 1---------------------------"; walther@60317: if UnparseC.term 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: walther@60230: val equs = [TermC.str2term "M_b 0 = 0"]; walther@60317: val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2"; Walther@60509: val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; walther@60262: writeln "---------- rewrite_terms_ 2---------------------------"; walther@60317: if UnparseC.term 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: walther@60230: val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"]; walther@60317: val t = TermC.str2term "M_b x = - 1 * q_0 * x \ 2 / 2 + x * c + c_2"; Walther@60509: val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; walther@60262: writeln "---------- rewrite_terms_ 3---------------------------"; walther@60317: if UnparseC.term 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: walther@60262: "----------- rewrite_inst_ bdvs ----------------------------------------------------------------"; walther@60262: "----------- rewrite_inst_ bdvs ----------------------------------------------------------------"; walther@60262: "----------- rewrite_inst_ bdvs ----------------------------------------------------------------"; neuper@37906: (*see smltest/Scripts/term_G.sml: inst_bdv 2*) walther@60242: val t = TermC.str2term"-1 * (q_0 * L \ 2) / 2 + (L * c_3 + c_4) = 0"; walther@60230: val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"), walther@60230: (TermC.str2term"bdv_2",TermC.str2term"c_2"), walther@60230: (TermC.str2term"bdv_3",TermC.str2term"c_3"), walther@60230: (TermC.str2term"bdv_4",TermC.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 walther@59852: (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty walther@60278: [(Eval ("EqSystem.occur_exactly_in", neuper@37906: eval_occur_exactly_in neuper@37906: "#eval_occur_exactly_in_")) neuper@37906: ]) walther@59871: false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t; walther@59868: (writeln o UnparseC.term) t; walther@60242: if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \ 2) / 2)" neuper@38031: then () else error "rewrite.sml rewrite_inst_ bdvs"; walther@60330: > Rewrite.trace_on:=true;false walther@59901: Rewrite.trace_on:=false;--------------------------------------------*) neuper@37906: neuper@38025: walther@60262: "----------- compare all prepat's existing 2010 ------------------------------------------------"; walther@60262: "----------- compare all prepat's existing 2010 ------------------------------------------------"; walther@60262: "----------- compare all prepat's existing 2010 ------------------------------------------------"; wneuper@59592: val thy = @{theory "Isac_Knowledge"}; neuper@38036: val t = @{term "a + b * x = (0 ::real)"}; walther@60230: val pat = TermC.parse_patt thy "?l = (?r ::real)"; walther@60230: val precond = TermC.parse_patt thy "is_polynomial (?l::real)";(*no infix def*) walther@60230: val precond = TermC.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; walther@59868: UnparseC.term 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. *) walther@60230: val t = TermC.str2term "(a + b) / c ::real"; walther@60230: val pat = TermC.parse_patt thy "?r / ?s ::real"; walther@60230: val pres = [TermC.parse_patt thy "?r is_expanded", TermC.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; walther@59997: if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]" neuper@38036: then () else error "rewrite.sml: prepat cancel subst"; walther@60318: Walther@60500: if ([], true) = eval__true ctxt 0 asms [] erls neuper@38036: then () else error "rewrite.sml: prepat cancel eval__true"; neuper@38036: neuper@52105: "===== Rational.thy: add_fractions_p ==="; walther@60230: (* if each pat* TermC.matches with the current term, the Rrls is applied neuper@48760: (there are no preconditions to be checked, they are @{term True}) *) walther@60230: val t = TermC.str2term "a / b + 1 / 2"; walther@60230: val pat = TermC.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); Walther@60500: if ([], true) = eval__true ctxt 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*) walther@60242: val t = TermC.str2term "x \ 2 * x"; walther@60230: val pat = TermC.parse_patt thy "?p :: real" walther@60230: val pres = [TermC.parse_patt thy "?p is_multUnordered"]; neuper@38036: val prepat = [(pres, pat)]; walther@59852: val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty walther@60278: [Eval ("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; walther@60242: if UnparseC.terms asms = "[\"x \ 2 * x is_multUnordered\"]" neuper@38036: then () else error "rewrite.sml: prepat order_mult_ subst"; walther@60318: Walther@60500: if ([], true) = eval__true ctxt 0 asms [] erls neuper@38036: then () else error "rewrite.sml: prepat order_mult_ eval__true"; neuper@38036: neuper@38036: walther@60262: "----------- fun app_rev, Rrls, ----------------------------------------------------------------"; walther@60262: "----------- fun app_rev, Rrls, ----------------------------------------------------------------"; walther@60262: "----------- fun app_rev, Rrls, ----------------------------------------------------------------"; walther@60242: val t = TermC.str2term "x \ 2 * x"; neuper@41928: neuper@38039: if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2"; walther@60242: val tm = TermC.str2term "(x \ 2 * x) is_multUnordered"; walther@60318: Walther@60504: (*+*)case eval_is_multUnordered "testid" "" tm ctxt of walther@60318: (*+*) SOME walther@60318: (*+*) ("testidx \ 2 * x_", walther@60336: (*+*) Const (\<^const_name>\Trueprop\, _) $ walther@60336: (*+*) (Const (\<^const_name>\HOL.eq\, _) $ walther@60336: (*+*) (Const (\<^const_name>\is_multUnordered\, _) $ walther@60336: (*+*) (Const (\<^const_name>\times\, _) $ wenzelm@60405: (*+*) (Const (\<^const_name>\realpow\, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $ walther@60336: (*+*) Const (\<^const_name>\True\, _))) => () walther@60318: (*+*)(* ^^^^^^ compare ---vvv *) walther@60318: (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED"; walther@60318: walther@60318: Walther@60504: eval_is_multUnordered "testid" "" tm ctxt; neuper@41928: Walther@60504: case eval_is_multUnordered "testid" "" tm ctxt of wenzelm@60309: SOME (_, Const (\<^const_name>\Trueprop\, _) $ wenzelm@60309: (Const (\<^const_name>\HOL.eq\, _) $ walther@60336: (Const (\<^const_name>\is_multUnordered\, _) $ _) $ wenzelm@60309: Const (\<^const_name>\True\, _))) => () neuper@41928: | _ => error "rewrite.sml diff. eval_is_multUnordered 2b"; neuper@38039: Walther@60500: tracing "----- begin rewrite x \ 2 * x ---"; Walther@60500: val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t; Walther@60500: tracing "----- end rewrite x \ 2 * x ---"; walther@60242: if UnparseC.term t' = "x * x \ 2" then () walther@60278: 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); Walther@60500: val (t', asm, rew) = app_rev ctxt (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) Walther@60500: in snd (eval__true ctxt (i+1) neuper@38039: (map (Envir.subst_term subst) pres) neuper@38039: [] erls) neuper@38039: end) walther@60270: handle Pattern.MATCH => 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 walther@59868: then ((*tracing("### app_rev': t = "^(UnparseC.term 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) Walther@60500: in snd (eval__true ctxt (i+1) neuper@38039: (map (Envir.subst_term subst) pres) neuper@38039: [] erls) neuper@38039: end) walther@60270: handle Pattern.MATCH => false; walther@60270: fun scan_ _ [] = 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 ---"; walther@60242: (*reestablish...*) val t = TermC.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); walther@60242: if UnparseC.terms 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) = walther@60242: (thy, (i+1), [TermC.str2term "(x \ 2 * x) is_multUnordered"], Walther@60477: [] : Subst.T, erls); Walther@60500: case eval__true ctxt i asms bdv rls of neuper@38039: ([], true) => () neuper@38039: | _ => error "rewrite.sml: diff. is_multUnordered, eval__true"; neuper@42223: walther@60262: "----------- 2011 thms with axclasses ----------------------------------------------------------"; walther@60262: "----------- 2011 thms with axclasses ----------------------------------------------------------"; walther@60262: "----------- 2011 thms with axclasses ----------------------------------------------------------"; walther@60337: val thm = @{thm div_by_1}; wneuper@59188: val prop = Thm.prop_of thm; walther@60230: TermC.atomty prop; (*Type 'a*) walther@60230: val t = TermC.str2term "(2*x)/1"; (*Type real*) neuper@42223: neuper@42223: val (thy, ro, er, inst) = wneuper@59592: (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); Walther@60500: val SOME (t, _) = rewrite_ ctxt ro er true thm t; (*real TermC.matches 'a ?via ring? etc*) neuper@42223: walther@59841: "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------"; walther@59841: "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------"; walther@59841: "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------"; walther@59841: val thy = @{theory RatEq}; walther@59841: val ctxt = Proof_Context.init_global thy; Walther@60424: val SOME t = TermC.parseNEW ctxt "(3 + -1 * x + x \ 2) / (9 * x + -6 * x \ 2 + x \ 3) = 1 / x"; walther@59841: val rls = assoc_rls "RatEq_eliminate" neuper@42394: walther@59841: val SOME (t''''', asm''''') = Walther@60500: rewrite_set_ ctxt true rls t; walther@59841: "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t); Walther@60500: rewrite__set_ ctxt 1 bool [] rls term; walther@59841: "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) Walther@60477: = (thy, 1, bool, []:Subst.T, rls, term); walther@59841: walther@59841: (*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * ) walther@59920: datatype switch = Applicable.Yes | Noap; walther@59841: fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *) walther@59920: | rew_once ruls asm ct Applicable.Yes [] = walther@59851: (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls walther@59878: | Rule_Set.Sequence _ => (ct, asm) walther@59867: | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\"")) walther@59841: | rew_once ruls asm ct apno (rul :: thms) = walther@59841: case rul of walther@59841: Rule.Thm (thmid, thm) => walther@59841: (trace1 i (" try thm: " ^ thmid); walther@59852: case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls) walther@59852: ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of walther@59841: NONE => rew_once ruls asm ct apno thms walther@59841: | SOME (ct', asm') => walther@59870: (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct'); walther@59920: rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms))) walther@59841: (* once again try the same rule, e.g. associativity against "()"*) walther@59878: | Rule.Eval (cc as (op_, _)) => walther@59841: let val _= trace1 i (" try calc: " ^ op_ ^ "'") walther@59841: val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*) walther@59878: in case Eval.adhoc_thm thy cc ct of walther@59841: NONE => rew_once ruls asm ct apno thms walther@59841: | SOME (_, thm') => walther@59841: let walther@59852: val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls) walther@59852: ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct; walther@59841: val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ walther@59875: ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE") walther@59870: val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt)) walther@59920: in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end walther@59841: end walther@59841: | Rule.Cal1 (cc as (op_, _)) => walther@59841: let val _= trace1 i (" try cal1: " ^ op_ ^ "'"); walther@59841: val ct = TermC.uminus_to_string ct walther@59878: in case Eval.adhoc_thm1_ thy cc ct of walther@59841: NONE => (ct, asm) walther@59841: | SOME (_, thm') => walther@59841: let walther@59852: val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls) walther@59852: ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct; walther@59841: val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ walther@59875: ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE") walther@59870: val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt)) walther@59841: in the pairopt end walther@59841: end walther@59841: | Rule.Rls_ rls' => walther@59841: (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of walther@59920: SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms walther@59841: | NONE => rew_once ruls asm ct apno thms) walther@59867: | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\""); walther@59852: val ruls = (#rules o Rule.Rule_Set.rep) rls; walther@59870: (* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*) walther@59841: val (ct', asm') = rew_once ruls [] ct Noap ruls; walther@59841: "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms)) walther@59841: = (ruls, []:term list, ct, Noap, ruls); walther@59841: val Rule.Thm (thmid, thm) = (*case*) rul (*of*); walther@59841: walther@59841: val SOME (ct', asm') = (*case*) walther@59852: rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls) walther@59852: ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*); walther@59841: "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) walther@59852: = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls), walther@59852: ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct); walther@59841: walther@59841: val (t', asms, _ (*lrd*), rew) = walther@59841: rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path) wenzelm@60203: (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct; walther@59841: "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) walther@59841: = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path), wenzelm@60203: (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct); walther@59841: val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r walther@59841: val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r walther@59841: ; walther@59868: (*+*)if UnparseC.term r' = walther@60242: (*+*) "\9 * x + -6 * x \ 2 + x \ 3 \ 0; x \ 0\\n" ^ walther@60242: (*+*) "\ ((3 + -1 * x + x \ 2) /\n" ^ walther@60242: (*+*) " (9 * x + -6 * x \ 2 + x \ 3) =\n" ^ walther@59841: (*+*) " 1 / x) =\n" ^ walther@60242: (*+*) " ((3 + -1 * x + x \ 2) * x =\n" ^ walther@60242: (*+*) " 1 * (9 * x + -6 * x \ 2 + x \ 3))" walther@59841: (*+*)then () else error "instantiated rule CHANGED"; walther@59841: walther@59841: val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r')) walther@59841: ; walther@60242: (*+*)if map UnparseC.term p' = ["x \ 0", "9 * x + -6 * x \ 2 + x \ 3 \ 0"] walther@59841: (*+*)then () else error "stored assumptions CHANGED"; walther@59841: walther@59841: val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r' walther@59841: ; walther@60242: (*+*)if UnparseC.term t' = "(3 + -1 * x + x \ 2) * x = 1 * (9 * x + -6 * x \ 2 + x \ 3)" walther@59841: (*+*)then () else error "rewritten term (an equality) CHANGED"; walther@59841: walther@59841: val (simpl_p', nofalse) = walther@59841: eval__true thy (i + 1) p' bdv rls; walther@59841: "~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls); walther@59841: (*if*) asms = [@{term True}] orelse asms = [] (*else*); walther@59841: walther@60242: (*+*)if map UnparseC.term asms = ["x \ 0", "9 * x + -6 * x \ 2 + x \ 3 \ 0"] walther@59841: (*+*)then () else error "asms before chk CHANGED"; walther@59841: walther@59841: fun chk indets [] = (indets, true) (*return asms<>True until false*) walther@59841: | chk indets (a :: asms) = walther@59841: (case rewrite__set_ thy (i + 1) false bdv rls a of walther@59841: NONE => (chk (indets @ [a]) asms) walther@59841: | SOME (t, a') => walther@59841: if t = @{term True} then (chk (indets @ a') asms) walther@59841: else if t = @{term False} then ([], false) walther@60242: (*asm false .. thm not applied \ ; continue until False vvv*) walther@59841: else chk (indets @ [t] @ a') asms); walther@59841: walther@59841: val (xxx, true) = walther@59841: chk [] asms; (*return from eval__true*); walther@59841: "~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms); walther@59841: walther@59851: (*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls; walther@59841: (*+*)(*val rules = wenzelm@60309: (*+*) [Eval (\<^const_name>\divide\, fn), walther@59841: (*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"), walther@59841: (*+*) : wenzelm@60309: (*+*) Eval (\<^const_name>\HOL.eq\, fn), walther@59841: (*+*) Thm ("not_true", "(\ True) = False"), walther@59841: (*+*) Thm ("not_false", "(\ False) = True"), walther@59841: (*+*) : wenzelm@60405: (*+*) Eval (\<^const_name>\realpow\, fn), walther@60278: (*+*) Eval ("RatEq.is_ratequation_in", fn)]: walther@59841: (*+*) rule list*) walther@59841: (*+*)chk: term list -> term list -> term list * bool walther@59841: walther@59841: rewrite__set_ thy (i + 1) false bdv rls a (*of*); walther@59841: walther@60330: (*+*)Rewrite.trace_on := false; (*true false*) walther@59841: walther@59841: (*this was False; vvvv--- means: indeterminate*) walther@59841: val (* SOME (t, a') *)NONE = (*case*) walther@59841: rewrite__set_ thy (i + 1) false bdv rls a (*of*); walther@59841: walther@59868: (*+*)UnparseC.term a = "x \ 0"; (* rewrite__set_ \ @{term True} ----------------- SHOULD BE indet !*) neuper@42394: (* neuper@42394: : walther@59841: #### rls: rateq_erls on: x \ 0 neuper@42394: : neuper@42394: ##### try calc: HOL.eq' <<<------------------------------- here the error comes from walther@59841: ===== calc. to: ~ False <<<------------------------------- \ x = 0 is NOT False neuper@42394: ##### try calc: HOL.eq' neuper@42394: ##### try thm: not_true neuper@42394: ##### try thm: not_false walther@59841: ===== rewrites to: True <<<------------------------------- so x \ 0 is NOT True walther@59841: and True, False are NOT stored ... walther@59841: : walther@59841: ### asms accepted: [x \ 0] stored: [] walther@59841: : *) walther@60330: Rewrite.trace_on := false; (*true false*) walther@59841: ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*) walther@59841: neuper@42394: 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) = Walther@60509: (@{theory}, Rewrite_Ord.function_empty, Rule_Set.empty, 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) = walther@60230: (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct) walther@60262: val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) 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')) walther@60262: val t' = (snd o HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r' wneuper@59252: ; walther@59868: if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term 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); walther@59868: if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then () wneuper@59252: else error "Pattern.match CHANGED"; wneuper@59381: walther@60262: "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------"; walther@60262: "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------"; walther@60262: "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------"; wneuper@59411: (* norm_equation is defined in Test.thy, other rls see Knowledg/**) wneuper@59411: val thy = @{theory}; wneuper@59411: val rls = norm_equation; walther@60230: val term = TermC.str2term "x + 1 = 2"; wneuper@59411: Walther@60500: (**)val SOME (t, asm) = rewrite_set_ ctxt false rls term; walther@60262: (** )##### try thm: "root_ge0" walther@60262: exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"): walther@60262: dest_eq walther@60262: 0 \ ?a \ (0 \ sqrt ?a) = True( **) walther@60318: if UnparseC.term t = "x + 1 + - 1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED"; wneuper@59411: walther@60262: "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term); walther@60262: "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) = Walther@60477: (thy, 1, bool, []: Subst.T, rls, term); walther@60262: (*deleted after error detection*) walther@59841: