Quelle RBT_Impl.thy Sprache: Isabelle

(*  Title:      HOL/Library/RBT_Impl.thy
    Author:     Markus Reiter, TU Muenchen
    Author:     Alexander Krauss, TU Muenchen
*)

section \<open>Implementation of Red-Black Trees\<close>

theory RBT_Impl
imports Main
begin

text \<open>
  For applications, you should use theory \<open>RBT\<close> which defines
  an abstract type of red-black tree obeying the invariant.
\<close>

subsection \<open>Datatype of RB trees\<close>

datatype color = R | B
datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"

lemma rbt_cases:
  obtains (Empty) "t = Empty"
  | (Red) l k v r where "t = Branch R l k v r"
  | (Black) l k v r where "t = Branch B l k v r"
proof (cases t)
  case Empty with that show thesis by blast
next
  case (Branch c) with that show thesis by (cases c) blast+
qed

subsection \<open>Tree properties\<close>

subsubsection \<open>Content of a tree\<close>

primrec entries :: "('a, 'b) rbt \ ('a \ 'b) list"
where
  "entries Empty = []"
| "entries (Branch _ l k v r) = entries l @ (k,v) # entries r"

abbreviation (input) entry_in_tree :: "'a \ 'b \ ('a, 'b) rbt \ bool"
where
  "entry_in_tree k v t \ (k, v) \ set (entries t)"

definition keys :: "('a, 'b) rbt \ 'a list" where
  "keys t = map fst (entries t)"

lemma keys_simps [simp]:
  "keys Empty = []"
  "keys (Branch c l k v r) = keys l @ k # keys r"
  by (simp_all add: keys_def)

lemma entry_in_tree_keys:
  assumes "(k, v) \ set (entries t)"
  shows "k \ set (keys t)"
proof -
  from assms have "fst (k, v) \ fst ` set (entries t)" by (rule imageI)
  then show ?thesis by (simp add: keys_def)
qed

lemma keys_entries:
  "k \ set (keys t) \ (\v. (k, v) \ set (entries t))"
  by (auto intro: entry_in_tree_keys) (auto simp add: keys_def)

lemma non_empty_rbt_keys:
  "t \ rbt.Empty \ keys t \ []"
  by (cases t) simp_all

subsubsection \<open>Search tree properties\<close>

context ord begin

definition rbt_less :: "'a \ ('a, 'b) rbt \ bool"
where
  rbt_less_prop: "rbt_less k t \ (\x\set (keys t). x < k)"

abbreviation rbt_less_symbol (infix \<open>|\<guillemotleft>\<close> 50)
where "t |\ x \ rbt_less x t"

definition rbt_greater :: "'a \ ('a, 'b) rbt \ bool" (infix \\|\ 50)
where
  rbt_greater_prop: "rbt_greater k t = (\x\set (keys t). k < x)"

lemma rbt_less_simps [simp]:
  "Empty |\ k = True"
  "Branch c lt kt v rt |\ k \ kt < k \ lt |\ k \ rt |\ k"
  by (auto simp add: rbt_less_prop)

lemma rbt_greater_simps [simp]:
  "k \| Empty = True"
  "k \| (Branch c lt kt v rt) \ k < kt \ k \| lt \ k \| rt"
  by (auto simp add: rbt_greater_prop)

lemmas rbt_ord_props = rbt_less_prop rbt_greater_prop

lemmas rbt_greater_nit = rbt_greater_prop entry_in_tree_keys
lemmas rbt_less_nit = rbt_less_prop entry_in_tree_keys

lemma (in order)
  shows rbt_less_eq_trans: "l |\ u \ u \ v \ l |\ v"
  and rbt_less_trans: "t |\ x \ x < y \ t |\ y"
  and rbt_greater_eq_trans: "u \ v \ v \| r \ u \| r"
  and rbt_greater_trans: "x < y \ y \| t \ x \| t"
  by (auto simp: rbt_ord_props)

primrec rbt_sorted :: "('a, 'b) rbt \ bool"
where
  "rbt_sorted Empty = True"
| "rbt_sorted (Branch c l k v r) = (l |\ k \ k \| r \ rbt_sorted l \ rbt_sorted r)"

end

context linorder begin

lemma rbt_sorted_entries:
  "rbt_sorted t \ List.sorted (map fst (entries t))"
by (induct t)  (force simp: sorted_append rbt_ord_props dest!: entry_in_tree_keys)+

lemma distinct_entries:
  "rbt_sorted t \ distinct (map fst (entries t))"
by (induct t) (force simp: sorted_append rbt_ord_props dest!: entry_in_tree_keys)+

lemma distinct_keys:
  "rbt_sorted t \ distinct (keys t)"
  by (simp add: distinct_entries keys_def)

subsubsection \<open>Tree lookup\<close>

primrec (in ord) rbt_lookup :: "('a, 'b) rbt \ 'a \ 'b"
where
  "rbt_lookup Empty k = None"
| "rbt_lookup (Branch _ l x y r) k =
   (if k < x then rbt_lookup l k else if x < k then rbt_lookup r k else Some y)"

lemma rbt_lookup_keys: "rbt_sorted t \ dom (rbt_lookup t) = set (keys t)"
  by (induct t) (auto simp: dom_def rbt_greater_prop rbt_less_prop)

lemma dom_rbt_lookup_Branch:
  "rbt_sorted (Branch c t1 k v t2) \
    dom (rbt_lookup (Branch c t1 k v t2))
    = Set.insert k (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
proof -
  assume "rbt_sorted (Branch c t1 k v t2)"
  then show ?thesis by (simp add: rbt_lookup_keys)
qed

lemma finite_dom_rbt_lookup [simp, intro!]: "finite (dom (rbt_lookup t))"
proof (induct t)
  case Empty then show ?case by simp
next
  case (Branch color t1 a b t2)
  let ?A = "Set.insert a (dom (rbt_lookup t1) \ dom (rbt_lookup t2))"
  have "dom (rbt_lookup (Branch color t1 a b t2)) \ ?A" by (auto split: if_split_asm)
  moreover from Branch have "finite (insert a (dom (rbt_lookup t1) \ dom (rbt_lookup t2)))" by simp
  ultimately show ?case by (rule finite_subset)
qed

end

context ord begin

lemma rbt_lookup_rbt_less[simp]: "t |\ k \ rbt_lookup t k = None"
by (induct t) auto

lemma rbt_lookup_rbt_greater[simp]: "k \| t \ rbt_lookup t k = None"
by (induct t) auto

lemma rbt_lookup_Empty: "rbt_lookup Empty = Map.empty"
by (rule ext) simp

end

context linorder begin

lemma map_of_entries:
  "rbt_sorted t \ map_of (entries t) = rbt_lookup t"
proof (induct t)
  case Empty thus ?case by (simp add: rbt_lookup_Empty)
next
  case (Branch c t1 k v t2)
  have "rbt_lookup (Branch c t1 k v t2) = rbt_lookup t2 ++ [k\v] ++ rbt_lookup t1"
  proof (rule ext)
    fix x
    from Branch have RBT_SORTED: "rbt_sorted (Branch c t1 k v t2)" by simp
    let ?thesis = "rbt_lookup (Branch c t1 k v t2) x = (rbt_lookup t2 ++ [k \ v] ++ rbt_lookup t1) x"

    have DOM_T1: "!!k'. k'\dom (rbt_lookup t1) \ k>k'"
    proof -
      fix k'
      from RBT_SORTED have "t1 |\ k" by simp
      with rbt_less_prop have "\k'\set (keys t1). k>k'" by auto
      moreover assume "k'\dom (rbt_lookup t1)"
      ultimately show "k>k'" using rbt_lookup_keys RBT_SORTED by auto
    qed

    have DOM_T2: "!!k'. k'\dom (rbt_lookup t2) \ k
    proof -
      fix k'
      from RBT_SORTED have "k \| t2" by simp
      with rbt_greater_prop have "\k'\set (keys t2). k
      moreover assume "k'\dom (rbt_lookup t2)"
      ultimately show "k using rbt_lookup_keys RBT_SORTED by auto
    qed

    {
      assume C: "x
      hence "rbt_lookup (Branch c t1 k v t2) x = rbt_lookup t1 x" by simp
      moreover from C have "x\dom [k\v]" by simp
      moreover have "x \ dom (rbt_lookup t2)"
      proof
        assume "x \ dom (rbt_lookup t2)"
        with DOM_T2 have "k by blast
        with C show False by simp
      qed
      ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
    } moreover {
      assume [simp]: "x=k"
      hence "rbt_lookup (Branch c t1 k v t2) x = [k \ v] x" by simp
      moreover have "x \ dom (rbt_lookup t1)"
      proof
        assume "x \ dom (rbt_lookup t1)"
        with DOM_T1 have "k>x" by blast
        thus False by simp
      qed
      ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
    } moreover {
      assume C: "x>k"
      hence "rbt_lookup (Branch c t1 k v t2) x = rbt_lookup t2 x" by (simp add: less_not_sym[of k x])
      moreover from C have "x\dom [k\v]" by simp
      moreover have "x\dom (rbt_lookup t1)" proof
        assume "x\dom (rbt_lookup t1)"
        with DOM_T1 have "k>x" by simp
        with C show False by simp
      qed
      ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
    } ultimately show ?thesis using less_linear by blast
  qed
  also from Branch
  have "rbt_lookup t2 ++ [k \ v] ++ rbt_lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
  finally show ?case by simp
qed

lemma rbt_lookup_in_tree: "rbt_sorted t \ rbt_lookup t k = Some v \ (k, v) \ set (entries t)"
  by (simp add: map_of_entries [symmetric] distinct_entries)

lemma set_entries_inject:
  assumes rbt_sorted: "rbt_sorted t1" "rbt_sorted t2"
  shows "set (entries t1) = set (entries t2) \ entries t1 = entries t2"
proof -
  from rbt_sorted have "distinct (map fst (entries t1))"
    "distinct (map fst (entries t2))"
    by (auto intro: distinct_entries)
  with rbt_sorted show ?thesis
    by (auto intro: map_sorted_distinct_set_unique rbt_sorted_entries simp add: distinct_map)
qed

lemma entries_eqI:
  assumes rbt_sorted: "rbt_sorted t1" "rbt_sorted t2"
  assumes rbt_lookup: "rbt_lookup t1 = rbt_lookup t2"
  shows "entries t1 = entries t2"
proof -
  from rbt_sorted rbt_lookup have "map_of (entries t1) = map_of (entries t2)"
    by (simp add: map_of_entries)
  with rbt_sorted have "set (entries t1) = set (entries t2)"
    by (simp add: map_of_inject_set distinct_entries)
  with rbt_sorted show ?thesis by (simp add: set_entries_inject)
qed

lemma entries_rbt_lookup:
  assumes "rbt_sorted t1" "rbt_sorted t2"
  shows "entries t1 = entries t2 \ rbt_lookup t1 = rbt_lookup t2"
  using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric])

