Incomplete proof of balancing node sizes after insert

balancing_node_sizes.thy

theory balancing
  imports Main
begin

type_synonym nodesizes = "nat list"

fun insert :: "nodesizes ⇒ nat ⇒ nodesizes" where
  "insert [] _ = []" |
  "insert (x#xs) 0 = (x+1)#xs" |
  "insert (x#xs) n = x # insert xs (n-1)"

fun lend_left_helper :: "nat option ⇒ nodesizes ⇒ nat ⇒ nodesizes" where
  "lend_left_helper _ [] _ = []" |
  "lend_left_helper _ [x] _ = [x]" |
  "lend_left_helper (Some p) (x # xs) 0 = (p + 1) # (x - 1) # xs" |
  "lend_left_helper None (x # xs) 0 = x # xs" |
  "lend_left_helper prev (x # xs) (Suc n) = 
    (case prev of
      Some p ⇒ p # lend_left_helper (Some x) xs n
    | None ⇒ lend_left_helper (Some x) xs n)"

definition lend_left :: "nodesizes ⇒ nat ⇒ nodesizes" where
  "lend_left xs n = lend_left_helper None xs n"

fun lend_right :: "nodesizes ⇒ nat ⇒ nodesizes" where
  "lend_right [] _ = []" |
  "lend_right [x] _ = [x]" |
  "lend_right (x # y # zs) 0 = (x-1) # (y+1) # zs" |
  "lend_right (x # xs) n = x # lend_right xs (n - 1)"

definition even_div_left :: "nat ⇒ nat" where
  "even_div_left x = x div 2"

definition even_div_right :: "nat ⇒ nat" where
  "even_div_right x = (if x mod 2 = 0 then x div 2 else (x div 2) + 1)"

lemma left_and_right_division_sums_to_x:
  shows "even_div_left x + even_div_right x = x"
proof (cases "x mod 2 = 0")
  case True
  then show ?thesis
    using even_div_left_def even_div_right_def by auto
next
  case False
  then show ?thesis
    using even_div_left_def even_div_right_def by presburger
qed

lemma left_and_right_division_balanced_when_even:
  assumes "x mod 2 = 0"
  shows "even_div_left x = even_div_right x"
  using assms(1)
  using even_div_left_def even_div_right_def by presburger

lemma left_and_right_division_balanced_when_odd:
  assumes "x mod 2 = 1"
  shows "even_div_left x + 1 = even_div_right x"
  using assms(1)
  using even_div_left_def even_div_right_def by presburger

fun split :: "nodesizes ⇒ nat ⇒ nodesizes" where
  "split [] _ = []" |
  "split (x # xs) 0 = [even_div_left x, even_div_right x] @ xs" |
  "split (x # xs) (Suc n) = split xs n"

definition "N ≡ 4"

fun balance_metric :: "nat list ⇒ nat" where
  "balance_metric [] = 0" |
  "balance_metric (x # xs) = (x - N) ^ 2 + balance_metric xs"

definition balance :: "nodesizes ⇒ nat ⇒ nodesizes" where
  "balance sizes n =
    (let metric_ops = [(balance_metric sizes, sizes),
                        (balance_metric (lend_left sizes n), lend_left sizes n),
                        (balance_metric (lend_right sizes n), lend_right sizes n),
                        (balance_metric (split sizes n), split sizes n)];
        min_metric_op = 
          (List.fold 
            (λacc tup. if (fst acc < fst tup) then acc else tup) 
            metric_ops 
            (hd metric_ops))
     in
        snd min_metric_op)"

definition balanced_insert :: "nodesizes ⇒ nat ⇒ nodesizes" where
  "balanced_insert sizes n = balance (insert sizes n) n"

lemma insert_commutative:
  assumes "∀x ∈ set sizes. x > 0 ∧ x < N"
  shows "insert (insert sizes x) y = insert (insert sizes y) x"
  unfolding insert.simps
proof (cases "x = y")
  case True
  then show ?thesis
    by auto
next
  case False
  then show ?thesis
  proof (cases "x < y")
    case True
    then show ?thesis sorry
  next
    case False
    then show ?thesis sorry
  qed
qed

lemma balanced_insert_commutative:
  assumes "∀x ∈ set sizes. x > 0 ∧ x < N"
  shows "balanced_insert (balanced_insert sizes x) y = balanced_insert (balanced_insert sizes y) x"
  quickcheck
  sorry

end