On Tue, 28 May 2013, Stefan Berghofer wrote:
Types as well as terms are unified. The outermost functions assume
the terms to be unified already have the same type. In resolution,
this is assured because both have type "prop".
So it is the expected behaviour that the unification functions cannot
cope with the above example, since it does not satisfy this
precondition.
I am getting a bit uneasy about that for two reasons:
(1) There might be really something wrong in Thm.bicompose_aux or
Thm.assumption that fails to "assure" such implicit assumptions of
unify.ML.
(2) The notorious problem of "hidden polymorphism", i.e. extra
generality of types that is not seen on the surface, and thus needs
to be treated while walking into the term structure.
The second point might be relevant for Pattern.match as well: it does one
typ_match thy on the outside, and then only for Free/Const/Bound, but not
for Var.
So we seem to be back at the implicit global assumption that the types of
Vars happen to work out "magically", without further ado. There used to
be that comment in really ancient Isabelle versions, before Stefan made an
explicit check that it does not go wrong, but here it did go wrong.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
