Re: [isabelle] Using Simplifier.asm_rewrite

Hi Tobias,

Thank you for the answer. I will do as you suggest. Anyway, my starting
theorem does not have schematic variables. In the process it seems
that I need some schematic variables, for example to combine theorems
with OF, but I will make schematic just the variables that are needed.


On 02/04/2016 09:39 AM, Tobias Nipkow wrote:
> This may have something to do with the fact that hypotheses in
> theorems may not contain schematic variables. Or because the rewrit
> step would (or appears to) require instantiation of a schematic
> variable in the term to be rewritten. If it does not work it is safe
> to assume that it is an inherent limitation and you have to convert
> schematic to ordinary variables first.
> Tobias
> On 03/02/2016 15:29, Viorel Preoteasa wrote:
>> I am trying to use asm_rewrite to simplify a term f(u,v,w) under some
>> assumptions p(u,v,w). p and f are given as a pair (p,f) and p and f have
>> the same domain type. For this I construct in ML the term
>> "p(u,v,w) ==> Aux_Var = f(u,v,w)".
>> In my test f(u,v,w) = ((if u + v < 10 then w else w + 1) + 2)
>> and p(u,v,w) = (u + v < 10), and the goal is to simplify
>> f to f(u,v,w) = w + 2 under the assumption p(u,v,w).
>> If I define in ML
>> val pair_a = @{term "(term for p, term for f)"};
>> and I apply the procedure described above all works well,
>> however if instead I define the pair as the right hand
>> side of a definition that contains the same term for the
>> pair, the simplification does not work. The "if" term stays
>> unsimplified
>> val pair_b =  Thm.term_of (Thm.rhs_of ( @{thm Test_Pair_def}));
>> The only difference between pair_a and pair_b seems to be the
>> types. In pair_a there are simple type variables, while in pair_b
>> there are schematic type variables.
>> Attached is the theory with the ML function implementing this
>> simplification. At the end it defines two variables simp_a_th
>> simp_b_th holding the simplifications of the two terms
>> pair_a and pair_b. In pair_a "if" is simplified, while in pair_b
>> "if" is not simplified. It works the same in Isabelle2015 and
>> also Isabelle2016-RC3.
>> Why is this difference? Is it possible to get the same simplification
>> result also on the pair_b term?
>> Best regards,
>> Viorel Preoteasa

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