theory AVL_lemmas
imports AVL
begin

primrec isbal :: "'a tree \<Rightarrow> bool" where
isbal_empty:  "isbal Leaf = True" |
isbal_branch: "isbal (Node n l r) = ((height l = height r | 
                                      height l = Suc(height r) | 
                                      Suc(height l) = height r) &
                                     isbal l & isbal r)"

context linorder begin

(* Case split lemmas for insert_avl *)
lemma insert_node_cases[case_names already lrrot rrot linsert rlrot lrot rinsert]: 
"(x=n \<Longrightarrow> P (Node n l r)) \<Longrightarrow>
 ((x\<noteq>n\<and>x<n\<and>height (insert_avl x l) = Suc(Suc(height r))\<and>bal (insert_avl x l) = Right) \<Longrightarrow> 
    P (lr_rot(n, (insert_avl x l), r))) \<Longrightarrow>
 ((x\<noteq>n\<and>x<n\<and>height (insert_avl x l) = Suc(Suc(height r))\<and>bal (insert_avl x l) \<noteq> Right) \<Longrightarrow> 
    P (r_rot(n, (insert_avl x l), r))) \<Longrightarrow>
 (x\<noteq>n\<and>x<n\<and>height (insert_avl x l) \<noteq> Suc(Suc(height r)) \<Longrightarrow> P (Node n (insert_avl x l) r)) \<Longrightarrow>
 ((x\<noteq>n\<and>\<not>x<n\<and>height (insert_avl x r) = Suc(Suc(height l))\<and>bal (insert_avl x r) = Left) \<Longrightarrow> 
    P (rl_rot(n, l, (insert_avl x r)))) \<Longrightarrow>
 ((x\<noteq>n\<and>\<not>x<n\<and>height (insert_avl x r) = Suc(Suc(height l))\<and>bal (insert_avl x r) \<noteq> Left) \<Longrightarrow> 
    P (l_rot(n, l, (insert_avl x r)))) \<Longrightarrow>
 (x\<noteq>n\<and>\<not>x<n\<Longrightarrow>height (insert_avl x r) \<noteq> Suc(Suc(height l)) \<Longrightarrow> P (Node n l (insert_avl x r))) \<Longrightarrow>
 P(insert_avl x (Node n l r))"
by (clarsimp simp add: l_bal_def r_bal_def Let_def)

lemma insert_node_bal_cases[case_names already lbal linsert rbal rinsert]:
"(x=n \<Longrightarrow> P (Node n l r)) \<Longrightarrow> 
 ((x\<noteq>n\<and>x<n\<and>height (insert_avl x l) = Suc(Suc(height r))) \<Longrightarrow> 
    P (l_bal n (insert_avl x l) r)) \<Longrightarrow>
 (x\<noteq>n\<and>x<n\<and>height (insert_avl x l) \<noteq> Suc(Suc(height r)) \<Longrightarrow> P (Node n (insert_avl x l) r)) \<Longrightarrow>
 ((x\<noteq>n\<and>\<not>x<n\<and>height (insert_avl x r) = Suc(Suc(height l))) \<Longrightarrow> 
    P (r_bal n l (insert_avl x r))) \<Longrightarrow>
 (x\<noteq>n\<and>\<not>x<n\<Longrightarrow>height (insert_avl x r) \<noteq> Suc(Suc(height l)) \<Longrightarrow> P (Node n l (insert_avl x r))) \<Longrightarrow>
 P(insert_avl x (Node n l r))"
by (clarsimp simp add: l_bal_def r_bal_def Let_def)

lemma isbal_r_rot[rule_format]: "height l = Suc(Suc(height r)) \<longrightarrow> bal l \<noteq> Right \<longrightarrow> 
                    isbal l \<longrightarrow> isbal r \<longrightarrow> isbal (r_rot (n, l, r))"
unfolding bal_def by (cases l, auto)

lemma isbal_lr_rot[rule_format]: "height l = Suc(Suc(height r)) \<longrightarrow> bal l = Right \<longrightarrow> 
                    isbal l \<longrightarrow> isbal r \<longrightarrow> isbal (lr_rot (n, l, r))"
unfolding bal_def proof (cases l, auto simp add: Orderings.max_def)
  fix a::'a and tree1::"'a tree" and tree2::"'a tree"
  assume "height tree2 = Suc (height r)" and "height tree1 = height r" and
         "isbal tree1" and "isbal tree2" and "isbal r"
  then show "isbal (lr_rot (n, Node a tree1 tree2, r))"
  by (cases "tree2", auto)
qed