lemma rbt_lookup_from_in_tree:
  assumes "rbt_sorted t1" "rbt_sorted t2"
  and "\v. (k, v) \ set (entries t1) \ (k, v) \ set (entries t2)"
  shows "rbt_lookup t1 k = rbt_lookup t2 k"
proof -
  from assms have "k \ dom (rbt_lookup t1) \ k \ dom (rbt_lookup t2)"
    by (simp add: keys_entries rbt_lookup_keys)
  with assms show ?thesis by (auto simp add: rbt_lookup_in_tree [symmetric])
qed

end

subsubsection \<open>Red-black properties\<close>

primrec color_of :: "('a, 'b) rbt \ color"
where
  "color_of Empty = B"
| "color_of (Branch c _ _ _ _) = c"

primrec bheight :: "('a,'b) rbt \ nat"
where
  "bheight Empty = 0"
| "bheight (Branch c lt k v rt) = (if c = B then Suc (bheight lt) else bheight lt)"

primrec inv1 :: "('a, 'b) rbt \ bool"
where
  "inv1 Empty = True"
| "inv1 (Branch c lt k v rt) \ inv1 lt \ inv1 rt \ (c = B \ color_of lt = B \ color_of rt = B)"

primrec inv1l :: "('a, 'b) rbt \ bool" \ \Weaker version\
where
  "inv1l Empty = True"
| "inv1l (Branch c l k v r) = (inv1 l \ inv1 r)"
lemma [simp]: "inv1 t \ inv1l t" by (cases t) simp+

primrec inv2 :: "('a, 'b) rbt \ bool"
where
  "inv2 Empty = True"
| "inv2 (Branch c lt k v rt) = (inv2 lt \ inv2 rt \ bheight lt = bheight rt)"

context ord begin

definition is_rbt :: "('a, 'b) rbt \ bool" where
  "is_rbt t \ inv1 t \ inv2 t \ color_of t = B \ rbt_sorted t"

lemma is_rbt_rbt_sorted [simp]:
  "is_rbt t \ rbt_sorted t" by (simp add: is_rbt_def)

theorem Empty_is_rbt [simp]:
  "is_rbt Empty" by (simp add: is_rbt_def)

end

subsection \<open>Insertion\<close>

text \<open>The function definitions are based on the book by Okasaki.\<close>

fun (* slow, due to massive case splitting *)
  balance :: "('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt"
where
  "balance (Branch R a w x b) s t (Branch R c y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
  "balance (Branch R (Branch R a w x b) s t c) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
  "balance (Branch R a w x (Branch R b s t c)) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
  "balance a w x (Branch R b s t (Branch R c y z d)) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
  "balance a w x (Branch R (Branch R b s t c) y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
  "balance a s t b = Branch B a s t b"

lemma balance_inv1: "\inv1l l; inv1l r\ \ inv1 (balance l k v r)"
  by (induct l k v r rule: balance.induct) auto

lemma balance_bheight: "bheight l = bheight r \ bheight (balance l k v r) = Suc (bheight l)"
  by (induct l k v r rule: balance.induct) auto

lemma balance_inv2:
  assumes "inv2 l" "inv2 r" "bheight l = bheight r"
  shows "inv2 (balance l k v r)"
  using assms
  by (induct l k v r rule: balance.induct) auto

context ord begin

lemma balance_rbt_greater[simp]: "(v \| balance a k x b) = (v \| a \ v \| b \ v < k)"
  by (induct a k x b rule: balance.induct) auto

lemma balance_rbt_less[simp]: "(balance a k x b |\ v) = (a |\ v \ b |\ v \ k < v)"
  by (induct a k x b rule: balance.induct) auto

end

lemma (in linorder) balance_rbt_sorted:
  fixes k :: "'a"
  assumes "rbt_sorted l" "rbt_sorted r" "l |\ k" "k \| r"
  shows "rbt_sorted (balance l k v r)"
using assms proof (induct l k v r rule: balance.induct)
  case ("2_2" a x w b y t c z s va vb vd vc)
  hence "y < z \ z \| Branch B va vb vd vc"
    by (auto simp add: rbt_ord_props)
  hence "y \| (Branch B va vb vd vc)" by (blast dest: rbt_greater_trans)
  with "2_2" show ?case by simp
next
  case ("3_2" va vb vd vc x w b y s c z)
  from "3_2" have "x < y \ Branch B va vb vd vc |\ x"
    by simp
  hence "Branch B va vb vd vc |\ y" by (blast dest: rbt_less_trans)
  with "3_2" show ?case by simp
next
  case ("3_3" x w b y s c z t va vb vd vc)
  from "3_3" have "y < z \ z \| Branch B va vb vd vc" by simp
  hence "y \| Branch B va vb vd vc" by (blast dest: rbt_greater_trans)
  with "3_3" show ?case by simp
next
  case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc)
  hence "x < y \ Branch B vd ve vg vf |\ x" by simp
  hence 1: "Branch B vd ve vg vf |\ y" by (blast dest: rbt_less_trans)
  from "3_4" have "y < z \ z \| Branch B va vb vii vc" by simp
  hence "y \| Branch B va vb vii vc" by (blast dest: rbt_greater_trans)
  with 1 "3_4" show ?case by simp
next
  case ("4_2" va vb vd vc x w b y s c z t dd)
  hence "x < y \ Branch B va vb vd vc |\ x" by simp
  hence "Branch B va vb vd vc |\ y" by (blast dest: rbt_less_trans)
  with "4_2" show ?case by simp
next
  case ("5_2" x w b y s c z t va vb vd vc)
  hence "y < z \ z \| Branch B va vb vd vc" by simp
  hence "y \| Branch B va vb vd vc" by (blast dest: rbt_greater_trans)
  with "5_2" show ?case by simp
next
  case ("5_3" va vb vd vc x w b y s c z t)
  hence "x < y \ Branch B va vb vd vc |\ x" by simp
  hence "Branch B va vb vd vc |\ y" by (blast dest: rbt_less_trans)
  with "5_3" show ?case by simp
