如何在归纳中引用变量

Question

我有一个在列表上匹配的函数：

fun merge where
  ‹merge [] [] = []› |
  ‹merge (v#vs) [] = (v#vs)› |
  ‹merge [] (v#vs) = (v#vs)› |
  ‹merge (x#xs) (y#ys) =
    (if x < y then x # merge xs (y#ys) else y # merge (x#xs) ys)›

当我试图证明这一点的正确性时，我很难从以下几个方面进行归纳：

...
lemma sorted_merge: 
  assumes s_xs: "sorted(xs)"
    and   s_ys: "sorted(ys)"
  shows ‹sorted(merge xs ys)›  
proof (induction xs ys rule: merge.induct [case_names base xs ys both])
  case base then show "?case" by auto
next
  case xs
  show "?case" 
  proof -

问题是，我可以证明sorted(merge xs [])的这种情况，但这并不能满足sorted(merge (v#vs) [])这一证明目标。

因此，我如何将xs修正为v#vs，或者以其他方式引用针对这一特定情况的被分析的xs案例？

Answer 1

因此，如何将

修正为v#vs，或者以其他方式引用分析过的针对这个特定情况的xs案例？

这一点在Isabelle2020参考手册(Isar)第6.5节中作了解释：

...通过使用显式形式case (c y1 ... ym) ..。证明作者能够选择适合当前上下文的本地名称.

因此，在您的情况下，您可以使用类似于

fun merge where
  ‹merge [] [] = []› 
| ‹merge (v#vs) [] = (v#vs)› 
| ‹merge [] (v#vs) = (v#vs)› 
| ‹merge (x#xs) (y#ys) = 
    (if x < y then x # merge xs (y#ys) else y # merge (x#xs) ys)›

lemma sorted_merge:
  assumes s_xs: "sorted(xs)" and s_ys: "sorted(ys)"
  shows ‹sorted(merge xs ys)›  
  using assms
proof(induction xs ys rule: merge.induct[case_names base xs ys both])
  case base then show ?case by auto
next
  case (xs v vs) then show ?case by auto
next
  case (ys v vs) then show ?case by auto
next
  case (both x xs y ys)
  show ?case 
  proof(cases ‹x < y›)
    case True with both(1,3,4) show ?thesis by (induction xs) force+
  next
    case False with both(2,3,4) show ?thesis by (induction ys) force+
  qed      
qed

伊莎贝尔版本Isabelle2020