# Re: [isabelle] Two small improvements for Isabelle/HOL

Hi Christoph,

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.

`Adding more automatically generated stuff is not for free in terms of
``performance and scalability. So one would want some good empirical
``evidence before doing something like that by default.
`

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

`Sledgehammer has seen quite a bit of improvement recently. The current
``development version gives me a metis call that completes in 94ms.
`

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.

`In the development version I get the same metis call as above, so
``nothing gained.
`

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.

`It is very hard to make such statements in general. Also, (in)finiteness
``proofs are a bit special. They are often trivial for humans but
``automation is particularly weak there. Probably
`

Additionally I think that a lemma "inj f ==> inj_on f A" would be nice to have.

`Well, this is just subset_inj_on[OF _ subset_UNIV]. A reason for having
``it explicitly could be that people might search for it. Unfortunately,
``even when it is present, a search for "inv inv_on" doesn't show it,
``since inv is just an abbreviation... Too bad.
`
Alex

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