some lemma refinements
authorhaftmann
Sat Mar 06 15:31:30 2010 +0100 (2010-03-06)
changeset 35618b7bfd4cbcfc0
parent 35617 a6528fb99641
child 35619 b5f6481772f3
some lemma refinements
src/HOL/Library/RBT.thy
     1.1 --- a/src/HOL/Library/RBT.thy	Sat Mar 06 15:31:30 2010 +0100
     1.2 +++ b/src/HOL/Library/RBT.thy	Sat Mar 06 15:31:30 2010 +0100
     1.3 @@ -151,8 +151,8 @@
     1.4  lemma lookup_Empty: "lookup Empty = empty"
     1.5  by (rule ext) simp
     1.6  
     1.7 -lemma lookup_map_of_entries:
     1.8 -  "sorted t \<Longrightarrow> lookup t = map_of (entries t)"
     1.9 +lemma map_of_entries:
    1.10 +  "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
    1.11  proof (induct t)
    1.12    case Empty thus ?case by (simp add: lookup_Empty)
    1.13  next
    1.14 @@ -213,11 +213,11 @@
    1.15      } ultimately show ?thesis using less_linear by blast
    1.16    qed
    1.17    also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
    1.18 -  finally show ?case .
    1.19 +  finally show ?case by simp
    1.20  qed
    1.21  
    1.22  lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
    1.23 -  by (simp_all add: lookup_map_of_entries distinct_entries)
    1.24 +  by (simp add: map_of_entries [symmetric] distinct_entries)
    1.25  
    1.26  lemma set_entries_inject:
    1.27    assumes sorted: "sorted t1" "sorted t2" 
    1.28 @@ -236,7 +236,7 @@
    1.29    shows "entries t1 = entries t2"
    1.30  proof -
    1.31    from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
    1.32 -    by (simp add: lookup_map_of_entries)
    1.33 +    by (simp add: map_of_entries)
    1.34    with sorted have "set (entries t1) = set (entries t2)"
    1.35      by (simp add: map_of_inject_set distinct_entries)
    1.36    with sorted show ?thesis by (simp add: set_entries_inject)
    1.37 @@ -245,7 +245,7 @@
    1.38  lemma entries_lookup:
    1.39    assumes "sorted t1" "sorted t2" 
    1.40    shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
    1.41 -  using assms by (auto intro: entries_eqI simp add: lookup_map_of_entries)
    1.42 +  using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric])
    1.43  
    1.44  lemma lookup_from_in_tree: 
    1.45    assumes "sorted t1" "sorted t2" 
    1.46 @@ -1013,11 +1013,9 @@
    1.47  theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t" 
    1.48  unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
    1.49  
    1.50 -theorem map_entry_map [simp]:
    1.51 -  "lookup (map_entry k f t) x = 
    1.52 -  (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
    1.53 -            else lookup t x)"
    1.54 -  by (induct t arbitrary: x) (auto split:option.splits)
    1.55 +theorem lookup_map_entry:
    1.56 +  "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
    1.57 +  by (induct t) (auto split: option.splits simp add: expand_fun_eq)
    1.58  
    1.59  
    1.60  subsection {* Mapping all entries *}
    1.61 @@ -1040,8 +1038,8 @@
    1.62  theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t" 
    1.63  unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
    1.64  
    1.65 -theorem lookup_map [simp]: "lookup (map f t) x = Option.map (f x) (lookup t x)"
    1.66 -by (induct t) auto
    1.67 +theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)"
    1.68 +  by (induct t) auto
    1.69  
    1.70  
    1.71  subsection {* Folding over entries *}
    1.72 @@ -1057,7 +1055,7 @@
    1.73  
    1.74  subsection {* Bulkloading a tree *}
    1.75  
    1.76 -definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where (*FIXME move*)
    1.77 +definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where
    1.78    "bulkload xs = foldr (\<lambda>(k, v). RBT.insert k v) xs RBT.Empty"
    1.79  
    1.80  lemma bulkload_is_rbt [simp, intro]: