[isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.



Hi all,

While updating some large proofs to Isabelle2013-1, I discovered
a change in the behaviour of "blast" in the presence of flex-flex pairs.
In particular, in Isabelle2013-1, "apply blast" appears to eliminate
flex-flex pairs, even if the particular goal blast is working on doesn't
actually involve any schematics. This can make the larger theorem being
worked on unprovable.

For example, consider the following snippet:

    (* Silly lemma to generate a flex-flex pair. *)
    schematic_lemma "!!x y a b. (1 = 1) & f ((x = y) = (a = b)) = ?P x y a b"
      apply (subst (1 3) eq_commute)
      apply (rule conjI)
       (* Two subgoals exist; only the second involves schematics. *)
       apply blast

In Isabelle2013 the "apply blast" would leave the flex-flex constraints
unchanged. In Isabelle2013-1 and Isabelle2013-2, the constraint
disappears. In more complex proofs, this can make finishing the proof
impossible.

Is this behaviour of Isabelle2013-1/2 expected, or is it a regression?

(I don't have a good grasp on the finer points of higher order
unification and flex-flex constraints, so please forgive me if I am
using incorrect terminology.)

Cheers,
David



________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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