(* symmetric *)
lemma isbal_l_rot[rule_format]: "Suc(Suc(height l)) = height r \<longrightarrow> bal r \<noteq> Left \<longrightarrow>
                  isbal l \<longrightarrow> isbal r \<longrightarrow> isbal (l_rot (n, l, r))"
sorry

(* symmetric *)
lemma isbal_rl_rot[rule_format]: "Suc(Suc(height l)) = height r \<longrightarrow> bal r = Left \<longrightarrow>
                  isbal l \<longrightarrow> isbal r \<longrightarrow> isbal (rl_rot (n, l, r))"
sorry

(* lemmas about height after rotation *)

lemma height_lr_rot[rule_format]: "bal l = Right \<longrightarrow> height l = Suc(Suc(height r))
                      \<longrightarrow> Suc(height (lr_rot (n, l, r))) = height (Node n l r)"
unfolding bal_def proof (cases l, auto simp add: Orderings.ord_class.max_def)
  fix a::'a and tree1::"'a tree" and tree2::"'a tree"
  assume "height tree1 < Suc (height r)" and "height tree2 = Suc (height r)"
  then show "height (lr_rot (n, Node a tree1 tree2, r)) = Suc (Suc (height r))"
  by (cases tree2, auto)
qed

lemma height_r_rot[rule_format]: "bal l \<noteq> Right \<longrightarrow> height l = Suc(Suc(height r))
                      \<longrightarrow> Suc(height (r_rot (n, l, r))) = height (Node n l r) |
                             (height (r_rot (n, l, r))) = height (Node n l r)"
unfolding bal_def by (cases l, auto)

lemma height_r_rot2: "bal l \<noteq> Right ==> height l = Suc(Suc(height r))
                      ==> Suc(height (r_rot (n, l, r))) = height (Node n l r) |
                             (height (r_rot (n, l, r))) = height (Node n l r)"
unfolding bal_def by (cases l, auto)


(* symmetric *)
lemma height_rl_rot[rule_format]: "bal r = Left \<longrightarrow> height r = Suc(Suc(height l))
                      \<longrightarrow> Suc(height (rl_rot (n, l, r))) = height (Node n l r)"
sorry

(* symmetric *)
lemma height_l_rot[rule_format]: "bal r \<noteq> Left \<longrightarrow> height r = Suc(Suc(height l))
                      \<longrightarrow> Suc(height (l_rot (n, l, r))) = height (Node n l r) |
                             (height (l_rot (n, l, r))) = height (Node n l r)"
sorry

lemma height_l_bal[rule_format]: "height l = Suc(Suc(height r)) \<longrightarrow> 
                     Suc(height (l_bal n l r)) = height (Node n l r) | 
                         height (l_bal n l r) = height (Node n l r)"
unfolding l_bal_def by (cases "bal l = Right", simp add: height_lr_rot, 
                        fastforce dest: height_r_rot simp: max_def)

(* symmetric *)
lemma height_r_bal[rule_format]: "height r = Suc(Suc(height l)) \<longrightarrow> 
                     Suc(height (r_bal n l r)) = height (Node n l r) | 
                         height (r_bal n l r) = height (Node n l r)"
sorry 

lemma height_insert[rule_format]: "isbal t \<longrightarrow> 
      height(insert_avl x t) = height t | height (insert_avl x t) = Suc(height t)"
proof (induct t)
  case Leaf show "?case" by simp
next
  case (Node a t1 t2)
  show "isbal (Node a t1 t2) \<longrightarrow>
       height (insert_avl x (Node a t1 t2)) = height (Node a t1 t2) \<or>
       height (insert_avl x (Node a t1 t2)) = Suc (height (Node a t1 t2))"
  proof (induct rule: insert_node_bal_cases)
    case already thus "?case" by (simp)
    next
    case lbal
    have hlb: "height (insert_avl x t1) = Suc (Suc (height t2)) \<Longrightarrow>
      Suc (height (l_bal a (insert_avl x t1) t2)) =
      height (Node a (insert_avl x t1) t2) \<or>
      height (l_bal a (insert_avl x t1) t2) =
      height (Node a (insert_avl x t1) t2)" by (rule height_l_bal)
    with Node.hyps lbal show "?case"
    by (clarsimp simp add: Orderings.max_def)
    next
    case linsert with Node.hyps show "?case" by (fastforce)
    next 
    (* symmetric (almost) *)
    case rbal show "?case" sorry
    next
    (* symmetric *)
    case rinsert show "?case" sorry
  qed
qed

(* lemmas about balancing after insert_avl *)
lemma isbal_insert_left[rule_format]:
assumes
  height: "height (insert_avl x l) \<noteq> Suc(Suc(height r))" and
  balinsertxl: "isbal(insert_avl x l)" and
  balnode: "isbal (Node n l r)"
