Email Gateway (Aug 03 2025 at 13:32): Email Gateway (Aug 03 2025 at 13:32):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I just happened to notice the following within a few lines of each other in src/HOL/Fun.thy
(Isabelle 2025):
lemma inj_on_subset:
assumes "inj_on f A"
and "B ⊆ A"
shows "inj_on f B"
proof (rule inj_onI)
fix a b
assume "a ∈ B" and "b ∈ B"
with assms have "a ∈ A" and "b ∈ A"
by auto
moreover assume "f a = f b"
ultimately show "a = b"
using assms by (auto dest: inj_onD)
qed
lemma subset_inj_on: "inj_on f B ⟹ A ⊆ B ⟹ inj_on f A"
unfolding inj_on_def by blast
They seem to be completely redundant, and in fact the first version can be proved by
the shorter proof:
using assms unfolding inj_on_def by blast
which corresponds to the proof that appears for the second version.
- Gene Stark
OpenPGP_0x5C7344E4A8F23061.asc
OpenPGP_signature.asc
Email Gateway (Aug 03 2025 at 16:29):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for pointing this out. I believe I got rid of it about four months ago, so it won't be in the next release.
On 3 Aug 2025, at 14:06, Eugene W. Stark <isabelle-users@starkeffect.com> wrote:
I just happened to notice the following within a few lines of each other in src/HOL/Fun.thy
(Isabelle 2025):
Last updated: Aug 20 2025 at 20:23 UTC