證明氣泡排序是由詞條排序

Question

我已經試過證明樂趣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 

Answer 1

首先，我會修復您的定義。例如，使用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 

我希望，這有助於看到所需的方向。