Re: [isabelle] Using Simplifier.asm_rewrite



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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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