Stream: Beginner Questions

Topic: Referring to a type class


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Aug 04 2020 at 11:32):

This can be done with the command interpretation.

view this post on Zulip Lukas Stevens (Aug 04 2020 at 11:41):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Aug 04 2020 at 11:46):

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

view this post on Zulip 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

view this post on Zulip Lukas Stevens (Aug 04 2020 at 11:51):

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

view this post on Zulip 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?

view this post on Zulip Lukas Stevens (Aug 04 2020 at 11:59):

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

view this post on Zulip Lukas Stevens (Aug 04 2020 at 11:59):

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

view this post on Zulip Lukas Stevens (Aug 04 2020 at 12:00):

And works in both cases.

view this post on Zulip 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?

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC