Email Gateway (Aug 22 2022 at 18:55): Email Gateway (Aug 22 2022 at 18:55):From: Denis Nikiforov <denis.nikif@gmail.com>
Hi
It seems that I "invented" a cool technique to "inherit" a class from a
locale.
Let "loc" is a locale defining some useful functions (g' in this case):
locale loc =
fixes f :: "'a ⇒ 'b"
assumes inj_f: "inj f"
begin
abbreviation "g' ≡ map_option f"
end
Let "cls" is a class which should be inherited from loc with 'b binded to
"'a ty":
datatype 'a ty = A | B
class cls =
fixes f :: "'a ⇒ 'a ty"
assumes inj_f: "inj f"
begin
interpretation loc f
apply standard
by (simp add: local.inj_f)
definition "g ≡ g'"
end
Here is a test case:
datatype dt = C | D
instantiation dt :: cls
begin
fun f_dt :: "dt ⇒ dt ty" where
"f_dt C = A"
| "f_dt D = B"
instance
apply intro_classes
by (smt f_dt.elims injI ty.distinct(1))
end
value "f C"
value "g (Some C)"
As you can see g is implemented in the locale. But it is overloaded as a
function defined for a class. Maybe it will be useful for somebody else.
This technique allows to combine pros of both classes and locales.
Last updated: Nov 21 2024 at 12:39 UTC