Theory AVL_Bal2_Set

(* Author: Tobias Nipkow *)

section "AVL Tree with Balance Factors (2)"

theory AVL_Bal2_Set
imports
  Cmp
  Isin2
begin

text ‹This version passes a flag (‹Same›/‹Diff›) back up to signal if the height changed.›

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›

datatype 'a alt = Same 'a | Diff 'a

type_synonym 'a tree_bal2 = "'a tree_bal alt"

fun tree :: "'a alt ⇒ 'a" where
"tree(Same t) = t" |
"tree(Diff t) = 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_bal2 ⇒ 'a ⇒ bal ⇒ 'a tree_bal ⇒ 'a tree_bal2" where
"balL AB' c bc C = (case AB' of
   Same AB ⇒ Same (Node AB (c,bc) C) |
   Diff AB ⇒ (case bc of
     Bal ⇒ Diff (Node AB (c,Lh) C) |
     Rh ⇒ Same (Node AB (c,Bal) C) |
     Lh ⇒ (case AB of
       Node A (a,Lh) B ⇒ Same(Node A (a,Bal) (Node B (c,Bal) C)) |
       Node A (a,Rh) B ⇒ Same(rot2 A a B c C))))"

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

fun ins :: "'a::linorder ⇒ 'a tree_bal ⇒ 'a tree_bal2" where
"ins x Leaf = Diff(Node Leaf (x, Bal) Leaf)" |
"ins x (Node l (a, b) r) = (case cmp x a of
   EQ ⇒ Same(Node l (a, b) r) |
   LT ⇒ balL (ins x l) a b r |
   GT ⇒ balR l a b (ins x r))"

definition insert :: "'a::linorder ⇒ 'a tree_bal ⇒ 'a tree_bal" where
"insert x t = tree(ins x t)"

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

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

fun split_max :: "'a tree_bal ⇒ 'a tree_bal2 * 'a" where
"split_max (Node l (a, ba) r) =
  (if r = Leaf then (Diff l,a) else let (r',a') = split_max r in (baldR l a ba r', a'))"

fun del :: "'a::linorder ⇒ 'a tree_bal ⇒ 'a tree_bal2" where
"del _ Leaf = Same Leaf" |
"del x (Node l (a, ba) r) =
  (case cmp x a of
     EQ ⇒ if l = Leaf then Diff r
           else let (l', a') = split_max l in baldL l' a' ba r |
     LT ⇒ baldL (del x l) a ba r |
     GT ⇒ baldR l a ba (del x r))"

definition delete :: "'a::linorder ⇒ 'a tree_bal ⇒ 'a tree_bal" where
"delete x t = tree(del x t)"

lemmas split_max_induct = split_max.induct[case_names Node Leaf]

lemmas splits = if_splits tree.splits alt.splits bal.splits

subsection ‹Proofs›

subsubsection "Proofs about insertion"

lemma avl_ins_case: "avl t ⟹ case ins x t of
   Same t' ⇒ avl t' ∧ height t' = height t |
   Diff t' ⇒ avl t' ∧ height t' = height t + 1 ∧
      (∀l a r. t' = Node l (a,Bal) r ⟶ a = x ∧ l = Leaf ∧ r = Leaf)"
apply(induction x t rule: ins.induct)
apply(auto simp: max_absorb1 split!: splits)
done

corollary avl_insert: "avl t ⟹ avl(insert x t)"
using avl_ins_case[of t x] by (simp add: insert_def split: splits)

(* The following aux lemma simplifies the inorder_ins proof *)

lemma ins_Diff[simp]: "avl t ⟹
  ins x t ≠ Diff Leaf ∧
  (ins x t = Diff (Node l (a,Bal) r) ⟷ t = Leaf ∧ a = x ∧ l=Leaf ∧ r=Leaf) ∧
  ins x t ≠ Diff (Node l (a,Rh) Leaf) ∧
  ins x t ≠ Diff (Node Leaf (a,Lh) r)"
by(drule avl_ins_case[of _ x]) (auto split: splits)

theorem inorder_ins:
  "⟦ avl t;  sorted(inorder t) ⟧ ⟹ inorder(tree(ins 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_baldL:
  "⟦ ba = Rh ⟶ r ≠ Leaf; avl r ⟧
  ⟹ inorder (tree(baldL l a ba r)) = inorder (tree l) @ a # inorder r"
by (auto split: splits)

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

lemma avl_split_max:
  "⟦ split_max t = (t',a); avl t; t ≠ Leaf ⟧ ⟹ case t' of
   Same t' ⇒ avl t' ∧ height t = height t' |
   Diff t' ⇒ avl t' ∧ height t = height t' + 1"
apply(induction t arbitrary: t' a rule: split_max_induct)
 apply(fastforce simp: max_absorb1 max_absorb2 split!: splits prod.splits)
apply simp
done

lemma avl_del_case: "avl t ⟹ case del x t of
   Same t' ⇒ avl t' ∧ height t = height t' |
   Diff t' ⇒ avl t' ∧ height t = height t' + 1"
apply(induction x t rule: del.induct)
 apply(auto simp: max_absorb1 max_absorb2 dest: avl_split_max split!: splits prod.splits)
done

corollary avl_delete: "avl t ⟹ avl(delete x t)"
using avl_del_case[of t x] by(simp add: delete_def split: splits)

lemma inorder_split_maxD:
  "⟦ split_max t = (t',a); t ≠ Leaf; avl t ⟧ ⟹
   inorder (tree 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[simp]: "height t ≠ 0 ⟹ t ≠ Leaf"
by auto

theorem inorder_del:
  "⟦ avl t; sorted(inorder t) ⟧  ⟹ inorder (tree(del x t)) = del_list x (inorder t)"
apply(induction t rule: tree2_induct)
apply(auto simp: del_list_simps inorder_baldL inorder_baldR avl_delete inorder_split_maxD
           simp del: baldR.simps baldL.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_ins insert_def)
next
  case 4 thus ?case by(simp add: inorder_del delete_def)
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