src/HOL/Library/RBT.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 61260 e6f03fae14d5
child 63194 0b7bdb75f451
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (*  Title:      HOL/Library/RBT.thy
     2     Author:     Lukas Bulwahn and Ondrej Kuncar
     3 *)
     4 
     5 section \<open>Abstract type of RBT trees\<close>
     6 
     7 theory RBT 
     8 imports Main RBT_Impl
     9 begin
    10 
    11 subsection \<open>Type definition\<close>
    12 
    13 typedef (overloaded) ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}"
    14   morphisms impl_of RBT
    15 proof -
    16   have "RBT_Impl.Empty \<in> ?rbt" by simp
    17   then show ?thesis ..
    18 qed
    19 
    20 lemma rbt_eq_iff:
    21   "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
    22   by (simp add: impl_of_inject)
    23 
    24 lemma rbt_eqI:
    25   "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
    26   by (simp add: rbt_eq_iff)
    27 
    28 lemma is_rbt_impl_of [simp, intro]:
    29   "is_rbt (impl_of t)"
    30   using impl_of [of t] by simp
    31 
    32 lemma RBT_impl_of [simp, code abstype]:
    33   "RBT (impl_of t) = t"
    34   by (simp add: impl_of_inverse)
    35 
    36 subsection \<open>Primitive operations\<close>
    37 
    38 setup_lifting type_definition_rbt
    39 
    40 lift_definition lookup :: "('a::linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" .
    41 
    42 lift_definition empty :: "('a::linorder, 'b) rbt" is RBT_Impl.Empty 
    43 by (simp add: empty_def)
    44 
    45 lift_definition insert :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_insert" 
    46 by simp
    47 
    48 lift_definition delete :: "'a::linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_delete" 
    49 by simp
    50 
    51 lift_definition entries :: "('a::linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries .
    52 
    53 lift_definition keys :: "('a::linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys .
    54 
    55 lift_definition bulkload :: "('a::linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload" ..
    56 
    57 lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
    58 by simp
    59 
    60 lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'c) rbt" is RBT_Impl.map
    61 by simp
    62 
    63 lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold .
    64 
    65 lift_definition union :: "('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_union"
    66 by (simp add: rbt_union_is_rbt)
    67 
    68 lift_definition foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
    69   is RBT_Impl.foldi .
    70 
    71 subsection \<open>Derived operations\<close>
    72 
    73 definition is_empty :: "('a::linorder, 'b) rbt \<Rightarrow> bool" where
    74   [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
    75 
    76 
    77 subsection \<open>Abstract lookup properties\<close>
    78 
    79 lemma lookup_RBT:
    80   "is_rbt t \<Longrightarrow> lookup (RBT t) = rbt_lookup t"
    81   by (simp add: lookup_def RBT_inverse)
    82 
    83 lemma lookup_impl_of:
    84   "rbt_lookup (impl_of t) = lookup t"
    85   by transfer (rule refl)
    86 
    87 lemma entries_impl_of:
    88   "RBT_Impl.entries (impl_of t) = entries t"
    89   by transfer (rule refl)
    90 
    91 lemma keys_impl_of:
    92   "RBT_Impl.keys (impl_of t) = keys t"
    93   by transfer (rule refl)
    94 
    95 lemma lookup_keys: 
    96   "dom (lookup t) = set (keys t)" 
    97   by transfer (simp add: rbt_lookup_keys)
    98 
    99 lemma lookup_empty [simp]:
   100   "lookup empty = Map.empty"
   101   by (simp add: empty_def lookup_RBT fun_eq_iff)
   102 
   103 lemma lookup_insert [simp]:
   104   "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
   105   by transfer (rule rbt_lookup_rbt_insert)
   106 
   107 lemma lookup_delete [simp]:
   108   "lookup (delete k t) = (lookup t)(k := None)"
   109   by transfer (simp add: rbt_lookup_rbt_delete restrict_complement_singleton_eq)
   110 
   111 lemma map_of_entries [simp]:
   112   "map_of (entries t) = lookup t"
   113   by transfer (simp add: map_of_entries)
   114 
   115 lemma entries_lookup:
   116   "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
   117   by transfer (simp add: entries_rbt_lookup)
   118 
   119 lemma lookup_bulkload [simp]:
   120   "lookup (bulkload xs) = map_of xs"
   121   by transfer (rule rbt_lookup_rbt_bulkload)
   122 
   123 lemma lookup_map_entry [simp]:
   124   "lookup (map_entry k f t) = (lookup t)(k := map_option f (lookup t k))"
   125   by transfer (rule rbt_lookup_rbt_map_entry)
   126 
   127 lemma lookup_map [simp]:
   128   "lookup (map f t) k = map_option (f k) (lookup t k)"
   129   by transfer (rule rbt_lookup_map)
   130 
   131 lemma fold_fold:
   132   "fold f t = List.fold (case_prod f) (entries t)"
   133   by transfer (rule RBT_Impl.fold_def)
   134 
   135 lemma impl_of_empty:
   136   "impl_of empty = RBT_Impl.Empty"
   137   by transfer (rule refl)
   138 
   139 lemma is_empty_empty [simp]:
   140   "is_empty t \<longleftrightarrow> t = empty"
   141   unfolding is_empty_def by transfer (simp split: rbt.split)
   142 
   143 lemma RBT_lookup_empty [simp]: (*FIXME*)
   144   "rbt_lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
   145   by (cases t) (auto simp add: fun_eq_iff)
   146 
   147 lemma lookup_empty_empty [simp]:
   148   "lookup t = Map.empty \<longleftrightarrow> t = empty"
   149   by transfer (rule RBT_lookup_empty)
   150 
   151 lemma sorted_keys [iff]:
   152   "sorted (keys t)"
   153   by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries)
   154 
   155 lemma distinct_keys [iff]:
   156   "distinct (keys t)"
   157   by transfer (simp add: RBT_Impl.keys_def distinct_entries)
   158 
   159 lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
   160   by transfer simp
   161 
   162 lemma lookup_union: "lookup (union s t) = lookup s ++ lookup t"
   163   by transfer (simp add: rbt_lookup_rbt_union)
   164 
   165 lemma lookup_in_tree: "(lookup t k = Some v) = ((k, v) \<in> set (entries t))"
   166   by transfer (simp add: rbt_lookup_in_tree)
   167 
   168 lemma keys_entries: "(k \<in> set (keys t)) = (\<exists>v. (k, v) \<in> set (entries t))"
   169   by transfer (simp add: keys_entries)
   170 
   171 lemma fold_def_alt:
   172   "fold f t = List.fold (case_prod f) (entries t)"
   173   by transfer (auto simp: RBT_Impl.fold_def)
   174 
   175 lemma distinct_entries: "distinct (List.map fst (entries t))"
   176   by transfer (simp add: distinct_entries)
   177 
   178 lemma non_empty_keys: "t \<noteq> empty \<Longrightarrow> keys t \<noteq> []"
   179   by transfer (simp add: non_empty_rbt_keys)
   180 
   181 lemma keys_def_alt:
   182   "keys t = List.map fst (entries t)"
   183   by transfer (simp add: RBT_Impl.keys_def)
   184 
   185 subsection \<open>Quickcheck generators\<close>
   186 
   187 quickcheck_generator rbt predicate: is_rbt constructors: empty, insert
   188 
   189 subsection \<open>Hide implementation details\<close>
   190 
   191 lifting_update rbt.lifting
   192 lifting_forget rbt.lifting
   193 
   194 hide_const (open) impl_of empty lookup keys entries bulkload delete map fold union insert map_entry foldi 
   195   is_empty
   196 hide_fact (open) empty_def lookup_def keys_def entries_def bulkload_def delete_def map_def fold_def 
   197   union_def insert_def map_entry_def foldi_def is_empty_def
   198 
   199 end