shows
  "isbal (Node n (insert_avl x l) r)"
proof -
  from balnode have 
  height2: "height (insert_avl x l) = height l \<or> height (insert_avl x l) = Suc (height l)" and
  balr: "isbal r"
  by (auto simp add: height_insert)
  with height balinsertxl balnode show "?thesis" by (simp, fastforce)
qed

(* symmetric *)
lemma isbal_insert_right[rule_format]:
assumes
  height: "height (insert_avl x r) \<noteq> Suc(Suc(height l))" and
  balinsertxl: "isbal(insert_avl x r)" and
  balnode: "isbal (Node n l r)"
shows
  "isbal (Node n l (insert_avl x r))"
sorry

(* insert-operation preserves isbal property *)
lemma isbal_insert[rule_format]: "isbal t \<longrightarrow> isbal(insert_avl x t)"
proof (induct t, simp)
  fix a::'a and t1::"'a tree" and t2::"'a tree"
  assume balt1: "isbal t1 \<longrightarrow> isbal (insert_avl x t1)" and
         balt2: "isbal t2 \<longrightarrow> isbal (insert_avl x t2)"
  then show "isbal (Node a t1 t2) \<longrightarrow> isbal (insert_avl x (Node a t1 t2))"
  proof (intro impI)
    assume balance_node: "isbal (Node a t1 t2)"
    then have balance_t1: "isbal t1" and balance_t2: "isbal t2" by (auto)
    with balt1 balt2 have 
    balance_insertt1: "isbal (insert_avl x t1)" and 
    balance_insertt2: "isbal (insert_avl x t2)"by (auto)
    show "isbal (insert_avl x (Node a t1 t2))"
    proof (induct rule: insert_node_cases)
      case already with balance_node show "?case" by (simp)
      next
      case lrrot
      with balance_insertt1 balance_t2
      show "?case" by (simp add: isbal_lr_rot)
      next
      case rrot
      with balance_insertt1 balance_t2
      show "?case" by (simp add: isbal_r_rot)
      next
      case linsert
      hence "height (insert_avl x t1) \<noteq> Suc (Suc (height t2))" by (elim conjE)
      from this balance_insertt1 balance_node show "?case" by (rule isbal_insert_left)
      next
      case rlrot show "?case" sorry
      next
      case lrot show "?case" sorry
      next
      case rinsert show "?case" sorry
    qed
  qed
qed

(******************************    isin    **********************************)

(* rotations preserve isin property *)

lemma isin_lr_rot[rule_format]: "height l = Suc(Suc(height r)) \<longrightarrow> bal l = Right \<longrightarrow> 
  isin x (lr_rot (n, l, r)) = isin x (Node n l r)"
proof (cases l, simp_all add: bal_def, intro impI)
  fix a::'a and t1::"'a tree" and t2::"'a tree"
  assume "l = Node a t1 t2" and
         "max (height t1) (height t2) = Suc (height r)" and
         "height t1 < height t2"
  thus "isin x (lr_rot (n, Node a t1 t2, r)) =
       (x = n \<or> x = a \<or> isin x t1 \<or> isin x t2 \<or> isin x r)"
  by (cases t2, simp_all add:bal_def, auto)
qed

lemma isin_r_rot[rule_format]: "height l = Suc(Suc(height r)) \<longrightarrow> bal l \<noteq> Right \<longrightarrow>
  isin x (r_rot (n, l, r)) = isin x (Node n l r)"
by (cases l, simp, intro impI, fastforce simp add: bal_def)

(* symmetric *)
lemma isin_rl_rot[rule_format]: "height r = Suc(Suc(height l)) \<longrightarrow> bal r = Left \<longrightarrow>
  isin x (rl_rot (n, l, r)) = isin x (Node n l r)"
sorry

(* symmetric *)
lemma isin_l_rot[rule_format]: "height r = Suc(Suc(height l)) \<longrightarrow> bal r \<noteq> Left \<longrightarrow>
  isin x (l_rot (n, l, r)) = isin x (Node n l r)"
sorry

(* isin insert *)
lemma isin_insert: "isin y (insert_avl x t) = (y=x | isin y t)"
proof (induct t)
  case Leaf thus "?case" by (simp)
  next
  case Node thus "?case"
    by (simp add: l_bal_def isin_lr_rot isin_r_rot
                  r_bal_def isin_rl_rot isin_l_rot Let_def, blast)
qed

(******************************    isord    **********************************)

(* rotations preserve isord property *)

