[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.