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.