merged
authorhaftmann
Sat Mar 06 20:16:31 2010 +0100 (2010-03-06)
changeset 356207415cd106942
parent 35616 b342390d296f
parent 35619 b5f6481772f3
child 35623 b0de8551fadf
merged
     1.1 --- a/src/HOL/IsaMakefile	Sat Mar 06 17:53:04 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Sat Mar 06 20:16:31 2010 +0100
     1.3 @@ -401,7 +401,7 @@
     1.4    Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML		\
     1.5    Library/Library/document/root.tex Library/Library/document/root.bib	\
     1.6    Library/Transitive_Closure_Table.thy Library/While_Combinator.thy	\
     1.7 -  Library/Product_ord.thy Library/Char_nat.thy				\
     1.8 +  Library/Product_ord.thy Library/Char_nat.thy Library/Table.thy	\
     1.9    Library/Sublist_Order.thy Library/List_lexord.thy			\
    1.10    Library/Coinductive_List.thy Library/AssocList.thy			\
    1.11    Library/Formal_Power_Series.thy Library/Binomial.thy			\
     2.1 --- a/src/HOL/Library/Library.thy	Sat Mar 06 17:53:04 2010 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Sat Mar 06 20:16:31 2010 +0100
     2.3 @@ -58,6 +58,7 @@
     2.4    SML_Quickcheck
     2.5    State_Monad
     2.6    Sum_Of_Squares
     2.7 +  Table
     2.8    Transitive_Closure_Table
     2.9    Univ_Poly
    2.10    While_Combinator
     3.1 --- a/src/HOL/Library/RBT.thy	Sat Mar 06 17:53:04 2010 +0100
     3.2 +++ b/src/HOL/Library/RBT.thy	Sat Mar 06 20:16:31 2010 +0100
     3.3 @@ -151,8 +151,8 @@
     3.4  lemma lookup_Empty: "lookup Empty = empty"
     3.5  by (rule ext) simp
     3.6  
     3.7 -lemma lookup_map_of_entries:
     3.8 -  "sorted t \<Longrightarrow> lookup t = map_of (entries t)"
     3.9 +lemma map_of_entries:
    3.10 +  "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
    3.11  proof (induct t)
    3.12    case Empty thus ?case by (simp add: lookup_Empty)
    3.13  next
    3.14 @@ -213,11 +213,11 @@
    3.15      } ultimately show ?thesis using less_linear by blast
    3.16    qed
    3.17    also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
    3.18 -  finally show ?case .
    3.19 +  finally show ?case by simp
    3.20  qed
    3.21  
    3.22  lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
    3.23 -  by (simp_all add: lookup_map_of_entries distinct_entries)
    3.24 +  by (simp add: map_of_entries [symmetric] distinct_entries)
    3.25  
    3.26  lemma set_entries_inject:
    3.27    assumes sorted: "sorted t1" "sorted t2" 
    3.28 @@ -236,7 +236,7 @@
    3.29    shows "entries t1 = entries t2"
    3.30  proof -
    3.31    from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
    3.32 -    by (simp add: lookup_map_of_entries)
    3.33 +    by (simp add: map_of_entries)
    3.34    with sorted have "set (entries t1) = set (entries t2)"
    3.35      by (simp add: map_of_inject_set distinct_entries)
    3.36    with sorted show ?thesis by (simp add: set_entries_inject)
    3.37 @@ -245,7 +245,7 @@
    3.38  lemma entries_lookup:
    3.39    assumes "sorted t1" "sorted t2" 
    3.40    shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
    3.41 -  using assms by (auto intro: entries_eqI simp add: lookup_map_of_entries)
    3.42 +  using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric])
    3.43  
    3.44  lemma lookup_from_in_tree: 
    3.45    assumes "sorted t1" "sorted t2" 
    3.46 @@ -1013,11 +1013,9 @@
    3.47  theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t" 
    3.48  unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
    3.49  
    3.50 -theorem map_entry_map [simp]:
    3.51 -  "lookup (map_entry k f t) x = 
    3.52 -  (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
    3.53 -            else lookup t x)"
    3.54 -  by (induct t arbitrary: x) (auto split:option.splits)
    3.55 +theorem lookup_map_entry:
    3.56 +  "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
    3.57 +  by (induct t) (auto split: option.splits simp add: expand_fun_eq)
    3.58  
    3.59  
    3.60  subsection {* Mapping all entries *}
    3.61 @@ -1040,8 +1038,8 @@
    3.62  theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t" 
    3.63  unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
    3.64  
    3.65 -theorem lookup_map [simp]: "lookup (map f t) x = Option.map (f x) (lookup t x)"
    3.66 -by (induct t) auto
    3.67 +theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)"
    3.68 +  by (induct t) auto
    3.69  
    3.70  
    3.71  subsection {* Folding over entries *}
    3.72 @@ -1057,7 +1055,7 @@
    3.73  
    3.74  subsection {* Bulkloading a tree *}
    3.75  
    3.76 -definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where (*FIXME move*)
    3.77 +definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where
    3.78    "bulkload xs = foldr (\<lambda>(k, v). RBT.insert k v) xs RBT.Empty"
    3.79  
    3.80  lemma bulkload_is_rbt [simp, intro]:
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Table.thy	Sat Mar 06 20:16:31 2010 +0100
     4.3 @@ -0,0 +1,139 @@
     4.4 +(* Author: Florian Haftmann, TU Muenchen *)
     4.5 +
     4.6 +header {* Tables: finite mappings implemented by red-black trees *}
     4.7 +
     4.8 +theory Table
     4.9 +imports Main RBT
    4.10 +begin
    4.11 +
    4.12 +subsection {* Type definition *}
    4.13 +
    4.14 +typedef (open) ('a, 'b) table = "{t :: ('a\<Colon>linorder, 'b) rbt. is_rbt t}"
    4.15 +  morphisms tree_of Table
    4.16 +proof -
    4.17 +  have "RBT.Empty \<in> ?table" by simp
    4.18 +  then show ?thesis ..
    4.19 +qed
    4.20 +
    4.21 +lemma is_rbt_tree_of [simp, intro]:
    4.22 +  "is_rbt (tree_of t)"
    4.23 +  using tree_of [of t] by simp
    4.24 +
    4.25 +lemma table_eq:
    4.26 +  "t1 = t2 \<longleftrightarrow> tree_of t1 = tree_of t2"
    4.27 +  by (simp add: tree_of_inject)
    4.28 +
    4.29 +code_abstype Table tree_of
    4.30 +  by (simp add: tree_of_inverse)
    4.31 +
    4.32 +
    4.33 +subsection {* Primitive operations *}
    4.34 +
    4.35 +definition lookup :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a \<rightharpoonup> 'b" where
    4.36 +  [code]: "lookup t = RBT.lookup (tree_of t)"
    4.37 +
    4.38 +definition empty :: "('a\<Colon>linorder, 'b) table" where
    4.39 +  "empty = Table RBT.Empty"
    4.40 +
    4.41 +lemma tree_of_empty [code abstract]:
    4.42 +  "tree_of empty = RBT.Empty"
    4.43 +  by (simp add: empty_def Table_inverse)
    4.44 +
    4.45 +definition update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
    4.46 +  "update k v t = Table (RBT.insert k v (tree_of t))"
    4.47 +
    4.48 +lemma tree_of_update [code abstract]:
    4.49 +  "tree_of (update k v t) = RBT.insert k v (tree_of t)"
    4.50 +  by (simp add: update_def Table_inverse)
    4.51 +
    4.52 +definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
    4.53 +  "delete k t = Table (RBT.delete k (tree_of t))"
    4.54 +
    4.55 +lemma tree_of_delete [code abstract]:
    4.56 +  "tree_of (delete k t) = RBT.delete k (tree_of t)"
    4.57 +  by (simp add: delete_def Table_inverse)
    4.58 +
    4.59 +definition entries :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a \<times> 'b) list" where
    4.60 +  [code]: "entries t = RBT.entries (tree_of t)"
    4.61 +
    4.62 +definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) table" where
    4.63 +  "bulkload xs = Table (RBT.bulkload xs)"
    4.64 +
    4.65 +lemma tree_of_bulkload [code abstract]:
    4.66 +  "tree_of (bulkload xs) = RBT.bulkload xs"
    4.67 +  by (simp add: bulkload_def Table_inverse)
    4.68 +
    4.69 +definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
    4.70 +  "map_entry k f t = Table (RBT.map_entry k f (tree_of t))"
    4.71 +
    4.72 +lemma tree_of_map_entry [code abstract]:
    4.73 +  "tree_of (map_entry k f t) = RBT.map_entry k f (tree_of t)"
    4.74 +  by (simp add: map_entry_def Table_inverse)
    4.75 +
    4.76 +definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
    4.77 +  "map f t = Table (RBT.map f (tree_of t))"
    4.78 +
    4.79 +lemma tree_of_map [code abstract]:
    4.80 +  "tree_of (map f t) = RBT.map f (tree_of t)"
    4.81 +  by (simp add: map_def Table_inverse)
    4.82 +
    4.83 +definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> 'c \<Rightarrow> 'c" where
    4.84 +  [code]: "fold f t = RBT.fold f (tree_of t)"
    4.85 +
    4.86 +
    4.87 +subsection {* Derived operations *}
    4.88 +
    4.89 +definition is_empty :: "('a\<Colon>linorder, 'b) table \<Rightarrow> bool" where
    4.90 +  [code]: "is_empty t = (case tree_of t of RBT.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
    4.91 +
    4.92 +
    4.93 +subsection {* Abstract lookup properties *}
    4.94 +
    4.95 +lemma lookup_Table:
    4.96 +  "is_rbt t \<Longrightarrow> lookup (Table t) = RBT.lookup t"
    4.97 +  by (simp add: lookup_def Table_inverse)
    4.98 +
    4.99 +lemma lookup_tree_of:
   4.100 +  "RBT.lookup (tree_of t) = lookup t"
   4.101 +  by (simp add: lookup_def)
   4.102 +
   4.103 +lemma entries_tree_of:
   4.104 +  "RBT.entries (tree_of t) = entries t"
   4.105 +  by (simp add: entries_def)
   4.106 +
   4.107 +lemma lookup_empty [simp]:
   4.108 +  "lookup empty = Map.empty"
   4.109 +  by (simp add: empty_def lookup_Table expand_fun_eq)
   4.110 +
   4.111 +lemma lookup_update [simp]:
   4.112 +  "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
   4.113 +  by (simp add: update_def lookup_Table lookup_insert lookup_tree_of)
   4.114 +
   4.115 +lemma lookup_delete [simp]:
   4.116 +  "lookup (delete k t) = (lookup t)(k := None)"
   4.117 +  by (simp add: delete_def lookup_Table lookup_delete lookup_tree_of restrict_complement_singleton_eq)
   4.118 +
   4.119 +lemma map_of_entries [simp]:
   4.120 +  "map_of (entries t) = lookup t"
   4.121 +  by (simp add: entries_def map_of_entries lookup_tree_of)
   4.122 +
   4.123 +lemma lookup_bulkload [simp]:
   4.124 +  "lookup (bulkload xs) = map_of xs"
   4.125 +  by (simp add: bulkload_def lookup_Table lookup_bulkload)
   4.126 +
   4.127 +lemma lookup_map_entry [simp]:
   4.128 +  "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
   4.129 +  by (simp add: map_entry_def lookup_Table lookup_map_entry lookup_tree_of)
   4.130 +
   4.131 +lemma lookup_map [simp]:
   4.132 +  "lookup (map f t) k = Option.map (f k) (lookup t k)"
   4.133 +  by (simp add: map_def lookup_Table lookup_map lookup_tree_of)
   4.134 +
   4.135 +lemma fold_fold:
   4.136 +  "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
   4.137 +  by (simp add: fold_def expand_fun_eq RBT.fold_def entries_tree_of)
   4.138 +
   4.139 +hide (open) const tree_of lookup empty update delete
   4.140 +  entries bulkload map_entry map fold
   4.141 +
   4.142 +end
     5.1 --- a/src/HOL/Map.thy	Sat Mar 06 17:53:04 2010 +0100
     5.2 +++ b/src/HOL/Map.thy	Sat Mar 06 20:16:31 2010 +0100
     5.3 @@ -398,6 +398,10 @@
     5.4    "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
     5.5    by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
     5.6  
     5.7 +lemma restrict_complement_singleton_eq:
     5.8 +  "f |` (- {x}) = f(x := None)"
     5.9 +  by (simp add: restrict_map_def expand_fun_eq)
    5.10 +
    5.11  
    5.12  subsection {* @{term [source] map_upds} *}
    5.13  
    5.14 @@ -707,4 +711,3 @@
    5.15  qed
    5.16  
    5.17  end
    5.18 -
     6.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy	Sat Mar 06 17:53:04 2010 +0100
     6.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy	Sat Mar 06 20:16:31 2010 +0100
     6.3 @@ -21,6 +21,7 @@
     6.4    Product_ord
     6.5    "~~/src/HOL/ex/Records"
     6.6    SetsAndFunctions
     6.7 +  Table
     6.8    Tree
     6.9    While_Combinator
    6.10    Word