Alex Mobius (Apr 20 2026 at 21:46): Alex Mobius (Apr 20 2026 at 21:46):Found this while doing some exercises:
lemma f_the_inv_into_f_bij_betw:
"bij_betw f A B ⟹ (bij_betw f A B ⟹ x ∈ B) ⟹ f (the_inv_into A f x) = x"
unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
Why the extra implication in the second premise? The inj_on version doesn't have anything of the sort.
Manuel Eberl (Apr 21 2026 at 19:20):Good question. This looks pretty odd.
Jan van Brügge (Apr 22 2026 at 13:00):I used theorems in that style when I had to use them with erule (so it chooses the right assumption and correctly deals with higher order unification), but still needed the assumption for later in the proof. Maybe this was a similar case? I'd love to have a version of erule/eresolve_tac that keeps the assumption and only uses it for unification
Alex Mobius (Apr 22 2026 at 14:41):@Jan van Brügge so you're saying that this is essentially for erule to leave the bij_betw in?
Jan van Brügge (Apr 22 2026 at 14:41):it is just a guess ¯\_(ツ)_/¯
Dmitriy Traytel (Apr 22 2026 at 14:58):Looking at the mercurial history, this is a lemma that used to live in src/HOL/BNF_Least_Fixpoint.thy. At that time, its only usage was in tactics used by the datatype command (src/HOL/Tools/BNF/bnf_lfp_tactics.ML). I do not recall the precise usage, but what Jan writes makes sense to me as a plausible explanation. In 2020, the lemma was moved to Fun.thy (rather than e.g., creating an alternative lemma that has a more canonical shape).
Last updated: May 01 2026 at 16:59 UTC