Gergely Buday (Jul 31 2023 at 14:24): Gergely Buday (Jul 31 2023 at 14:24):I defined the equality type class and am trying to prove that usual natural number equality fits this type class:
theory EqualityClass
imports Main
begin
class eq =
fixes eq :: "'a ⇒ 'a ⇒ bool" (infixl "=eq=" 60)
assumes refl: "x =eq= x"
and symm: "x =eq= y ⟹ y =eq= x"
and trans: "x =eq= y ⟹ y =eq= z ⟹ x =eq= z"
instantiation nat :: eq
begin
fun nat_eq :: "nat ⇒ nat ⇒ bool"
where
"nat_eq 0 0 = True"
| "nat_eq 0 _ = False"
| "nat_eq _ 0 = False"
| "nat_eq (Suc n) (Suc m) = nat_eq n m"
instance
proof
fix n :: nat
have "nat_eq n n"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case by simp
qed
show "⋀x. x =eq= x"
It is not clear how could I feed that the reflexivity of nat_eq foots the bill for the equality class reflexivity prescription. How can I have a proper show statement there? For the type class tutorial example, this was
class semigroup =
fixes mult :: "'a ⇒ 'a ⇒ 'a" (infixl "⊗" 70)
assumes assoc: "(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)"
instantiation int :: semigroup
begin
definition mult_int_def: "i ⊗ j = i + (j::int)"
instance
proof
fix i j k :: int
have "(i+j) + k = i + (j+k)" by simp
then show "(i ⊗ j) ⊗ k = i ⊗ (j ⊗ k)" unfolding mult_int_def .
qed
nat_eq vs mult_int in the example
Mathias Fleury (Jul 31 2023 at 14:32):you swapped the names
Mathias Fleury (Jul 31 2023 at 14:32):it should be eq_nat
Gergely Buday (Jul 31 2023 at 14:46):I see, so it is a fixed syntax. I corrected it but now the induction proof fails. I wonder how a name change can affect that.
Mathias Fleury (Jul 31 2023 at 15:19):class eq =
fixes eq :: "'a ⇒ 'a ⇒ bool" (infixl "=eq=" 60)
assumes refl: "x =eq= x"
and symm: "x =eq= y ⟹ y =eq= x"
and trans: "x =eq= y ⟹ y =eq= z ⟹ x =eq= z"
instantiation nat :: eq
begin
fun nat_eq :: "nat ⇒ nat ⇒ bool"
where
"nat_eq 0 0 = True"
| "nat_eq 0 _ = False"
| "nat_eq _ 0 = False"
| "nat_eq (Suc n) (Suc m) = nat_eq n m"
definition eq_nat where
‹eq_nat = nat_eq›
instance
proof
have "nat_eq n n" for n
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case by simp
qed
then show "x =eq= x" for x :: nat
unfolding eq_nat_def by blast
Or
instantiation nat :: eq
begin
fun eq_nat :: "nat ⇒ nat ⇒ bool"
where
"eq_nat 0 0 = True"
| "eq_nat 0 _ = False"
| "eq_nat _ 0 = False"
| "eq_nat (Suc n) (Suc m) = eq_nat n m"
instance
proof
have "n =eq= n" for n :: nat
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case by simp
qed
then show "x =eq= x" for x :: nat
by blast
no clue what error you are talking about…
Last updated: Apr 28 2024 at 16:17 UTC