如何在 "apply" 中与伊莎贝尔一起使用 "using"

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"。

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

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

如何在 "apply" 中与伊莎贝尔一起使用 "using"

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

isabelle