Isabelle Failed to refine any pending goal during instantiation

Question

datatype 'a list = Cons 'a  "'a list"  | Nil

instantiation list :: (order) order
begin

fun less_eq_list :: "'a list ⇒ 'a list ⇒ bool" where
"less_eq_list Nil Nil = True" |
"less_eq_list (Cons _ _) Nil = True" |
"less_eq_list Nil (Cons _ _) = False" |
"less_eq_list (Cons _ a) (Cons _ b) = less_eq_list a b"

instance 
proof
  fix x y:: "'a list"
  show "x ≤ x"
    apply(induct_tac x)
    apply(auto)
    done
(* at this point the state is

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

goal (3 subgoals):
 1. ⋀x y. (x < y) = (x ≤ y ∧ ¬ y ≤ x)
 2. ⋀x y z. x ≤ y ⟹ y ≤ z ⟹ x ≤ z
 3. ⋀x y. x ≤ y ⟹ y ≤ x ⟹ x = y

*)
  show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
(* I get an error here

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (?x2 < ?y2) = (?x2 ≤ ?y2 ∧ ¬ ?y2 ≤ ?x2)
*)
qed
end

What is wrong with this? The proof of "x ≤ x" worked like a charm. Somehow "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" doesn't match any subgoal.

Answer 1

Class order is a subclass of preorder, which in turn is a subclass of ord. Class ord requires you to define both less_eq (≤) and less (<). In your code, you have correctly defined less_eq_list but forgot to define less_list, and that's why you got an error when trying to prove (x < y) = (x ≤ y ∧ ¬ y ≤ x).