next
  case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf)
  hence "x < y \ Branch B va vb vg vc |\ x" by simp
  hence 1: "Branch B va vb vg vc |\ y" by (blast dest: rbt_less_trans)
  from "5_4" have "y < z \ z \| Branch B vd ve vii vf" by simp
  hence "y \| Branch B vd ve vii vf" by (blast dest: rbt_greater_trans)
  with 1 "5_4" show ?case by simp
qed simp+

lemma entries_balance [simp]:
  "entries (balance l k v r) = entries l @ (k, v) # entries r"
  by (induct l k v r rule: balance.induct) auto

lemma keys_balance [simp]:
  "keys (balance l k v r) = keys l @ k # keys r"
  by (simp add: keys_def)

lemma balance_in_tree:
  "entry_in_tree k x (balance l v y r) \ entry_in_tree k x l \ k = v \ x = y \ entry_in_tree k x r"
  by (auto simp add: keys_def)

lemma (in linorder) rbt_lookup_balance[simp]:
fixes k :: "'a"
assumes "rbt_sorted l" "rbt_sorted r" "l |\ k" "k \| r"
shows "rbt_lookup (balance l k v r) x = rbt_lookup (Branch B l k v r) x"
by (rule rbt_lookup_from_in_tree) (auto simp:assms balance_in_tree balance_rbt_sorted)

primrec paint :: "color \ ('a,'b) rbt \ ('a,'b) rbt"
where
  "paint c Empty = Empty"
| "paint c (Branch _ l k v r) = Branch c l k v r"

lemma paint_inv1l[simp]: "inv1l t \ inv1l (paint c t)" by (cases t) auto
lemma paint_inv1[simp]: "inv1l t \ inv1 (paint B t)" by (cases t) auto
lemma paint_inv2[simp]: "inv2 t \ inv2 (paint c t)" by (cases t) auto
lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto
lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto

context ord begin

lemma paint_rbt_sorted[simp]: "rbt_sorted t \ rbt_sorted (paint c t)" by (cases t) auto
lemma paint_rbt_lookup[simp]: "rbt_lookup (paint c t) = rbt_lookup t" by (rule ext) (cases t, auto)
lemma paint_rbt_greater[simp]: "(v \| paint c t) = (v \| t)" by (cases t) auto
lemma paint_rbt_less[simp]: "(paint c t |\ v) = (t |\ v)" by (cases t) auto

fun
  rbt_ins :: "('a \ 'b \ 'b \ 'b) \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt"
where
  "rbt_ins f k v Empty = Branch R Empty k v Empty" |
  "rbt_ins f k v (Branch B l x y r) = (if k < x then balance (rbt_ins f k v l) x y r
                                       else if k > x then balance l x y (rbt_ins f k v r)
                                       else Branch B l x (f k y v) r)" |
  "rbt_ins f k v (Branch R l x y r) = (if k < x then Branch R (rbt_ins f k v l) x y r
                                       else if k > x then Branch R l x y (rbt_ins f k v r)
                                       else Branch R l x (f k y v) r)"

lemma ins_inv1_inv2:
  assumes "inv1 t" "inv2 t"
  shows "inv2 (rbt_ins f k x t)" "bheight (rbt_ins f k x t) = bheight t"
  "color_of t = B \ inv1 (rbt_ins f k x t)" "inv1l (rbt_ins f k x t)"
  using assms
  by (induct f k x t rule: rbt_ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight)

end

context linorder begin

lemma ins_rbt_greater[simp]: "(v \| rbt_ins f (k :: 'a) x t) = (v \| t \ k > v)"
  by (induct f k x t rule: rbt_ins.induct) auto
lemma ins_rbt_less[simp]: "(rbt_ins f k x t |\ v) = (t |\ v \ k < v)"
  by (induct f k x t rule: rbt_ins.induct) auto
lemma ins_rbt_sorted[simp]: "rbt_sorted t \ rbt_sorted (rbt_ins f k x t)"
  by (induct f k x t rule: rbt_ins.induct) (auto simp: balance_rbt_sorted)

lemma keys_ins: "set (keys (rbt_ins f k v t)) = { k } \ set (keys t)"
  by (induct f k v t rule: rbt_ins.induct) auto

lemma rbt_lookup_ins:
  fixes k :: "'a"
  assumes "rbt_sorted t"
  shows "rbt_lookup (rbt_ins f k v t) x = ((rbt_lookup t)(k |-> case rbt_lookup t k of None \ v
                                                                | Some w \<Rightarrow> f k w v)) x"
using assms by (induct f k v t rule: rbt_ins.induct) auto

end

context ord begin

definition rbt_insert_with_key :: "('a \ 'b \ 'b \ 'b) \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt"
where "rbt_insert_with_key f k v t = paint B (rbt_ins f k v t)"

definition rbt_insertw_def: "rbt_insert_with f = rbt_insert_with_key (\_. f)"

definition rbt_insert :: "'a \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where
  "rbt_insert = rbt_insert_with_key (\_ _ nv. nv)"

end

context linorder begin

lemma rbt_insertwk_rbt_sorted: "rbt_sorted t \ rbt_sorted (rbt_insert_with_key f (k :: 'a) x t)"
  by (auto simp: rbt_insert_with_key_def)

theorem rbt_insertwk_is_rbt:
  assumes inv: "is_rbt t"
  shows "is_rbt (rbt_insert_with_key f k x t)"
using assms
unfolding rbt_insert_with_key_def is_rbt_def
by (auto simp: ins_inv1_inv2)

lemma rbt_lookup_rbt_insertwk:
  assumes "rbt_sorted t"
  shows "rbt_lookup (rbt_insert_with_key f k v t) x = ((rbt_lookup t)(k |-> case rbt_lookup t k of None \ v
                                                       | Some w \<Rightarrow> f k w v)) x"
unfolding rbt_insert_with_key_def using assms
by (simp add:rbt_lookup_ins)

lemma rbt_insertw_rbt_sorted: "rbt_sorted t \ rbt_sorted (rbt_insert_with f k v t)"
  by (simp add: rbt_insertwk_rbt_sorted rbt_insertw_def)
theorem rbt_insertw_is_rbt: "is_rbt t \ is_rbt (rbt_insert_with f k v t)"
  by (simp add: rbt_insertwk_is_rbt rbt_insertw_def)

lemma rbt_lookup_rbt_insertw:
  "is_rbt t \
    rbt_lookup (rbt_insert_with f k v t) =
      (rbt_lookup t)(k \<mapsto> (if k \<in> dom (rbt_lookup t) then f (the (rbt_lookup t k)) v else v))"
  by (rule ext, cases "rbt_lookup t k") (auto simp: rbt_lookup_rbt_insertwk dom_def rbt_insertw_def)

lemma rbt_insert_rbt_sorted: "rbt_sorted t \ rbt_sorted (rbt_insert k v t)"
  by (simp add: rbt_insertwk_rbt_sorted rbt_insert_def)
theorem rbt_insert_is_rbt [simp]: "is_rbt t \ is_rbt (rbt_insert k v t)"
  by (simp add: rbt_insertwk_is_rbt rbt_insert_def)

lemma rbt_lookup_rbt_insert: "is_rbt t \ rbt_lookup (rbt_insert k v t) = (rbt_lookup t)(k\v)"
  by (rule ext) (simp add: rbt_insert_def rbt_lookup_rbt_insertwk split: option.split)

end

subsection \<open>Deletion\<close>

lemma bheight_paintR'[simp]: "color_of t = B \ bheight (paint R t) = bheight t - 1"
by (cases t rule: rbt_cases) auto

text \<open>
  The function definitions are based on the Haskell code by Stefan Kahrs
  at \<^url>\<open>http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html\<close>.
\<close>

fun
  balance_left :: "('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt"
where
  "balance_left (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" |
  "balance_left bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" |
  "balance_left bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))" |
  "balance_left t k x s = Empty"

lemma balance_left_inv2_with_inv1:
  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
  shows "bheight (balance_left lt k v rt) = bheight lt + 1"
  and   "inv2 (balance_left lt k v rt)"
using assms
by (induct lt k v rt rule: balance_left.induct) (auto simp: balance_inv2 balance_bheight)

lemma balance_left_inv2_app:
  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B"
  shows "inv2 (balance_left lt k v rt)"
        "bheight (balance_left lt k v rt) = bheight rt"
using assms
by (induct lt k v rt rule: balance_left.induct) (auto simp add: balance_inv2 balance_bheight)+

lemma balance_left_inv1: "\inv1l a; inv1 b; color_of b = B\ \ inv1 (balance_left a k x b)"
  by (induct a k x b rule: balance_left.induct) (simp add: balance_inv1)+

