How to use "using" in "apply" with Isabelle

user_1704411 0
Viewed 129

I have the following proof in Isar style:

fun intersperse :: "'a ⇒ 'a list ⇒ 'a list" where
  "intersperse _ [] = []" |
  "intersperse _ [x] = [x]" |
  "intersperse a (x#xs) = x#a#(intersperse a xs)"

lemma "map f (intersperse a xs) = intersperse (f a) (map f xs)"
proof (induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons x xs)
  thus ?case
  proof (cases xs)
    case Nil
    then show ?thesis by simp
  next
    case (Cons y ys)
    then show ?thesis using Cons.IH by auto
  qed
qed

I have attempted to convert this to apply style by first showing the second half in the induction. Here is one of my tries:

lemma "map f (intersperse a (x # xs)) = intersperse (f a) (map f (x # xs))"
  apply(cases xs)
   apply(simp)
  apply(auto) using Cons.IH

However the last line here doesn't appear to be valid syntax. I also tried

lemma "map f (intersperse a (x # xs)) = intersperse (f a) (map f (x # xs))"
  apply(cases xs)
   apply(simp)
  apply(auto simp add: Cons.IH)

However then I get the error Undefined fact: "Cons.IH".

What is the correct syntax for converting a "using" statement to an apply style proof?

isabelle
1 Answers

The name "Cons.IH" is created by the "case Suc". However, the corresponding theorem is part of the assumptions, so you do need to do that.

So what is the proper way here?

The first (bad idea) is to port the proof idea to apply, by calling case_tac to mimic the proof (cases does not work, because you are working on a locally bound variable):

lemma "map f (intersperse a xs) = intersperse (f a) (map f xs)"
  apply (induction xs)
   apply simp
  apply (rename_tac aa xs)
  apply (case_tac xs)
   apply auto
  done

But the better way is to use the correct induction theorem, namely the one adapted to your function:

lemma "map f (intersperse a xs) = intersperse (f a) (map f xs)"
  apply (induction xs rule: intersperse.induct)
   apply auto
  done
user_128242070
Related