From: Mike Stannett <cl-isabelle-users@lists.cam.ac.uk>
We've been looking at the behaviour of polymorphic constants, and have
derived something that seems a bit anomalous. The following proof,
involving a polymorphic constant called polyval, shows that
"polyval = (0::nat) ∧ polyval = (True::bool)"
which seems to say that polyval is two different constants, of different
types, at the same time. Is this intended?, i.e. does the declaration of
polyval as a polymorphic constant mean "polyval is a constant whose type is
as yet undetermined" or "each type is declared to contain its own constant
called polyval"?
fun demo :: "nat ⇒ bool ⇒ nat"
where "demo x y = (if y then x + 1 else 0)"
consts polyval :: "'a"
abbreviation polyresult :: "nat"
where "polyresult ≡ demo (polyval :: nat) (polyval :: bool)"
lemma michael:
assumes "polyresult = 1"
shows "polyval = (True::bool)"
by (metis assms demo.elims zero_neq_one)
lemma mps:
assumes "polyresult = 1"
shows "polyval = (0 :: nat)"
using assms michael by fastforce
lemma unexpected:
assumes "polyresult = 1"
shows "polyval = (0::nat) ∧ polyval = (True::bool)"
proof -
have lhs: "polyval = (0::nat)" using assms mps by blast
have rhs: "polyval = (True::bool)" using assms michael by blast
show ?thesis using lhs rhs by blast
qed
Regards, Michael Foster/Mike Stannett
From: Peter Lammich <lammich@in.tum.de>
That's the expected behavior of Isabelle's top-level polymorphism: the
polymorphic types can be instantiated to whatever (sort-compatible) type.
Note however, that this does not hold for fixed/bound variables, e.g. in
"let polyval::'a = undefined in (polyval::nat) < 5"
you get a type-error, as 'a is not equal to nat.
From: Lawrence Paulson <lp15@cam.ac.uk>
This is how overloading works. Your ability to write x+y without knowing whether + refers to addition on natural numbers, integers, rationals, reals, complex numbers, quaternions, etc, hinges on it.
And thanks to the axiomatic type class system, things are organised such that innumerable arithmetic laws are made available to all types satisfying the necessary underlying axioms. And similarly for overloading in other domains.
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC