9 imports RBT Mapping |
9 imports RBT Mapping |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Implementation of mappings *} |
12 subsection {* Implementation of mappings *} |
13 |
13 |
14 lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is lookup . |
14 context includes rbt.lifting begin |
|
15 lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is RBT.lookup . |
|
16 end |
15 |
17 |
16 code_datatype Mapping |
18 code_datatype Mapping |
17 |
19 |
|
20 context includes rbt.lifting begin |
|
21 |
18 lemma lookup_Mapping [simp, code]: |
22 lemma lookup_Mapping [simp, code]: |
19 "Mapping.lookup (Mapping t) = lookup t" |
23 "Mapping.lookup (Mapping t) = RBT.lookup t" |
20 by (transfer fixing: t) rule |
24 by (transfer fixing: t) rule |
21 |
25 |
22 lemma empty_Mapping [code]: "Mapping.empty = Mapping empty" |
26 lemma empty_Mapping [code]: "Mapping.empty = Mapping RBT.empty" |
23 proof - |
27 proof - |
24 note RBT.empty.transfer[transfer_rule del] |
28 note RBT.empty.transfer[transfer_rule del] |
25 show ?thesis by transfer simp |
29 show ?thesis by transfer simp |
26 qed |
30 qed |
27 |
31 |
28 lemma is_empty_Mapping [code]: |
32 lemma is_empty_Mapping [code]: |
29 "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t" |
33 "Mapping.is_empty (Mapping t) \<longleftrightarrow> RBT.is_empty t" |
30 unfolding is_empty_def by (transfer fixing: t) simp |
34 unfolding is_empty_def by (transfer fixing: t) simp |
31 |
35 |
32 lemma insert_Mapping [code]: |
36 lemma insert_Mapping [code]: |
33 "Mapping.update k v (Mapping t) = Mapping (insert k v t)" |
37 "Mapping.update k v (Mapping t) = Mapping (RBT.insert k v t)" |
34 by (transfer fixing: t) simp |
38 by (transfer fixing: t) simp |
35 |
39 |
36 lemma delete_Mapping [code]: |
40 lemma delete_Mapping [code]: |
37 "Mapping.delete k (Mapping t) = Mapping (delete k t)" |
41 "Mapping.delete k (Mapping t) = Mapping (RBT.delete k t)" |
38 by (transfer fixing: t) simp |
42 by (transfer fixing: t) simp |
39 |
43 |
40 lemma map_entry_Mapping [code]: |
44 lemma map_entry_Mapping [code]: |
41 "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)" |
45 "Mapping.map_entry k f (Mapping t) = Mapping (RBT.map_entry k f t)" |
42 apply (transfer fixing: t) by (case_tac "lookup t k") auto |
46 apply (transfer fixing: t) by (case_tac "RBT.lookup t k") auto |
43 |
47 |
44 lemma keys_Mapping [code]: |
48 lemma keys_Mapping [code]: |
45 "Mapping.keys (Mapping t) = set (keys t)" |
49 "Mapping.keys (Mapping t) = set (RBT.keys t)" |
46 by (transfer fixing: t) (simp add: lookup_keys) |
50 by (transfer fixing: t) (simp add: lookup_keys) |
47 |
51 |
48 lemma ordered_keys_Mapping [code]: |
52 lemma ordered_keys_Mapping [code]: |
49 "Mapping.ordered_keys (Mapping t) = keys t" |
53 "Mapping.ordered_keys (Mapping t) = RBT.keys t" |
50 unfolding ordered_keys_def |
54 unfolding ordered_keys_def |
51 by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique) |
55 by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique) |
52 |
56 |
53 lemma Mapping_size_card_keys: (*FIXME*) |
57 lemma Mapping_size_card_keys: (*FIXME*) |
54 "Mapping.size m = card (Mapping.keys m)" |
58 "Mapping.size m = card (Mapping.keys m)" |
55 unfolding size_def by transfer simp |
59 unfolding size_def by transfer simp |
56 |
60 |
57 lemma size_Mapping [code]: |
61 lemma size_Mapping [code]: |
58 "Mapping.size (Mapping t) = length (keys t)" |
62 "Mapping.size (Mapping t) = length (RBT.keys t)" |
59 unfolding size_def |
63 unfolding size_def |
60 by (transfer fixing: t) (simp add: lookup_keys distinct_card) |
64 by (transfer fixing: t) (simp add: lookup_keys distinct_card) |
61 |
65 |
62 context |
66 context |
63 notes RBT.bulkload.transfer[transfer_rule del] |
67 notes RBT.bulkload.transfer[transfer_rule del] |
64 begin |
68 begin |
65 lemma tabulate_Mapping [code]: |
69 lemma tabulate_Mapping [code]: |
66 "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))" |
70 "Mapping.tabulate ks f = Mapping (RBT.bulkload (List.map (\<lambda>k. (k, f k)) ks))" |
67 by transfer (simp add: map_of_map_restrict) |
71 by transfer (simp add: map_of_map_restrict) |
68 |
72 |
69 lemma bulkload_Mapping [code]: |
73 lemma bulkload_Mapping [code]: |
70 "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))" |
74 "Mapping.bulkload vs = Mapping (RBT.bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))" |
71 by transfer (simp add: map_of_map_restrict fun_eq_iff) |
75 by transfer (simp add: map_of_map_restrict fun_eq_iff) |
72 end |
76 end |
73 |
77 |
74 lemma equal_Mapping [code]: |
78 lemma equal_Mapping [code]: |
75 "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2" |
79 "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> RBT.entries t1 = RBT.entries t2" |
76 by (transfer fixing: t1 t2) (simp add: entries_lookup) |
80 by (transfer fixing: t1 t2) (simp add: entries_lookup) |
77 |
81 |
78 lemma [code nbe]: |
82 lemma [code nbe]: |
79 "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True" |
83 "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True" |
80 by (fact equal_refl) |
84 by (fact equal_refl) |
81 |
85 |
82 |
86 end |
83 hide_const (open) impl_of lookup empty insert delete |
87 |
84 entries keys bulkload map_entry map fold |
|
85 (*>*) |
88 (*>*) |
86 |
89 |
87 text {* |
90 text {* |
88 This theory defines abstract red-black trees as an efficient |
91 This theory defines abstract red-black trees as an efficient |
89 representation of finite maps, backed by the implementation |
92 representation of finite maps, backed by the implementation |