282 val subst = [(TermC.parse_test @{context} "(bdv::real)", TermC.parse_test @{context} "(x::real)")]; |
282 val subst = [(TermC.parse_test @{context} "(bdv::real)", TermC.parse_test @{context} "(x::real)")]; |
283 val SOME (t''''', _) = rewrite_set_inst_ ctxt true subst d2_polyeq_bdv_only_simplify t; |
283 val SOME (t''''', _) = rewrite_set_inst_ ctxt true subst d2_polyeq_bdv_only_simplify t; |
284 (* steps in rls d2_polyeq_bdv_only_simplify:*) |
284 (* steps in rls d2_polyeq_bdv_only_simplify:*) |
285 |
285 |
286 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*) |
286 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*) |
287 t |> UnparseC.term; t |> TermC.atomty; |
287 t |> UnparseC.term; t |> TermC.atom_trace_detail @{context}; |
288 val thm = @{thm d2_prescind1}; |
288 val thm = @{thm d2_prescind1}; |
289 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty; |
289 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atom_trace_detail @{context}; |
290 val SOME (t', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t; UnparseC.term t'; |
290 val SOME (t', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t; UnparseC.term t'; |
291 |
291 |
292 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) |
292 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) |
293 --> x = 0 | -6 + 5 * x = 0*) |
293 --> x = 0 | -6 + 5 * x = 0*) |
294 t' |> UnparseC.term; t' |> TermC.atomty; |
294 t' |> UnparseC.term; t' |> TermC.atom_trace_detail @{context}; |
295 val thm = @{thm d2_reduce_equation1}; |
295 val thm = @{thm d2_reduce_equation1}; |
296 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty; |
296 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atom_trace_detail @{context}; |
297 val SOME (t'', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t'; UnparseC.term t''; |
297 val SOME (t'', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t'; UnparseC.term t''; |
298 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" |
298 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" |
299 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))" |
299 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))" |
300 *) |
300 *) |
301 if UnparseC.term t'' = "x = 0 \<or> - 6 + 5 * x = 0" then () |
301 if UnparseC.term t'' = "x = 0 \<or> - 6 + 5 * x = 0" then () |