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

Hi Alexander,

Am Samstag, den 11.12.2010, 12:39 +0100 schrieb Alexander Krauss:
> > 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.
> This is a notorious problem, and there is no satisfactory solution. From 
> 2011 on I'll be working on an infrastructure to deal with this 
> (basically recovering what type systems do on the level of reasoning), 
> but I am not expecting to have something usable for quite some time.

great, I am looking forward to that. And at least I’m not doing
something stupid :-).

> > PS: Is it ok to create personal branches, named appropriately, on
> > where I could push my work
> > to cite it here?
> Please don't do this! Having everybody's private branches centrally is a 
> maintenance nightmare. Instead you can easily publish your own branch 
> (read: clone of the repository with your own changes) on the web. This 
> is what Mercurial is good at. If you don't have a server, there are also 
> public hosting sites.

Ok, just asking.


Joachim Breitner
  e-Mail: mail at
  ICQ#: 74513189
  Jabber-ID: nomeata at

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

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