[isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable



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
Description: This is a digitally signed message part



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