lemma balance_left_inv1l: "\ inv1l lt; inv1 rt \ \ inv1l (balance_left lt k x rt)"
by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1)

lemma (in linorder) balance_left_rbt_sorted:
  "\ rbt_sorted l; rbt_sorted r; rbt_less k l; k \| r \ \ rbt_sorted (balance_left l k v r)"
apply (induct l k v r rule: balance_left.induct)
apply (auto simp: balance_rbt_sorted)
apply (unfold rbt_greater_prop rbt_less_prop)
by force+

context order begin

lemma balance_left_rbt_greater:
  fixes k :: "'a"
  assumes "k \| a" "k \| b" "k < x"
  shows "k \| balance_left a x t b"
using assms
by (induct a x t b rule: balance_left.induct) auto

lemma balance_left_rbt_less:
  fixes k :: "'a"
  assumes "a |\ k" "b |\ k" "x < k"
  shows "balance_left a x t b |\ k"
using assms
by (induct a x t b rule: balance_left.induct) auto

end

lemma balance_left_in_tree:
  assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r"
  shows "entry_in_tree k v (balance_left l a b r) = (entry_in_tree k v l \ k = a \ v = b \ entry_in_tree k v r)"
using assms
by (induct l k v r rule: balance_left.induct) (auto simp: balance_in_tree)

fun
  balance_right :: "('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt"
where
  "balance_right a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" |
  "balance_right (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" |
  "balance_right (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)" |
  "balance_right t k x s = Empty"

lemma balance_right_inv2_with_inv1:
  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
  shows "inv2 (balance_right lt k v rt) \ bheight (balance_right lt k v rt) = bheight lt"
using assms
by (induct lt k v rt rule: balance_right.induct) (auto simp: balance_inv2 balance_bheight)

lemma balance_right_inv1: "\inv1 a; inv1l b; color_of a = B\ \ inv1 (balance_right a k x b)"
by (induct a k x b rule: balance_right.induct) (simp add: balance_inv1)+

lemma balance_right_inv1l: "\ inv1 lt; inv1l rt \ \inv1l (balance_right lt k x rt)"
by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1)

lemma (in linorder) balance_right_rbt_sorted:
  "\ rbt_sorted l; rbt_sorted r; rbt_less k l; k \| r \ \ rbt_sorted (balance_right l k v r)"
apply (induct l k v r rule: balance_right.induct)
apply (auto simp:balance_rbt_sorted)
apply (unfold rbt_less_prop rbt_greater_prop)
by force+

context order begin

lemma balance_right_rbt_greater:
  fixes k :: "'a"
  assumes "k \| a" "k \| b" "k < x"
  shows "k \| balance_right a x t b"
using assms by (induct a x t b rule: balance_right.induct) auto

lemma balance_right_rbt_less:
  fixes k :: "'a"
  assumes "a |\ k" "b |\ k" "x < k"
  shows "balance_right a x t b |\ k"
using assms by (induct a x t b rule: balance_right.induct) auto

end

lemma balance_right_in_tree:
  assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r"
  shows "entry_in_tree x y (balance_right l k v r) = (entry_in_tree x y l \ x = k \ y = v \ entry_in_tree x y r)"
using assms by (induct l k v r rule: balance_right.induct) (auto simp: balance_in_tree)

fun
  combine :: "('a,'b) rbt \ ('a,'b) rbt \ ('a,'b) rbt"
where
  "combine Empty x = x"
| "combine x Empty = x"
| "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of
                                    Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
                                    bc \<Rightarrow> Branch R a k x (Branch R bc s y d))"
| "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of
                                    Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
                                    bc \<Rightarrow> balance_left a k x (Branch B bc s y d))"
| "combine a (Branch R b k x c) = Branch R (combine a b) k x c"
| "combine (Branch R a k x b) c = Branch R a k x (combine b c)"

lemma combine_inv2:
  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
  shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)"
using assms
by (induct lt rt rule: combine.induct)
   (auto simp: balance_left_inv2_app split: rbt.splits color.splits)

lemma combine_inv1:
  assumes "inv1 lt" "inv1 rt"
  shows "color_of lt = B \ color_of rt = B \ inv1 (combine lt rt)"
         "inv1l (combine lt rt)"
using assms
by (induct lt rt rule: combine.induct)
   (auto simp: balance_left_inv1 split: rbt.splits color.splits)

context linorder begin

lemma combine_rbt_greater[simp]:
  fixes k :: "'a"
  assumes "k \| l" "k \| r"
  shows "k \| combine l r"
using assms
by (induct l r rule: combine.induct)
   (auto simp: balance_left_rbt_greater split:rbt.splits color.splits)

lemma combine_rbt_less[simp]:
  fixes k :: "'a"
  assumes "l |\ k" "r |\ k"
  shows "combine l r |\ k"
using assms
by (induct l r rule: combine.induct)
   (auto simp: balance_left_rbt_less split:rbt.splits color.splits)

lemma combine_rbt_sorted:
  fixes k :: "'a"
  assumes "rbt_sorted l" "rbt_sorted r" "l |\ k" "k \| r"
  shows "rbt_sorted (combine l r)"
using assms proof (induct l r rule: combine.induct)
  case (3 a x v b c y w d)
  hence ineqs: "a |\ x" "x \| b" "b |\ k" "k \| c" "c |\ y" "y \| d"
    by auto
  with 3
  show ?case
    by (cases "combine b c" rule: rbt_cases)
      (auto, (metis combine_rbt_greater combine_rbt_less ineqs ineqs rbt_less_simps(2) rbt_greater_simps(2) rbt_greater_trans rbt_less_trans)+)
next
  case (4 a x v b c y w d)
  hence "x < k \ rbt_greater k c" by simp
  hence "rbt_greater x c" by (blast dest: rbt_greater_trans)
  with 4 have 2: "rbt_greater x (combine b c)" by (simp add: combine_rbt_greater)
  from 4 have "k < y \ rbt_less k b" by simp
  hence "rbt_less y b" by (blast dest: rbt_less_trans)
  with 4 have 3: "rbt_less y (combine b c)" by (simp add: combine_rbt_less)
  show ?case
  proof (cases "combine b c" rule: rbt_cases)
    case Empty
    from 4 have "x < y \ rbt_greater y d" by auto
    hence "rbt_greater x d" by (blast dest: rbt_greater_trans)
    with 4 Empty have "rbt_sorted a" and "rbt_sorted (Branch B Empty y w d)"
      and "rbt_less x a" and "rbt_greater x (Branch B Empty y w d)" by auto
    with Empty show ?thesis by (simp add: balance_left_rbt_sorted)
  next
    case (Red lta va ka rta)
    with 2 4 have "x < va \ rbt_less x a" by simp
    hence 5: "rbt_less va a" by (blast dest: rbt_less_trans)
    from Red 3 4 have "va < y \ rbt_greater y d" by simp
    hence "rbt_greater va d" by (blast dest: rbt_greater_trans)
    with Red 2 3 4 5 show ?thesis by simp
  next
    case (Black lta va ka rta)
    from 4 have "x < y \ rbt_greater y d" by auto
    hence "rbt_greater x d" by (blast dest: rbt_greater_trans)
    with Black 2 3 4 have "rbt_sorted a" and "rbt_sorted (Branch B (combine b c) y w d)"
      and "rbt_less x a" and "rbt_greater x (Branch B (combine b c) y w d)" by auto
    with Black show ?thesis by (simp add: balance_left_rbt_sorted)
  qed
next
  case (5 va vb vd vc b x w c)
  hence "k < x \ rbt_less k (Branch B va vb vd vc)" by simp
  hence "rbt_less x (Branch B va vb vd vc)" by (blast dest: rbt_less_trans)
  with 5 show ?case by (simp add: combine_rbt_less)
next
  case (6 a x v b va vb vd vc)
  hence "x < k \ rbt_greater k (Branch B va vb vd vc)" by simp
  hence "rbt_greater x (Branch B va vb vd vc)" by (blast dest: rbt_greater_trans)
  with 6 show ?case by (simp add: combine_rbt_greater)
qed simp+

end

lemma combine_in_tree:
  assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r"
  shows "entry_in_tree k v (combine l r) = (entry_in_tree k v l \ entry_in_tree k v r)"
