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



On Fri, 28 May 2010, Joachim Breitner wrote:

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)"

As a rule of thumb, whenever an inference does not work as anticipated, there is a > 50% chance that it is due to more general types than expected. When copying large parts of machine generated goal state back into the text the formal syntactic connection between certain terms is often lost, and the system will infer different types where they should actually coincide.

The goal state of 'obtain' consists mostly of formal noise to make automated tools happy. If you do not manage to solve it "by auto" or "by blast+" or similar, you should compose this piece of existential reasoning carefully. The Isar context gives you a rule called "that" for the final step, when you have the things you introduce here already in your hands -- due suitable preceeing steps. If you apply that rule too early, say in the very beginning, it is unlikely to be able to finish an 'obtain'.


	Makarius


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