The following code doesn't typecheck:
type_synonym env = "char list ⇀ val"
interpretation map: order "op ⊆⇩m :: (env ⇒ env ⇒ bool)" "(λa b. a ≠ b ∧ a ⊆⇩m b)"
by unfold_locales (auto intro: map_le_trans simp: map_le_antisym)
lemma
assumes "mono (f :: env ⇒ env)"
shows "True"
by simp
Isabelle complains with the following error at the lemma:
Type unification failed: No type arity option :: order
Type error in application: incompatible operand type
Operator: mono :: (??'a ⇒ ??'b) ⇒ bool
Operand: f :: (char list ⇒ val option) ⇒ char list ⇒ val option
Why so? Did I miss something to use the interpretation? I suspect I need something like a newtype wrapper here...
When you interpret a locale like order which corresponds to a type class, you only get the theorems proved inside the context of the locale. However, the constant mono is only defined on the type class. The reason is that mono's type contains two type variables, whereas only one is available inside locales from type classes. You can notice this because there is no map.mono stemming from your interpretation.
If you instantiate the type class order for the option type with None being less than Some x, then you can use mono for maps, because the function space instantiates order with the pointwise order. However, the ordering <= on maps will only be semantically equivalent to ⊆⇩m, not syntactically, so none of the existing theorems about ⊆⇩m will work for <= and vice versa. Moreover, your theories will be incompatible with other people's that instantiate order for option differently.
Therefore, I recommend to go without type classes. The predicate monotone explicitly takes the order to be used. This is a bit more writing, but in the end, you are more flexible than with type classes. For example, you can write monotone (op ⊆⇩m) (op ⊆⇩m) f to express that f is a monotone transformation of environments.