Theory AVL_Bal_Set

(* Author: Tobias Nipkow *)

section "AVL Tree with Balance Factors (1)"

theory AVL_Bal_Set
imports
  Cmp
  Isin2
begin

text ‹This version detects height increase/decrease from above via the change in balance factors.›

datatype bal = Lh | Bal | Rh

type_synonym 'a tree_bal = "('a * bal) tree"

text ‹Invariant:›

fun avl :: "'a tree_bal ⇒ bool" where
"avl Leaf = True" |
"avl (Node l (a,b) r) =
  ((case b of
    Bal ⇒ height r = height l |
    Lh ⇒ height l = height r + 1 |
    Rh ⇒ height r = height l + 1)
  ∧ avl l ∧ avl r)"


subsection ‹Code›

fun is_bal where
"is_bal (Node l (a,b) r) = (b = Bal)"

fun incr where
"incr t t' = (t = Leaf ∨ is_bal t ∧ ¬ is_bal t')"

fun rot2 where
"rot2 A a B c C = (case B of
  (Node B⇩1 (b, bb) B⇩2) ⇒
    let b⇩1 = if bb = Rh then Lh else Bal;
        b⇩2 = if bb = Lh then Rh else Bal
    in Node (Node A (a,b⇩1) B⇩1) (b,Bal) (Node B⇩2 (c,b⇩2) C))"

fun balL :: "'a tree_bal ⇒ 'a ⇒ bal ⇒ 'a tree_bal ⇒ 'a tree_bal" where
"balL AB c bc C = (case bc of
     Bal ⇒ Node AB (c,Lh) C |
     Rh ⇒ Node AB (c,Bal) C |
     Lh ⇒ (case AB of
       Node A (a,Lh) B ⇒ Node A (a,Bal) (Node B (c,Bal) C) |
       Node A (a,Bal) B ⇒ Node A (a,Rh) (Node B (c,Lh) C) |
       Node A (a,Rh) B ⇒ rot2 A a B c C))"

fun balR :: "'a tree_bal ⇒ 'a ⇒ bal ⇒ 'a tree_bal ⇒ 'a tree_bal" where
"balR A a ba BC = (case ba of
     Bal ⇒ Node A (a,Rh) BC |
     Lh ⇒ Node A (a,Bal) BC |
     Rh ⇒ (case BC of
       Node B (c,Rh) C ⇒ Node (Node A (a,Bal) B) (c,Bal) C |
       Node B (c,Bal) C ⇒ Node (Node A (a,Rh) B) (c,Lh) C |
       Node B (c,Lh) C ⇒ rot2 A a B c C))"

fun insert :: "'a::linorder ⇒ 'a tree_bal ⇒ 'a tree_bal" where
"insert x Leaf = Node Leaf (x, Bal) Leaf" |
"insert x (Node l (a, b) r) = (case cmp x a of
   EQ ⇒ Node l (a, b) r |
   LT ⇒ let l' = insert x l in if incr l l' then balL l' a b r else Node l' (a,b) r |
   GT ⇒ let r' = insert x r in if incr r r' then balR l a b r' else Node l (a,b) r')"

fun decr where
"decr t t' = (t ≠ Leaf ∧ (t' = Leaf ∨ ¬ is_bal t ∧ is_bal t'))"

fun split_max :: "'a tree_bal ⇒ 'a tree_bal * 'a" where
"split_max (Node l (a, ba) r) =
  (if r = Leaf then (l,a)
   else let (r',a') = split_max r;
            t' = if decr r r' then balL l a ba r' else Node l (a,ba) r'
        in (t', a'))"

