Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Inherit a class from a locale


view this post on Zulip 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: Mar 28 2024 at 16:17 UTC