3

我在 Isabelle/HOL 中实现了一些插入排序算法，用于生成代码（ML、Python 等）。我确信相应的函数可以正常工作，但我需要创建一些定理来证明它并确保它可以正常工作。我的功能是：

(* The following functions are used to prove the algorithm works fine *)
fun menor_igual :: "nat ⇒ nat list ⇒ bool" where
"menor_igual n [] = True" |
"menor_igual n (x # xs) = (n ≤ x ∧ menor_igual n xs)"

fun ordenado :: "nat list ⇒ bool" where
"ordenado [] = True" |
"ordenado (x # xs) = (menor_igual x xs ∧ ordenado xs)"

fun cuantos :: "nat list ⇒ nat ⇒ nat" where
"cuantos [] num = 0" |
"cuantos (x # xs) num = (if x = num then Suc (cuantos xs num) else cuantos xs num)"


(* These functions make the algorithm itself *)
fun insertar:: "nat ⇒ nat list ⇒ nat list" where
"insertar num [] = [num]" |
"insertar num (x # xs) = (if (num ≤ x) then (num # x # xs) else x # insertar num xs)"

fun asc :: "nat list ⇒ nat list" where
"asc [] = []" |
"asc (x # xs) = insertar x (asc xs)"

问题是我不知道如何正确创建定理。我需要证明有序列表与原始列表具有相同的长度，并且两个列表具有相同的元素名称。我的第一个定理是：

theorem "ordenado (asc xs)"
apply (induction xs rule: asc.induct)
apply auto

theorem "cuantos (asc xs) x = cuantos xs x"
apply (induction xs rule: asc.induct)
apply auto

第一个定理试图证明列表是正确排序的，第二个定理试图证明两个列表具有相同的长度。

当我应用归纳和自动时，我希望得到 0 个子目标，这说明定理是正确的并且算法工作正常，但是在那之后我不知道如何删除子目标，我的意思是我不知道该怎么做简化规则（lemma [simp]: ""）来做，我会感谢你的帮助。

4

1 回答 1

2

后

theorem "ordenado (asc xs)"
apply (induction xs rule: asc.induct)
apply auto

您仍然需要证明以下子目标：

1. ⋀x xs.
      ordenado (asc xs) ⟹
      ordenado (insertar x (asc xs))

也就是说，假设它asc xs是排序的，你必须证明它insertar x (asc xs)是排序的。insertar这建议首先证明一个关于和之间相互作用的辅助引理ordenado

lemma ordenado_insertar [simp]:
  "ordenado (insertar x xs) = ordenado xs"
 ...

这表明insertar x xs当且仅当xs已经排序时才排序。为了证明这个引理，您将再次需要辅助引理。这一次关于和 之间的menor_igual交互。menor_igualinsertar

lemma le_menor_igual [simp]:
  "y ≤ x ⟹ menor_igual x xs ⟹ menor_igual y xs"
  ...

lemma menor_igual_insertar [simp]:
  "menor_igual y (insertar x xs) ⟷ y ≤ x ∧ menor_igual y xs"
  ...

第一个声明，如果y较小等于x并且x较小等于 的所有元素xs，则y较小等于 的所有元素xs，依此类推...

我把证明留作练习；）。

对于您的第二个定理，我建议遵循相同的配方。首先尝试induct然后auto（就像您已经做过的那样），然后找出仍然缺少哪些属性，将它们证明为辅助引理并完成您的证明。

于 2014-11-24T16:12:37.447 回答