如何在 Isabelle 的“应用”中使用“使用”

Question

我有以下 Isar 风格的证明：

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

我试图通过首先在归纳中显示下半部分来将其转换为apply 样式。这是我的尝试之一：

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

但是这里的最后一行似乎不是有效的语法。我也试过了

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)

然后我收到错误Undefined fact: "Cons.IH"。

将“使用”语句转换为应用样式证明的正确语法是什么？

Answer 1

名称“Cons.IH”是由“case Suc”创建的。但是，相应的定理是假设的一部分，因此您确实需要这样做。

那么这里的正确方法是什么？

第一个（坏主意）是通过调用case_tac 来模拟证明（案例不起作用，因为您正在处理本地绑定的变量）来移植要应用的证明想法：

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

但更好的方法是使用正确的归纳定理，即适用于您的函数的那个​​：

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