prove bubble sort is ordered by lemma

Question

I already tried to prove that fun bubble_main is ordered but no approach seems to work. Could someone here help me to prove the lemma is_ordered (bubble_main L) please.

I just delete all my previous lemmas because none seems to help Isabelle find a proof. Here is my code/theory:

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

First of all, I would repair your definitions. E.g., using your version of is_sorted is too strict in the sense, that [0,0] is not sorted. This is also detected by quick check.

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

bubble_all has to call itself recursively.

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

and bubble_main has to invoke bubble_all.

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

Then there are several auxiliary lemmas required to prove the result. Some I listed here, others are visible in the 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

And of course, the main algorithm is bubble_all, so you should prove the property for bubble_all, not for bubble_main inductively. Moreover, an induction over the length of the list (or the number of iterations) is advantageous here, since the list is changed by bubble_all in the recursive call.

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

The final theorem is then easily achieved.

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

I hope, this helps a bit to see the direction what is required.