AVL tree Isabelle/HOL

AVL.thy

(* Mikael Sand msand@abo.fi *)
theory AVLproject
imports Main Int
begin

datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"

primrec height :: "'a tree \<Rightarrow> nat" where
  "height Tip = 0" |
  "height (Node l v r) = 1 + max (height l) (height r)"

primrec AVLtree :: "'a tree \<Rightarrow> bool" where
  "AVLtree Tip = True" |
  "AVLtree (Node l v r) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1 + height l) \<and> AVLtree l \<and> AVLtree r )"

primrec set_of :: "'a tree \<Rightarrow> 'a set" where
  "set_of Tip = {}" |
  "set_of (Node l v r) = insert v (set_of l \<union> set_of r)"

primrec sorted_tree :: "('a::order) tree \<Rightarrow> bool" where
  "sorted_tree Tip = True" |
  "sorted_tree (Node l v r) = ((\<forall>v'\<in> set_of l. v' < v) \<and> (\<forall>v'\<in> set_of r. v < v') \<and> sorted_tree l \<and> sorted_tree r)"

primrec contains :: "'a tree \<Rightarrow> 'a \<Rightarrow> bool" where
  "contains Tip c = False" |
  "contains (Node l v r) c = (v = c \<or> contains l c \<or> contains r c)"

primrec inorder :: "'a tree \<Rightarrow> 'a list" where
  "inorder Tip = []" |
  "inorder (Node l v r) = (inorder l) @ (v # (inorder r))"

fun rotate_left :: "'a tree \<Rightarrow> 'a tree" where
  "rotate_left (Node (Node ll vl lr) v r) = (Node ll vl (Node lr v r))" |
  "rotate_left t = t"

fun rotate_right :: "'a tree \<Rightarrow> 'a tree" where
  "rotate_right (Node l v (Node rl vr rr)) = (Node (Node l v rl) vr rr)" |
  "rotate_right t = t"

fun rotate_leftright  :: "'a tree \<Rightarrow> 'a tree" where
  "rotate_leftright (Node (Node ll vl (Node lrl vlr lrr)) v r) = (Node (Node ll vl lrl) vlr (Node lrr v r))" |
  "rotate_leftright t = t"
 
fun rotate_rightleft :: "'a tree \<Rightarrow> 'a tree" where
  "rotate_rightleft (Node l v (Node (Node rll vrl rlr) vr rr)) = (Node (Node l v rll) vrl (Node rlr vr rr))" |
  "rotate_rightleft t = t"

fun balance_left :: "'a tree => 'a tree" where
  "balance_left (Node (Node ll vl lr) v r) = (
    if height ll >= height lr
    then Node ll vl (Node lr v r) (*rotate_left*)
    else case lr of Node lrl vlr lrr \<Rightarrow> Node (Node ll vl lrl) vlr (Node lrr v r))" | (*rotate_leftright*)
  "balance_left t = t"

fun balance_right :: "'a tree => 'a tree" where
  "balance_right (Node l v (Node rl vr rr)) = (
    if height rr >= height rl
    then Node (Node l v rl) vr rr (*rotate_right*)
    else case rl of Node rll vrl rlr \<Rightarrow> Node (Node l v rll) vrl (Node rlr vr rr))" | (*rotate_rightleft*)
  "balance_right t = t"

primrec AVL_balance_left :: "'a tree => 'a tree" where
  "AVL_balance_left Tip = Tip" |
  "AVL_balance_left (Node l v r) = (
    if height l = height r + 2 
    then balance_left (Node l v r) 
    else (Node l v r)
  )"

primrec AVL_balance_right :: "'a tree => 'a tree" where
  "AVL_balance_right Tip = Tip" |
  "AVL_balance_right (Node l v r) = (
    if height r = height l + 2 
    then balance_right (Node l v r)
    else (Node l v r)
  )"

primrec AVLinsert :: "int \<Rightarrow> int tree \<Rightarrow> int tree" where
  "AVLinsert i Tip = Node Tip i Tip" |
  "AVLinsert i (Node l v r) = (
    if i = v 
    then Node l v r
    else 
      if v < i
      then AVL_balance_right (Node l v (AVLinsert i r))
      else AVL_balance_left (Node (AVLinsert i l) v r)
    )"

fun AVLfindmax :: "'a tree => 'a" where
  "AVLfindmax Tip = undefined" |
  "AVLfindmax (Node _ v Tip) = v" |
  "AVLfindmax (Node _ _ r) = AVLfindmax r"

fun AVLdeletemax :: "'a tree => 'a tree" where
  "AVLdeletemax Tip = Tip" |
  "AVLdeletemax (Node l v Tip) = l" |
  "AVLdeletemax (Node l v r) = AVL_balance_left (Node l v (AVLdeletemax r))"

primrec AVLdelete :: "int => int tree => int tree" where
  "AVLdelete i Tip = Tip" |
  "AVLdelete i (Node l v r) = (
    if i = v
    then
      if l = Tip
      then r
      else (AVL_balance_right (Node (AVLdeletemax l) (AVLfindmax l) r))
    else
      if v < i
      then AVL_balance_left (Node l v (AVLdelete i r))
      else AVL_balance_right (Node (AVLdelete i l) v r)
  )"

