# [isabelle] Two small improvements for Isabelle/HOL

Hallo,
a colleague and I came to the conclusion that it would be nice to have
injectivity theorems for datatype constructors (example below). These
are really easily proven - but I think they could help sledgehammer or
tactics like auto/blast.
Our example:
datatype ident = Ident string
theorem infinite_idents:
"\<not> finite (UNIV :: ident set)"
apply clarify
apply (drule_tac h="inv Ident" in finite_imageI)
sledgehammer
This gives me a "metis line" that doesn't work (I only use E and
SPASS). But if I insert
lemma Ident_inj:
"inj Ident"
by (simp add:inj_on_def)
before our theorem both E and SPASS can find a working solution really
quickly. So I think it would help to add theorems like "inj
<Constructor>" to the theorems generated for datatypes. I know about
<type>.inject which basically contains "inj <Constructor>" but
automatic methods apparently don't find that connection.
Additionally I think that a lemma "inj f ==> inj_on f A" would be nice to have.
Regards,
Christoph Feller

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*