Email Gateway (Aug 22 2022 at 10:01): Email Gateway (Aug 22 2022 at 10:01):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isabelle wizards,
I have defined a function with several arguments with the function package, but not all
arguments are supplied in the definition. For example,
fun foo :: "bool ⇒ bool ⇒ bool"
where
"foo True = id"
| "foo False = Not"
The function package generates an elimination rule foo.elims to do case distinctions on
foo. For the function foo, it generates the rule
⟦foo ?x = ?y; ⟦?x; ?y = id⟧ ⟹ ?P; ⟦¬ ?x; ?y = Not⟧ ⟹ ?P⟧ ⟹ ?P
Unfortunately, this rule cannot be used directly if the function is fully applied as in
notepad begin
fix x y
assume "foo x y = True"
then have "x = y"
proof(cases rule: foo.elims)
Is there any clever way to transform foo.elims such that I can use it in such a situation?
I.e., I'd like to transform the rule to something like
⟦foo ?x ?z = ?y; ⟦?x; ?y = id ?z⟧ ⟹ ?P; ⟦¬ ?x; ?y = Not ?z⟧ ⟹ ?P⟧ ⟹ ?P
(In this case, I could of course use foo.cases, but this does not work if I want to do the
case splits automatically with auto & friends.)
I'd prefer to leave the definition eta-contracted, because it is clearer and the
simplifier rewrites partially applied occurrences of foo (which is important because
congruence rules and the induction method sporadically eta-expand terms and then cause
strange effects).
Cheers,
Andreas
Email Gateway (Aug 22 2022 at 10:01):From: Larry Paulson <lp15@cam.ac.uk>
But you could just as easily use the expanded form in the definition, and then derive the contracted forms afterwards. That is likely to be clearer than any massaging of the elimination and induction rules.
Larry Paulson
Email Gateway (Aug 22 2022 at 10:01):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Larry,
You are right that I can almost derive the eta-contracted simp rules with
foo.simp[abs_def]. However, the generated cases rule then also requires all arguments of
the function (given as a tuple). Do you know a way to manipulate the .cases rule? Is that
easier than manipulating .elims?
Andreas
Last updated: Nov 21 2024 at 12:39 UTC