在 Isabelle 中证明递归函数

Question

我定义了以下递归函数：

primrec span :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list * 'a list" where
"span P [] = ([], [])"
| "span P (x#xs) = 
  (let (ys, zs) = span P xs in 
   if P x then (x#ys, zs) else (ys, x#zs))"

通过过滤器p将一个列表拆分为两个子列表，并在中间插入x。
现在我想证明以下引理：

lemma invariant_length:
shows "length (fst (span P l)) + length (snd (span P l)) = length l"

我用归纳法证明了

lemma invariant_length:
shows "length (fst (span P l)) + length (snd (span P l)) = length l"
proof (induction l)
case Nil
  then show ?case by auto
next
  case (Cons a l)
  show ?case
  proof(cases "P a")
    case True
    then have "span P (a # l) = (a # fst (span P l), snd (span P l))"
      by [where I stuck]
    then have "length (fst (span P (a # l))) + length (snd (span P (a # l))) 
               = length (a # fst (span P l)) + length(snd (span P l)) " 
      by simp
    then have "length (fst (span P (a # l))) + length (snd (span P (a # l))) 
               = Suc(length (fst (span P l))) + length(snd (span P l)) " 
      by simp
    with Cons have "length (fst (span P (a # l))) + length (snd (span P (a # l))) = Suc (length l)" 
      by simp
    then show ?thesis by simp
  next
    case False
        then have "span P (a # l) = (fst (span P l), a # snd (span P l))"
      by [where I stuck]
    then have "length (fst (span P (a # l))) + length (snd (span P (a # l))) 
               = length (fst (span P l)) + length(a # snd (span P l)) " 
      by simp
    then have "length (fst (span P (a # l))) + length (snd (span P (a # l))) 
               = length (fst (span P l)) + Suc(length(snd (span P l)))" 
      by simp
    with Cons have "length (fst (span P (a # l))) + length (snd (span P (a # l))) = Suc (length l)" 
      by simp
    then show ?thesis by simp
  qed
qed

我在归纳步骤中卡在了两种情况的第一步，这里我标记为[where I stuck]。我在这里尝试使用 auto 或 simp 但伊莎贝尔说

Failed to finish proof⌂:
goal (1 subgoal):
 1. P a ⟹ (case span P l of (ys, x) ⇒ (a # ys, x)) = (a # fst (span P l), snd (span P l))

我该如何继续？

Answer 1

lemma invariant_length:
  "length (fst (span P l)) + length (snd (span P l)) = length l"
  by (induction l; simp add: prod.case_eq_if)

在 Isabelle 中证明递归函数

Prove a recursive function in Isabelle

isabelle

theorem-proving