using assms
proof (induct l r rule: combine.induct)
  case (4 _ _ _ b c)
  hence a: "bheight (combine b c) = bheight b" by (simp add: combine_inv2)
  from 4 have b: "inv1l (combine b c)" by (simp add: combine_inv1)

  show ?case
  proof (cases "combine b c" rule: rbt_cases)
    case Empty
    with 4 a show ?thesis by (auto simp: balance_left_in_tree)
  next
    case (Red lta ka va rta)
    with 4 show ?thesis by auto
  next
    case (Black lta ka va rta)
    with a b 4  show ?thesis by (auto simp: balance_left_in_tree)
  qed
qed (auto split: rbt.splits color.splits)

context ord begin

fun
  rbt_del_from_left :: "'a \ ('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" and
  rbt_del_from_right :: "'a \ ('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" and
  rbt_del :: "'a\ ('a,'b) rbt \ ('a,'b) rbt"
where
  "rbt_del x Empty = Empty" |
  "rbt_del x (Branch c a y s b) =
   (if x < y then rbt_del_from_left x a y s b
    else (if x > y then rbt_del_from_right x a y s b else combine a b))" |
  "rbt_del_from_left x (Branch B lt z v rt) y s b = balance_left (rbt_del x (Branch B lt z v rt)) y s b" |
  "rbt_del_from_left x a y s b = Branch R (rbt_del x a) y s b" |
  "rbt_del_from_right x a y s (Branch B lt z v rt) = balance_right a y s (rbt_del x (Branch B lt z v rt))" |
  "rbt_del_from_right x a y s b = Branch R a y s (rbt_del x b)"

end

context linorder begin

lemma
  assumes "inv2 lt" "inv1 lt"
  shows
  "\inv2 rt; bheight lt = bheight rt; inv1 rt\ \
   inv2 (rbt_del_from_left x lt k v rt) \<and>
   bheight (rbt_del_from_left x lt k v rt) = bheight lt \<and>
   (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_left x lt k v rt) \<or>
    (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_left x lt k v rt))"
  and "\inv2 rt; bheight lt = bheight rt; inv1 rt\ \
  inv2 (rbt_del_from_right x lt k v rt) \<and>
  bheight (rbt_del_from_right x lt k v rt) = bheight lt \<and>
  (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_right x lt k v rt) \<or>
   (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_right x lt k v rt))"
  and rbt_del_inv1_inv2: "inv2 (rbt_del x lt) \ (color_of lt = R \ bheight (rbt_del x lt) = bheight lt \ inv1 (rbt_del x lt)
  \<or> color_of lt = B \<and> bheight (rbt_del x lt) = bheight lt - 1 \<and> inv1l (rbt_del x lt))"
