86 val thy = @{theory Complex_Main}; |
86 val thy = @{theory Complex_Main}; |
87 val ctxt = @{context}; |
87 val ctxt = @{context}; |
88 val thm = @{thm add.commute}; |
88 val thm = @{thm add.commute}; |
89 val tm = @{term "x + y*z::real"}; |
89 val tm = @{term "x + y*z::real"}; |
90 |
90 |
91 val SOME (r,_) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm); |
91 val SOME (r,_) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm); |
92 (*is displayed on _TOP_ of <response> buffer...*) |
92 (*is displayed on _TOP_ of <response> buffer...*) |
93 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r); |
93 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r); |
94 if r = @{term "y*z + x::real"} |
94 if r = @{term "y*z + x::real"} |
95 then () else error "rewrite.sml diff.result in rewriting"; |
95 then () else error "rewrite.sml diff.result in rewriting"; |
96 |
96 |
97 "----- rewriting a subterm"; |
97 "----- rewriting a subterm"; |
98 val tm = @{term "w*(x + y*z)::real"}; |
98 val tm = @{term "w*(x + y*z)::real"}; |
99 |
99 |
100 val SOME (r, _) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm); |
100 val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm); |
101 |
101 |
102 "----- ordered rewriting"; |
102 "----- ordered rewriting"; |
103 fun tord (_:subst) pp = LibraryC.termless pp; |
103 fun tord (_:subst) pp = LibraryC.termless pp; |
104 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then () |
104 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then () |
105 else error "rewrite.sml diff.behav. in ord.rewr."; |
105 else error "rewrite.sml diff.behav. in ord.rewr."; |
148 "----------- conditional rewriting creating an assumption---------------------------------------"; |
148 "----------- conditional rewriting creating an assumption---------------------------------------"; |
149 "----------- conditional rewriting creating an assumption---------------------------------------"; |
149 "----------- conditional rewriting creating an assumption---------------------------------------"; |
150 val thm = @{thm nonzero_divide_mult_cancel_right}; |
150 val thm = @{thm nonzero_divide_mult_cancel_right}; |
151 val tm = @{term "x / (2 * x)::real"}; |
151 val tm = @{term "x / (2 * x)::real"}; |
152 |
152 |
153 val SOME (rew, asm) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm); |
153 val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm; |
154 |
154 |
155 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *) |
155 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *) |
156 else error "rewrite.sml diff.result in cond.rew."; |
156 else error "rewrite.sml diff.result in cond.rew."; |
157 |
157 |
158 if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*) |
158 if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*) |
166 "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------"; |
166 "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------"; |
167 val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a"*) |
167 val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a"*) |
168 val tm = @{term "x / (2 * x)::real"}; |
168 val tm = @{term "x / (2 * x)::real"}; |
169 val erls = eval_rls; |
169 val erls = eval_rls; |
170 |
170 |
171 (**)val SOME (rew, asm) = rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm; |
171 (**)val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm; |
172 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"): |
172 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"): |
173 dest_Trueprop |
173 dest_Trueprop |
174 ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **) |
174 ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **) |
175 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) = |
175 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) = |
176 (thy, dummy_ord, erls, false, thm, tm); |
176 (thy, Rewrite_Ord.function_empty, erls, false, thm, tm); |
177 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) = |
177 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) = |
178 (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term); |
178 (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term); |
179 |
179 |
180 (**) val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path) |
180 (**) val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path) |
181 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct; |
181 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct; |
208 "----------- step through 'and rew_sub': ----------------"; |
208 "----------- step through 'and rew_sub': ----------------"; |
209 "----------- step through 'and rew_sub': ----------------"; |
209 "----------- step through 'and rew_sub': ----------------"; |
210 "----------- step through 'and rew_sub': ----------------"; |
210 "----------- step through 'and rew_sub': ----------------"; |
211 (*and make asms without Trueprop, beginning with the result:*) |
211 (*and make asms without Trueprop, beginning with the result:*) |
212 val tm = @{term "x / (2 * x)::real"}; |
212 val tm = @{term "x / (2 * x)::real"}; |
213 val (t', asm, _, _) = rew_sub ctxt 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm; |
213 val (t', asm, _, _) = rew_sub ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true [] (Thm.prop_of thm) tm; |
214 (*show_types := false;*) |
214 (*show_types := false;*) |
215 "----- evaluate arguments"; |
215 "----- evaluate arguments"; |
216 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = |
216 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = |
217 (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm); |
217 (thy, 0, [], Rewrite_Ord.function_empty, Rule_Set.empty, true, [], (Thm.prop_of thm), tm); |
218 "----- step 1: LHS, RHS of rule"; |
218 "----- step 1: LHS, RHS of rule"; |
219 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop |
219 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop |
220 o Logic.strip_imp_concl) r; |
220 o Logic.strip_imp_concl) r; |
221 UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a"; |
221 UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a"; |
222 UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?a"; |
222 UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?a"; |
243 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
243 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
244 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
244 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
245 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
245 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
246 "----- step 0: args for rewrite_terms_, local fun"; |
246 "----- step 0: args for rewrite_terms_, local fun"; |
247 val (thy, ord, erls, equs, t) = |
247 val (thy, ord, erls, equs, t) = |
248 (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"], |
248 (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.str2term "x = 0"], |
249 TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2"); |
249 TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2"); |
250 "----- step 1: args for rew_"; |
250 "----- step 1: args for rew_"; |
251 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t); |
251 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t); |
252 "----- step 2: rew_sub"; |
252 "----- step 2: rew_sub"; |
253 rew_sub ctxt 1 [] ord erls false [] (HOLogic.Trueprop $ r) t; |
253 rew_sub ctxt 1 [] ord erls false [] (HOLogic.Trueprop $ r) t; |
254 "----- step 3: step through rew_sub -- inefficient: goes into subterms"; |
254 "----- step 3: step through rew_sub -- inefficient: goes into subterms"; |
255 |
255 |
256 |
256 |
257 val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t; |
257 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; |
258 writeln "---------- rewrite_terms_ 1---------------------------"; |
258 writeln "---------- rewrite_terms_ 1---------------------------"; |
259 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
259 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
260 else error "rewrite.sml rewrite_terms_ [x = 0]"; |
260 else error "rewrite.sml rewrite_terms_ [x = 0]"; |
261 |
261 |
262 val equs = [TermC.str2term "M_b 0 = 0"]; |
262 val equs = [TermC.str2term "M_b 0 = 0"]; |
263 val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2"; |
263 val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2"; |
264 val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t; |
264 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; |
265 writeln "---------- rewrite_terms_ 2---------------------------"; |
265 writeln "---------- rewrite_terms_ 2---------------------------"; |
266 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
266 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
267 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]"; |
267 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]"; |
268 |
268 |
269 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"]; |
269 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"]; |
270 val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2"; |
270 val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2"; |
271 val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t; |
271 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; |
272 writeln "---------- rewrite_terms_ 3---------------------------"; |
272 writeln "---------- rewrite_terms_ 3---------------------------"; |
273 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
273 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
274 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]"; |
274 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]"; |
275 |
275 |
276 |
276 |
656 |
656 |
657 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; |
657 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; |
658 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; |
658 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; |
659 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; |
659 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; |
660 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) = |
660 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) = |
661 (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"}); |
661 (@{theory}, Rewrite_Ord.function_empty, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"}); |
662 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) = |
662 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) = |
663 (thy, 1, [], rew_ord, erls, bool, thm, term); |
663 (thy, 1, [], rew_ord, erls, bool, thm, term); |
664 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = |
664 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = |
665 (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct) |
665 (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct) |
666 val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r |
666 val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r |