src/HOL/Library/Tree.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 31459 ae39b7b2a68a
child 35158 63d0ed5a027c
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
haftmann@31459
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@31459
     2
haftmann@31459
     3
header {* Trees implementing mappings. *}
haftmann@31459
     4
haftmann@31459
     5
theory Tree
haftmann@31459
     6
imports Mapping
haftmann@31459
     7
begin
haftmann@31459
     8
haftmann@31459
     9
subsection {* Type definition and operations *}
haftmann@31459
    10
haftmann@31459
    11
datatype ('a, 'b) tree = Empty
haftmann@31459
    12
  | Branch 'b 'a "('a, 'b) tree" "('a, 'b) tree"
haftmann@31459
    13
haftmann@31459
    14
primrec lookup :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> 'a \<rightharpoonup> 'b" where
haftmann@31459
    15
  "lookup Empty = (\<lambda>_. None)"
haftmann@31459
    16
  | "lookup (Branch v k l r) = (\<lambda>k'. if k' = k then Some v
haftmann@31459
    17
       else if k' \<le> k then lookup l k' else lookup r k')"
haftmann@31459
    18
haftmann@31459
    19
primrec update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) tree \<Rightarrow> ('a, 'b) tree" where
haftmann@31459
    20
  "update k v Empty = Branch v k Empty Empty"
haftmann@31459
    21
  | "update k' v' (Branch v k l r) = (if k' = k then
haftmann@31459
    22
      Branch v' k l r else if k' \<le> k
haftmann@31459
    23
      then Branch v k (update k' v' l) r
haftmann@31459
    24
      else Branch v k l (update k' v' r))"
haftmann@31459
    25
haftmann@31459
    26
primrec keys :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> 'a list" where
haftmann@31459
    27
  "keys Empty = []"
haftmann@31459
    28
  | "keys (Branch _ k l r) = k # keys l @ keys r"
haftmann@31459
    29
haftmann@31459
    30
definition size :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> nat" where
haftmann@31459
    31
  "size t = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))"
haftmann@31459
    32
haftmann@31459
    33
fun bulkload :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) tree" where
haftmann@31459
    34
  [simp del]: "bulkload ks f = (case ks of [] \<Rightarrow> Empty | _ \<Rightarrow> let
haftmann@31459
    35
     mid = length ks div 2;
haftmann@31459
    36
     ys = take mid ks;
haftmann@31459
    37
     x = ks ! mid;
haftmann@31459
    38
     zs = drop (Suc mid) ks
haftmann@31459
    39
   in Branch (f x) x (bulkload ys f) (bulkload zs f))"
haftmann@31459
    40
haftmann@31459
    41
haftmann@31459
    42
subsection {* Properties *}
haftmann@31459
    43
haftmann@31459
    44
lemma dom_lookup:
haftmann@31459
    45
  "dom (Tree.lookup t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
haftmann@31459
    46
proof -
haftmann@31459
    47
  have "dom (Tree.lookup t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (keys t))"
haftmann@31459
    48
  by (induct t) (auto simp add: dom_if)
haftmann@31459
    49
  also have "\<dots> = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
haftmann@31459
    50
    by simp
haftmann@31459
    51
  finally show ?thesis .
haftmann@31459
    52
qed
haftmann@31459
    53
haftmann@31459
    54
lemma lookup_finite:
haftmann@31459
    55
  "finite (dom (lookup t))"
haftmann@31459
    56
  unfolding dom_lookup by simp
haftmann@31459
    57
haftmann@31459
    58
lemma lookup_update:
haftmann@31459
    59
  "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
haftmann@31459
    60
  by (induct t) (simp_all add: expand_fun_eq)
haftmann@31459
    61
haftmann@31459
    62
lemma lookup_bulkload:
haftmann@31459
    63
  "sorted ks \<Longrightarrow> lookup (bulkload ks f) = (Some o f) |` set ks"
haftmann@31459
    64
proof (induct ks f rule: bulkload.induct)
haftmann@31459
    65
  case (1 ks f) show ?case proof (cases ks)
haftmann@31459
    66
    case Nil then show ?thesis by (simp add: bulkload.simps)
haftmann@31459
    67
  next
haftmann@31459
    68
    case (Cons w ws)
haftmann@31459
    69
    then have case_simp: "\<And>w v::('a, 'b) tree. (case ks of [] \<Rightarrow> v | _ \<Rightarrow> w) = w"
haftmann@31459
    70
      by (cases ks) auto
haftmann@31459
    71
    from Cons have "ks \<noteq> []" by simp
haftmann@31459
    72
    then have "0 < length ks" by simp
haftmann@31459
    73
    let ?mid = "length ks div 2"
haftmann@31459
    74
    let ?ys = "take ?mid ks"
haftmann@31459
    75
    let ?x = "ks ! ?mid"
haftmann@31459
    76
    let ?zs = "drop (Suc ?mid) ks"
