Re: [isabelle] How tactic fold instantiates variables



I donât have anything to explain about the code, other than to note that the comments refer to critical pairs. This is a reminder that a set of rewrite rules can be ambiguous. Instantiating variables is one way to cope with ambiguity, and it also helps if folding the right hand side would involve higher-order matching.

Larry Paulson


> On 23 Jun 2015, at 22:17, Makarius <makarius at sketis.net> wrote:
> 
> (This old thread still looks unsettled.)
> 
> On Fri, 29 May 2015, Daniel Raggi wrote:
> 
>> When folding a definition, why would someone (in some cases), need to
>> specify instantiations of variables using [where "X = ..."]?
>> 
>> I can see how it's useful to do it in some cases to avoid having to
>> backtrack.
> 
> First note that (fold eq) is the same as (unfold eq [symmetric]).
> 
> For more than one equation, there is a slight difference in the initial order, although the details are unclear to me; see src/Pure/raw_simplifer.ML:
> 
>   val rev_defs = sort_lhs_depths o map Thm.symmetric;
> 
> Larry might be able to explain that code "from the depths of time", as he usually says; see
> http://isabelle.in.tum.de/repos/isabelle/rev/e7588b53d6b0
> 





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