[isabelle] Thm.cterm_of does not check sort constraints



Hello,

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
›

This outputs

val it = "- (1::nat)": cterm

It's not a soundness problem, but I still find this behaviour somewhat
unexpected. I would naïvely have thought it would be impossible to get
the natural number "-1". Is this intended? Is this for performance reasons?

(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)

Manuel




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