Re: [isabelle] question about using identities for rewriting



auto, blast, force all do logical reasoning. If you need just pure rewriting, try simp, or even just subst.

Larry Paulson


On 23 Apr 2014, at 00:46, noam neer <noamneer at gmail.com> wrote:

> well, suppose I have two expressions that differ only in some
> sub-sub-...-sub-expresion,
> and I want to prove them equal. is there a way to tell 'auto' (or any
> other tactic) to focus
> its efforts and transformation on that part, thus reducing the number
> of transformations it tries ?
> 
> On Tue, Apr 22, 2014 at 10:53 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>> Rewriting does not backtrack. The assumption is that you are using a rewrite system that normalises in some way, so that backtracking serves no purpose.
>> 
>> Larry Paulson
>> 
>> 
>> On 22 Apr 2014, at 20:42, noam neer <noamneer at gmail.com> wrote:
>> 
>>> so, if I understand correctly, the automatic simplifier picks and
>>> applies transformations to the terms until it proves them equal (if
>>> this ever happens,)
>>> and it never backtracks or starts afresh from the original problem to
>>> try a new path ?
>> 
> 
> 
> 
> -- 
> I can't see very far,
> I must be standing on the shoulders of midgets.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.