[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.
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
SPASS). But if I insert
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and