added trees implementing mappings
authorhaftmann
Thu Jun 04 16:55:20 2009 +0200 (2009-06-04)
changeset 31459ae39b7b2a68a
parent 31458 b1cf26f2919b
child 31460 d97fa41cc600
added trees implementing mappings
src/HOL/IsaMakefile
src/HOL/Library/Mapping.thy
src/HOL/Library/Tree.thy
src/HOL/ex/Codegenerator_Candidates.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Jun 04 16:11:04 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jun 04 16:55:20 2009 +0200
     1.3 @@ -349,6 +349,7 @@
     1.4    Library/Preorder.thy \
     1.5    Library/Product_plus.thy \
     1.6    Library/Product_Vector.thy \
     1.7 +  Library/Tree.thy \
     1.8    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
     1.9    Library/reify_data.ML Library/reflection.ML \
    1.10    Library/LaTeXsugar.thy Library/OptionalSugar.thy
     2.1 --- a/src/HOL/Library/Mapping.thy	Thu Jun 04 16:11:04 2009 +0200
     2.2 +++ b/src/HOL/Library/Mapping.thy	Thu Jun 04 16:55:20 2009 +0200
     2.3 @@ -1,6 +1,4 @@
     2.4 -(*  Title:      HOL/Library/Mapping.thy
     2.5 -    Author:     Florian Haftmann, TU Muenchen
     2.6 -*)
     2.7 +(* Author: Florian Haftmann, TU Muenchen *)
     2.8  
     2.9  header {* An abstract view on maps for code generation. *}
    2.10  
    2.11 @@ -132,4 +130,23 @@
    2.12    by (rule sym)
    2.13      (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
    2.14  
    2.15 +
    2.16 +subsection {* Some technical code lemmas *}
    2.17 +
    2.18 +lemma [code]:
    2.19 +  "map_case f m = f (Mapping.lookup m)"
    2.20 +  by (cases m) simp
    2.21 +
    2.22 +lemma [code]:
    2.23 +  "map_rec f m = f (Mapping.lookup m)"
    2.24 +  by (cases m) simp
    2.25 +
    2.26 +lemma [code]:
    2.27 +  "Nat.size (m :: (_, _) map) = 0"
    2.28 +  by (cases m) simp
    2.29 +
    2.30 +lemma [code]:
    2.31 +  "map_size f g m = 0"
    2.32 +  by (cases m) simp
    2.33 +
    2.34  end
    2.35 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Tree.thy	Thu Jun 04 16:55:20 2009 +0200
     3.3 @@ -0,0 +1,142 @@
     3.4 +(* Author: Florian Haftmann, TU Muenchen *)
     3.5 +
     3.6 +header {* Trees implementing mappings. *}
     3.7 +
     3.8 +theory Tree
     3.9 +imports Mapping
    3.10 +begin
    3.11 +
    3.12 +subsection {* Type definition and operations *}
    3.13 +
    3.14 +datatype ('a, 'b) tree = Empty
    3.15 +  | Branch 'b 'a "('a, 'b) tree" "('a, 'b) tree"
    3.16 +
    3.17 +primrec lookup :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> 'a \<rightharpoonup> 'b" where
    3.18 +  "lookup Empty = (\<lambda>_. None)"
    3.19 +  | "lookup (Branch v k l r) = (\<lambda>k'. if k' = k then Some v
    3.20 +       else if k' \<le> k then lookup l k' else lookup r k')"
    3.21 +
    3.22 +primrec update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) tree \<Rightarrow> ('a, 'b) tree" where
    3.23 +  "update k v Empty = Branch v k Empty Empty"
    3.24 +  | "update k' v' (Branch v k l r) = (if k' = k then
    3.25 +      Branch v' k l r else if k' \<le> k
    3.26 +      then Branch v k (update k' v' l) r
    3.27 +      else Branch v k l (update k' v' r))"
    3.28 +
    3.29 +primrec keys :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> 'a list" where
    3.30 +  "keys Empty = []"
    3.31 +  | "keys (Branch _ k l r) = k # keys l @ keys r"
    3.32 +
    3.33 +definition size :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> nat" where
    3.34 +  "size t = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))"
    3.35 +
    3.36 +fun bulkload :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) tree" where
    3.37 +  [simp del]: "bulkload ks f = (case ks of [] \<Rightarrow> Empty | _ \<Rightarrow> let
    3.38 +     mid = length ks div 2;
    3.39 +     ys = take mid ks;
    3.40 +     x = ks ! mid;
    3.41 +     zs = drop (Suc mid) ks
    3.42 +   in Branch (f x) x (bulkload ys f) (bulkload zs f))"
    3.43 +
    3.44 +
    3.45 +subsection {* Properties *}
    3.46 +
    3.47 +lemma dom_lookup:
    3.48 +  "dom (Tree.lookup t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
    3.49 +proof -
    3.50 +  have "dom (Tree.lookup t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (keys t))"
    3.51 +  by (induct t) (auto simp add: dom_if)
    3.52 +  also have "\<dots> = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
    3.53 +    by simp
    3.54 +  finally show ?thesis .
    3.55 +qed
    3.56 +
    3.57 +lemma lookup_finite:
    3.58 +  "finite (dom (lookup t))"
    3.59 +  unfolding dom_lookup by simp
    3.60 +
    3.61 +lemma lookup_update:
    3.62 +  "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
    3.63 +  by (induct t) (simp_all add: expand_fun_eq)
    3.64 +
    3.65 +lemma lookup_bulkload:
    3.66 +  "sorted ks \<Longrightarrow> lookup (bulkload ks f) = (Some o f) |` set ks"
    3.67 +proof (induct ks f rule: bulkload.induct)
    3.68 +  case (1 ks f) show ?case proof (cases ks)
    3.69 +    case Nil then show ?thesis by (simp add: bulkload.simps)
    3.70 +  next
    3.71 +    case (Cons w ws)
    3.72 +    then have case_simp: "\<And>w v::('a, 'b) tree. (case ks of [] \<Rightarrow> v | _ \<Rightarrow> w) = w"
    3.73 +      by (cases ks) auto
    3.74 +    from Cons have "ks \<noteq> []" by simp
    3.75 +    then have "0 < length ks" by simp
    3.76 +    let ?mid = "length ks div 2"
    3.77 +    let ?ys = "take ?mid ks"
    3.78 +    let ?x = "ks ! ?mid"
    3.79 +    let ?zs = "drop (Suc ?mid) ks"
    3.80 +    from `ks \<noteq> []` have ks_split: "ks = ?ys @ [?x] @ ?zs"
    3.81 +      by (simp add: id_take_nth_drop)
    3.82 +    then have in_ks: "\<And>x. x \<in> set ks \<longleftrightarrow> x \<in> set (?ys @ [?x] @ ?zs)"
    3.83 +      by simp
    3.84 +    with ks_split have ys_x: "\<And>y. y \<in> set ?ys \<Longrightarrow> y \<le> ?x"
    3.85 +      and x_zs: "\<And>z. z \<in> set ?zs \<Longrightarrow> ?x \<le> z"
    3.86 +    using `sorted ks` sorted_append [of "?ys" "[?x] @ ?zs"] sorted_append [of "[?x]" "?zs"]
    3.87 +      by simp_all
    3.88 +    have ys: "lookup (bulkload ?ys f) = (Some o f) |` set ?ys"
    3.89 +      by (rule "1.hyps"(1)) (auto intro: Cons sorted_take `sorted ks`)
    3.90 +    have zs: "lookup (bulkload ?zs f) = (Some o f) |` set ?zs"
    3.91 +      by (rule "1.hyps"(2)) (auto intro: Cons sorted_drop `sorted ks`)
    3.92 +    show ?thesis using `0 < length ks`
    3.93 +      by (simp add: bulkload.simps)
    3.94 +        (auto simp add: restrict_map_def in_ks case_simp Let_def ys zs expand_fun_eq
    3.95 +           dest: in_set_takeD in_set_dropD ys_x x_zs)
    3.96 +  qed
    3.97 +qed
    3.98 +
    3.99 +
   3.100 +subsection {* Trees as mappings *}
   3.101 +
   3.102 +definition Tree :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> ('a, 'b) map" where
   3.103 +  "Tree t = Map (Tree.lookup t)"
   3.104 +
   3.105 +lemma [code, code del]:
   3.106 +  "(eq_class.eq :: (_, _) map \<Rightarrow> _) = eq_class.eq" ..
   3.107 +
   3.108 +lemma [code, code del]:
   3.109 +  "Mapping.delete k m = Mapping.delete k m" ..
   3.110 +
   3.111 +code_datatype Tree
   3.112 +
   3.113 +lemma empty_Tree [code]:
   3.114 +  "Mapping.empty = Tree Empty"
   3.115 +  by (simp add: Tree_def Mapping.empty_def)
   3.116 +
   3.117 +lemma lookup_Tree [code]:
   3.118 +  "Mapping.lookup (Tree t) = lookup t"
   3.119 +  by (simp add: Tree_def)
   3.120 +
   3.121 +lemma update_Tree [code]:
   3.122 +  "Mapping.update k v (Tree t) = Tree (update k v t)"
   3.123 +  by (simp add: Tree_def lookup_update)
   3.124 +
   3.125 +lemma keys_Tree [code]:
   3.126 +  "Mapping.keys (Tree t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
   3.127 +  by (simp add: Tree_def dom_lookup)
   3.128 +
   3.129 +lemma size_Tree [code]:
   3.130 +  "Mapping.size (Tree t) = size t"
   3.131 +proof -
   3.132 +  have "card (dom (Tree.lookup t)) = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))"
   3.133 +    unfolding dom_lookup by (subst distinct_card) (auto simp add: comp_def)
   3.134 +  then show ?thesis by (auto simp add: Tree_def Mapping.size_def size_def)
   3.135 +qed
   3.136 +
   3.137 +lemma tabulate_Tree [code]:
   3.138 +  "Mapping.tabulate ks f = Tree (bulkload (sort ks) f)"
   3.139 +proof -
   3.140 +  have "Mapping.lookup (Mapping.tabulate ks f) = Mapping.lookup (Tree (bulkload (sort ks) f))"
   3.141 +    by (simp add: lookup_Tree lookup_bulkload lookup_tabulate)
   3.142 +  then show ?thesis by (simp add: lookup_inject)
   3.143 +qed
   3.144 +
   3.145 +end
     4.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy	Thu Jun 04 16:11:04 2009 +0200
     4.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy	Thu Jun 04 16:55:20 2009 +0200
     4.3 @@ -18,6 +18,7 @@
     4.4    Primes
     4.5    Product_ord
     4.6    SetsAndFunctions
     4.7 +  Tree
     4.8    While_Combinator
     4.9    Word
    4.10    "~~/src/HOL/ex/Commutative_Ring_Complete"