1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 10 14:46:55 2020 +0200
1.3 @@ -0,0 +1,805 @@
1.4 +(* Title: "ProgLang/rewrite.sml"
1.5 + Author: Walther Neuper 050908
1.6 + (c) copyright due to lincense terms.
1.7 +*)
1.8 +
1.9 +"--------------------------------------------------------";
1.10 +"table of contents --------------------------------------";
1.11 +"--------------------------------------------------------";
1.12 +"----------- assemble rewrite ---------------------------";
1.13 +"----------- test rewriting without Isac session --------";
1.14 +"----------- conditional rewriting without Isac session -";
1.15 +"----------- step through 'and rew_sub': ----------------";
1.16 +"----------- step through 'fun rewrite_terms_' ---------";
1.17 +"----------- rewrite_inst_ bdvs -------------------------";
1.18 +"----------- check diff 2002--2009-3 --------------------";
1.19 +"----------- compare all prepat's existing 2010 ---------";
1.20 +"----------- fun app_rev, Rrls, -------------------------";
1.21 +"----------- 2011 thms with axclasses -------------------";
1.22 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.23 +"----------- fun assoc_thm' -----------------------------";
1.24 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.25 +"----------- fun mk_thm ------------------------------------------------------------------------";
1.26 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.27 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.28 +"--------------------------------------------------------";
1.29 +"--------------------------------------------------------";
1.30 +"--------------------------------------------------------";
1.31 +
1.32 +
1.33 +"----------- assemble rewrite ---------------------------";
1.34 +"----------- assemble rewrite ---------------------------";
1.35 +"----------- assemble rewrite ---------------------------";
1.36 +"===== rewriting by thm with 'a";
1.37 +(*show_types := true;*)
1.38 +
1.39 +val thy = @{theory Complex_Main};
1.40 +val ctxt = @{context};
1.41 +val thm = @{thm add.commute};
1.42 +val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
1.43 +"----- from old: fun rewrite__";
1.44 +val bdv = [];
1.45 +val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm);
1.46 +"----- from old: and rew_sub";
1.47 +val (LHS,RHS) = (dest_equals o strip_trueprop
1.48 + o Logic.strip_imp_concl) r;
1.49 +(* old
1.50 +val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
1.51 +"----- fun match_rew in Pure/pattern.ML";
1.52 +val rtm = the_default RHS (Term.rename_abs LHS t RHS);
1.53 +
1.54 +writeln(Syntax.string_of_term ctxt rtm);
1.55 +writeln(Syntax.string_of_term ctxt LHS);
1.56 +writeln(Syntax.string_of_term ctxt t);
1.57 +
1.58 +(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
1.59 +val (rew, RHS) = (Envir.subst_term
1.60 + (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
1.61 +(*lookup in isabelle?trace?response...*)
1.62 +writeln(Syntax.string_of_term ctxt rew);
1.63 +writeln(Syntax.string_of_term ctxt RHS);
1.64 +"===== rewriting: prep insertion into rew_sub";
1.65 +val thy = @{theory Complex_Main};
1.66 +val ctxt = @{context};
1.67 +val thm = @{thm nonzero_divide_mult_cancel_right};
1.68 +val r = Thm.prop_of thm;
1.69 +val tm = @{term "x / (2 * x)::real"};
1.70 +"----- and rew_sub";
1.71 +val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
1.72 + o Logic.strip_imp_concl) r;
1.73 +val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
1.74 + (Vartab.empty, Vartab.empty)) r;
1.75 +val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
1.76 +val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
1.77 + o Logic.strip_imp_concl) r';
1.78 +
1.79 +(*is displayed on top of <response> buffer...*)
1.80 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
1.81 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
1.82 +(**)
1.83 +
1.84 +"----------- test rewriting without Isac's thys ---------";
1.85 +"----------- test rewriting without Isac's thys ---------";
1.86 +"----------- test rewriting without Isac's thys ---------";
1.87 +
1.88 +"===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
1.89 +val thy = @{theory Complex_Main};
1.90 +val ctxt = @{context};
1.91 +val thm = @{thm add.commute};
1.92 +val tm = @{term "x + y*z::real"};
1.93 +
1.94 +val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
1.95 + handle _ => error "rewrite.sml diff.behav. in rewriting";
1.96 +(*is displayed on _TOP_ of <response> buffer...*)
1.97 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
1.98 +if r = @{term "y*z + x::real"}
1.99 +then () else error "rewrite.sml diff.result in rewriting";
1.100 +
1.101 +"----- rewriting a subterm";
1.102 +val tm = @{term "w*(x + y*z)::real"};
1.103 +
1.104 +val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
1.105 + handle _ => error "rewrite.sml diff.behav. in rew_sub";
1.106 +
1.107 +"----- ordered rewriting";
1.108 +fun tord (_:subst) pp = LibraryC.termless pp;
1.109 +if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
1.110 +else error "rewrite.sml diff.behav. in ord.rewr.";
1.111 +
1.112 +val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm)
1.113 + handle _ => error "rewrite.sml diff.behav. in rewriting";
1.114 +(*is displayed on _TOP_ of <response> buffer...*)
1.115 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
1.116 +
1.117 +val tm = @{term "x*y + z::real"};
1.118 +val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm)
1.119 + handle _ => error "rewrite.sml diff.behav. in rewriting";
1.120 +
1.121 +
1.122 +"----------- conditional rewriting without Isac's thys --";
1.123 +"----------- conditional rewriting without Isac's thys --";
1.124 +"----------- conditional rewriting without Isac's thys --";
1.125 +
1.126 +"===== prepr cond.rew. with Pattern.match";
1.127 +val thy = @{theory Complex_Main};
1.128 +val ctxt = @{context};
1.129 +val thm = @{thm nonzero_divide_mult_cancel_right};
1.130 +val rule = Thm.prop_of thm;
1.131 +val tm = @{term "x / (2 * x)::real"};
1.132 +
1.133 +val prem = Logic.strip_imp_prems rule;
1.134 +val nps = Logic.count_prems rule;
1.135 +val prems = Logic.strip_prems (nps, [], rule);
1.136 +
1.137 +val eq = Logic.strip_imp_concl rule;
1.138 +val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
1.139 +
1.140 +val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
1.141 +val rule' = Envir.subst_term mtcs rule;
1.142 +
1.143 +val prems' = (fst o Logic.strip_prems)
1.144 + (Logic.count_prems rule', [], rule');
1.145 +val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
1.146 + o Logic.strip_imp_concl) rule';
1.147 +
1.148 +"----- conditional rewriting creating an assumption";
1.149 +"----- conditional rewriting creating an assumption";
1.150 +val thm = @{thm nonzero_divide_mult_cancel_right};
1.151 +val tm = @{term "x / (2 * x)::real"};
1.152 +val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
1.153 + handle _ => error "rewrite.sml diff.behav. in cond.rew.";
1.154 +
1.155 +if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
1.156 +else error "rewrite.sml diff.result in cond.rew.";
1.157 +
1.158 +if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
1.159 +then () else error "rewrite.sml diff.asm in cond.rew.";
1.160 +"----- conditional rewriting immediately: can only be done with ";
1.161 +"------Isabelle numerals, because erls cannot handle them yet.";
1.162 +
1.163 +
1.164 +"----------- step through 'and rew_sub': ----------------";
1.165 +"----------- step through 'and rew_sub': ----------------";
1.166 +"----------- step through 'and rew_sub': ----------------";
1.167 +(*and make asms without Trueprop, beginning with the result:*)
1.168 +val tm = @{term "x / (2 * x)::real"};
1.169 +val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
1.170 +(*show_types := false;*)
1.171 +"----- evaluate arguments";
1.172 +val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
1.173 + (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
1.174 +"----- step 1: LHS, RHS of rule";
1.175 + val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
1.176 + o Logic.strip_imp_concl) r;
1.177 +UnparseC.term2str r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
1.178 +UnparseC.term2str LHS = "?b / (?a * ?b)"; UnparseC.term2str RHS = "(1::?'a) / ?a";
1.179 +"----- step 2: the rule instantiated";
1.180 + val r' = Envir.subst_term
1.181 + (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
1.182 +UnparseC.term2str r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
1.183 +"----- step 3: get the (instantiated) assumption(s)";
1.184 + val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
1.185 +UnparseC.term2str (hd p') = "x \<noteq> 0";
1.186 +"=====vvv make asms without Trueprop ---vvv";
1.187 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
1.188 + (Logic.count_prems r', [], r'));
1.189 +case p' of
1.190 + [Const ("HOL.Not", _) $ (Const ("HOL.eq", _)
1.191 + $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
1.192 + | _ => error "rewrite.sml assumption changed";
1.193 +"=====^^^ make asms without Trueprop ---^^^";
1.194 +"----- step 4: get the (instantiated) RHS";
1.195 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
1.196 + o Logic.strip_imp_concl) r';
1.197 +UnparseC.term2str t' = "1 / 2";
1.198 +
1.199 +"----------- step through 'fun rewrite_terms_' ---------";
1.200 +"----------- step through 'fun rewrite_terms_' ---------";
1.201 +"----------- step through 'fun rewrite_terms_' ---------";
1.202 +"----- step 0: args for rewrite_terms_, local fun";
1.203 +val (thy, ord, erls, equs, t) =
1.204 + (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [str2term "x = 0"],
1.205 + str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
1.206 +"----- step 1: args for rew_";
1.207 +val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
1.208 +"----- step 2: rew_sub";
1.209 +rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
1.210 +"----- step 3: step through rew_sub -- inefficient: goes into subterms";
1.211 +
1.212 +
1.213 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.214 +writeln "----------- rewrite_terms_ 1---------------------------";
1.215 +if UnparseC.term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.216 +else error "rewrite.sml rewrite_terms_ [x = 0]";
1.217 +
1.218 +val equs = [str2term "M_b 0 = 0"];
1.219 +val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
1.220 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.221 +writeln "----------- rewrite_terms_ 2---------------------------";
1.222 +if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.223 +else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.224 +
1.225 +val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
1.226 +val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
1.227 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.228 +writeln "----------- rewrite_terms_ 3---------------------------";
1.229 +if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.230 +else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
1.231 +
1.232 +
1.233 +"----------- rewrite_inst_ bdvs -------------------------";
1.234 +"----------- rewrite_inst_ bdvs -------------------------";
1.235 +"----------- rewrite_inst_ bdvs -------------------------";
1.236 +(*see smltest/Scripts/term_G.sml: inst_bdv 2*)
1.237 +val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
1.238 +val bdvs = [(str2term"bdv_1",str2term"c"),
1.239 + (str2term"bdv_2",str2term"c_2"),
1.240 + (str2term"bdv_3",str2term"c_3"),
1.241 + (str2term"bdv_4",str2term"c_4")];
1.242 +(*------------ outcommented WN071210, after inclusion into ROOT.ML
1.243 +val SOME (t,_) =
1.244 + rewrite_inst_ thy e_rew_ord
1.245 + (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
1.246 + [(Num_Calc ("EqSystem.occur'_exactly'_in",
1.247 + eval_occur_exactly_in
1.248 + "#eval_occur_exactly_in_"))
1.249 + ])
1.250 + false bdvs (num_str @{separate_bdvs_add) t;
1.251 +(writeln o UnparseC.term2str) t;
1.252 +if UnparseC.term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
1.253 +then () else error "rewrite.sml rewrite_inst_ bdvs";
1.254 +> trace_rewrite:=true;
1.255 +trace_rewrite:=false;--------------------------------------------*)
1.256 +
1.257 +
1.258 +"----------- check diff 2002--2009-3 --------------------";
1.259 +"----------- check diff 2002--2009-3 --------------------";
1.260 +"----------- check diff 2002--2009-3 --------------------";
1.261 +(*----- 2002 -------------------------------------------------------------------
1.262 +# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
1.263 +q_0 * x ^^^ 2 / 2)
1.264 +## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
1.265 +/ 2)
1.266 +### try thm: real_diff_minus
1.267 +### try thm: sym_real_mult_minus1
1.268 +## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
1.269 +/ 2)
1.270 +### try thm: rat_mult_poly_l
1.271 +### try thm: rat_mult_poly_r
1.272 +#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
1.273 +==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
1.274 + 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
1.275 +##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
1.276 +is_polyexp
1.277 +###### try calc: Poly.is'_polyexp'
1.278 +====== calc. to: False
1.279 +###### try calc: Poly.is'_polyexp'
1.280 +###### try calc: Poly.is'_polyexp'
1.281 +#### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
1.282 +----- 2002 NONE rewrite --------------------------------------------------------
1.283 +----- 2009 should maintain this behaviour, but: --------------------------------
1.284 +# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
1.285 +## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
1.286 +### try thm: real_diff_minus
1.287 +### try thm: sym_real_mult_minus1
1.288 +## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
1.289 +### try thm: rat_mult_poly_l
1.290 +### try thm: rat_mult_poly_r
1.291 +#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
1.292 +==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
1.293 + 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
1.294 +##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
1.295 +###### try calc: Poly.is'_polyexp'
1.296 +====== calc. to: False
1.297 +###### try calc: Poly.is'_polyexp'
1.298 +###### try calc: Poly.is'_polyexp'
1.299 +#### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
1.300 +=== rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
1.301 +----- 2009 -------------------------------------------------------------------*)
1.302 +
1.303 +(*the situation as was before repair (asm without Trueprop) is outcommented*)
1.304 +val thy = @{theory "Isac_Knowledge"};
1.305 +"===== example which raised the problem =================";
1.306 +val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
1.307 +"----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
1.308 +val subs = [(@{term "bdv"}, @{term "x"})];
1.309 +val rls = norm_Rational_noadd_fractions;
1.310 +val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
1.311 +if UnparseC.term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x ^^^ 2 / 2)" andalso
1.312 + UnparseC.terms2str asms = "[]" then {}
1.313 +else error "this was NONE with Isabelle2013-2 ?!?"
1.314 +"----- rewrite_ rat_mult_poly_r--------------------------";
1.315 +val thm = @{thm rat_mult_poly_r};
1.316 + "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
1.317 +val erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.318 + [Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
1.319 +val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
1.320 +(*t' = t''; (*false because of further rewrites in t'*)*)
1.321 +"----- rew_sub --------------------------------";
1.322 +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
1.323 +(*t'' = t'''; (*true*)*)
1.324 +"----- rewrite_set_ erls --------------------------------";
1.325 +val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
1.326 +val NONE = rewrite_set_ thy true erls cond;
1.327 +(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
1.328 +
1.329 +writeln "===== maximally simplified example =====================";
1.330 +val t = @{term "a / b * (x / x ^^^ 2)"};
1.331 + "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
1.332 +writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
1.333 +val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
1.334 +UnparseC.term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
1.335 +(*checked visually: trace_rewrite looks like above for 2009*)
1.336 +
1.337 +writeln "----- rewrite_ rat_mult_poly_r--------------------------";
1.338 +val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
1.339 +(*t' = t''; (*false because of further rewrites in t'*)*)
1.340 +writeln "----- rew_sub --------------------------------";
1.341 +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
1.342 +(*t'' = t'''; (*true*)*)
1.343 +writeln "----- rewrite_set_ erls --------------------------------";
1.344 +val cond = @{term "(x / x ^^^ 2)"};
1.345 +val NONE = rewrite_set_ thy true erls cond;
1.346 +(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
1.347 +
1.348 +
1.349 +"----------- compare all prepat's existing 2010 ---------";
1.350 +"----------- compare all prepat's existing 2010 ---------";
1.351 +"----------- compare all prepat's existing 2010 ---------";
1.352 +val thy = @{theory "Isac_Knowledge"};
1.353 +val t = @{term "a + b * x = (0 ::real)"};
1.354 +val pat = parse_patt thy "?l = (?r ::real)";
1.355 +val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
1.356 +val precond = parse_patt thy "(?l::real) is_expanded";
1.357 +
1.358 +val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.359 +val preinst = Envir.subst_term inst precond;
1.360 +UnparseC.term2str preinst;
1.361 +
1.362 +"===== Rational.thy: cancel ===";
1.363 +(* pat matched with the current term gives an environment
1.364 + (or not: hen the Rrls not applied);
1.365 + if pre1 and pre2 evaluate to @{term True} in this environment,
1.366 + then the Rrls is applied. *)
1.367 +val t = str2term "(a + b) / c ::real";
1.368 +val pat = parse_patt thy "?r / ?s ::real";
1.369 +val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
1.370 +val prepat = [(pres, pat)];
1.371 +val erls = rational_erls;
1.372 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
1.373 +
1.374 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.375 +val asms = map (Envir.subst_term subst) pres;
1.376 +if UnparseC.terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
1.377 +then () else error "rewrite.sml: prepat cancel subst";
1.378 +if ([], true) = eval__true thy 0 asms [] erls
1.379 +then () else error "rewrite.sml: prepat cancel eval__true";
1.380 +
1.381 +"===== Rational.thy: add_fractions_p ===";
1.382 +(* if each pat* matches with the current term, the Rrls is applied
1.383 + (there are no preconditions to be checked, they are @{term True}) *)
1.384 +val t = str2term "a / b + 1 / 2";
1.385 +val pat = parse_patt thy "?r / ?s + ?u / ?v";
1.386 +val pres = [@{term True}];
1.387 +val prepat = [(pres, pat)];
1.388 +val erls = rational_erls;
1.389 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
1.390 +
1.391 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.392 +if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
1.393 +then () else error "rewrite.sml: prepat add_fractions_p";
1.394 +
1.395 +"===== Poly.thy: order_mult_ ===";
1.396 + (* ?p matched with the current term gives an environment,
1.397 + which evaluates (the instantiated) "p is_multUnordered" to true*)
1.398 +val t = str2term "x^^^2 * x";
1.399 +val pat = parse_patt thy "?p :: real"
1.400 +val pres = [parse_patt thy "?p is_multUnordered"];
1.401 +val prepat = [(pres, pat)];
1.402 +val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
1.403 + [Num_Calc ("Poly.is'_multUnordered",
1.404 + eval_is_multUnordered "")];
1.405 +
1.406 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.407 +val asms = map (Envir.subst_term subst) pres;
1.408 +if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
1.409 +then () else error "rewrite.sml: prepat order_mult_ subst";
1.410 +if ([], true) = eval__true thy 0 asms [] erls
1.411 +then () else error "rewrite.sml: prepat order_mult_ eval__true";
1.412 +
1.413 +
1.414 +"----------- fun app_rev, Rrls, -------------------------";
1.415 +"----------- fun app_rev, Rrls, -------------------------";
1.416 +"----------- fun app_rev, Rrls, -------------------------";
1.417 +val t = str2term "x^^^2 * x";
1.418 +
1.419 +if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
1.420 +val tm = str2term "(x^^^2 * x) is_multUnordered";
1.421 +eval_is_multUnordered "testid" "" tm thy;
1.422 +
1.423 +case eval_is_multUnordered "testid" "" tm thy of
1.424 + SOME (_, Const ("HOL.Trueprop", _) $
1.425 + (Const ("HOL.eq", _) $
1.426 + (Const ("Poly.is'_multUnordered", _) $ _) $
1.427 + Const ("HOL.True", _))) => ()
1.428 + | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
1.429 +
1.430 +tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := false;
1.431 +val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
1.432 +tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
1.433 +if UnparseC.term2str t' = "x * x ^^^ 2" then ()
1.434 +else error "rewrite.sml Poly.is'_multUnordered doesn't work";
1.435 +
1.436 +(* for achieving the previous result, the following code was taken apart *)
1.437 +"----- rewrite__set_ ---";
1.438 +val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
1.439 + val (t', asm, rew) = app_rev thy (i+1) rrls t;
1.440 +"----- app_rev ---";
1.441 +val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
1.442 + fun chk_prepat thy erls [] t = true
1.443 + | chk_prepat thy erls prepat t =
1.444 + let fun chk (pres, pat) =
1.445 + (let val subst: Type.tyenv * Envir.tenv =
1.446 + Pattern.match thy (pat, t)
1.447 + (Vartab.empty, Vartab.empty)
1.448 + in snd (eval__true thy (i+1)
1.449 + (map (Envir.subst_term subst) pres)
1.450 + [] erls)
1.451 + end)
1.452 + handle _ => false
1.453 + fun scan_ f [] = false (*scan_ NEVER called by []*)
1.454 + | scan_ f (pp::pps) = if f pp then true
1.455 + else scan_ f pps;
1.456 + in scan_ chk prepat end;
1.457 +
1.458 + (*.apply the normal_form of a rev-set.*)
1.459 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
1.460 + if chk_prepat thy erls prepat t
1.461 + then ((*tracing("### app_rev': t = "^(UnparseC.term2str t));*)
1.462 + normal_form t)
1.463 + else NONE;
1.464 +(*fixme val NONE = app_rev' thy rrls t;*)
1.465 +"----- app_rev' ---";
1.466 +val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
1.467 +(*fixme false*) chk_prepat thy erls prepat t;
1.468 +"----- chk_prepat ---";
1.469 +val (thy, erls, prepat, t) = (thy, erls, prepat, t);
1.470 + fun chk (pres, pat) =
1.471 + (let val subst: Type.tyenv * Envir.tenv =
1.472 + Pattern.match thy (pat, t)
1.473 + (Vartab.empty, Vartab.empty)
1.474 + in snd (eval__true thy (i+1)
1.475 + (map (Envir.subst_term subst) pres)
1.476 + [] erls)
1.477 + end)
1.478 + handle _ => false;
1.479 + fun scan_ f [] = false (*scan_ NEVER called by []*)
1.480 + | scan_ f (pp::pps) = if f pp then true
1.481 + else scan_ f pps;
1.482 +tracing "=== poly.sml: scan_ chk prepat begin";
1.483 +scan_ chk prepat;
1.484 +tracing "=== poly.sml: scan_ chk prepat end";
1.485 +
1.486 +"----- chk ---";
1.487 +(*reestablish...*) val t = str2term "x ^^^ 2 * x";
1.488 +val [(pres, pat)] = prepat;
1.489 + val subst: Type.tyenv * Envir.tenv =
1.490 + Pattern.match thy (pat, t)
1.491 + (Vartab.empty, Vartab.empty);
1.492 +
1.493 +(*fixme: asms = ["p is_multUnordered"]...instantiate*)
1.494 +"----- eval__true ---";
1.495 +val asms = (map (Envir.subst_term subst) pres);
1.496 +if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
1.497 +else error "rewrite.sml: diff. is_multUnordered, asms";
1.498 +val (thy, i, asms, bdv, rls) =
1.499 + (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
1.500 + [] : (term * term) list, erls);
1.501 +case eval__true thy i asms bdv rls of
1.502 + ([], true) => ()
1.503 + | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
1.504 +
1.505 +"----------- 2011 thms with axclasses -------------------";
1.506 +"----------- 2011 thms with axclasses -------------------";
1.507 +"----------- 2011 thms with axclasses -------------------";
1.508 +val thm = num_str @{thm div_by_1};
1.509 +val prop = Thm.prop_of thm;
1.510 +atomty prop; (*Type 'a*)
1.511 +val t = str2term "(2*x)/1"; (*Type real*)
1.512 +
1.513 +val (thy, ro, er, inst) =
1.514 + (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
1.515 +val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
1.516 +
1.517 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.518 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.519 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.520 +val thy = @{theory RatEq};
1.521 +val ctxt = Proof_Context.init_global thy;
1.522 +val SOME t = parseNEW ctxt "(3 + -1 * x + x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + x ^^^ 3) = 1 / x";
1.523 +val rls = assoc_rls "RatEq_eliminate"
1.524 +
1.525 +val SOME (t''''', asm''''') =
1.526 + rewrite_set_ thy true rls t;
1.527 +"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
1.528 + rewrite__set_ thy 1 bool [] rls term;
1.529 +"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
1.530 + = (thy, 1, bool, []:(term * term) list, rls, term);
1.531 +
1.532 +(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
1.533 + datatype switch = Appl | Noap;
1.534 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
1.535 + | rew_once ruls asm ct Appl [] =
1.536 + (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
1.537 + | Rule_Set.Seqence _ => (ct, asm)
1.538 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
1.539 + | rew_once ruls asm ct apno (rul :: thms) =
1.540 + case rul of
1.541 + Rule.Thm (thmid, thm) =>
1.542 + (trace1 i (" try thm: " ^ thmid);
1.543 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.544 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
1.545 + NONE => rew_once ruls asm ct apno thms
1.546 + | SOME (ct', asm') =>
1.547 + (trace1 i (" rewrites to: " ^ UnparseC.t2str thy ct');
1.548 + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
1.549 + (* once again try the same rule, e.g. associativity against "()"*)
1.550 + | Rule.Num_Calc (cc as (op_, _)) =>
1.551 + let val _= trace1 i (" try calc: " ^ op_ ^ "'")
1.552 + val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
1.553 + in case Num_Calc.adhoc_thm thy cc ct of
1.554 + NONE => rew_once ruls asm ct apno thms
1.555 + | SOME (_, thm') =>
1.556 + let
1.557 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.558 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
1.559 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.560 + Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
1.561 + val _ = trace1 i (" calc. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
1.562 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
1.563 + end
1.564 + | Rule.Cal1 (cc as (op_, _)) =>
1.565 + let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
1.566 + val ct = TermC.uminus_to_string ct
1.567 + in case Num_Calc.adhoc_thm1_ thy cc ct of
1.568 + NONE => (ct, asm)
1.569 + | SOME (_, thm') =>
1.570 + let
1.571 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.572 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
1.573 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.574 + Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
1.575 + val _ = trace1 i (" cal1. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
1.576 + in the pairopt end
1.577 + end
1.578 + | Rule.Rls_ rls' =>
1.579 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
1.580 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
1.581 + | NONE => rew_once ruls asm ct apno thms)
1.582 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
1.583 + val ruls = (#rules o Rule.Rule_Set.rep) rls;
1.584 +(* val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)*)
1.585 + val (ct', asm') = rew_once ruls [] ct Noap ruls;
1.586 +"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
1.587 + = (ruls, []:term list, ct, Noap, ruls);
1.588 + val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
1.589 +
1.590 + val SOME (ct', asm') = (*case*)
1.591 + rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.592 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
1.593 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
1.594 + = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
1.595 + ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
1.596 +
1.597 + val (t', asms, _ (*lrd*), rew) =
1.598 + rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.599 + (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct;
1.600 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
1.601 + = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
1.602 + (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm), ct);
1.603 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.604 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
1.605 +;
1.606 +(*+*)if UnparseC.term2str r' =
1.607 +(*+*) "\<lbrakk>9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
1.608 +(*+*) "\<Longrightarrow> ((3 + -1 * x + x ^^^ 2) /\n" ^
1.609 +(*+*) " (9 * x + -6 * x ^^^ 2 + x ^^^ 3) =\n" ^
1.610 +(*+*) " 1 / x) =\n" ^
1.611 +(*+*) " ((3 + -1 * x + x ^^^ 2) * x =\n" ^
1.612 +(*+*) " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3))"
1.613 +(*+*)then () else error "instantiated rule CHANGED";
1.614 +
1.615 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.616 +;
1.617 +(*+*)if map UnparseC.term2str p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
1.618 +(*+*)then () else error "stored assumptions CHANGED";
1.619 +
1.620 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.621 +;
1.622 +(*+*)if UnparseC.term2str t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
1.623 +(*+*)then () else error "rewritten term (an equality) CHANGED";
1.624 +
1.625 + val (simpl_p', nofalse) =
1.626 + eval__true thy (i + 1) p' bdv rls;
1.627 +"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
1.628 + (*if*) asms = [@{term True}] orelse asms = [] (*else*);
1.629 +
1.630 +(*+*)if map UnparseC.term2str asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
1.631 +(*+*)then () else error "asms before chk CHANGED";
1.632 +
1.633 + fun chk indets [] = (indets, true) (*return asms<>True until false*)
1.634 + | chk indets (a :: asms) =
1.635 + (case rewrite__set_ thy (i + 1) false bdv rls a of
1.636 + NONE => (chk (indets @ [a]) asms)
1.637 + | SOME (t, a') =>
1.638 + if t = @{term True} then (chk (indets @ a') asms)
1.639 + else if t = @{term False} then ([], false)
1.640 + (*asm false .. thm not applied ^^^; continue until False vvv*)
1.641 + else chk (indets @ [t] @ a') asms);
1.642 +
1.643 + val (xxx, true) =
1.644 + chk [] asms; (*return from eval__true*);
1.645 +"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
1.646 +
1.647 +(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
1.648 +(*+*)(*val rules =
1.649 +(*+*) [Num_Calc ("Rings.divide_class.divide", fn),
1.650 +(*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
1.651 +(*+*) :
1.652 +(*+*) Num_Calc ("HOL.eq", fn),
1.653 +(*+*) Thm ("not_true", "(\<not> True) = False"),
1.654 +(*+*) Thm ("not_false", "(\<not> False) = True"),
1.655 +(*+*) :
1.656 +(*+*) Num_Calc ("Prog_Expr.pow", fn),
1.657 +(*+*) Num_Calc ("RatEq.is'_ratequation'_in", fn)]:
1.658 +(*+*) rule list*)
1.659 +(*+*)chk: term list -> term list -> term list * bool
1.660 +
1.661 + rewrite__set_ thy (i + 1) false bdv rls a (*of*);
1.662 +
1.663 +(*+*)trace_rewrite := true;
1.664 +
1.665 + (*this was False; vvvv--- means: indeterminate*)
1.666 + val (* SOME (t, a') *)NONE = (*case*)
1.667 + rewrite__set_ thy (i + 1) false bdv rls a (*of*);
1.668 +
1.669 +(*+*)UnparseC.term2str a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
1.670 +(*
1.671 + :
1.672 + #### rls: rateq_erls on: x \<noteq> 0
1.673 + :
1.674 + ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
1.675 + ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
1.676 + ##### try calc: HOL.eq'
1.677 + ##### try thm: not_true
1.678 + ##### try thm: not_false
1.679 + ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
1.680 + and True, False are NOT stored ...
1.681 + :
1.682 + ### asms accepted: [x \<noteq> 0] stored: []
1.683 + : *)
1.684 +trace_rewrite := false;
1.685 +( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
1.686 +
1.687 +
1.688 +"----------- fun assoc_thm' -----------------------------";
1.689 +"----------- fun assoc_thm' -----------------------------";
1.690 +"----------- fun assoc_thm' -----------------------------";
1.691 +val thy = @{theory ProgLang}
1.692 +
1.693 +val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
1.694 +if string_of_thm' thy tth = "6 = 2 * 3" then ()
1.695 +else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
1.696 +
1.697 +val tth = assoc_thm' thy ("add_0_left","");
1.698 +if string_of_thm' thy tth = "0 + ?a = ?a" then ()
1.699 +else error "assoc_thm' (add_0_left,\"\") changed";
1.700 +
1.701 +val tth = assoc_thm' thy ("sym_add_0_left","");
1.702 +if string_of_thm' thy tth = "?t = 0 + ?t" then ()
1.703 +else error "assoc_thm' (sym_add_0_left,\"\") changed";
1.704 +
1.705 +val tth = assoc_thm' thy ("add_commute","");
1.706 +if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
1.707 +else error "assoc_thm' (add_commute,\"\") changed"
1.708 +
1.709 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.710 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.711 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.712 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
1.713 + (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
1.714 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
1.715 + (thy, 1, [], rew_ord, erls, bool, thm, term);
1.716 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
1.717 + (thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)
1.718 + val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.719 + val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
1.720 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.721 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.722 +;
1.723 +if UnparseC.term2str lhss = "?a * (?b + ?c)" andalso UnparseC.term2str t = "x * (y + z)" then ()
1.724 +else error "ARGS FOR Pattern.match CHANGED";
1.725 +val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
1.726 +if (Envir.subst_term match r |> UnparseC.term2str) = "x * (y + z) = x * y + x * z" then ()
1.727 + else error "Pattern.match CHANGED";
1.728 +
1.729 +"----------- fun mk_thm ------------------------------------------------------------------------";
1.730 +"----------- fun mk_thm ------------------------------------------------------------------------";
1.731 +"----------- fun mk_thm ------------------------------------------------------------------------";
1.732 +val thy = @{theory Isac_Knowledge}
1.733 +
1.734 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.735 +val thm = @{thm realpow_twoI};
1.736 +val patt_str = "?r ^^^ 2 = ?r * ?r";
1.737 +val term_str = "r ^^^ 2 = r * r";
1.738 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.739 +case parse_patt thy patt_str of
1.740 + Const ("HOL.eq", _) $ (Const ("Prog_Expr.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
1.741 + (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
1.742 +| _ => error "parse_patt ?r ^^^ 2 = ?r * ?r changed";
1.743 +case parse thy term_str of
1.744 + NONE => ()
1.745 +| _ => writeln "parse does NOT take patterns with '?'";
1.746 +
1.747 +val t1 = (#prop o Thm.rep_thm) (num_str thm);
1.748 +if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
1.749 +
1.750 +val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
1.751 +if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
1.752 +
1.753 +(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
1.754 +(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
1.755 + gives a strange thm*);
1.756 +(*while this..*)
1.757 +val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
1.758 + ..gives another strange thm; but it is used and works with rewriting: *);
1.759 +
1.760 +val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
1.761 +if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
1.762 +
1.763 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.764 +val thm = @{thm real_mult_div_cancel2};
1.765 +val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
1.766 +val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
1.767 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.768 +case parse_patt thy patt_str of
1.769 + Const ("Pure.imp", _) $
1.770 + (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
1.771 + (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
1.772 + (Const ("HOL.Trueprop", _) $
1.773 + (Const ("HOL.eq", _) $ _ $ _ )) => ()
1.774 +| _ => error "parse_patt ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n changed";
1.775 +case parse thy term_str of
1.776 + NONE => ()
1.777 +| _ => writeln "parse does NOT take patterns with '?'";
1.778 +
1.779 +val t1 = (#prop o Thm.rep_thm) (num_str thm);
1.780 +if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
1.781 +
1.782 +val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
1.783 +if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
1.784 +
1.785 +(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
1.786 +(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
1.787 + gives a strange thm*);
1.788 +(*while this*)
1.789 +val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
1.790 + gives another strange thm; but it is used and words with rewriting: *);
1.791 +
1.792 +val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
1.793 +if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
1.794 +
1.795 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.796 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.797 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.798 +(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
1.799 +val thy = @{theory};
1.800 +val rls = norm_equation;
1.801 +val term = str2term "x + 1 = 2";
1.802 +
1.803 +val SOME (t, asm) = rewrite_set_ thy false rls term;
1.804 +if UnparseC.term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
1.805 +
1.806 +"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
1.807 +"~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
1.808 +