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
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
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'.
This archive was generated by a fusion of
Pipermail (Mailman edition) and