`Define a function count :: 'a ⇒ 'a list ⇒ nat that counts the number of occurrences of an element in a list. Prove count x xs ≤ length xs.`

```
"count x [] = 0"
| "count x (y#xs) = (if (x=y) then (1 + count x xs) else (count x xs))"
lemma count_cons: "count x (y#xs) ≤ 1 + count x xs"
proof (induction xs)
case Nil
then show ?case by simp
next
case (Cons a xs)
then show ?case by simp
qed
lemma count_less: "count x xs ≤ length xs"
proof (induction xs)
case Nil
then show ?case by simp
next
case (Cons a xs)
then show ?case by (simp add:count_cons)
qed
```

This does not work on the Cons case. by auto works but that is not very readable or elegant.

Can you give me a hint what is missing? Not a solution.

What is unreadable about `by auto`

?

update: ```Failed to finish proof⌂:

goal (1 subgoal):

- count x xs ≤ length xs ⟹ x = a ⟶ count a xs ≤ length xs```

@Mathias Fleury I would like to show the used lemmas other than trivial arithmetic equalities.

Also, one of the goals of theorem proving is to understand what's going on and that is not possible with auto.

```
lemma count_less: "count x xs ≤ length xs"
by (induction xs) auto
```

works on Isabelle2020 and RC2.

Gergely Buday said:

Also, one of the goals of theorem proving is to understand what's going on and that is not possible with auto.

So you prefer

```
lemma count_less: "count x xs ≤ length xs"
by (induction xs) (simp, smt?)+
```

because you can understand what is going on?

Oh well.

Last updated: Sep 25 2021 at 09:17 UTC