Julin Shaji (Feb 20 2025 at 11:18): Julin Shaji (Feb 20 2025 at 11:18):I was trying to get familiar with classes and made classes for semigroup and
monoid.
Then I wanted to show that the type of pairs of monoids is also a monoid.
How can that be shown.
This is what I had been trying:
theory Example
imports Main
begin
class semigroup =
fixes sgop :: ‹'a ⇒ 'a ⇒ 'a› (infixl ‹⊗› 70)
assumes assoc : ‹(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)›
class monoid = semigroup +
fixes unit :: ‹'a› (‹𝟭›)
assumes unitl : ‹unit ⊗ x = x›
assumes unitr : ‹x ⊗ unit = x›
instantiation prod :: (monoid, monoid) monoid
begin
instance proof
fix p :: ‹'a::monoid × 'b::monoid›
show ‹p ⊗ 𝟭 = p›
(* What can be done next? *)
(* unfolding unit-prod-def *)
end
end
you need to also define what sgop and unit are for products, then a few calls to simp can prove that products are an instance of your monoid class:
instantiation prod :: (monoid, monoid) monoid
begin
definition sgop_prod :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b" where
"sgop_prod a b = (case a of (a⇩1, a⇩2) ⇒ case b of (b⇩1, b⇩2) ⇒ (a⇩1 ⊗ b⇩1, a⇩2 ⊗ b⇩2))"
definition unit_prod where "unit_prod ≡ (unit, unit)"
instance
apply (standard)
apply (simp add: assoc case_prod_unfold sgop_prod_def)
apply (simp add: sgop_prod_def unit_prod_def unitl)
apply (simp add: sgop_prod_def unit_prod_def unitr)
done
end
(but note that you might want to move sgop_prod into an instance specific to semigroup, so it can also be used for things which aren't also monoids)
Julin Shaji (Feb 20 2025 at 14:26):For pattern matching on products, can we directly do like
definition sgop_prod :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b" where
"sgop_prod ((a1, b1), (a2, b2)) = (a1 ⊗ a2, b1 ⊗ b2)"
instead of separately doing case?
terru (Feb 20 2025 at 14:49):I'm not sure if there's a good way to do that with definition. But you can do it if you define sgop_prod using something like fun, for example.
Julin Shaji (Feb 20 2025 at 17:45):Is there any difference between doing instance and instance proof?
Julin Shaji (Feb 20 2025 at 17:45):Something about prove mode and state mode.
terru (Feb 20 2025 at 18:16):proof starts a structured isar proof (instead of the simple apply-script style proof i gave above)
Julin Shaji (Feb 21 2025 at 04:22):When should we use the isar version? Is there some convention?
Julin Shaji (Feb 21 2025 at 04:22):Also, how would the same proof with isar look like?
Julin Shaji (Feb 21 2025 at 04:25):I tried:
theory Example
imports Main
begin
class semigroup =
fixes sgop :: ‹'a ⇒ 'a ⇒ 'a› (infixl ‹⊗› 70)
assumes assoc : ‹(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)›
class monoid = semigroup +
fixes unit :: ‹'a› (‹𝟭›)
assumes unitl : ‹unit ⊗ x = x›
and unitr : ‹x ⊗ unit = x›
instantiation prod :: (semigroup, semigroup) semigroup
begin
definition sgop_prod :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b" where
"sgop_prod x y =
(case x of (a1, b1) ⇒
(case y of (a2, b2) ⇒ (a1 ⊗ a2, b1 ⊗ b2)))"
instance proof
fix p :: ‹'a::semigroup × 'b::semigroup›
show ‹p ⊗ 𝟭 = p›
(*
proof (state)
goal (1 subgoal):
1. ⋀x y z. x ⊗ y ⊗ z = x ⊗ (y ⊗ z)
Type unification failed: No type arity prod :: monoid
Type error in application: incompatible operand type
Operator: (⊗) p :: 'a × 'b ⇒ 'a × 'b
Operand: 𝟭 :: ??'a
*)
Looks like it is not realizing that I wanted to talk about semigroup instead of monoid.
Julin Shaji (Feb 21 2025 at 04:26):Oh wait.. I think I got the statement wrong.
Julin Shaji (Feb 21 2025 at 04:28):Is this right?
instance proof
fix p q r :: ‹'a::semigroup × 'b::semigroup›
show ‹(p ⊗ q) ⊗ r = p ⊗ (q ⊗ r)›
unfolding sgop_prod_def
unfolding case_prod_unfold
by simp
(I edited this comment a few times)
Julin Shaji (Feb 21 2025 at 04:30):How do we know a proof method named case_prod_unfold is available?
Is it something that isabelle automatically derives for a given class?
Julin Shaji (Feb 21 2025 at 04:31):Is there someplace where we can see the list of such autogenerated definitions?
Bob Rubbens (Feb 21 2025 at 08:07):There's the "What's in main" document that comes with isabelle. Find it in the documentation panel of jEdit, under the reference manuals section. In there is a type case_prod. (I found it by first searching for case_prod in the isar reference manual, and then in the what's in main document) In this case, case_prod_unfold is not auto generated, e.g. the type curry that is also defined there does not have curry_unfold. Also if you control-click it you go to the definition. There is, however, curry_case_prod.
For completeness: you can inspect these definitions with e.g. thm case_prod_unfold (at the global level). I found the curry_case_prod definition using find_theorems name: curry_.
I guess in your specific case, you would've needed the insight that your proof was about tuples, and hence that looking up all lemmas related to case_prod would be helpful... Maybe it's me but those kinds of insights I never have on my own :p
Last updated: Mar 09 2025 at 12:28 UTC