*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Sat, 29 May 2010 07:24:35 -0700*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <1275052913.2458.11.camel@kirk>*References*: <1275052913.2458.11.camel@kirk>*Sender*: huffman.brian.c at gmail.com

Hi Joachim, I managed to reproduce your problem, and I think I can help explain what is going on. At this point in your proof: > goal (1 subgoal): > 1. xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1) Try turning on Isabelle > Settings > Show Consts in Proof General. You can see that the two occurrences of "free_group" actually have slightly different types. (The records that they return do have the same type in the "carrier" field, at least.) If you go back up to the definition of "free_group" (for which you have not provided a type annotation), Isabelle will print out the inferred type as you step over the definition in Proof General: constants free_group :: "('a => bool) => (| carrier :: (bool * 'a) list => bool, mult :: (bool * 'b) list => (bool * 'b) list => (bool * 'b) list, one :: (bool * 'b) list |)" So the "carrier" field is constrained to match the type of the set argument, but strangely, the "mult" and "one" fields are allowed to have different element types. As a workaround, you can just give a type annotation for "free_group", and then everything should work out as you expect: definition free_group :: "'a set => ((bool * 'a) list) monoid" where ... If there is a bug in Isabelle, it is in the type inference for records. It seems really strange that the inferred type for "free_group" would allow different element types for "carrier" vs. "mult" and "one". Especially since the types of the accessor functions "mult" and "one" actually require the element types to be the same! This is really strange behavior, but at least it is easy to work around it using a type annotation. - Brian On Fri, May 28, 2010 at 6:21 AM, Joachim Breitner <mail at joachim-breitner.de> wrote: > 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 >

**Follow-Ups**:

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

- Previous by Date: Re: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable
- Next by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Previous by Thread: Re: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable
- 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