Email Gateway (Aug 22 2022 at 19:24): Email Gateway (Aug 22 2022 at 19:24):From: Martin Desharnais <martin.desharnais@gmail.com>
Dear Isabelle users
I am trying to get to get to know locales and get a strange error
message when using the type abstracted over in a datatype definition.
Consider the following example.
locale semantics =
fixes
step :: "'state ⇒ 'state ⇒ bool" and
inital_state :: "'state ⇒ bool" and
final_state :: "'state ⇒ bool"
begin
definition stuck :: "'state ⇒ bool" where
"stuck s1 ≡ (∄s2. step s1 s2)"
inductive star :: "'state ⇒ 'state ⇒ bool" where
star_refl: "star s s" |
star_step: "step s1 s2 ⟹ star s2 s3 ⟹ star s1 s3"
datatype behaviour =
Terminates 'state | Goes_wrong
inductive has_behaviour :: "'state ⇒ behaviour ⇒ bool" where
state_terminates:
"star s1 s2 ⟹ final_state s2 ⟹
has_behaviour s1 (Terminates s2)" |
state_goes_wrong:
"star s1 s2 ⟹ stuck s2 ⟹ ¬final_state s2 ⟹
has_behaviour s1 Goes_wrong"
end
The constructor "Terminates" of the datatype "behaviour" is intended to
contain a value of the state type abstracted over by the locale. The
definition fails with the following error message.
Extra type variables on right-hand side: "'state"
If I change the definition to add the type variable on the right-hand
side, the definition still fails with the following error message.
Locally fixed type argument "'state" in datatype specification
I can solve the problem by using a fresh type variable and instantiate
the "behaviour" datatype with the "'state" type in every usage (e.g. in
the inductive definition "has_behaviour"), but this is a unnecessary
overhead that would not scale well when the number of abstracted types
involved increases.
Why is the definition using the abstracted type "'state" directly failing?
Is there a workaround that does not involve type parametrization of the
"behaviour" datatype?
Regards,
Martin Desharnais
Email Gateway (Aug 22 2022 at 19:25):From: Traytel Dmitriy <traytel@inf.ethz.ch>
Hi Martin,
this is fundamental: typedefs in locales may not depend on locally fixed type parameters (or term parameters). See the error messages in the example below.
Since datatypes ultimately reduce to typedefs, they inherit this limitation.
The only workarounds I know is to either parametrize the datatype (outside of the locale) or to monomorphize the state.
Cheers,
Dmitriy
locale A =
fixes a :: 'a
fixes A :: "nat set"
begin
typedef foo = "UNIV :: 'a set"
typedef 'a foo = "UNIV :: 'a set"
typedef foo = "A"
end
Last updated: Apr 25 2024 at 08:20 UTC