CODEWITHSUNDEEP
isabelleproofjedit
Gergely
Gergely

Reputation: 7487

Proving a type classed theorem in Isabelle

I am to prove a triviality using type classes:

class 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"
begin

  theorem "(myle:: ('b::order) ⇒ 'b ⇒ bool) x x"
  proof -
    show ?thesis by (rule refl)
  qed

end

Here, Isabelle/jEdit highlights by (rule refl) in pink and says

Failed to apply initial proof method⌂:
goal (1 subgoal):
 1. myle x x

What is the problem here? Otherwise the proof seems to go through.

Upvotes: 1

Views: 86

Answers (1)

Peter Zeller
Peter Zeller

Reputation: 2276

myle and ≼ are not the same function.

The type annotation (myle:: ('b::order) ⇒ 'b ⇒ bool) just states that myle is a function that takes two elements of type 'b and returns a boolean and that 'b is a type belonging to the order typeclass.

If you want to prove something about ≼ just use the same symbol or the name lesseq.

Upvotes: 3

Related Questions