author | wenzelm |
Mon, 11 Jul 2016 10:43:27 +0200 | |
changeset 63433 | aa03b0487bf5 |
parent 63195 | f3f08c0d4aaf |
child 63462 | c1fe30f2bc32 |
permissions | -rw-r--r-- |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/AList_Mapping.thy |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
3 |
*) |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
4 |
|
60500 | 5 |
section \<open>Implementation of mappings with Association Lists\<close> |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
6 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
7 |
theory AList_Mapping |
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46171
diff
changeset
|
8 |
imports AList Mapping |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
9 |
begin |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
10 |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset
|
11 |
lift_definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" is map_of . |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
12 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
13 |
code_datatype Mapping |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
14 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
15 |
lemma lookup_Mapping [simp, code]: |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
16 |
"Mapping.lookup (Mapping xs) = map_of xs" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset
|
17 |
by transfer rule |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
18 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
19 |
lemma keys_Mapping [simp, code]: |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset
|
20 |
"Mapping.keys (Mapping xs) = set (map fst xs)" |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset
|
21 |
by transfer (simp add: dom_map_of_conv_image_fst) |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
22 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
23 |
lemma empty_Mapping [code]: |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
24 |
"Mapping.empty = Mapping []" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset
|
25 |
by transfer simp |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
26 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
27 |
lemma is_empty_Mapping [code]: |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
28 |
"Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset
|
29 |
by (case_tac xs) (simp_all add: is_empty_def null_def) |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
30 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
31 |
lemma update_Mapping [code]: |
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46171
diff
changeset
|
32 |
"Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset
|
33 |
by transfer (simp add: update_conv') |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
34 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
35 |
lemma delete_Mapping [code]: |
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46171
diff
changeset
|
36 |
"Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset
|
37 |
by transfer (simp add: delete_conv') |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
38 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
39 |
lemma ordered_keys_Mapping [code]: |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
40 |
"Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))" |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
41 |
by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
42 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
43 |
lemma size_Mapping [code]: |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
44 |
"Mapping.size (Mapping xs) = length (remdups (map fst xs))" |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
45 |
by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst) |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
46 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
47 |
lemma tabulate_Mapping [code]: |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
48 |
"Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset
|
49 |
by transfer (simp add: map_of_map_restrict) |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
50 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
51 |
lemma bulkload_Mapping [code]: |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
52 |
"Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset
|
53 |
by transfer (simp add: map_of_map_restrict fun_eq_iff) |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
54 |
|
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
55 |
lemma equal_Mapping [code]: |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
56 |
"HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow> |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
57 |
(let ks = map fst xs; ls = map fst ys |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
58 |
in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))" |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
59 |
proof - |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
60 |
have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
61 |
by (auto simp add: image_def intro!: bexI) |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49929
diff
changeset
|
62 |
show ?thesis apply transfer |
57850 | 63 |
by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux) |
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
64 |
qed |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
65 |
|
63194 | 66 |
lemma map_values_Mapping [code]: |
63195 | 67 |
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b" and xs :: "('c \<times> 'a) list" |
68 |
shows "Mapping.map_values f (Mapping xs) = Mapping (map (\<lambda>(x,y). (x, f x y)) xs)" |
|
63194 | 69 |
proof (transfer, rule ext, goal_cases) |
70 |
case (1 f xs x) |
|
71 |
thus ?case by (induction xs) auto |
|
72 |
qed |
|
73 |
||
63195 | 74 |
lemma combine_with_key_code [code]: |
75 |
"Mapping.combine_with_key f (Mapping xs) (Mapping ys) = |
|
76 |
Mapping.tabulate (remdups (map fst xs @ map fst ys)) |
|
77 |
(\<lambda>x. the (combine_options (f x) (map_of xs x) (map_of ys x)))" |
|
78 |
proof (transfer, rule ext, rule sym, goal_cases) |
|
79 |
case (1 f xs ys x) |
|
80 |
show ?case |
|
81 |
by (cases "map_of xs x"; cases "map_of ys x"; simp) |
|
82 |
(force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff |
|
83 |
dest: map_of_SomeD split: option.splits)+ |
|
84 |
qed |
|
85 |
||
63194 | 86 |
lemma combine_code [code]: |
87 |
"Mapping.combine f (Mapping xs) (Mapping ys) = |
|
88 |
Mapping.tabulate (remdups (map fst xs @ map fst ys)) |
|
89 |
(\<lambda>x. the (combine_options f (map_of xs x) (map_of ys x)))" |
|
90 |
proof (transfer, rule ext, rule sym, goal_cases) |
|
91 |
case (1 f xs ys x) |
|
92 |
show ?case |
|
93 |
by (cases "map_of xs x"; cases "map_of ys x"; simp) |
|
63195 | 94 |
(force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff |
63194 | 95 |
dest: map_of_SomeD split: option.splits)+ |
96 |
qed |
|
97 |
||
98 |
(* TODO: Move? *) |
|
99 |
lemma map_of_filter_distinct: |
|
100 |
assumes "distinct (map fst xs)" |
|
101 |
shows "map_of (filter P xs) x = |
|
102 |
(case map_of xs x of None \<Rightarrow> None | Some y \<Rightarrow> if P (x,y) then Some y else None)" |
|
103 |
using assms |
|
104 |
by (auto simp: map_of_eq_None_iff filter_map distinct_map_filter dest: map_of_SomeD |
|
105 |
simp del: map_of_eq_Some_iff intro!: map_of_is_SomeI split: option.splits) |
|
106 |
(* END TODO *) |
|
107 |
||
108 |
lemma filter_Mapping [code]: |
|
109 |
"Mapping.filter P (Mapping xs) = Mapping (filter (\<lambda>(k,v). P k v) (AList.clearjunk xs))" |
|
110 |
by (transfer, rule ext) |
|
111 |
(subst map_of_filter_distinct, simp_all add: map_of_clearjunk split: option.split) |
|
112 |
||
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
113 |
lemma [code nbe]: |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
114 |
"HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True" |
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset
|
115 |
by (fact equal_refl) |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
58881
diff
changeset
|
116 |
|
44913 | 117 |
end |