lemma isord_lr_rot[rule_format]: 
"height l = Suc(Suc(height r)) \<longrightarrow> bal l = Right \<longrightarrow> isordP (Node n l r) P \<longrightarrow> 
  isordP (lr_rot (n, l, r)) P"
proof (cases l, simp, intro impI)
  fix a::'a and t1::"'a tree" and t2::"'a tree"
  have simp1[simp]: "\<And>a x n. a < n \<Longrightarrow> (x < n \<and> x < a) = (x < a)" by auto
  have simp2[simp]: "\<And>a x n Q. a < n \<Longrightarrow> (x < n \<and> Q \<and> x < a) = (x < a \<and> Q)" by auto
  have simp3[simp]: "\<And>a x n. n < a \<Longrightarrow> (n < x \<and> a < x) = (a < x)" by auto
  have and_commutes: "\<And> a b. (a \<and> b) = (b \<and> a)" by auto
  assume "l = Node a t1 t2" and "height l = Suc (Suc (height r))" and
         "bal l = bal.Right" and "isordP (Node n l r) P"
  thus "isordP (lr_rot (n, l, r)) P"
  unfolding bal_def 
    by (cases t2, simp_all, simp add:and_commutes)
qed

lemma isord_r_rot[rule_format]:
"height l = Suc(Suc(height r)) \<longrightarrow> bal l \<noteq> Right \<longrightarrow> isordP (Node n l r) P \<longrightarrow> 
  isordP (r_rot (n, l, r)) P"
proof (cases l, simp, intro impI)
  fix a t1 t2
  have simp1[simp]: "\<And>a x n. a < n \<Longrightarrow> (x < n \<and> x < a) = (x < a)" by auto
  have simp2[simp]: "\<And>a x n Q. a < n \<Longrightarrow> (x < n \<and> Q \<and> x < a) = (x < a \<and> Q)" by auto
  have simp3[simp]: "\<And>a x n. n < a \<Longrightarrow> (n < x \<and> a < x) = (a < x)" by auto
  have and_commutes: "\<And> a b. (a \<and> b) = (b \<and> a)" "\<And> a b c. (a \<and> b \<and> c) = (b \<and> a \<and> c)" by auto
  assume "l = Node a t1 t2" and "height l = Suc (Suc (height r))" and
         "bal l \<noteq> bal.Right" and "isordP (Node n l r) P"
  thus "isordP (r_rot (n, l, r)) P"
  unfolding bal_def 
    by (cases t2, simp_all, simp add:and_commutes)
qed

(* symmetric *)
lemma isord_rl_rot[rule_format]:
"height r = Suc(Suc(height l)) \<longrightarrow> bal r = Left \<longrightarrow> isordP (Node n l r) P \<longrightarrow>
  isordP (rl_rot (n, l, r)) P"
sorry

(* symmetric *)
lemma isord_l_rot[rule_format]:
"height r = Suc(Suc(height l)) \<longrightarrow> bal r \<noteq> Left \<longrightarrow> isordP (Node n l r) P \<longrightarrow> 
  isordP (l_rot (n, l, r)) P"
sorry

lemma isordP_insert[rule_format]: "P x \<longrightarrow> isordP t P \<longrightarrow> isordP (insert_avl x t) P"
proof (induct t arbitrary: P,simp)
  case (Node a l r)
  show "?case"
  proof (intro impI)
    assume px: "P x"
    assume isordnode: "isordP (Node a l r) P"
    show "isordP (insert_avl x (Node a l r)) P"
    proof (induct rule: insert_node_cases)
      case already with isordnode show "?case" by simp
      next
      case lrrot with isordnode px 
      show "?case" by (intro isord_lr_rot, simp_all, intro Node.hyps(1)[rule_format], simp_all)
      next
      case rrot with isordnode px 
      show "?case" by (intro isord_r_rot, simp_all, intro Node.hyps(1)[rule_format], simp_all)
      next
      case lrot with isordnode px 
      show "?case" by (intro isord_l_rot, simp_all, intro Node.hyps(2)[rule_format], simp_all, auto)
      next
      case rlrot with isordnode px 
      show "?case" by (intro isord_rl_rot, simp_all, intro Node.hyps(2)[rule_format], simp_all, auto)
      next
      case linsert with isordnode px
      show "?case" by (simp, intro Node.hyps(1)[rule_format], simp_all)
      next
      case rinsert with isordnode px
      show "?case" by (simp, intro Node.hyps(2)[rule_format], simp_all, auto)
    qed
  qed
qed

lemma isord_insert[rule_format]: "isord t \<longrightarrow> isord (insert_avl x t)"
by (simp add:isordP_insert isord_def)

end

end