Gergely Buday (May 28 2025 at 15:45): Gergely Buday (May 28 2025 at 15:45):I have
locale monoid_op =
base: monoid m e for m::"'a ⇒ 'a ⇒ 'a" and e::"'a" +
fixes mult :: "'a ⇒ 'a ⇒ 'a" defines "mult a b ≡ m b a"
fixes unit :: "'a" defines "unit ≡ e"
I can do
interpretation list_monoid: monoid List.append "[]"
proof unfold_locales
show "⋀a. [] @ a = a" unfolding append_Nil ..
next
show "⋀a. a @ [] = a" unfolding append.right_neutral ..
qed
but when I am trying to do
interpretation list_monoid_op: monoid_op List.append "[]"
proof unfold_locales
I get
proof (state)
goal (2 subgoals):
1. ⋀a b. mult a b ≡ b @ a
2. unit ≡ []
where mult is a free variable, I cannot unfold its definitions from the monoid_op definition.
How should I do this?
Mathias Fleury (May 28 2025 at 17:10):Why you should do this is the real question here. This seems extremely silly to me…
Mathias Fleury (May 28 2025 at 17:11):locale monoid_op =
base: monoid m e for m::"'a ⇒ 'a ⇒ 'a" and e::"'a"
begin
definition mult where ‹mult = m›
end
does the same job and is much easier
Gergely Buday (May 28 2025 at 17:11):Farmer in his Little Theories paper gives this example
Jan van Brügge (May 29 2025 at 10:10):In the locale documentation it says that defines is only for backwards compatibility, ie you should not use it for new developments
Last updated: Jun 08 2025 at 08:25 UTC