Re: [isabelle] Thm.cterm_of does not check sort constraints

On 29/05/2020 12:00, Manuel Eberl wrote:
> I just noticed something odd. When a polymorphic constant has sort
> constraints, you normally cannot write it down with its type
> instantiated to a type that does not fulfil these constraints. For
> instance, term ‹-1 :: nat› or @{cterm "-1 :: nat"} do not work because
> "nat" does not have the sort "uminus".
> However, when one constructs the term in ML and then certifies it with
> Thm.cterm_of, it works:
> ML_val ‹
> let
>   val t =
>     Const (@{const_name "uminus"}, @{typ "nat ⇒ nat"}) $ @{term "1 :: nat"}
> in
>   Thm.cterm_of @{context} t
> end
> ›

That is the normal expected behaviour: sort constraints for constants are
merely an extra sanity check in abstract syntax (Syntax.check operations), but
have no relevance for the logic.

Even more, there can be additional type constraints for constants that
Syntax.check will observe, but Thm.cterm_of doesn't.

> Is this for performance reasons?

No, it is to get concepts right and have an implementation that fits to these
concepts. Arriving there has required many years, approx. from 1994 to 2008.

> (For those wondering why this is okay on a logical level, the negation
> operator is essentially acting as an unspecified function, so "-1 ::
> nat" is not /actually/ -1, but it is equal to some "proper" natural
> number, we just don't know which one)

Conventional logic can always have terms that are uninterpreted or "non-denoting".


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