*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] How to avoid x \<in> carrier G proofs*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Sat, 11 Dec 2010 12:39:01 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1292065055.2896.11.camel@kirk.ehbuehl.net>*References*: <1292065055.2896.11.camel@kirk.ehbuehl.net>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

Hi Joachim,

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?

Alex

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

**References**:**[isabelle] How to avoid x \<in> carrier G proofs***From:*Joachim Breitner

- Previous by Date: [isabelle] How to avoid x \<in> carrier G proofs
- Next by Date: Re: [isabelle] How to avoid x \<in> carrier G proofs
- Previous by Thread: [isabelle] How to avoid x \<in> carrier G proofs
- 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