Re: [isabelle] Specification depends on extra type variables
On Fri, Mar 26, 2010 at 5:49 AM, Viorel Preoteasa
<viorel.preoteasa at abo.fi> wrote:
> I am trying to define a constant which depends on an extra type
> Another approach which seem to work is by defining an uninterpreted
> constant, and give its concrete definition using an axiom:
> f :: "'a => bool";
> axioms f_def:
> "f a = (? g . !u . g u = a)";
> Is the axiomatic solution unsound?
In this particular case, axiom f_def is sound. But this style of axiom
will be unsound in all but the most trivial of instances.
For clarity, here's a type-annotated version of your axiom:
axioms f_def: "f (a::'a) = (EX (g::'b => 'a) . ALL (u::'a). g u = a)"
When you write an axiom with a free type variable (or a free term
variable, for that matter) it like declaring an infinite collection of
axioms all at once, one for each possible instantiation of the free
Your axiom f_def happens to be sound, but only because the RHS is
always true no matter what 'b is. (Constant functions exist for every
type 'b.) So you might as well have written
axioms f_def: "f (a::'a) = True"
But I'd guess that your real example is not so trivial. Here's a
variation where the value of the RHS actually does depend on which
type 'b is instantiated to, since injective functions exist between
some pairs of types, but not all.
axioms f_def2: "f (a::'a) = (EX (g::'b => 'a). inj g)"
Let's look at two different type instances of axiom f_def2:
"f (a::bool) = (EX (g::bool => bool). inj g)"
"f (a::bool) = (EX (g::nat => bool). inj g)"
The first one is equivalent to "f (a::bool) = True", and the second is
equivalent to "f (a:bool) = False". This is clearly unsound. The
general lesson here is that declaring axioms is dangerous, and you
should avoid doing so whenever possible.
If you really want to avoid explicitly passing around an extra dummy
parameter, here's what I would recommend: Declare a locale that fixes
the dummy type parameter of type "'b itself", and define your
constants (which may refer to the locally-fixed type 'b) inside the
This archive was generated by a fusion of
Pipermail (Mailman edition) and