*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] How to avoid x \<in> carrier G proofs*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Sat, 11 Dec 2010 11:57:35 +0100*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Hi, 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? Thanks, Joachim 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**

**Follow-Ups**:**Re: [isabelle] How to avoid x \<in> carrier G proofs***From:*Alexander Krauss

**Re: [isabelle] How to avoid x \<in> carrier G proofs***From:*Gerwin Klein

- Previous by Date: Re: [isabelle] Invoking parse translations for subterms inside my parse translation? [SOLVED]
- Next by Date: Re: [isabelle] How to avoid x \<in> carrier G proofs
- Previous by Thread: Re: [isabelle] Invoking parse translations for subterms inside my parse translation? [SOLVED]
- Next by Thread: Re: [isabelle] How to avoid x \<in> carrier G proofs
- Cl-isabelle-users December 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list