fun delete :: "'a::linorder ⇒ 'a tree_bal ⇒ 'a tree_bal" where
"delete _ Leaf = Leaf" |
"delete x (Node l (a, ba) r) =
  (case cmp x a of
     EQ ⇒ if l = Leaf then r
           else let (l', a') = split_max l in
                if decr l l' then balR l' a' ba r else Node l' (a',ba) r |
     LT ⇒ let l' = delete x l in if decr l l' then balR l' a ba r else Node l' (a,ba) r |
     GT ⇒ let r' = delete x r in if decr r r' then balL l a ba r' else Node l (a,ba) r')"


subsection ‹Proofs›

lemmas split_max_induct = split_max.induct[case_names Node Leaf]

lemmas splits = if_splits tree.splits bal.splits

declare Let_def [simp]

subsubsection "Proofs about insertion"

lemma avl_insert: "avl t ⟹
  avl(insert x t) ∧
  height(insert x t) = height t + (if incr t (insert x t) then 1 else 0)"
apply(induction x t rule: insert.induct)
apply(auto split!: splits)
done

text ‹The following two auxiliary lemma merely simplify the proof of ‹inorder_insert›.›

lemma [simp]: "[] ≠ ins_list x xs"
by(cases xs) auto

lemma [simp]: "avl t ⟹ insert x t ≠ ⟨l, (a, Rh), ⟨⟩⟩ ∧ insert x t ≠ ⟨⟨⟩, (a, Lh), r⟩"
by(drule avl_insert[of _ x]) (auto split: splits)

theorem inorder_insert:
  "⟦ avl t;  sorted(inorder t) ⟧ ⟹ inorder(insert x t) = ins_list x (inorder t)"
apply(induction t)
apply (auto simp: ins_list_simps split!: splits)
done


subsubsection "Proofs about deletion"

lemma inorder_balR:
  "⟦ ba = Rh ⟶ r ≠ Leaf; avl r ⟧
  ⟹ inorder (balR l a ba r) = inorder l @ a # inorder r"
by (auto split: splits)

lemma inorder_balL:
  "⟦ ba = Lh ⟶ l ≠ Leaf; avl l ⟧
   ⟹ inorder (balL l a ba r) = inorder l @ a # inorder r"
by (auto split: splits)

lemma height_1_iff: "avl t ⟹ height t = Suc 0 ⟷ (∃x. t = Node Leaf (x,Bal) Leaf)"
by(cases t) (auto split: splits prod.splits)

lemma avl_split_max:
  "⟦ split_max t = (t',a); avl t; t ≠ Leaf ⟧ ⟹
   avl t' ∧ height t = height t' + (if decr t t' then 1 else 0)"
apply(induction t arbitrary: t' a rule: split_max_induct)
 apply(auto simp: max_absorb1 max_absorb2 height_1_iff split!: splits prod.splits)
done

lemma avl_delete: "avl t ⟹
  avl (delete x t) ∧
  height t = height (delete x t) + (if decr t (delete x t) then 1 else 0)"
apply(induction x t rule: delete.induct)
 apply(auto simp: max_absorb1 max_absorb2 height_1_iff dest: avl_split_max split!: splits prod.splits)
done

lemma inorder_split_maxD:
  "⟦ split_max t = (t',a); t ≠ Leaf; avl t ⟧ ⟹
   inorder t' @ [a] = inorder t"
apply(induction t arbitrary: t' rule: split_max.induct)
 apply(fastforce split!: splits prod.splits)
apply simp
done

lemma neq_Leaf_if_height_neq_0: "height t ≠ 0 ⟹ t ≠ Leaf"
by auto

lemma split_max_Leaf: "⟦ t ≠ Leaf; avl t ⟧ ⟹ split_max t = (⟨⟩, x) ⟷ t = Node Leaf (x,Bal) Leaf"
by(cases t) (auto split: splits prod.splits)

theorem inorder_delete:
  "⟦ avl t; sorted(inorder t) ⟧  ⟹ inorder (delete x t) = del_list x (inorder t)"
apply(induction t rule: tree2_induct)
apply(auto simp: del_list_simps inorder_balR inorder_balL avl_delete inorder_split_maxD
                 split_max_Leaf neq_Leaf_if_height_neq_0
           simp del: balL.simps balR.simps split!: splits prod.splits)
done


subsubsection ‹Set Implementation›

interpretation S: Set_by_Ordered
where empty = Leaf and isin = isin
  and insert = insert
  and delete = delete
  and inorder = inorder and inv = avl
proof (standard, goal_cases)
  case 1 show ?case by (simp)
next
  case 2 thus ?case by(simp add: isin_set_inorder)
next
  case 3 thus ?case by(simp add: inorder_insert)
next
  case 4 thus ?case by(simp add: inorder_delete)
next
  case 5 thus ?case by (simp)
next
  case 6 thus ?case by (simp add: avl_insert)
next
  case 7 thus ?case by (simp add: avl_delete)
qed

end