CODEWITHSUNDEEP
isabelle
contall
contall

Reputation: 51

How do I define exchange(X) to make this theorem without error?

I am learning to use Isabelle to prove certain theories, but I encountered a problem. I would like to know how can I define exchange(X) to ensure that the theorem presented in the code listing below can be stated without causing an error?

theorem exchange_wp2_1:
  "
  preOrder(T) =X @ preOrder(q) @ F(S) ∧ exchange(X) ∧ q ≠ null ⟹
    preOrder(T)=X @ (data q) @ preOrder(ltree q) @ F ([rtree q] @ S)
  "

Error:

Type unification failed:Cash of types "_list" and "_tree" Type error in application:incompatible operand type Operator: exchange::?? 'tree⇒bool Operator: X::?? 'b list

Upvotes: 0

Views: 50

Answers (1)

René Thiemann
René Thiemann

Reputation: 1271

I don't know exactly the definitions of preOrder and exchange, but it seems that preOrder returns a list, whereas exchange expects a tree as input. So, in your expression, it is unclear what type X should have: is it a tree or a list?

preOrder(T) = X        (so X is list)
exchange X             (so X is a tree)

this is what the error message tells you.

Upvotes: 0

Related Questions