Proving insertion sort algorithm using Isabelle

Question

I did some implementation of the insert sort algorithm in Isabelle/HOL for the generation of code (ML, Python, among others). I'm sure the corresponding functions work fine, but I need to create some theorems to prove it and be super sure it works. My functions are these:

(* The following functions are used to prove the algorithm works fine *)
fun menor_igual :: "nat ⇒ nat list ⇒ bool" where
"menor_igual n [] = True" |
"menor_igual n (x # xs) = (n ≤ x ∧ menor_igual n xs)"

fun ordenado :: "nat list ⇒ bool" where
"ordenado [] = True" |
"ordenado (x # xs) = (menor_igual x xs ∧ ordenado xs)"

fun cuantos :: "nat list ⇒ nat ⇒ nat" where
"cuantos [] num = 0" |
"cuantos (x # xs) num = (if x = num then Suc (cuantos xs num) else cuantos xs num)"


(* These functions make the algorithm itself *)
fun insertar:: "nat ⇒ nat list ⇒ nat list" where
"insertar num [] = [num]" |
"insertar num (x # xs) = (if (num ≤ x) then (num # x # xs) else x # insertar num xs)"

fun asc :: "nat list ⇒ nat list" where
"asc [] = []" |
"asc (x # xs) = insertar x (asc xs)"

The issues is I don't know how to create the theorems correctly. I need to prove that the ordered list has the same length as the original list, and that both lists have the same name of elements. My first theorems are these:

theorem "ordenado (asc xs)"
apply (induction xs rule: asc.induct)
apply auto

theorem "cuantos (asc xs) x = cuantos xs x"
apply (induction xs rule: asc.induct)
apply auto

The first theorem tries to prove that the list is correctly ordered, the second one tries to prove that both lists have the same length.

When I apply induction and auto I expect to get 0 subgoals, that says the theorems are right and the algorithm works fine, but after that I don't know how to remove the subgolas, I mean I don't know how to do the simplification rules (lemma [simp]: "") to do it, I'll appreciate your help.

Answer 1

After

theorem "ordenado (asc xs)"
apply (induction xs rule: asc.induct)
apply auto

you still have to prove the following subgoal:

1. ⋀x xs.
      ordenado (asc xs) ⟹
      ordenado (insertar x (asc xs))

That is, assuming that asc xs is sorted, you have to prove that insertar x (asc xs) is sorted. This suggests to first prove an auxiliary lemma about the interaction between insertar and ordenado

lemma ordenado_insertar [simp]:
  "ordenado (insertar x xs) = ordenado xs"
 ...

which states that insertar x xs is sorted if and only if xs was already sorted. In order to prove this lemma you will again need auxiliary lemmas. This time about menor_igual and the interaction between menor_igual and insertar.

lemma le_menor_igual [simp]:
  "y ≤ x ⟹ menor_igual x xs ⟹ menor_igual y xs"
  ...

lemma menor_igual_insertar [simp]:
  "menor_igual y (insertar x xs) ⟷ y ≤ x ∧ menor_igual y xs"
  ...

The first one states that if y is smaller-equal x and x is smaller-equal all elements of xs, then y is smaller-equal all elements of xs, etc. ...

I leave the proofs as an exercise ;).

For your second theorem I suggest to follow the same recipe. First try induct followed by auto (as you already did), then find out what properties are still missing, prove them as auxiliary lemmas and finish your proofs.