2

我已经尝试证明乐趣bubble_main是有序的，但似乎没有任何方法有效。有人可以帮我证明引理吗is_ordered (bubble_main L)？

我只是删除了我以前所有的引理，因为似乎没有一个可以帮助Isabelle找到证据。这是我的代码/理论：

text{*check if the list is ordered ascendant*}
fun is_sorted :: "nat list ⇒ bool" where
"is_sorted (x1 # x2 # xs) = (x1 < x2 ∧ is_sorted (x2 # xs))" |
"is_sorted x = True"


fun bubble_once :: "nat list ⇒ nat list" where
"bubble_once (x1 # x2 # xs) = (if x1 < x2 
                     then x1 # bubble_once (x2 # xs) 
                     else x2 # bubble_once (x1 # xs))" |
"bubble_once xs = xs"

text{*calls fun bubble_once  *}
fun bubble_all where
"bubble_all 0 L = L"|
"bubble_all (Suc n) L = burbuja_all n (bubble_once L)"


text{*main function *}
fun bubble_main where
"bubble_main L = bubble_main (length L) L"

text{*-----prove by induction-----*}

lemma "is_sorted (bubble_main L)"
apply (induction L)
apply auto
quickcheck  
oops
4

1 回答 1

3

首先，我会修复你的定义。例如，使用你的版本is_sorted在某种意义上太严格了，[0,0] 没有排序。这也可以通过快速检查来检测。

fun is_sorted :: "nat list ⇒ bool" where
  "is_sorted (x1 # x2 # xs) = (x1 <= x2 ∧ is_sorted (x2 # xs))" |
  "is_sorted x = True"

bubble_all必须递归调用自己。 

fun bubble_all where
  "bubble_all 0 L = L"|
  "bubble_all (Suc n) L = bubble_all n (bubble_once L)"

并且bubble_main必须调用bubble_all.

fun bubble_main where
  "bubble_main L = bubble_all (length L) L"

然后需要几个辅助引理来证明结果。我在这里列出了一些，其他在sorry's 中可见。

lemma length_bubble_once[simp]: "length (bubble_once L) = length L"
  by (induct rule: bubble_once.induct, auto)

lemma is_sorted_last: assumes "⋀ x. x ∈ set xs ⟹ x ≤ y"
  and "is_sorted xs"
  shows "is_sorted (xs @ [y])" sorry

当然，主要算法是bubble_all，所以你应该证明 的属性bubble_all，而不是bubble_main归纳的。此外，对列表长度（或迭代次数）的归纳在这里是有利的，因为列表bubble_all在递归调用中被更改。

lemma bubble_all_sorted: "n ≥ length L ⟹ is_sorted (bubble_all n L)"
proof (induct n arbitrary: L)
  case (0 L) thus ?case by auto
next
  case (Suc n L)
  show ?case
  proof (cases "L = []")
    case True
    from Suc(1)[of L] True
    show ?thesis by auto
  next
    case False
    let ?BL = "bubble_once L"
    from False have "length ?BL ≠ 0" by auto
    hence "?BL ≠ []" by (cases "?BL", auto)
    hence "?BL = butlast ?BL @ [last ?BL]" by auto
    then obtain xs x where BL: "?BL = xs @ [x]" ..
    from BL have x_large: "⋀ y. y ∈ set xs ⟹ y ≤ x" sorry 
    from Suc(2) have "length ?BL ≤ Suc n" by auto    
    with BL have "length xs ≤ n" by auto
    from Suc(1)[OF this] have sorted: "is_sorted (bubble_all n xs)" .
    from x_large have id: "bubble_all n (xs @ [x]) = bubble_all n xs @ [x]" sorry
    show ?thesis unfolding bubble_all.simps BL id
    proof (rule is_sorted_last[OF x_large sorted])
      fix x
      assume "x ∈ set (bubble_all n xs)"
      thus "x ∈ set xs" sorry
    qed
  qed
qed

然后很容易实现最终定理。

lemma "is_sorted (bubble_main L)"
  using bubble_all_sorted by simp

我希望，这有助于了解所需的方向。

于 2013-11-22T16:23:47.160 回答