*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable*From*: Makarius <makarius at sketis.net>*Date*: Sat, 29 May 2010 22:02:16 +0200 (CEST)*In-reply-to*: <1275052913.2458.11.camel@kirk>*References*: <1275052913.2458.11.camel@kirk>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Fri, 28 May 2010, Joachim Breitner wrote:

While proving that bijective sets of generators produce isomorphic FreeGroups, I came across a problem where I cannot continue, and it seems tobe an Isabelle bug.In line of 337 of http://darcs.nomeata.de/afp-Free-Groups/Free-Groups.thy I try to do this assume "x ∈ image (map (prod_fun id f)) (carrier (free_group gens1))" then obtain y :: "(bool × 'b) list" where "x = map (prod_fun id f) y" and "y ∈ carrier (free_group gens1)"

Makarius

**References**:**[isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Date: Re: [isabelle] problem with sort inference
- Previous by Thread: Re: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable
- Next by Thread: [isabelle] Automated proofs for lattices
- Cl-isabelle-users May 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