a couple of additions to RBT formalization to allow us to implement RBT_Set
authorkuncar
Tue Jul 31 13:55:39 2012 +0200 (2012-07-31)
changeset 48621877df57629e3
parent 48620 fc9be489e2fb
child 48622 caaa1a02c650
a couple of additions to RBT formalization to allow us to implement RBT_Set
src/HOL/Library/RBT_Impl.thy
src/HOL/Quotient_Examples/Lift_RBT.thy
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Jul 31 13:55:39 2012 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Jul 31 13:55:39 2012 +0200
     1.3 @@ -62,6 +62,9 @@
     1.4    "k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))"
     1.5    by (auto intro: entry_in_tree_keys) (auto simp add: keys_def)
     1.6  
     1.7 +lemma non_empty_rbt_keys: 
     1.8 +  "t \<noteq> rbt.Empty \<Longrightarrow> keys t \<noteq> []"
     1.9 +  by (cases t) simp_all
    1.10  
    1.11  subsubsection {* Search tree properties *}
    1.12  
    1.13 @@ -121,6 +124,11 @@
    1.14    (force simp: sorted_append sorted_Cons rbt_ord_props 
    1.15        dest!: entry_in_tree_keys)+
    1.16  
    1.17 +lemma distinct_keys:
    1.18 +  "rbt_sorted t \<Longrightarrow> distinct (keys t)"
    1.19 +  by (simp add: distinct_entries keys_def)
    1.20 +
    1.21 +
    1.22  subsubsection {* Tree lookup *}
    1.23  
    1.24  primrec (in ord) rbt_lookup :: "('a, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
    1.25 @@ -1059,7 +1067,7 @@
    1.26      qed
    1.27    qed
    1.28  
    1.29 -  from Branch have is_rbt: "is_rbt (RBT_Impl.rbt_union (RBT_Impl.rbt_insert k v s) l)"
    1.30 +  from Branch have is_rbt: "is_rbt (rbt_union (rbt_insert k v s) l)"
    1.31      by (auto intro: rbt_union_is_rbt rbt_insert_is_rbt)
    1.32    with Branch have IHs:
    1.33      "rbt_lookup (rbt_union (rbt_union (rbt_insert k v s) l) r) = rbt_lookup (rbt_union (rbt_insert k v s) l) ++ rbt_lookup r"
    1.34 @@ -1148,6 +1156,20 @@
    1.35    "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
    1.36    by (simp_all add: fold_def fun_eq_iff)
    1.37  
    1.38 +(* fold with continuation predicate *)
    1.39 +
    1.40 +fun foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
    1.41 +  where
    1.42 +  "foldi c f Empty s = s" |
    1.43 +  "foldi c f (Branch col l k v r) s = (
    1.44 +    if (c s) then
    1.45 +      let s' = foldi c f l s in
    1.46 +        if (c s') then
    1.47 +          foldi c f r (f k v s')
    1.48 +        else s'
    1.49 +    else 
    1.50 +      s
    1.51 +  )"
    1.52  
    1.53  subsection {* Bulkloading a tree *}
    1.54  
     2.1 --- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Tue Jul 31 13:55:39 2012 +0200
     2.2 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Tue Jul 31 13:55:39 2012 +0200
     2.3 @@ -69,7 +69,13 @@
     2.4  lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold 
     2.5  by simp
     2.6  
     2.7 -export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML
     2.8 +lift_definition union :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_union"
     2.9 +by (simp add: rbt_union_is_rbt)
    2.10 +
    2.11 +lift_definition foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
    2.12 +  is RBT_Impl.foldi by simp
    2.13 +
    2.14 +export_code lookup empty insert delete entries keys bulkload map_entry map fold union foldi in SML
    2.15  
    2.16  subsection {* Derived operations *}
    2.17  
    2.18 @@ -155,5 +161,30 @@
    2.19    "distinct (keys t)"
    2.20    by transfer (simp add: RBT_Impl.keys_def distinct_entries)
    2.21  
    2.22 +lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
    2.23 +  by transfer simp
    2.24 +
    2.25 +lemma lookup_union: "lookup (union s t) = lookup s ++ lookup t"
    2.26 +  by transfer (simp add: rbt_lookup_rbt_union)
    2.27 +
    2.28 +lemma lookup_in_tree: "(lookup t k = Some v) = ((k, v) \<in> set (entries t))"
    2.29 +  by transfer (simp add: rbt_lookup_in_tree)
    2.30 +
    2.31 +lemma keys_entries: "(k \<in> set (keys t)) = (\<exists>v. (k, v) \<in> set (entries t))"
    2.32 +  by transfer (simp add: keys_entries)
    2.33 +
    2.34 +lemma fold_def_alt:
    2.35 +  "fold f t = List.fold (prod_case f) (entries t)"
    2.36 +  by transfer (auto simp: RBT_Impl.fold_def)
    2.37 +
    2.38 +lemma distinct_entries: "distinct (List.map fst (entries t))"
    2.39 +  by transfer (simp add: distinct_entries)
    2.40 +
    2.41 +lemma non_empty_keys: "t \<noteq> Lift_RBT.empty \<Longrightarrow> keys t \<noteq> []"
    2.42 +  by transfer (simp add: non_empty_rbt_keys)
    2.43 +
    2.44 +lemma keys_def_alt:
    2.45 +  "keys t = List.map fst (entries t)"
    2.46 +  by transfer (simp add: RBT_Impl.keys_def)
    2.47  
    2.48  end
    2.49 \ No newline at end of file