Stream: Beginner Questions

Topic: Referring to a type class

Gergely Buday (Aug 04 2020 at 10:52):

Here I got the answer that I did not specify correctly that my function myle belongs to the type class at the beginning:

https://stackoverflow.com/questions/62891358/proving-a-type-classed-theorem-in-isabelle

How can I specify that a function of type `'a => 'a => bool" conforms the type class specification, other than referring to the function name in the type class definition?

Lukas Stevens (Aug 04 2020 at 11:30):

As Peter wrote in the SO Post, the function mle as you wrote it down refers to any function that takes two 'b of class order and returns a bool. What you want is to prove the theorem "x ≼ x". Note that the operator ≼ is locally fixed so outside of the context you can instantiate it with any other concrete operator (e.g. myle) that fulfils the axioms of the order typeclass.

Lukas Stevens (Aug 04 2020 at 11:32):

This can be done with the command interpretation.

Lukas Stevens (Aug 04 2020 at 11:41):

Or instantiation if you want to instantiate the class for a whole type.

Gergely Buday (Aug 04 2020 at 11:43):

I want to prove this theorem: for any myle function that conforms my type class, and for any x, x <= x. Can I state this in Isabelle?

Lukas Stevens (Aug 04 2020 at 11:45):

That is exactly "x ≼ x". When you leave the context after end the theorem is automatically generalised.

Lukas Stevens (Aug 04 2020 at 11:46):

You can see this if you type thm order.refl after end.

Lukas Stevens (Aug 04 2020 at 11:49):

For a detailed introduction to type classes and locales read the documentation: https://isabelle.in.tum.de/documentation.html

Lukas Stevens (Aug 04 2020 at 11:51):

What you also can do is write "(x::'a::order) ≼ x" after end.

Gergely Buday (Aug 04 2020 at 11:55):

I'm getting to it.

Now,

lemma (in order) "lesseq x x"
proof -
show ?thesis by (rule local.refl)
qed

works smoothly, while

theorem "order myle ⟹ myle x x"
proof -
show ?thesis by (rule order.refl)
qed

says

show myle x x
Successful attempt to solve goal by exported rule:
myle x x
proof (state)
this:
myle x x

goal:
No subgoals!
Failed to finish proof⌂:
goal (1 subgoal):

1. ProofsAndFormalizations.class.order (λa b. b)

Again something similar as at my first attempt.

What is wrong here?

Lukas Stevens (Aug 04 2020 at 11:59):

The second one works if you use locale instead of class.

Lukas Stevens (Aug 04 2020 at 11:59):

But the first one is the canonical way to do it.

Lukas Stevens (Aug 04 2020 at 12:00):

And works in both cases.

Gergely Buday (Aug 04 2020 at 12:20):

I'm afraid it does not work for me, not even with locale:

theory Locale

imports Main

begin

locale order =
fixes lesseq :: " 'a ⇒ 'a ⇒ bool" (infix "≼" 50)
assumes refl: "x ≼ x"
and trans: "x ≼ y ⟹ y ≼ z ⟹ x ≼ z"
and antisym: "x ≼ y ⟹ y ≼ x ⟹ x = y"

theorem ‹order (myle :: 'a ⇒ 'a ⇒ bool) ⟹ myle x x›
proof -
show ?thesis by (rule order.refl)
qed

end

Failed to finish proof⌂:
goal (1 subgoal):

1. order (λa b. b)

How does the K* combinator pop up here?

Gergely Buday (Aug 04 2020 at 12:28):

theorem assumes "order myle"
shows "myle x x"
proof -
from assms show ?thesis by (rule order.refl)
qed

did the trick.

Last updated: Dec 21 2024 at 16:20 UTC