[isabelle] How to avoid x \<in> carrier G proofs


I’m trying to add the Nielsen-Schreier theorem to the FreeGroups theory
in AFP. I’m following a proof in a modern text book¹ which seems to be
sufficiently rigorous to base on. Yet, I needed almost 500 lines and a
whole day just to almost proof the first item in the first lemma  – that
is less than half a page of proof-related definitions and lemmata in the
book. I get the feeling that I’m doing it wrong.

Most of the time I seem to be spending with proving that some element is
in the carrier of the group, i.e. "x \<in> carrier (free_group gens)",
which is “obvious” to the mathematician. Most group-related lemmata have
such a proposition in their premises, so I need to careful cite the
right carrier-statements before any kind of automation would work.

To me it seems that if I had a type for the set of group elements, then
type inference would had no trouble showing these requirements. But, if
I understand correctly, that would require dependent types (because the
type would encapsulate the parameter "gens"), which are not supported in
Isabelle. Is that right? Is it also right within a locale, or can locale
contexts introduce types?

Are there work-arounds or other best practice to handle such a problem?


PS: Is it ok to create personal branches, named appropriately, on
http://afp.hg.sourceforge.net/hgweb/afp/afp/ where I could push my work
to cite it here?

¹ http://books.google.de/books?id=RGzK_DOTijsC&lpg=PA285&dq=schreier-nielsen&pg=PA285#v=onepage&q&f=false

Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de

Attachment: signature.asc
Description: This is a digitally signed message part

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