CODEWITHSUNDEEP
isabellehol
kjam
kjam

Reputation: 839

Isabelle/HOL: How to handle `let` and `if`?

I'm completely new to Isabelle/HOL and trying to read the Concrete Semantics book.

I'm stuck with one of the very first exercises:

Exercise 2.3. 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.

This is what I've got so far:

fun count :: "'a ⇒ 'a list ⇒ nat" where
  "count x [] = 0" |
  "count x (y # ys) = (let n = count x ys in (if x = y then Suc n else n))"

lemma count_bound [simp]: "count x y ≤ length y"
  apply(induction y)
  apply(auto)

Auto solves the goal for the empty list, but does not handle the second one. I'm left with the following:

⋀a y. count x y ≤ length y ⟹
           (let n = count x y in if x = a then Suc n else n)
           ≤ Suc (length y)

Intuitively I understand that I need to substitute value of the let-binding and split if into two cases. But so far the book gave me zero information on how to do this.

Upvotes: 0

Views: 108

Answers (0)

Related Questions