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