Re: [isabelle] "Coercion inference failed"



On Wed, 30 Mar 2011, egglue at gmail.com wrote:

axiomatization
f :: "'a => 'b" and
g :: "nat => nat" where
ax : "f = g"

Why are 'a and 'b fixed under "axiomatization"?

The specification is considered as one logical unit, where f and g are always the same local entity, with fixed types. The context is essentially this:

  fix_type 'a and 'b  -- "implicit"
  fix g :: "'a => 'b" and g :: "nat => nat"
  assume ax : "f = g"

Later the types become arbitrary in the result, so the consts f and g in the target context can be used at different type.

It is always the same game. This is how naive polymorphism works. There is no type quantification. (It would make the logic very complicated, or break down).


It seems that I can produce very much the same declaration with:

axiomatization
f:: "'a => 'b" and
g :: "nat => nat"

axioms
ax : "f = g"

Why is f polymorphic in "axioms" but not in "axiomatization"?

'axioms' is an obsolete form, better do it like this:

axiomatization
  f :: "'a => 'b" and
  g :: "nat => nat"

axiomatization where
  ax : "f = g"

Separate specifications have separate scopes wrt. polymorphism. The consts axiomatized in the first one can be used at different types at the second one.


	Makarius





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