On Wed, 29 May 2013, Makarius wrote:
Without the latter, src/HOL/Metis_Examples/Clausification.thy crashes at
the very end, due to divergence of types of certain Vars, types that
cannot be unified. This is very odd, but should not be a problem at the
moment: Metis should work as before.
Just for completeness, here is the original crash of Metis proof
reconstruction at Isabelle/0fa3b456a267:
lemma ex_tl: "EX ys. tl ys = xs"
using tl.simps(2) by fast
lemma "(∃ys∷nat list. tl ys = xs) ∧ (∃bs∷int list. tl bs = as)"
by (metis ex_tl)
Metis: Failed to replay Metis proof
inst_inference: ("COMP", 1,
["Meson.skolem (Meson.COMBK (tl ((?MesonSK_0_0_0_ys1∷nat
list ⇒ nat list) (xs∷nat \
list)) = xs) (0∷nat)) ⟹
tl ((?MesonSK_0_0_0_ys1∷int list ⇒ int list)
(?MesonV_0_1_0_xs1∷int list)) = (as\
∷int list) ⟹ False"
[.],
"PROP ?psi2 ⟹ PROP ?psi2"])
The failure of COMP is via cterm_instantiate/instantiate_normalize: after
the instantiation, there are ?ys1 of different types, so the extra type
unification of Vars in COMP will fail.
(Note that the pretty-printed exception content is produced via regular
and documented @{make_string} sneaked into the proper spot in the ML code,
without committing that. Many people only know the "secret"
PolyML.makestring, with its unformatted text-only output.)
In 6ba76ad4e679 this crash is avoided: already incremented composition
problems omit the extra type unification, just like plain resolution. This
merely pushed the inherent problem elsewhere, so in 568b2cd65d50
resolve_inc_tyvars is back where types of equal Vars are *not* unified,
despite its lengthy workaround for exactly that.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