using assms
proof (induct x lt k v rt and x lt k v rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
case (2 y c _ y')
  have "y = y' \ y < y' \ y > y'" by auto
  thus ?case proof (elim disjE)
    assume "y = y'"
    with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
  next
    assume "y < y'"
    with 2 show ?thesis by (cases c) auto
  next
    assume "y' < y"
    with 2 show ?thesis by (cases c) auto
  qed
next
  case (3 y lt z v rta y' ss bb)
  thus ?case by (cases "color_of (Branch B lt z v rta) = B \ color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+
next
  case (5 y a y' ss lt z v rta)
  thus ?case by (cases "color_of a = B \ color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+
next
  case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \ color_of Empty = B") simp+
qed auto

lemma
  rbt_del_from_left_rbt_less: "\ lt |\ v; rt |\ v; k < v\ \ rbt_del_from_left x lt k y rt |\ v"
  and rbt_del_from_right_rbt_less: "\lt |\ v; rt |\ v; k < v\ \ rbt_del_from_right x lt k y rt |\ v"
  and rbt_del_rbt_less: "lt |\ v \ rbt_del x lt |\ v"
by (induct x lt k y rt and x lt k y rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
   (auto simp: balance_left_rbt_less balance_right_rbt_less)

lemma rbt_del_from_left_rbt_greater: "\v \| lt; v \| rt; k > v\ \ v \| rbt_del_from_left x lt k y rt"
  and rbt_del_from_right_rbt_greater: "\v \| lt; v \| rt; k > v\ \ v \| rbt_del_from_right x lt k y rt"
  and rbt_del_rbt_greater: "v \| lt \ v \| rbt_del x lt"
by (induct x lt k y rt and x lt k y rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
   (auto simp: balance_left_rbt_greater balance_right_rbt_greater)

lemma "\rbt_sorted lt; rbt_sorted rt; lt |\ k; k \| rt\ \ rbt_sorted (rbt_del_from_left x lt k y rt)"
  and "\rbt_sorted lt; rbt_sorted rt; lt |\ k; k \| rt\ \ rbt_sorted (rbt_del_from_right x lt k y rt)"
  and rbt_del_rbt_sorted: "rbt_sorted lt \ rbt_sorted (rbt_del x lt)"
proof (induct x lt k y rt and x lt k y rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
  case (3 x lta zz v rta yy ss bb)
  from 3 have "Branch B lta zz v rta |\ yy" by simp
  hence "rbt_del x (Branch B lta zz v rta) |\ yy" by (rule rbt_del_rbt_less)
  with 3 show ?case by (simp add: balance_left_rbt_sorted)
next
  case ("4_2" x vaa vbb vdd vc yy ss bb)
  hence "Branch R vaa vbb vdd vc |\ yy" by simp
  hence "rbt_del x (Branch R vaa vbb vdd vc) |\ yy" by (rule rbt_del_rbt_less)
  with "4_2" show ?case by simp
next
  case (5 x aa yy ss lta zz v rta)
  hence "yy \| Branch B lta zz v rta" by simp
  hence "yy \| rbt_del x (Branch B lta zz v rta)" by (rule rbt_del_rbt_greater)
  with 5 show ?case by (simp add: balance_right_rbt_sorted)
next
  case ("6_2" x aa yy ss vaa vbb vdd vc)
  hence "yy \| Branch R vaa vbb vdd vc" by simp
  hence "yy \| rbt_del x (Branch R vaa vbb vdd vc)" by (rule rbt_del_rbt_greater)
  with "6_2" show ?case by simp
qed (auto simp: combine_rbt_sorted)

lemma "\rbt_sorted lt; rbt_sorted rt; lt |\ kt; kt \| rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\ \ entry_in_tree k v (rbt_del_from_left x lt kt y rt) = (False \ (x \ k \ entry_in_tree k v (Branch c lt kt y rt)))"
  and "\rbt_sorted lt; rbt_sorted rt; lt |\ kt; kt \| rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\ \ entry_in_tree k v (rbt_del_from_right x lt kt y rt) = (False \ (x \ k \ entry_in_tree k v (Branch c lt kt y rt)))"
  and rbt_del_in_tree: "\rbt_sorted t; inv1 t; inv2 t\ \ entry_in_tree k v (rbt_del x t) = (False \ (x \ k \ entry_in_tree k v t))"
proof (induct x lt kt y rt and x lt kt y rt and x t rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
  case (2 xx c aa yy ss bb)
  have "xx = yy \ xx < yy \ xx > yy" by auto
  from this 2 show ?case proof (elim disjE)
    assume "xx = yy"
    with 2 show ?thesis proof (cases "xx = k")
      case True
      from 2 \<open>xx = yy\<close> \<open>xx = k\<close> have "rbt_sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
      hence "\ entry_in_tree k v aa" "\ entry_in_tree k v bb" by (auto simp: rbt_less_nit rbt_greater_prop)
      with \<open>xx = yy\<close> 2 \<open>xx = k\<close> show ?thesis by (simp add: combine_in_tree)
    qed (simp add: combine_in_tree)
  qed simp+
next
  case (3 xx lta zz vv rta yy ss bb)
  define mt where [simp]: "mt = Branch B lta zz vv rta"
  from 3 have "inv2 mt \ inv1 mt" by simp
  hence "inv2 (rbt_del xx mt) \ (color_of mt = R \ bheight (rbt_del xx mt) = bheight mt \ inv1 (rbt_del xx mt) \ color_of mt = B \ bheight (rbt_del xx mt) = bheight mt - 1 \ inv1l (rbt_del xx mt))" by (blast dest: rbt_del_inv1_inv2)
  with 3 have 4: "entry_in_tree k v (rbt_del_from_left xx mt yy ss bb) = (False \ xx \ k \ entry_in_tree k v mt \ (k = yy \ v = ss) \ entry_in_tree k v bb)" by (simp add: balance_left_in_tree)
  thus ?case proof (cases "xx = k")
    case True
    from 3 True have "yy \| bb \ yy > k" by simp
    hence "k \| bb" by (blast dest: rbt_greater_trans)
    with 3 4 True show ?thesis by (auto simp: rbt_greater_nit)
  qed auto
next
  case ("4_1" xx yy ss bb)
  show ?case proof (cases "xx = k")
    case True
    with "4_1" have "yy \| bb \ k < yy" by simp
    hence "k \| bb" by (blast dest: rbt_greater_trans)
    with "4_1" \<open>xx = k\<close>
   have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: rbt_greater_nit)
    thus ?thesis by auto
  qed simp+
next
  case ("4_2" xx vaa vbb vdd vc yy ss bb)
  thus ?case proof (cases "xx = k")
    case True
    with "4_2" have "k < yy \ yy \| bb" by simp
    hence "k \| bb" by (blast dest: rbt_greater_trans)
    with True "4_2" show ?thesis by (auto simp: rbt_greater_nit)
  qed auto
next
  case (5 xx aa yy ss lta zz vv rta)
  define mt where [simp]: "mt = Branch B lta zz vv rta"
  from 5 have "inv2 mt \ inv1 mt" by simp
  hence "inv2 (rbt_del xx mt) \ (color_of mt = R \ bheight (rbt_del xx mt) = bheight mt \ inv1 (rbt_del xx mt) \ color_of mt = B \ bheight (rbt_del xx mt) = bheight mt - 1 \ inv1l (rbt_del xx mt))" by (blast dest: rbt_del_inv1_inv2)
  with 5 have 3: "entry_in_tree k v (rbt_del_from_right xx aa yy ss mt) = (entry_in_tree k v aa \ (k = yy \ v = ss) \ False \ xx \ k \ entry_in_tree k v mt)" by (simp add: balance_right_in_tree)
  thus ?case proof (cases "xx = k")
    case True
    from 5 True have "aa |\ yy \ yy < k" by simp
    hence "aa |\ k" by (blast dest: rbt_less_trans)
    with 3 5 True show ?thesis by (auto simp: rbt_less_nit)
  qed auto
next
  case ("6_1" xx aa yy ss)
  show ?case proof (cases "xx = k")
    case True
    with "6_1" have "aa |\ yy \ k > yy" by simp
    hence "aa |\ k" by (blast dest: rbt_less_trans)
    with "6_1" \<open>xx = k\<close> show ?thesis by (auto simp: rbt_less_nit)
  qed simp
next
  case ("6_2" xx aa yy ss vaa vbb vdd vc)
  thus ?case proof (cases "xx = k")
    case True
    with "6_2" have "k > yy \ aa |\ yy" by simp
    hence "aa |\ k" by (blast dest: rbt_less_trans)
    with True "6_2" show ?thesis by (auto simp: rbt_less_nit)
  qed auto
qed simp

definition (in ord) rbt_delete where
  "rbt_delete k t = paint B (rbt_del k t)"

theorem rbt_delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (rbt_delete k t)"
proof -
  from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto
  hence "inv2 (rbt_del k t) \ (color_of t = R \ bheight (rbt_del k t) = bheight t \ inv1 (rbt_del k t) \ color_of t = B \ bheight (rbt_del k t) = bheight t - 1 \ inv1l (rbt_del k t))" by (rule rbt_del_inv1_inv2)
  hence "inv2 (rbt_del k t) \ inv1l (rbt_del k t)" by (cases "color_of t") auto
  with assms show ?thesis
    unfolding is_rbt_def rbt_delete_def
    by (auto intro: paint_rbt_sorted rbt_del_rbt_sorted)
qed

lemma rbt_delete_in_tree:
  assumes "is_rbt t"
  shows "entry_in_tree k v (rbt_delete x t) = (x \ k \ entry_in_tree k v t)"
  using assms unfolding is_rbt_def rbt_delete_def
  by (auto simp: rbt_del_in_tree)

lemma rbt_lookup_rbt_delete:
  assumes is_rbt: "is_rbt t"
  shows "rbt_lookup (rbt_delete k t) = (rbt_lookup t)|`(-{k})"
proof
  fix x
  show "rbt_lookup (rbt_delete k t) x = (rbt_lookup t |` (-{k})) x"
  proof (cases "x = k")
    assume "x = k"
    with is_rbt show ?thesis
      by (cases "rbt_lookup (rbt_delete k t) k") (auto simp: rbt_lookup_in_tree rbt_delete_in_tree)
  next
    assume "x \ k"
    thus ?thesis
      by auto (metis is_rbt rbt_delete_is_rbt rbt_delete_in_tree is_rbt_rbt_sorted rbt_lookup_from_in_tree)
  qed
qed

end

subsection \<open>Modifying existing entries\<close>

context ord begin

primrec
  rbt_map_entry :: "'a \ ('b \ 'b) \ ('a, 'b) rbt \ ('a, 'b) rbt"
where
  "rbt_map_entry k f Empty = Empty"
| "rbt_map_entry k f (Branch c lt x v rt) =
    (if k < x then Branch c (rbt_map_entry k f lt) x v rt
    else if k > x then (Branch c lt x v (rbt_map_entry k f rt))
    else Branch c lt x (f v) rt)"

lemma rbt_map_entry_color_of: "color_of (rbt_map_entry k f t) = color_of t" by (induct t) simp+
lemma rbt_map_entry_inv1: "inv1 (rbt_map_entry k f t) = inv1 t" by (induct t) (simp add: rbt_map_entry_color_of)+
lemma rbt_map_entry_inv2: "inv2 (rbt_map_entry k f t) = inv2 t" "bheight (rbt_map_entry k f t) = bheight t" by (induct t) simp+
lemma rbt_map_entry_rbt_greater: "rbt_greater a (rbt_map_entry k f t) = rbt_greater a t" by (induct t) simp+
lemma rbt_map_entry_rbt_less: "rbt_less a (rbt_map_entry k f t) = rbt_less a t" by (induct t) simp+
lemma rbt_map_entry_rbt_sorted: "rbt_sorted (rbt_map_entry k f t) = rbt_sorted t"
  by (induct t) (simp_all add: rbt_map_entry_rbt_less rbt_map_entry_rbt_greater)

theorem rbt_map_entry_is_rbt [simp]: "is_rbt (rbt_map_entry k f t) = is_rbt t"
unfolding is_rbt_def by (simp add: rbt_map_entry_inv2 rbt_map_entry_color_of rbt_map_entry_rbt_sorted rbt_map_entry_inv1 )

end

theorem (in linorder) rbt_lookup_rbt_map_entry:
  "rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := map_option f (rbt_lookup t k))"
  by (induct t) (auto split: option.splits simp add: fun_eq_iff)

subsection \<open>Mapping all entries\<close>

primrec
  map :: "('a \ 'b \ 'c) \ ('a, 'b) rbt \ ('a, 'c) rbt"
where
  "map f Empty = Empty"
| "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)"

lemma map_entries [simp]: "entries (map f t) = List.map (\(k, v). (k, f k v)) (entries t)"
  by (induct t) auto
lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def)
lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+
lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+
lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+

context ord begin

lemma map_rbt_greater: "rbt_greater k (map f t) = rbt_greater k t" by (induct t) simp+
lemma map_rbt_less: "rbt_less k (map f t) = rbt_less k t" by (induct t) simp+
lemma map_rbt_sorted: "rbt_sorted (map f t) = rbt_sorted t"  by (induct t) (simp add: map_rbt_less map_rbt_greater)+
theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t"
unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_rbt_sorted map_color_of)

end

theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = map_option (f x) (rbt_lookup t x)"
  by (induct t) (auto simp: antisym_conv3)
(* FIXME: simproc "antisym less" does not work for linorder context, only for linorder type class
    by (induct t) auto *)

hide_const (open) map

subsection \<open>Folding over entries\<close>

definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a, 'b) rbt \ 'c \ 'c" where
  "fold f t = List.fold (case_prod f) (entries t)"

lemma fold_simps [simp]:
  "fold f Empty = id"
  "fold f (Branch c lt k v rt) = fold f rt \ f k v \ fold f lt"
  by (simp_all add: fold_def fun_eq_iff)

lemma fold_code [code]:
  "fold f Empty x = x"
  "fold f (Branch c lt k v rt) x = fold f rt (f k v (fold f lt x))"
by(simp_all)

\<comment> \<open>fold with continuation predicate\<close>
fun foldi :: "('c \ bool) \ ('a \ 'b \ 'c \ 'c) \ ('a :: linorder, 'b) rbt \ 'c \ 'c"
  where
  "foldi c f Empty s = s" |
  "foldi c f (Branch col l k v r) s = (
    if (c s) then
      let s' = foldi c f l s in
        if (c s') then
          foldi c f r (f k v s')
        else s'
    else
      s
  )"

subsection \<open>Bulkloading a tree\<close>

definition (in ord) rbt_bulkload :: "('a \ 'b) list \ ('a, 'b) rbt" where
  "rbt_bulkload xs = foldr (\(k, v). rbt_insert k v) xs Empty"

context linorder begin

lemma rbt_bulkload_is_rbt [simp, intro]:
  "is_rbt (rbt_bulkload xs)"
  unfolding rbt_bulkload_def by (induct xs) auto

lemma rbt_lookup_rbt_bulkload:
  "rbt_lookup (rbt_bulkload xs) = map_of xs"
proof -
  obtain ys where "ys = rev xs" by simp
  have "\t. is_rbt t \
    rbt_lookup (List.fold (case_prod rbt_insert) ys t) = rbt_lookup t ++ map_of (rev ys)"
      by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert case_prod_beta)
  from this Empty_is_rbt have
    "rbt_lookup (List.fold (case_prod rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs"
     by (simp add: \<open>ys = rev xs\<close>)
  then show ?thesis by (simp add: rbt_bulkload_def rbt_lookup_Empty foldr_conv_fold)
qed

end

subsection \<open>Building a RBT from a sorted list\<close>

text \<open>
  These functions have been adapted from
  Andrew W. Appel, Efficient Verified Red-Black Trees (September 2011)
\<close>

fun rbtreeify_f :: "nat \ ('a \ 'b) list \ ('a, 'b) rbt \ ('a \ 'b) list"
  and rbtreeify_g :: "nat \ ('a \ 'b) list \ ('a, 'b) rbt \ ('a \ 'b) list"
where
  "rbtreeify_f n kvs =
   (if n = 0 then (Empty, kvs)
    else if n = 1 then
      case kvs of (k, v) # kvs' \ (Branch R Empty k v Empty, kvs')
    else if (n mod 2 = 0) then
      case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \
        apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs')
    else case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \
        apfst (Branch B t1 k v) (rbtreeify_f (n div 2) kvs'))"

| "rbtreeify_g n kvs =
   (if n = 0 \<or> n = 1 then (Empty, kvs)
    else if n mod 2 = 0 then
      case rbtreeify_g (n div 2) kvs of (t1, (k, v) # kvs') \
        apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs')
    else case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \
        apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs'))"

definition rbtreeify :: "('a \ 'b) list \ ('a, 'b) rbt"
where "rbtreeify kvs = fst (rbtreeify_g (Suc (length kvs)) kvs)"

declare rbtreeify_f.simps [simp del] rbtreeify_g.simps [simp del]

lemma rbtreeify_f_code [code]:
  "rbtreeify_f n kvs =
   (if n = 0 then (Empty, kvs)
    else if n = 1 then
      case kvs of (k, v) # kvs' \
        (Branch R Empty k v Empty, kvs')
    else let (n', r) = Euclidean_Rings.divmod_nat n 2 in
      if r = 0 then
        case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
          apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
      else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
          apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
by (subst rbtreeify_f.simps) (simp only: Let_def Euclidean_Rings.divmod_nat_def prod.case)

lemma rbtreeify_g_code [code]:
  "rbtreeify_g n kvs =
   (if n = 0 \<or> n = 1 then (Empty, kvs)
    else let (n', r) = Euclidean_Rings.divmod_nat n 2 in
      if r = 0 then
        case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
          apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
      else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
          apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
by(subst rbtreeify_g.simps)(simp only: Let_def Euclidean_Rings.divmod_nat_def prod.case)

lemma Suc_double_half: "Suc (2 * n) div 2 = n"
by simp

lemma div2_plus_div2: "n div 2 + n div 2 = (n :: nat) - n mod 2"
by arith

lemma rbtreeify_f_rec_aux_lemma:
  "\k - n div 2 = Suc k'; n \ k; n mod 2 = Suc 0\
  \<Longrightarrow> k' - n div 2 = k - n"
apply(rule add_right_imp_eq[where a = "n - n div 2"])
apply(subst add_diff_assoc2, arith)
apply(simp add: div2_plus_div2)
done

lemma rbtreeify_f_simps:
  "rbtreeify_f 0 kvs = (Empty, kvs)"
  "rbtreeify_f (Suc 0) ((k, v) # kvs) =
  (Branch R Empty k v Empty, kvs)"
  "0 < n \ rbtreeify_f (2 * n) kvs =
   (case rbtreeify_f n kvs of (t1, (k, v) # kvs') \
     apfst (Branch B t1 k v) (rbtreeify_g n kvs'))"
  "0 < n \ rbtreeify_f (Suc (2 * n)) kvs =
   (case rbtreeify_f n kvs of (t1, (k, v) # kvs') \
     apfst (Branch B t1 k v) (rbtreeify_f n kvs'))"
by(subst (1) rbtreeify_f.simps, simp add: Suc_double_half)+

lemma rbtreeify_g_simps:
  "rbtreeify_g 0 kvs = (Empty, kvs)"
  "rbtreeify_g (Suc 0) kvs = (Empty, kvs)"
  "0 < n \ rbtreeify_g (2 * n) kvs =
   (case rbtreeify_g n kvs of (t1, (k, v) # kvs') \
     apfst (Branch B t1 k v) (rbtreeify_g n kvs'))"
  "0 < n \ rbtreeify_g (Suc (2 * n)) kvs =
   (case rbtreeify_f n kvs of (t1, (k, v) # kvs') \
     apfst (Branch B t1 k v) (rbtreeify_g n kvs'))"
by(subst (1) rbtreeify_g.simps, simp add: Suc_double_half)+

declare rbtreeify_f_simps[simp] rbtreeify_g_simps[simp]

lemma length_rbtreeify_f: "n \ length kvs
  \<Longrightarrow> length (snd (rbtreeify_f n kvs)) = length kvs - n"
  and length_rbtreeify_g:"\ 0 < n; n \ Suc (length kvs) \
  \<Longrightarrow> length (snd (rbtreeify_g n kvs)) = Suc (length kvs) - n"
proof(induction n kvs and n kvs rule: rbtreeify_f_rbtreeify_g.induct)
  case (1 n kvs)
  show ?case
  proof(cases "n \ 1")
    case True thus ?thesis using "1.prems"
      by(cases n kvs rule: nat.exhaust[case_product list.exhaust]) auto
  next
    case False
    hence "n \ 0" "n \ 1" by simp_all
    note IH = "1.IH"[OF this]
    show ?thesis
    proof(cases "n mod 2 = 0")
      case True
      hence "length (snd (rbtreeify_f n kvs)) =
        length (snd (rbtreeify_f (2 * (n div 2)) kvs))"
        by(metis minus_nat.diff_0 minus_mod_eq_mult_div [symmetric])
      also from "1.prems" False obtain k v kvs'
        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
      also have "0 < n div 2" using False by(simp)
      note rbtreeify_f_simps(3)[OF this]
      also note kvs[symmetric]
      also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
      from "1.prems" have "n div 2 \ length kvs" by simp
      with True have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
      with "1.prems" False obtain t1 k' v' kvs''
        where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
         by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
      note this also note prod.case also note list.simps(5)
      also note prod.case also note snd_apfst
      also have "0 < n div 2" "n div 2 \ Suc (length kvs'')"
        using len "1.prems" False unfolding kvs'' by simp_all
      with True kvs''[symmetric] refl refl
      have "length (snd (rbtreeify_g (n div 2) kvs'')) =
        Suc (length kvs'') - n div 2" by(rule IH)
      finally show ?thesis using len[unfolded kvs''] "1.prems" True
        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] minus_mod_eq_mult_div [symmetric])
    next
      case False
      hence "length (snd (rbtreeify_f n kvs)) =
        length (snd (rbtreeify_f (Suc (2 * (n div 2))) kvs))"
        by (simp add: mod_eq_0_iff_dvd)
      also from "1.prems" \<open>\<not> n \<le> 1\<close> obtain k v kvs'
        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
      also have "0 < n div 2" using \<open>\<not> n \<le> 1\<close> by(simp)
      note rbtreeify_f_simps(4)[OF this]
      also note kvs[symmetric]
      also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
      from "1.prems" have "n div 2 \ length kvs" by simp
      with False have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
      with "1.prems" \<open>\<not> n \<le> 1\<close> obtain t1 k' v' kvs''
        where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
        by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
      note this also note prod.case also note list.simps(5)
      also note prod.case also note snd_apfst
      also have "n div 2 \ length kvs''"
        using len "1.prems" False unfolding kvs'' by simp arith
      with False kvs''[symmetric] refl refl
      have "length (snd (rbtreeify_f (n div 2) kvs'')) = length kvs'' - n div 2"
        by(rule IH)
      finally show ?thesis using len[unfolded kvs''] "1.prems" False
        by simp(rule rbtreeify_f_rec_aux_lemma[OF sym])
    qed
  qed
next
  case (2 n kvs)
  show ?case
  proof(cases "n > 1")
    case False with \<open>0 < n\<close> show ?thesis
      by(cases n kvs rule: nat.exhaust[case_product list.exhaust]) simp_all
  next
    case True
    hence "\ (n = 0 \ n = 1)" by simp
    note IH = "2.IH"[OF this]
    show ?thesis
    proof(cases "n mod 2 = 0")
      case True
      hence "length (snd (rbtreeify_g n kvs)) =
        length (snd (rbtreeify_g (2 * (n div 2)) kvs))"
        by(metis minus_nat.diff_0 minus_mod_eq_mult_div [symmetric])
      also from "2.prems" True obtain k v kvs'
        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
      also have "0 < n div 2" using \<open>1 < n\<close> by(simp)
      note rbtreeify_g_simps(3)[OF this]
      also note kvs[symmetric]
      also let ?rest1 = "snd (rbtreeify_g (n div 2) kvs)"
      from "2.prems" \<open>1 < n\<close>
      have "0 < n div 2" "n div 2 \ Suc (length kvs)" by simp_all
      with True have len: "length ?rest1 = Suc (length kvs) - n div 2" by(rule IH)
      with "2.prems" obtain t1 k' v' kvs''
        where kvs'': "rbtreeify_g (n div 2) kvs = (t1, (k', v') # kvs'')"
        by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
      note this also note prod.case also note list.simps(5)
      also note prod.case also note snd_apfst
      also have "n div 2 \ Suc (length kvs'')"
        using len "2.prems" unfolding kvs'' by simp
      with True kvs''[symmetric] refl refl \<open>0 < n div 2\<close>
      have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
        by(rule IH)
      finally show ?thesis using len[unfolded kvs''] "2.prems" True
        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] minus_mod_eq_mult_div [symmetric])
    next
      case False
      hence "length (snd (rbtreeify_g n kvs)) =
        length (snd (rbtreeify_g (Suc (2 * (n div 2))) kvs))"
        by (simp add: mod_eq_0_iff_dvd)
      also from "2.prems" \<open>1 < n\<close> obtain k v kvs'
        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
      also have "0 < n div 2" using \<open>1 < n\<close> by(simp)
      note rbtreeify_g_simps(4)[OF this]
      also note kvs[symmetric]
      also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
      from "2.prems" have "n div 2 \ length kvs" by simp
      with False have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
      with "2.prems" \<open>1 < n\<close> False obtain t1 k' v' kvs''
        where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
        by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm, arith)
      note this also note prod.case also note list.simps(5)
      also note prod.case also note snd_apfst
      also have "n div 2 \ Suc (length kvs'')"
        using len "2.prems" False unfolding kvs'' by simp arith
      with False kvs''[symmetric] refl refl \<open>0 < n div 2\<close>
      have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
        by(rule IH)
      finally show ?thesis using len[unfolded kvs''] "2.prems" False
        by(simp add: div2_plus_div2)
    qed
  qed
qed

lemma rbtreeify_induct [consumes 1, case_names f_0 f_1 f_even f_odd g_0 g_1 g_even g_odd]:
  fixes P Q
  defines "f0 == (\kvs. P 0 kvs)"
  and "f1 == (\k v kvs. P (Suc 0) ((k, v) # kvs))"
  and "feven ==
    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> length kvs; P n kvs;
       rbtreeify_f n kvs = (t, (k, v) # kvs'); n \ Suc (length kvs'); Q n kvs' \
     \<Longrightarrow> P (2 * n) kvs)"
  and "fodd ==
    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> length kvs; P n kvs;
       rbtreeify_f n kvs = (t, (k, v) # kvs'); n \ length kvs'; P n kvs' \
    \<Longrightarrow> P (Suc (2 * n)) kvs)"
  and "g0 == (\kvs. Q 0 kvs)"
  and "g1 == (\kvs. Q (Suc 0) kvs)"
  and "geven ==
    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> Suc (length kvs); Q n kvs;
       rbtreeify_g n kvs = (t, (k, v) # kvs'); n \ Suc (length kvs'); Q n kvs' \
    \<Longrightarrow> Q (2 * n) kvs)"
  and "godd ==
    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> length kvs; P n kvs;
       rbtreeify_f n kvs = (t, (k, v) # kvs'); n \ Suc (length kvs'); Q n kvs' \
    \<Longrightarrow> Q (Suc (2 * n)) kvs)"
  shows "\ n \ length kvs;
           PROP f0; PROP f1; PROP feven; PROP fodd;
           PROP g0; PROP g1; PROP geven; PROP godd \<rbrakk>
         \<Longrightarrow> P n kvs"
  and "\ n \ Suc (length kvs);
          PROP f0; PROP f1; PROP feven; PROP fodd;
          PROP g0; PROP g1; PROP geven; PROP godd \<rbrakk>
       \<Longrightarrow> Q n kvs"
proof -
  assume f0: "PROP f0" and f1: "PROP f1" and feven: "PROP feven" and fodd: "PROP fodd"
    and g0: "PROP g0" and g1: "PROP g1" and geven: "PROP geven" and godd: "PROP godd"
  show "n \ length kvs \ P n kvs" and "n \ Suc (length kvs) \ Q n kvs"
  proof(induction rule: rbtreeify_f_rbtreeify_g.induct)
    case (1 n kvs)
    show ?case
    proof(cases "n \ 1")
      case True thus ?thesis using "1.prems"
        by(cases n kvs rule: nat.exhaust[case_product list.exhaust])
          (auto simp add: f0[unfolded f0_def] f1[unfolded f1_def])
    next
      case False
      hence ns: "n \ 0" "n \ 1" by simp_all
      hence ge0: "n div 2 > 0" by simp
      note IH = "1.IH"[OF ns]
      show ?thesis
      proof(cases "n mod 2 = 0")
        case True note ge0
        moreover from "1.prems" have n2: "n div 2 \ length kvs" by simp
        moreover from True n2 have "P (n div 2) kvs" by(rule IH)
        moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs'
          where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
          by(cases "snd (rbtreeify_f (n div 2) kvs)")
            (auto simp add: snd_def split: prod.split_asm)
        moreover from "1.prems" length_rbtreeify_f[OF n2] ge0
        have n2': "n div 2 \ Suc (length kvs')" by(simp add: kvs')
        moreover from True kvs'[symmetric] refl refl n2'
        have "Q (n div 2) kvs'" by(rule IH)
        moreover note feven[unfolded feven_def]
          (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *)
        ultimately have "P (2 * (n div 2)) kvs" by -
        thus ?thesis using True by (metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute)
      next
        case False note ge0
        moreover from "1.prems" have n2: "n div 2 \ length kvs" by simp
        moreover from False n2 have "P (n div 2) kvs" by(rule IH)
        moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs'
          where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
          by(cases "snd (rbtreeify_f (n div 2) kvs)")
            (auto simp add: snd_def split: prod.split_asm)
        moreover from "1.prems" length_rbtreeify_f[OF n2] ge0 False
        have n2': "n div 2 \ length kvs'" by(simp add: kvs') arith
        moreover from False kvs'[symmetric] refl refl n2' have "P (n div 2) kvs'" by(rule IH)
        moreover note fodd[unfolded fodd_def]
        ultimately have "P (Suc (2 * (n div 2))) kvs" by -
        thus ?thesis using False
          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend minus_mod_eq_mult_div [symmetric])
      qed
    qed
  next
    case (2 n kvs)
    show ?case
    proof(cases "n \ 1")
      case True thus ?thesis using "2.prems"
        by(cases n kvs rule: nat.exhaust[case_product list.exhaust])
          (auto simp add: g0[unfolded g0_def] g1[unfolded g1_def])
    next
      case False
      hence ns: "\ (n = 0 \ n = 1)" by simp
      hence ge0: "n div 2 > 0" by simp
      note IH = "2.IH"[OF ns]
      show ?thesis
      proof(cases "n mod 2 = 0")
        case True note ge0
--> --------------------

--> maximum size reached

--> --------------------

quality98%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.35Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.