lemma is_balanced_balance_left:
  "AVLtree l \<Longrightarrow> AVLtree r \<Longrightarrow> height l = height r + 2 \<Longrightarrow> AVLtree (balance_left (Node l v r))"
  apply (case_tac "l")
  apply (auto)
  apply (auto split: tree.split)
done

lemma is_balanced_balance_right:
  "AVLtree l \<Longrightarrow> AVLtree r \<Longrightarrow> height r = height l + 2 \<Longrightarrow> AVLtree (balance_right (Node l v r))"
  apply (case_tac "r")
  apply (auto)
  apply (auto split: tree.split)
done

lemma height_balance_left: "height l = height r + 2 \<Longrightarrow> (height (balance_left (Node l v r)) = height r + 2 \<or> height (balance_left (Node l v r)) = height r + 3)"
  apply (case_tac "l")
  apply (auto split: tree.split)
done

lemma height_balance_right: "height r = height l + 2 \<Longrightarrow> (height (balance_right (Node l v r)) = height l + 2 \<or> height (balance_right (Node l v r)) = height l + 3)"
  apply (case_tac "r")
  apply (auto split: tree.split)
done

lemma height_insert:
 "AVLtree t
  \<Longrightarrow> height (AVLinsert x t) = height t \<or> height (AVLinsert x t) = height t + 1"
proof (induct t)
  case Tip show ?case by simp
next
  case (Node t1 a t2) then show ?case proof (cases "x < a")
    case True show ?thesis
    proof (cases "height (AVLinsert x t1) = height t2 + 2")
      case True with height_balance_left [of _ _ a]
      have "height (balance_left (Node (AVLinsert x t1) a t2)) = height t2 + 2
          \<or> height (balance_left (Node (AVLinsert x t1) a t2)) = height t2 + 3" by simp
      with `x < a`  show ?thesis
      apply simp
      apply auto
      apply (smt AVLtree.simps(2) Node.prems)
      apply (metis True add_2_eq_Suc')
      apply (smt AVLtree.simps(2) Node(1) Node.prems)
      by (metis True add_2_eq_Suc')
    next
      case False with `x < a` Node show ?thesis by auto
    qed
  next
    case False show ?thesis
    proof (cases "height (AVLinsert x t2) = height t1 + 2")
      case True with height_balance_right [of _ _ a]
      have "height (balance_right (Node t1 a (AVLinsert x t2))) = height t1 + 2 \<or>
        height (balance_right (Node t1 a (AVLinsert x t2))) = height t1 + 3" by simp
      with `\<not> x < a` Node show ?thesis
      apply auto
      done
    next
      case False with `\<not> x < a` Node show ?thesis by auto
    qed
  qed
qed

theorem is_balanced_insert: 
  "AVLtree t \<Longrightarrow> AVLtree(AVLinsert x t)"
proof (induct t)
  case Tip show ?case by simp
next
  case (Node t1 a t2) show ?case proof (cases "x < a")
    case True show ?thesis
    proof (cases "height (AVLinsert x t1) = height t2 + 2")
      case True with `x < a` Node show ?thesis
        by (simp add: is_balanced_balance_left)
    next
      case False with `x < a` Node show ?thesis
        using height_insert [of t1 x] by auto
    qed
  next
    case False show ?thesis
    proof (cases "height (AVLinsert x t2) = height t1 + 2")
      case True with `\<not> x < a` Node show ?thesis
        by (simp add: is_balanced_balance_right)
    next
      case False with `\<not> x < a` Node show ?thesis
        using height_insert [of t2 x] by auto
    qed
  qed
qed

lemma set_of_balance_left: "height l = height r + 2 \<Longrightarrow> set_of (balance_left (Node l v r)) = insert v (set_of l \<union> set_of r)"
  by (cases l) (auto split: tree.splits)

lemma set_of_balance_right: "height r = height l + 2 \<Longrightarrow> set_of (balance_right (Node l v r)) = insert v (set_of l \<union> set_of r)"
  by (cases r) (auto split: tree.splits)

theorem set_of_insert: "set_of (AVLinsert x t) = insert x (set_of t)"
  by (induct t) (auto simp add:set_of_balance_left set_of_balance_right Let_def)

theorem is_in_correct: "sorted_tree t \<Longrightarrow> contains t c = (c : set_of t)"
  by (induct t) (auto simp add: less_le_not_le)

lemma sorted_tree_balance_left: "sorted_tree (Node l v r) \<Longrightarrow> height l = Suc (Suc (height r)) \<Longrightarrow> sorted_tree (balance_left (Node l v r))"
  by (cases l) (auto split: tree.splits intro: order_less_trans)

lemma sorted_tree_balance_right: "sorted_tree (Node l v r) \<Longrightarrow> height r = height l + 2 \<Longrightarrow> sorted_tree (balance_right (Node l v r))"
  by (cases r) (auto split:tree.splits intro: order_less_trans)

theorem sorted_tree_insert: "sorted_tree t \<Longrightarrow> sorted_tree (AVLinsert x t)"
  by (induct t) (simp_all add:sorted_tree_balance_left sorted_tree_balance_right set_of_insert linorder_not_less order_neq_le_trans Let_def)

lemma is_leaf :"AVLtree t \<and> (height t) = 0 \<Longrightarrow> t = Tip"
  by (metis Suc_eq_plus1_left Zero_neq_Suc height.simps(2) tree.exhaust)

end