*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] Specification depends on extra type variables*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Sat, 27 Mar 2010 08:04:35 -0700*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4BACAD70.4090409@abo.fi>*References*: <4BAB71A4.1020204@uibk.ac.at> <4BAC7B81.5090401@in.tum.de> <4BACAD70.4090409@abo.fi>*Sender*: huffman.brian.c at gmail.com

On Fri, Mar 26, 2010 at 5:49 AM, Viorel Preoteasa <viorel.preoteasa at abo.fi> wrote: > Hello, > > I am trying to define a constant which depends on an extra type > variable. ... > Another approach which seem to work is by defining an uninterpreted > constant, and give its concrete definition using an axiom: > > consts > 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 variables. 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 locale. - Brian

**Follow-Ups**:**Re: [isabelle] Specification depends on extra type variables***From:*Viorel Preoteasa

**References**:**[isabelle] Antiquotation for Theorem Names***From:*Christian Sternagel

**Re: [isabelle] Antiquotation for Theorem Names***From:*Alexander Krauss

**[isabelle] Specification depends on extra type variables***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] Specification depends on extra type variables
- Next by Date: Re: [isabelle] Without using metis
- Previous by Thread: Re: [isabelle] Specification depends on extra type variables
- Next by Thread: Re: [isabelle] Specification depends on extra type variables
- Cl-isabelle-users March 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list