theory - バブルソートが補題順であることを証明する

Question

私はすでに楽しみbubble_mainが注文されていることを証明しようとしましたが、どのアプローチも機能していないようです. ここで誰かが補題を証明するのを手伝ってくれませんかis_ordered (bubble_main L)。

イザベルが証明を見つけるのに役立つものはないように見えるので、以前の補題をすべて削除しました。ここに私のコード/理論があります:

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