Email Gateway (Aug 22 2022 at 12:38): Email Gateway (Aug 22 2022 at 12:38):From: Makarius <makarius@sketis.net>
On Wed, 3 Feb 2016, Viorel Preoteasa wrote:
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
unsimplifiedval 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.
Schematic type variables in goal states or terms that should be simplified
are notorious for surprises. The quickest way to avoid that in the given
example is to use Logic.unvarify_global on pair_b, but note that "global"
operations don't work in local contexts, and locale contexts are the rule
and not the exception.
Attached is the theory with the ML function implementing this
simplification.
Some more notes after reading through this for 10min:
always use formal antiquotation instead of literal string constants,
e.g. @{const_name Trueprop}, @{type_name fun};
observe maximum line length of 80-100 chars;
never use hardwired Free variables like "Aux_Var", "u", "v", "w" in
production code;
see "implementation" manual ch. 0 about Isabelle/ML usage;
The manual provides general background information and a few examples,
with important functions mentioned in the text as entry points to the
sources. E.g. Variable.import, Variable.export, Variable.trade may help
to get a feeling how the context discipline with locally fixed and
exported schematic variables works.
Makarius
Email Gateway (Aug 22 2022 at 12:46):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
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
TestAsmRewrite.thy
Email Gateway (Aug 22 2022 at 12:47):From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s
Email Gateway (Aug 22 2022 at 12:48):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
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.
Viorel
Last updated: Apr 26 2024 at 12:28 UTC