*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Fri, 28 May 2010 15:21:53 +0200*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Hi, I’m currently working on a submission to the AFP, formalizing the construction of Free Groups. While proving that bijective sets of generators produce isomorphic Free Groups, I came across a problem where I cannot continue, and it seems to be 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)" and expected to close this using "by auto", as I did in similar situations before. This fails. Unwrapping the proof and trying to do it manually with Isar steps, I end up with this state (as given by i3p): proof (prove): step 38 goal (1 subgoal): 1. xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1) variables: thesis :: bool f :: 'b ⇒ 'c x :: (bool × 'c) list gens1 :: 'b ⇒ bool xa :: (bool × 'b) list type variables: 'b, 'c, 'h, 'i :: type but "apply assumption" does not work. It is also not a i3p bug, as the IsaMakefile also fails to build the theory. I’d be grateful if someone else could try it and see if he can reproduce the problem, and maybe tell me how I can work around the issue. The theory Free-Groups also uses http://darcs.nomeata.de/afp-Free-Groups/Cancelation.thy and if you have darcs installed, you can just run darcs get http://darcs.nomeata.de/afp-Free-Groups/ Thanks, Joachim -- 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] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable***From:*Lawrence Paulson

**Re: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable***From:*Brian Huffman

**Re: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable***From:*Makarius

- Previous by Date: [isabelle] PhD position available on `The Productive Use of Failure in Formal Methods'
- Next by Date: [isabelle] Automated proofs for lattices
- Previous by Thread: [isabelle] PhD position available on `The Productive Use of Failure in Formal Methods'
- Next by Thread: Re: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable
- 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