Re: [isabelle] Two small improvements for Isabelle/HOL
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.
datatype ident = Ident string
"\<not> finite (UNIV :: ident set)"
apply (drule_tac h="inv Ident" in finite_imageI)
This gives me a "metis line" that doesn't work (I only use E and
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
by (simp add:inj_on_def)
before our theorem both E and SPASS can find a working solution really
In the development version I get the same metis call as above, so
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and