Re: [isabelle] Specification depends on extra type variables



Hello Brian,

Thank you for your answer. Almost for sure I would have an inconsistency similar to what you showed if I would use the axiomatic approach. I have used the locale to introduce the extra types. Moreover, my definition depends also on a constant
(pair) and I fixed that in the locale too.

This solution is satisfactory, but reading your example, I realized that what I would
need is an existential quantification on the extra type:

axioms f_def2: "f (a::'a) = (EX 'b::type . (EX (g::'b => 'a). inj g))"

Like this there is no danger of inconsistencies. Is there something in Isabelle which
would allow something similar to this?

Viorel


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







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