如何在归纳中引用变量

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

Hence how do I fix xs to be v#vs, or to otherwise refer to the case analysed xs for this specific case?

这个在Isabelle2020(Isar-ref)的参考手册第6.5节有解释：

... By using the explicit form case (c y1 ... ym) ... the proof author is able to chose local names that fit nicely into the current context ...

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

的东西

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

伊莎贝尔版本：伊莎贝尔2020

如何在归纳中引用变量

How to refer to variables in induction

isabelle