haftmann@31459
    77
    from `ks \<noteq> []` have ks_split: "ks = ?ys @ [?x] @ ?zs"
haftmann@31459
    78
      by (simp add: id_take_nth_drop)
haftmann@31459
    79
    then have in_ks: "\<And>x. x \<in> set ks \<longleftrightarrow> x \<in> set (?ys @ [?x] @ ?zs)"
haftmann@31459
    80
      by simp
haftmann@31459
    81
    with ks_split have ys_x: "\<And>y. y \<in> set ?ys \<Longrightarrow> y \<le> ?x"
haftmann@31459
    82
      and x_zs: "\<And>z. z \<in> set ?zs \<Longrightarrow> ?x \<le> z"
haftmann@31459
    83
    using `sorted ks` sorted_append [of "?ys" "[?x] @ ?zs"] sorted_append [of "[?x]" "?zs"]
haftmann@31459
    84
      by simp_all
haftmann@31459
    85
    have ys: "lookup (bulkload ?ys f) = (Some o f) |` set ?ys"
haftmann@31459
    86
      by (rule "1.hyps"(1)) (auto intro: Cons sorted_take `sorted ks`)
haftmann@31459
    87
    have zs: "lookup (bulkload ?zs f) = (Some o f) |` set ?zs"
haftmann@31459
    88
      by (rule "1.hyps"(2)) (auto intro: Cons sorted_drop `sorted ks`)
haftmann@31459
    89
    show ?thesis using `0 < length ks`
haftmann@31459
    90
      by (simp add: bulkload.simps)
haftmann@31459
    91
        (auto simp add: restrict_map_def in_ks case_simp Let_def ys zs expand_fun_eq
haftmann@31459
    92
           dest: in_set_takeD in_set_dropD ys_x x_zs)
haftmann@31459
    93
  qed
haftmann@31459
    94
qed
haftmann@31459
    95
haftmann@31459
    96
haftmann@31459
    97
subsection {* Trees as mappings *}
haftmann@31459
    98
haftmann@31459
    99
definition Tree :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> ('a, 'b) map" where
haftmann@31459
   100
  "Tree t = Map (Tree.lookup t)"
haftmann@31459
   101
haftmann@31459
   102
lemma [code, code del]:
haftmann@31459
   103
  "(eq_class.eq :: (_, _) map \<Rightarrow> _) = eq_class.eq" ..
haftmann@31459
   104
haftmann@31459
   105
lemma [code, code del]:
haftmann@31459
   106
  "Mapping.delete k m = Mapping.delete k m" ..
haftmann@31459
   107
haftmann@31459
   108
code_datatype Tree
haftmann@31459
   109
haftmann@31459
   110
lemma empty_Tree [code]:
haftmann@31459
   111
  "Mapping.empty = Tree Empty"
haftmann@31459
   112
  by (simp add: Tree_def Mapping.empty_def)
haftmann@31459
   113
haftmann@31459
   114
lemma lookup_Tree [code]:
haftmann@31459
   115
  "Mapping.lookup (Tree t) = lookup t"
haftmann@31459
   116
  by (simp add: Tree_def)
haftmann@31459
   117
haftmann@31459
   118
lemma update_Tree [code]:
haftmann@31459
   119
  "Mapping.update k v (Tree t) = Tree (update k v t)"
haftmann@31459
   120
  by (simp add: Tree_def lookup_update)
haftmann@31459
   121
haftmann@31459
   122
lemma keys_Tree [code]:
haftmann@31459
   123
  "Mapping.keys (Tree t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
haftmann@31459
   124
  by (simp add: Tree_def dom_lookup)
haftmann@31459
   125
haftmann@31459
   126
lemma size_Tree [code]:
haftmann@31459
   127
  "Mapping.size (Tree t) = size t"
haftmann@31459
   128
proof -
haftmann@31459
   129
  have "card (dom (Tree.lookup t)) = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))"
haftmann@31459
   130
    unfolding dom_lookup by (subst distinct_card) (auto simp add: comp_def)
haftmann@31459
   131
  then show ?thesis by (auto simp add: Tree_def Mapping.size_def size_def)
haftmann@31459
   132
qed
haftmann@31459
   133
haftmann@31459
   134
lemma tabulate_Tree [code]:
haftmann@31459
   135
  "Mapping.tabulate ks f = Tree (bulkload (sort ks) f)"
haftmann@31459
   136
proof -
haftmann@31459
   137
  have "Mapping.lookup (Mapping.tabulate ks f) = Mapping.lookup (Tree (bulkload (sort ks) f))"
haftmann@31459
   138
    by (simp add: lookup_Tree lookup_bulkload lookup_tabulate)
haftmann@31459
   139
  then show ?thesis by (simp add: lookup_inject)
haftmann@31459
   140
qed
haftmann@31459
   141
haftmann@31459
   142
end