我已经尝试证明 fun 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
最佳答案
首先,我会修复你的定义。例如,使用您的版本
的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
中看到。的。
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
我希望这有助于了解所需的方向。
关于theory - 证明冒泡排序是按引理排序的,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/20147547/