Hi all, just a synopsis of the whole matter of sort constraints for constants.
a) Sort constraints for code generation. Concerning sort constraints
and datatype constructors, everything has been said already in this
thread. Generally, for code generation sort constraints *have*
operational relevance. This is a fundamental difference to the logic
itself where there is no notion of execution.
b) Sort constraints have *no* logical relevance. Indeed, given a
definition foo :: "'a::s" where
"foo ['a::s] = rhs"
is internally stored as
"foo [?'a::{}] == rhs"
which is the »most correct« form of a definition because only then it is
definitional: foo [?'a::{}] can be unfolded for arbitrary instances of
?'a . Note that foo_def carries a sort constraint for 'a; this is an
example how a specification by definition may be more special than the
underlying primitive definition, and is not restricted to sort
constraints, e.g. as in:
definition foo :: "'a::s" where
"P ==> foo ['a::s] = rhs"
c) Sort constraints as syntactic device. Here the parser is instructed
to enfore sort constraints on constants.
Hope this helps,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
