How to ensure that instantiations of type variables are different

Question

In Isabelle, is there a way to ensure that instantiations for two type variables in a locale or proposition are different?

For a concrete example, I want to reason about a composite entity without committing to a specific representation. To this end I define a class of components, with some operations on them:

class Component = fixes oper :: "'a ⇒ 'a"

I also define a Composite, which has the same operations, lifted by applying them component-wise plus selectors for the components:

class Composite = Component (* + ... *)

locale ComponentAccess = 
  fixes set :: "'c :: Composite ⇒ 'a :: Component ⇒ 'c"
  and get :: "'c ⇒ 'a"
  assumes (* e.g. *) "get (set c a) = a"
  and "set c (get c) = c"
  and "oper (set c1 a1) = set (oper c1) (oper a2)"

Now I want to state some axioms for a pairwise composite, e.g.:

locale CompositeAxioms =
  a: ComponentAccess set get + b: ComponentAccess set' get'
  for set :: "'c :: Composite ⇒ 'a1 :: Component ⇒ 'c"
  and get :: "'c ⇒ 'a1"
  and set' :: "'c ⇒ 'a2 :: Component ⇒ 'c" 
  and get' :: "'c ⇒ 'a2" +
  assumes set_disj_commut: "set' (set c a1) a2 = set (set' c a2) a1"

However, the above law is only sensible if 'a1 and 'a2 are instantiated to different types. Otherwise we trivially get unwanted consequences, like reverting a component setting:

lemma 
  fixes set get
  assumes "CompositeAxioms set get set get"
  shows "set (set c a1) a2 = set (set c a2) a1"
using assms CompositeAxioms.set_disj_commut by blast

In the above locale and it's assumes, is there a way of ensuring that 'a1 and 'a2 are always instantiated to different types?

Update (clarification). Actually, the 'law' makes sense only if set and set' are different. But then I would have to compare two functions over different types which, I think, is not possible. Since I define get/set operations in type classes and use sort constraints to ensure that a composite has certain components, my gets and sets always differ in the component type. Hence the question.

Andreas Lochbihler Andreas Lochbihler · Accepted Answer · 2015-07-21T07:44:24

You can express in Isabelle/HOL that two types are different by using the reflection of types as terms. To that end, the types must be representable, i.e., instantiate the class typerep. Most types in HOL do so. Then, you can write

TYPEREP('a) ~= TYPEREP('b)

to express that 'a and 'b can only be instantiated to different types. However, TYPEREP is normally used only for internal purposes (especially in the code generator), so there is no reasoning infrastructure available and I do not know how to exploit such an assumption.

Anyway, I wonder why you want to formulate such a constraint at all. If a user instantiates your locale CompositeAxioms with both components being the same (and leave the swapping law for set and set' as is), it is the user who has to show the swapping law. If he can, then the set function is a bit strange, but soundness is not affected. Moreover, a locale assumption like TYPEREP('a) ~= TYPEREP('b) would unnecessarily restrict the generality of your development, is it might be perfectly sensible to use the same representation type with different instances for set and get.

How to ensure that instantiations of type variables are different

1 Answers