Email Gateway (Jul 14 2022 at 14:04): Email Gateway (Jul 14 2022 at 14:04):From: Tobias Nipkow <nipkow@in.tum.de>
Given
definition f :: "nat ⇒ nat ⇒ bool" where "f x y = True"
abbreviation "g x == f 0 x"
lemma lem: "∀x. g x"
by(simp add: f_def)
the antiquotation @{thm lem} in a LaTeX document prints as "All g", i.e. it was
eta contracted. The lemma itself is not contracted internally. ML‹Thm.concl_of
@{thm lem}› yields
Const ("HOL.Trueprop", "bool ⇒ prop") $
(Const ("HOL.All", "(nat ⇒ bool) ⇒ bool") $
Abs ("x", "nat",
Const ("Sorting_FDS.f", "nat ⇒ nat ⇒ bool") $ Const
("Groups.zero_class.zero", "nat") $ Bound 0)):
When I remove the abbreviation and phrase the lemma as "∀x. f 0 x", it works
fine, nothing is contracted.
The behaviour itself, I expect, is well known. My question: can I avoid the eta
contraction by some trick (without having to modify the lemma)? This, for
example, does not help: @{thm [eta_contract=false] lem}.
Any help is much appreciated
Tobias
smime.p7s
Email Gateway (Jul 20 2022 at 13:43):From: Tobias Nipkow <nipkow@in.tum.de>
A followup: the behaviour I described in my earlier email has got nothing to do
with latex document preparation. It can be observed already when working with
Isabelle interactively, e.g. when looking at the `result' of the proof of lem:
theorem lem: All g
Tobias
smime.p7s
Last updated: Apr 20 2024 at 01:05 UTC