haftmann@35617: (* Author: Florian Haftmann, TU Muenchen *) haftmann@35617: haftmann@36147: header {* Abstract type of Red-Black Trees *} haftmann@35617: haftmann@36147: (*<*) haftmann@36147: theory RBT bulwahn@43124: imports Main RBT_Impl haftmann@35617: begin haftmann@35617: haftmann@35617: subsection {* Type definition *} haftmann@35617: haftmann@36147: typedef (open) ('a, 'b) rbt = "{t :: ('a\linorder, 'b) RBT_Impl.rbt. is_rbt t}" haftmann@36147: morphisms impl_of RBT wenzelm@45694: proof wenzelm@45694: show "RBT_Impl.Empty \ {t. is_rbt t}" by simp haftmann@35617: qed haftmann@35617: haftmann@39380: lemma rbt_eq_iff: haftmann@39380: "t1 = t2 \ impl_of t1 = impl_of t2" haftmann@39380: by (simp add: impl_of_inject) haftmann@39380: haftmann@39380: lemma rbt_eqI: haftmann@39380: "impl_of t1 = impl_of t2 \ t1 = t2" haftmann@39380: by (simp add: rbt_eq_iff) haftmann@39380: haftmann@36147: lemma is_rbt_impl_of [simp, intro]: haftmann@36147: "is_rbt (impl_of t)" haftmann@36147: using impl_of [of t] by simp haftmann@35617: haftmann@39380: lemma RBT_impl_of [simp, code abstype]: haftmann@36147: "RBT (impl_of t) = t" haftmann@36147: by (simp add: impl_of_inverse) haftmann@35617: haftmann@35617: haftmann@35617: subsection {* Primitive operations *} haftmann@35617: haftmann@36147: definition lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" where haftmann@36147: [code]: "lookup t = RBT_Impl.lookup (impl_of t)" haftmann@35617: haftmann@36147: definition empty :: "('a\linorder, 'b) rbt" where haftmann@36147: "empty = RBT RBT_Impl.Empty" haftmann@35617: haftmann@36147: lemma impl_of_empty [code abstract]: haftmann@36147: "impl_of empty = RBT_Impl.Empty" haftmann@36147: by (simp add: empty_def RBT_inverse) haftmann@35617: haftmann@36147: definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where haftmann@36147: "insert k v t = RBT (RBT_Impl.insert k v (impl_of t))" haftmann@35617: haftmann@36147: lemma impl_of_insert [code abstract]: haftmann@36147: "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)" haftmann@36147: by (simp add: insert_def RBT_inverse) haftmann@35617: haftmann@36147: definition delete :: "'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" where haftmann@36147: "delete k t = RBT (RBT_Impl.delete k (impl_of t))" haftmann@35617: haftmann@36147: lemma impl_of_delete [code abstract]: haftmann@36147: "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)" haftmann@36147: by (simp add: delete_def RBT_inverse) haftmann@35617: haftmann@36147: definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" where haftmann@36147: [code]: "entries t = RBT_Impl.entries (impl_of t)" haftmann@35617: haftmann@36147: definition keys :: "('a\linorder, 'b) rbt \ 'a list" where haftmann@36147: [code]: "keys t = RBT_Impl.keys (impl_of t)" haftmann@36111: haftmann@36147: definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" where haftmann@36147: "bulkload xs = RBT (RBT_Impl.bulkload xs)" haftmann@35617: haftmann@36147: lemma impl_of_bulkload [code abstract]: haftmann@36147: "impl_of (bulkload xs) = RBT_Impl.bulkload xs" haftmann@36147: by (simp add: bulkload_def RBT_inverse) haftmann@35617: haftmann@36147: definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" where haftmann@36147: "map_entry k f t = RBT (RBT_Impl.map_entry k f (impl_of t))" haftmann@35617: haftmann@36147: lemma impl_of_map_entry [code abstract]: haftmann@36147: "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)" haftmann@36147: by (simp add: map_entry_def RBT_inverse) haftmann@35617: haftmann@36147: definition map :: "('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" where haftmann@36147: "map f t = RBT (RBT_Impl.map f (impl_of t))" haftmann@35617: haftmann@36147: lemma impl_of_map [code abstract]: haftmann@36147: "impl_of (map f t) = RBT_Impl.map f (impl_of t)" haftmann@36147: by (simp add: map_def RBT_inverse) haftmann@35617: haftmann@36147: definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" where haftmann@36147: [code]: "fold f t = RBT_Impl.fold f (impl_of t)" haftmann@35617: haftmann@35617: haftmann@35617: subsection {* Derived operations *} haftmann@35617: haftmann@36147: definition is_empty :: "('a\linorder, 'b) rbt \ bool" where haftmann@36147: [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \ True | _ \ False)" haftmann@35617: haftmann@35617: haftmann@35617: subsection {* Abstract lookup properties *} haftmann@35617: haftmann@36147: lemma lookup_RBT: haftmann@36147: "is_rbt t \ lookup (RBT t) = RBT_Impl.lookup t" haftmann@36147: by (simp add: lookup_def RBT_inverse) haftmann@35617: haftmann@36147: lemma lookup_impl_of: haftmann@36147: "RBT_Impl.lookup (impl_of t) = lookup t" haftmann@35617: by (simp add: lookup_def) haftmann@35617: haftmann@36147: lemma entries_impl_of: haftmann@36147: "RBT_Impl.entries (impl_of t) = entries t" haftmann@35617: by (simp add: entries_def) haftmann@35617: haftmann@36147: lemma keys_impl_of: haftmann@36147: "RBT_Impl.keys (impl_of t) = keys t" haftmann@36111: by (simp add: keys_def) haftmann@36111: haftmann@35617: lemma lookup_empty [simp]: haftmann@35617: "lookup empty = Map.empty" nipkow@39302: by (simp add: empty_def lookup_RBT fun_eq_iff) haftmann@35617: haftmann@36147: lemma lookup_insert [simp]: haftmann@36147: "lookup (insert k v t) = (lookup t)(k \ v)" haftmann@36147: by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of) haftmann@35617: haftmann@35617: lemma lookup_delete [simp]: haftmann@35617: "lookup (delete k t) = (lookup t)(k := None)" haftmann@36147: by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq) haftmann@35617: haftmann@35617: lemma map_of_entries [simp]: haftmann@35617: "map_of (entries t) = lookup t" haftmann@36147: by (simp add: entries_def map_of_entries lookup_impl_of) haftmann@35617: haftmann@36111: lemma entries_lookup: haftmann@36111: "entries t1 = entries t2 \ lookup t1 = lookup t2" haftmann@36111: by (simp add: entries_def lookup_def entries_lookup) haftmann@36111: haftmann@35617: lemma lookup_bulkload [simp]: haftmann@35617: "lookup (bulkload xs) = map_of xs" haftmann@36147: by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload) haftmann@35617: haftmann@35617: lemma lookup_map_entry [simp]: haftmann@35617: "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))" haftmann@37027: by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of) haftmann@35617: haftmann@35617: lemma lookup_map [simp]: haftmann@35617: "lookup (map f t) k = Option.map (f k) (lookup t k)" haftmann@40612: by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of) haftmann@35617: haftmann@35617: lemma fold_fold: haftmann@46133: "fold f t = List.fold (prod_case f) (entries t)" nipkow@39302: by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of) haftmann@35617: haftmann@36111: lemma is_empty_empty [simp]: haftmann@36111: "is_empty t \ t = empty" haftmann@39380: by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split) haftmann@36111: haftmann@36111: lemma RBT_lookup_empty [simp]: (*FIXME*) haftmann@36147: "RBT_Impl.lookup t = Map.empty \ t = RBT_Impl.Empty" nipkow@39302: by (cases t) (auto simp add: fun_eq_iff) haftmann@36111: haftmann@36111: lemma lookup_empty_empty [simp]: haftmann@36111: "lookup t = Map.empty \ t = empty" haftmann@36147: by (cases t) (simp add: empty_def lookup_def RBT_inject RBT_inverse) haftmann@36111: haftmann@36111: lemma sorted_keys [iff]: haftmann@36111: "sorted (keys t)" haftmann@36147: by (simp add: keys_def RBT_Impl.keys_def sorted_entries) haftmann@36111: haftmann@36111: lemma distinct_keys [iff]: haftmann@36111: "distinct (keys t)" haftmann@36147: by (simp add: keys_def RBT_Impl.keys_def distinct_entries) haftmann@36111: bulwahn@45928: subsection {* Quickcheck generators *} bulwahn@45928: bulwahn@46565: quickcheck_generator rbt predicate: is_rbt constructors: empty, insert haftmann@36111: haftmann@35617: end