author | nipkow |
Thu, 01 Aug 2024 14:07:34 +0200 | |
changeset 80629 | 06350a8745c9 |
parent 74157 | 8e2355ddce1b |
permissions | -rw-r--r-- |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
1 |
(* Title: HOL/Library/Mapping.thy |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
2 |
Author: Florian Haftmann and Ondrej Kuncar |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
3 |
*) |
29708 | 4 |
|
60500 | 5 |
section \<open>An abstract view on maps for code generation.\<close> |
29708 | 6 |
|
7 |
theory Mapping |
|
73832 | 8 |
imports Main AList |
29708 | 9 |
begin |
10 |
||
60500 | 11 |
subsection \<open>Parametricity transfer rules\<close> |
51379 | 12 |
|
63462 | 13 |
lemma map_of_foldr: "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty" (* FIXME move *) |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
14 |
using map_add_map_of_foldr [of Map.empty] by auto |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
15 |
|
63343 | 16 |
context includes lifting_syntax |
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
51379
diff
changeset
|
17 |
begin |
56528 | 18 |
|
63462 | 19 |
lemma empty_parametric: "(A ===> rel_option B) Map.empty Map.empty" |
56528 | 20 |
by transfer_prover |
51379 | 21 |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
22 |
lemma lookup_parametric: "((A ===> B) ===> A ===> B) (\<lambda>m k. m k) (\<lambda>m k. m k)" |
56528 | 23 |
by transfer_prover |
51379 | 24 |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
25 |
lemma update_parametric: |
51379 | 26 |
assumes [transfer_rule]: "bi_unique A" |
56528 | 27 |
shows "(A ===> B ===> (A ===> rel_option B) ===> A ===> rel_option B) |
28 |
(\<lambda>k v m. m(k \<mapsto> v)) (\<lambda>k v m. m(k \<mapsto> v))" |
|
29 |
by transfer_prover |
|
51379 | 30 |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
31 |
lemma delete_parametric: |
51379 | 32 |
assumes [transfer_rule]: "bi_unique A" |
63462 | 33 |
shows "(A ===> (A ===> rel_option B) ===> A ===> rel_option B) |
56528 | 34 |
(\<lambda>k m. m(k := None)) (\<lambda>k m. m(k := None))" |
35 |
by transfer_prover |
|
51379 | 36 |
|
56528 | 37 |
lemma is_none_parametric [transfer_rule]: |
38 |
"(rel_option A ===> HOL.eq) Option.is_none Option.is_none" |
|
61068 | 39 |
by (auto simp add: Option.is_none_def rel_fun_def rel_option_iff split: option.split) |
51379 | 40 |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
41 |
lemma dom_parametric: |
51379 | 42 |
assumes [transfer_rule]: "bi_total A" |
63462 | 43 |
shows "((A ===> rel_option B) ===> rel_set A) dom dom" |
61068 | 44 |
unfolding dom_def [abs_def] Option.is_none_def [symmetric] by transfer_prover |
51379 | 45 |
|
73832 | 46 |
lemma graph_parametric: |
47 |
assumes "bi_total A" |
|
48 |
shows "((A ===> rel_option B) ===> rel_set (rel_prod A B)) Map.graph Map.graph" |
|
49 |
proof |
|
50 |
fix f g assume "(A ===> rel_option B) f g" |
|
51 |
with assms[unfolded bi_total_def] show "rel_set (rel_prod A B) (Map.graph f) (Map.graph g)" |
|
52 |
unfolding graph_def rel_set_def rel_fun_def |
|
53 |
by auto (metis option_rel_Some1 option_rel_Some2)+ |
|
54 |
qed |
|
55 |
||
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
56 |
lemma map_of_parametric [transfer_rule]: |
51379 | 57 |
assumes [transfer_rule]: "bi_unique R1" |
55944 | 58 |
shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of" |
56528 | 59 |
unfolding map_of_def by transfer_prover |
51379 | 60 |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
61 |
lemma map_entry_parametric [transfer_rule]: |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
62 |
assumes [transfer_rule]: "bi_unique A" |
63462 | 63 |
shows "(A ===> (B ===> B) ===> (A ===> rel_option B) ===> A ===> rel_option B) |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
64 |
(\<lambda>k f m. (case m k of None \<Rightarrow> m |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
65 |
| Some v \<Rightarrow> m (k \<mapsto> (f v)))) (\<lambda>k f m. (case m k of None \<Rightarrow> m |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
66 |
| Some v \<Rightarrow> m (k \<mapsto> (f v))))" |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
67 |
by transfer_prover |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
68 |
|
63462 | 69 |
lemma tabulate_parametric: |
51379 | 70 |
assumes [transfer_rule]: "bi_unique A" |
63462 | 71 |
shows "(list_all2 A ===> (A ===> B) ===> A ===> rel_option B) |
56528 | 72 |
(\<lambda>ks f. (map_of (map (\<lambda>k. (k, f k)) ks))) (\<lambda>ks f. (map_of (map (\<lambda>k. (k, f k)) ks)))" |
73 |
by transfer_prover |
|
51379 | 74 |
|
63462 | 75 |
lemma bulkload_parametric: |
76 |
"(list_all2 A ===> HOL.eq ===> rel_option A) |
|
77 |
(\<lambda>xs k. if k < length xs then Some (xs ! k) else None) |
|
78 |
(\<lambda>xs k. if k < length xs then Some (xs ! k) else None)" |
|
56528 | 79 |
proof |
80 |
fix xs ys |
|
81 |
assume "list_all2 A xs ys" |
|
63462 | 82 |
then show |
83 |
"(HOL.eq ===> rel_option A) |
|
84 |
(\<lambda>k. if k < length xs then Some (xs ! k) else None) |
|
85 |
(\<lambda>k. if k < length ys then Some (ys ! k) else None)" |
|
56528 | 86 |
apply induct |
63476 | 87 |
apply auto |
56528 | 88 |
unfolding rel_fun_def |
63462 | 89 |
apply clarsimp |
90 |
apply (case_tac xa) |
|
63476 | 91 |
apply (auto dest: list_all2_lengthD list_all2_nthD) |
56528 | 92 |
done |
93 |
qed |
|
51379 | 94 |
|
63462 | 95 |
lemma map_parametric: |
96 |
"((A ===> B) ===> (C ===> D) ===> (B ===> rel_option C) ===> A ===> rel_option D) |
|
56528 | 97 |
(\<lambda>f g m. (map_option g \<circ> m \<circ> f)) (\<lambda>f g m. (map_option g \<circ> m \<circ> f))" |
98 |
by transfer_prover |
|
63462 | 99 |
|
100 |
lemma combine_with_key_parametric: |
|
101 |
"((A ===> B ===> B ===> B) ===> (A ===> rel_option B) ===> (A ===> rel_option B) ===> |
|
102 |
(A ===> rel_option B)) (\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x)) |
|
103 |
(\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x))" |
|
63194 | 104 |
unfolding combine_options_def by transfer_prover |
63462 | 105 |
|
106 |
lemma combine_parametric: |
|
107 |
"((B ===> B ===> B) ===> (A ===> rel_option B) ===> (A ===> rel_option B) ===> |
|
108 |
(A ===> rel_option B)) (\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x)) |
|
109 |
(\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x))" |
|
63194 | 110 |
unfolding combine_options_def by transfer_prover |
51379 | 111 |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
112 |
end |
51379 | 113 |
|
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
51379
diff
changeset
|
114 |
|
60500 | 115 |
subsection \<open>Type definition and primitive operations\<close> |
29708 | 116 |
|
49834 | 117 |
typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set" |
63462 | 118 |
morphisms rep Mapping .. |
37700
bd90378b8171
refrain from using datatype declaration -- opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset
|
119 |
|
59485 | 120 |
setup_lifting type_definition_mapping |
37700
bd90378b8171
refrain from using datatype declaration -- opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset
|
121 |
|
56528 | 122 |
lift_definition empty :: "('a, 'b) mapping" |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
123 |
is Map.empty parametric empty_parametric . |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
124 |
|
56528 | 125 |
lift_definition lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<Rightarrow> 'b option" |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
126 |
is "\<lambda>m k. m k" parametric lookup_parametric . |
56528 | 127 |
|
63194 | 128 |
definition "lookup_default d m k = (case Mapping.lookup m k of None \<Rightarrow> d | Some v \<Rightarrow> v)" |
129 |
||
56528 | 130 |
lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
131 |
is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric . |
37700
bd90378b8171
refrain from using datatype declaration -- opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset
|
132 |
|
56528 | 133 |
lift_definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
134 |
is "\<lambda>k m. m(k := None)" parametric delete_parametric . |
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
135 |
|
63194 | 136 |
lift_definition filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
63462 | 137 |
is "\<lambda>P m k. case m k of None \<Rightarrow> None | Some v \<Rightarrow> if P k v then Some v else None" . |
63194 | 138 |
|
56528 | 139 |
lift_definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
140 |
is dom parametric dom_parametric . |
29708 | 141 |
|
73832 | 142 |
lift_definition entries :: "('a, 'b) mapping \<Rightarrow> ('a \<times> 'b) set" |
143 |
is Map.graph parametric graph_parametric . |
|
144 |
||
56528 | 145 |
lift_definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
146 |
is "\<lambda>ks f. (map_of (List.map (\<lambda>k. (k, f k)) ks))" parametric tabulate_parametric . |
29708 | 147 |
|
56528 | 148 |
lift_definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
149 |
is "\<lambda>xs k. if k < length xs then Some (xs ! k) else None" parametric bulkload_parametric . |
29708 | 150 |
|
56528 | 151 |
lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
152 |
is "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_parametric . |
63462 | 153 |
|
63194 | 154 |
lift_definition map_values :: "('c \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('c, 'a) mapping \<Rightarrow> ('c, 'b) mapping" |
63462 | 155 |
is "\<lambda>f m x. map_option (f x) (m x)" . |
63194 | 156 |
|
63462 | 157 |
lift_definition combine_with_key :: |
63194 | 158 |
"('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping" |
159 |
is "\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x)" parametric combine_with_key_parametric . |
|
160 |
||
63462 | 161 |
lift_definition combine :: |
63194 | 162 |
"('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping" |
163 |
is "\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x)" parametric combine_parametric . |
|
164 |
||
63462 | 165 |
definition "All_mapping m P \<longleftrightarrow> |
166 |
(\<forall>x. case Mapping.lookup m x of None \<Rightarrow> True | Some y \<Rightarrow> P x y)" |
|
29708 | 167 |
|
59485 | 168 |
declare [[code drop: map]] |
169 |
||
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
170 |
|
60500 | 171 |
subsection \<open>Functorial structure\<close> |
40605 | 172 |
|
55467
a5c9002bc54d
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
blanchet
parents:
55466
diff
changeset
|
173 |
functor map: map |
55466 | 174 |
by (transfer, auto simp add: fun_eq_iff option.map_comp option.map_id)+ |
40605 | 175 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
176 |
|
60500 | 177 |
subsection \<open>Derived operations\<close> |
29708 | 178 |
|
61076 | 179 |
definition ordered_keys :: "('a::linorder, 'b) mapping \<Rightarrow> 'a list" |
63462 | 180 |
where "ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])" |
35194 | 181 |
|
73832 | 182 |
definition ordered_entries :: "('a::linorder, 'b) mapping \<Rightarrow> ('a \<times> 'b) list" |
183 |
where "ordered_entries m = (if finite (entries m) then sorted_key_list_of_set fst (entries m) |
|
184 |
else [])" |
|
185 |
||
186 |
definition fold :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> 'c \<Rightarrow> 'c" |
|
187 |
where "fold f m a = List.fold (case_prod f) (ordered_entries m) a" |
|
188 |
||
56528 | 189 |
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" |
63462 | 190 |
where "is_empty m \<longleftrightarrow> keys m = {}" |
35157 | 191 |
|
56528 | 192 |
definition size :: "('a, 'b) mapping \<Rightarrow> nat" |
63462 | 193 |
where "size m = (if finite (keys m) then card (keys m) else 0)" |
35157 | 194 |
|
56528 | 195 |
definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
63462 | 196 |
where "replace k v m = (if k \<in> keys m then update k v m else m)" |
29814 | 197 |
|
56528 | 198 |
definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
63462 | 199 |
where "default k v m = (if k \<in> keys m then m else update k v m)" |
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset
|
200 |
|
60500 | 201 |
text \<open>Manual derivation of transfer rule is non-trivial\<close> |
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
202 |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
203 |
lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" is |
63462 | 204 |
"\<lambda>k f m. |
205 |
(case m k of |
|
206 |
None \<Rightarrow> m |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
207 |
| Some v \<Rightarrow> m (k \<mapsto> (f v)))" parametric map_entry_parametric . |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
208 |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
209 |
lemma map_entry_code [code]: |
63462 | 210 |
"map_entry k f m = |
211 |
(case lookup m k of |
|
212 |
None \<Rightarrow> m |
|
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
49973
diff
changeset
|
213 |
| Some v \<Rightarrow> update k (f v) m)" |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
49973
diff
changeset
|
214 |
by transfer rule |
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset
|
215 |
|
56528 | 216 |
definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
63462 | 217 |
where "map_default k v f m = map_entry k f (default k v m)" |
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset
|
218 |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
219 |
definition of_alist :: "('k \<times> 'v) list \<Rightarrow> ('k, 'v) mapping" |
63462 | 220 |
where "of_alist xs = foldr (\<lambda>(k, v) m. update k v m) xs empty" |
51379 | 221 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
222 |
instantiation mapping :: (type, type) equal |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
223 |
begin |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
224 |
|
63462 | 225 |
definition "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)" |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
226 |
|
60679 | 227 |
instance |
63462 | 228 |
apply standard |
229 |
unfolding equal_mapping_def |
|
230 |
apply transfer |
|
231 |
apply auto |
|
232 |
done |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
233 |
|
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
234 |
end |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
235 |
|
63343 | 236 |
context includes lifting_syntax |
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
51379
diff
changeset
|
237 |
begin |
56528 | 238 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
239 |
lemma [transfer_rule]: |
51379 | 240 |
assumes [transfer_rule]: "bi_total A" |
63462 | 241 |
and [transfer_rule]: "bi_unique B" |
67399 | 242 |
shows "(pcr_mapping A B ===> pcr_mapping A B ===> (=)) HOL.eq HOL.equal" |
63462 | 243 |
unfolding equal by transfer_prover |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
244 |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
245 |
lemma of_alist_transfer [transfer_rule]: |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
246 |
assumes [transfer_rule]: "bi_unique R1" |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
247 |
shows "(list_all2 (rel_prod R1 R2) ===> pcr_mapping R1 R2) map_of of_alist" |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
248 |
unfolding of_alist_def [abs_def] map_of_foldr [abs_def] by transfer_prover |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
249 |
|
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
51379
diff
changeset
|
250 |
end |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset
|
251 |
|
56528 | 252 |
|
60500 | 253 |
subsection \<open>Properties\<close> |
29708 | 254 |
|
63462 | 255 |
lemma mapping_eqI: "(\<And>x. lookup m x = lookup m' x) \<Longrightarrow> m = m'" |
63195 | 256 |
by transfer (simp add: fun_eq_iff) |
257 |
||
63462 | 258 |
lemma mapping_eqI': |
259 |
assumes "\<And>x. x \<in> Mapping.keys m \<Longrightarrow> Mapping.lookup_default d m x = Mapping.lookup_default d m' x" |
|
260 |
and "Mapping.keys m = Mapping.keys m'" |
|
261 |
shows "m = m'" |
|
63195 | 262 |
proof (intro mapping_eqI) |
63462 | 263 |
show "Mapping.lookup m x = Mapping.lookup m' x" for x |
63195 | 264 |
proof (cases "Mapping.lookup m x") |
265 |
case None |
|
63462 | 266 |
then have "x \<notin> Mapping.keys m" |
267 |
by transfer (simp add: dom_def) |
|
268 |
then have "x \<notin> Mapping.keys m'" |
|
269 |
by (simp add: assms) |
|
270 |
then have "Mapping.lookup m' x = None" |
|
271 |
by transfer (simp add: dom_def) |
|
272 |
with None show ?thesis |
|
273 |
by simp |
|
63195 | 274 |
next |
275 |
case (Some y) |
|
63462 | 276 |
then have A: "x \<in> Mapping.keys m" |
277 |
by transfer (simp add: dom_def) |
|
278 |
then have "x \<in> Mapping.keys m'" |
|
279 |
by (simp add: assms) |
|
280 |
then have "\<exists>y'. Mapping.lookup m' x = Some y'" |
|
281 |
by transfer (simp add: dom_def) |
|
282 |
with Some assms(1)[OF A] show ?thesis |
|
283 |
by (auto simp add: lookup_default_def) |
|
63195 | 284 |
qed |
285 |
qed |
|
286 |
||
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
287 |
lemma lookup_update[simp]: "lookup (update k v m) k = Some v" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
288 |
by transfer simp |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
289 |
|
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
290 |
lemma lookup_update_neq[simp]: "k \<noteq> k' \<Longrightarrow> lookup (update k v m) k' = lookup m k'" |
49973 | 291 |
by transfer simp |
292 |
||
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
293 |
lemma lookup_update': "lookup (update k v m) k' = (if k = k' then Some v else lookup m k')" |
49973 | 294 |
by transfer simp |
295 |
||
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
296 |
lemma lookup_empty[simp]: "lookup empty k = None" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
297 |
by transfer simp |
63194 | 298 |
|
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
299 |
lemma lookup_delete[simp]: "lookup (delete k m) k = None" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
300 |
by transfer simp |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
301 |
|
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
302 |
lemma lookup_delete_neq[simp]: "k \<noteq> k' \<Longrightarrow> lookup (delete k m) k' = lookup m k'" |
49973 | 303 |
by transfer simp |
304 |
||
63194 | 305 |
lemma lookup_filter: |
63462 | 306 |
"lookup (filter P m) k = |
307 |
(case lookup m k of |
|
308 |
None \<Rightarrow> None |
|
309 |
| Some v \<Rightarrow> if P k v then Some v else None)" |
|
63194 | 310 |
by transfer simp_all |
311 |
||
63462 | 312 |
lemma lookup_map_values: "lookup (map_values f m) k = map_option (f k) (lookup m k)" |
63194 | 313 |
by transfer simp_all |
314 |
||
315 |
lemma lookup_default_empty: "lookup_default d empty k = d" |
|
316 |
by (simp add: lookup_default_def lookup_empty) |
|
317 |
||
63462 | 318 |
lemma lookup_default_update: "lookup_default d (update k v m) k = v" |
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
319 |
by (simp add: lookup_default_def) |
63194 | 320 |
|
321 |
lemma lookup_default_update_neq: |
|
63462 | 322 |
"k \<noteq> k' \<Longrightarrow> lookup_default d (update k v m) k' = lookup_default d m k'" |
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
323 |
by (simp add: lookup_default_def) |
63194 | 324 |
|
63462 | 325 |
lemma lookup_default_update': |
63194 | 326 |
"lookup_default d (update k v m) k' = (if k = k' then v else lookup_default d m k')" |
327 |
by (auto simp: lookup_default_update lookup_default_update_neq) |
|
328 |
||
329 |
lemma lookup_default_filter: |
|
63462 | 330 |
"lookup_default d (filter P m) k = |
63194 | 331 |
(if P k (lookup_default d m k) then lookup_default d m k else d)" |
332 |
by (simp add: lookup_default_def lookup_filter split: option.splits) |
|
333 |
||
334 |
lemma lookup_default_map_values: |
|
335 |
"lookup_default (f k d) (map_values f m) k = f k (lookup_default d m k)" |
|
63462 | 336 |
by (simp add: lookup_default_def lookup_map_values split: option.splits) |
63194 | 337 |
|
338 |
lemma lookup_combine_with_key: |
|
63462 | 339 |
"Mapping.lookup (combine_with_key f m1 m2) x = |
340 |
combine_options (f x) (Mapping.lookup m1 x) (Mapping.lookup m2 x)" |
|
63194 | 341 |
by transfer (auto split: option.splits) |
63462 | 342 |
|
63194 | 343 |
lemma combine_altdef: "combine f m1 m2 = combine_with_key (\<lambda>_. f) m1 m2" |
344 |
by transfer' (rule refl) |
|
345 |
||
346 |
lemma lookup_combine: |
|
63462 | 347 |
"Mapping.lookup (combine f m1 m2) x = |
63194 | 348 |
combine_options f (Mapping.lookup m1 x) (Mapping.lookup m2 x)" |
349 |
by transfer (auto split: option.splits) |
|
63462 | 350 |
|
351 |
lemma lookup_default_neutral_combine_with_key: |
|
63194 | 352 |
assumes "\<And>x. f k d x = x" "\<And>x. f k x d = x" |
63462 | 353 |
shows "Mapping.lookup_default d (combine_with_key f m1 m2) k = |
354 |
f k (Mapping.lookup_default d m1 k) (Mapping.lookup_default d m2 k)" |
|
63194 | 355 |
by (auto simp: lookup_default_def lookup_combine_with_key assms split: option.splits) |
63462 | 356 |
|
357 |
lemma lookup_default_neutral_combine: |
|
63194 | 358 |
assumes "\<And>x. f d x = x" "\<And>x. f x d = x" |
63462 | 359 |
shows "Mapping.lookup_default d (combine f m1 m2) x = |
360 |
f (Mapping.lookup_default d m1 x) (Mapping.lookup_default d m2 x)" |
|
63194 | 361 |
by (auto simp: lookup_default_def lookup_combine assms split: option.splits) |
362 |
||
63462 | 363 |
lemma lookup_map_entry: "lookup (map_entry x f m) x = map_option f (lookup m x)" |
63195 | 364 |
by transfer (auto split: option.splits) |
365 |
||
63462 | 366 |
lemma lookup_map_entry_neq: "x \<noteq> y \<Longrightarrow> lookup (map_entry x f m) y = lookup m y" |
63195 | 367 |
by transfer (auto split: option.splits) |
368 |
||
369 |
lemma lookup_map_entry': |
|
63462 | 370 |
"lookup (map_entry x f m) y = |
63195 | 371 |
(if x = y then map_option f (lookup m y) else lookup m y)" |
372 |
by transfer (auto split: option.splits) |
|
373 |
||
63462 | 374 |
lemma lookup_default: "lookup (default x d m) x = Some (lookup_default d m x)" |
375 |
unfolding lookup_default_def default_def |
|
376 |
by transfer (auto split: option.splits) |
|
377 |
||
378 |
lemma lookup_default_neq: "x \<noteq> y \<Longrightarrow> lookup (default x d m) y = lookup m y" |
|
379 |
unfolding lookup_default_def default_def |
|
380 |
by transfer (auto split: option.splits) |
|
63195 | 381 |
|
382 |
lemma lookup_default': |
|
63462 | 383 |
"lookup (default x d m) y = |
384 |
(if x = y then Some (lookup_default d m x) else lookup m y)" |
|
63195 | 385 |
unfolding lookup_default_def default_def |
386 |
by transfer (auto split: option.splits) |
|
387 |
||
63462 | 388 |
lemma lookup_map_default: "lookup (map_default x d f m) x = Some (f (lookup_default d m x))" |
389 |
unfolding lookup_default_def default_def |
|
390 |
by (simp add: map_default_def lookup_map_entry lookup_default lookup_default_def) |
|
391 |
||
392 |
lemma lookup_map_default_neq: "x \<noteq> y \<Longrightarrow> lookup (map_default x d f m) y = lookup m y" |
|
393 |
unfolding lookup_default_def default_def |
|
394 |
by (simp add: map_default_def lookup_map_entry_neq lookup_default_neq) |
|
63195 | 395 |
|
396 |
lemma lookup_map_default': |
|
63462 | 397 |
"lookup (map_default x d f m) y = |
398 |
(if x = y then Some (f (lookup_default d m x)) else lookup m y)" |
|
399 |
unfolding lookup_default_def default_def |
|
400 |
by (simp add: map_default_def lookup_map_entry' lookup_default' lookup_default_def) |
|
63195 | 401 |
|
63462 | 402 |
lemma lookup_tabulate: |
63194 | 403 |
assumes "distinct xs" |
63462 | 404 |
shows "Mapping.lookup (Mapping.tabulate xs f) x = (if x \<in> set xs then Some (f x) else None)" |
63194 | 405 |
using assms by transfer (auto simp: map_of_eq_None_iff o_def dest!: map_of_SomeD) |
406 |
||
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
407 |
lemma lookup_of_alist: "lookup (of_alist xs) k = map_of xs k" |
63194 | 408 |
by transfer simp_all |
409 |
||
63462 | 410 |
lemma keys_is_none_rep [code_unfold]: "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))" |
61068 | 411 |
by transfer (auto simp add: Option.is_none_def) |
29708 | 412 |
|
413 |
lemma update_update: |
|
414 |
"update k v (update k w m) = update k v m" |
|
415 |
"k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)" |
|
63462 | 416 |
by (transfer; simp add: fun_upd_twist)+ |
29708 | 417 |
|
63462 | 418 |
lemma update_delete [simp]: "update k v (delete k m) = update k v m" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
419 |
by transfer simp |
29708 | 420 |
|
421 |
lemma delete_update: |
|
422 |
"delete k (update k v m) = delete k m" |
|
423 |
"k \<noteq> l \<Longrightarrow> delete k (update l v m) = update l v (delete k m)" |
|
63462 | 424 |
by (transfer; simp add: fun_upd_twist)+ |
29708 | 425 |
|
63462 | 426 |
lemma delete_empty [simp]: "delete k empty = empty" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
427 |
by transfer simp |
29708 | 428 |
|
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
429 |
lemma Mapping_delete_if_notin_keys[simp]: |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
430 |
"k \<notin> keys m \<Longrightarrow> delete k m = m" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
431 |
by transfer simp |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
432 |
|
35157 | 433 |
lemma replace_update: |
37052 | 434 |
"k \<notin> keys m \<Longrightarrow> replace k v m = m" |
435 |
"k \<in> keys m \<Longrightarrow> replace k v m = update k v m" |
|
63462 | 436 |
by (transfer; auto simp add: replace_def fun_upd_twist)+ |
437 |
||
63194 | 438 |
lemma map_values_update: "map_values f (update k v m) = update k (f k v) (map_values f m)" |
439 |
by transfer (simp_all add: fun_eq_iff) |
|
63462 | 440 |
|
441 |
lemma size_mono: "finite (keys m') \<Longrightarrow> keys m \<subseteq> keys m' \<Longrightarrow> size m \<le> size m'" |
|
63194 | 442 |
unfolding size_def by (auto intro: card_mono) |
29708 | 443 |
|
63462 | 444 |
lemma size_empty [simp]: "size empty = 0" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
445 |
unfolding size_def by transfer simp |
29708 | 446 |
|
447 |
lemma size_update: |
|
37052 | 448 |
"finite (keys m) \<Longrightarrow> size (update k v m) = |
449 |
(if k \<in> keys m then size m else Suc (size m))" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
450 |
unfolding size_def by transfer (auto simp add: insert_dom) |
29708 | 451 |
|
63462 | 452 |
lemma size_delete: "size (delete k m) = (if k \<in> keys m then size m - 1 else size m)" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
453 |
unfolding size_def by transfer simp |
29708 | 454 |
|
63462 | 455 |
lemma size_tabulate [simp]: "size (tabulate ks f) = length (remdups ks)" |
456 |
unfolding size_def by transfer (auto simp add: map_of_map_restrict card_set comp_def) |
|
29708 | 457 |
|
63194 | 458 |
lemma keys_filter: "keys (filter P m) \<subseteq> keys m" |
459 |
by transfer (auto split: option.splits) |
|
460 |
||
461 |
lemma size_filter: "finite (keys m) \<Longrightarrow> size (filter P m) \<le> size m" |
|
462 |
by (intro size_mono keys_filter) |
|
463 |
||
63462 | 464 |
lemma bulkload_tabulate: "bulkload xs = tabulate [0..<length xs] (nth xs)" |
56528 | 465 |
by transfer (auto simp add: map_of_map_restrict) |
29826 | 466 |
|
63462 | 467 |
lemma is_empty_empty [simp]: "is_empty empty" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
468 |
unfolding is_empty_def by transfer simp |
37052 | 469 |
|
63462 | 470 |
lemma is_empty_update [simp]: "\<not> is_empty (update k v m)" |
471 |
unfolding is_empty_def by transfer simp |
|
472 |
||
473 |
lemma is_empty_delete: "is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
474 |
unfolding is_empty_def by transfer (auto simp del: dom_eq_empty_conv) |
37052 | 475 |
|
63462 | 476 |
lemma is_empty_replace [simp]: "is_empty (replace k v m) \<longleftrightarrow> is_empty m" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
477 |
unfolding is_empty_def replace_def by transfer auto |
37052 | 478 |
|
63462 | 479 |
lemma is_empty_default [simp]: "\<not> is_empty (default k v m)" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
480 |
unfolding is_empty_def default_def by transfer auto |
37052 | 481 |
|
63462 | 482 |
lemma is_empty_map_entry [simp]: "is_empty (map_entry k f m) \<longleftrightarrow> is_empty m" |
56528 | 483 |
unfolding is_empty_def by transfer (auto split: option.split) |
37052 | 484 |
|
63462 | 485 |
lemma is_empty_map_values [simp]: "is_empty (map_values f m) \<longleftrightarrow> is_empty m" |
63194 | 486 |
unfolding is_empty_def by transfer (auto simp: fun_eq_iff) |
487 |
||
63462 | 488 |
lemma is_empty_map_default [simp]: "\<not> is_empty (map_default k v f m)" |
37052 | 489 |
by (simp add: map_default_def) |
490 |
||
63462 | 491 |
lemma keys_dom_lookup: "keys m = dom (Mapping.lookup m)" |
56545 | 492 |
by transfer rule |
493 |
||
63462 | 494 |
lemma keys_empty [simp]: "keys empty = {}" |
73832 | 495 |
by transfer (fact dom_empty) |
496 |
||
497 |
lemma in_keysD: "k \<in> keys m \<Longrightarrow> \<exists>v. lookup m k = Some v" |
|
498 |
by transfer (fact domD) |
|
499 |
||
63462 | 500 |
lemma keys_update [simp]: "keys (update k v m) = insert k (keys m)" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
501 |
by transfer simp |
37052 | 502 |
|
63462 | 503 |
lemma keys_delete [simp]: "keys (delete k m) = keys m - {k}" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
504 |
by transfer simp |
37052 | 505 |
|
63462 | 506 |
lemma keys_replace [simp]: "keys (replace k v m) = keys m" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
507 |
unfolding replace_def by transfer (simp add: insert_absorb) |
37052 | 508 |
|
63462 | 509 |
lemma keys_default [simp]: "keys (default k v m) = insert k (keys m)" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
510 |
unfolding default_def by transfer (simp add: insert_absorb) |
37052 | 511 |
|
63462 | 512 |
lemma keys_map_entry [simp]: "keys (map_entry k f m) = keys m" |
56528 | 513 |
by transfer (auto split: option.split) |
37052 | 514 |
|
63462 | 515 |
lemma keys_map_default [simp]: "keys (map_default k v f m) = insert k (keys m)" |
37052 | 516 |
by (simp add: map_default_def) |
517 |
||
63462 | 518 |
lemma keys_map_values [simp]: "keys (map_values f m) = keys m" |
63194 | 519 |
by transfer (simp_all add: dom_def) |
520 |
||
63462 | 521 |
lemma keys_combine_with_key [simp]: |
63194 | 522 |
"Mapping.keys (combine_with_key f m1 m2) = Mapping.keys m1 \<union> Mapping.keys m2" |
63462 | 523 |
by transfer (auto simp: dom_def combine_options_def split: option.splits) |
63194 | 524 |
|
525 |
lemma keys_combine [simp]: "Mapping.keys (combine f m1 m2) = Mapping.keys m1 \<union> Mapping.keys m2" |
|
526 |
by (simp add: combine_altdef) |
|
527 |
||
63462 | 528 |
lemma keys_tabulate [simp]: "keys (tabulate ks f) = set ks" |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset
|
529 |
by transfer (simp add: map_of_map_restrict o_def) |
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset
|
530 |
|
63194 | 531 |
lemma keys_of_alist [simp]: "keys (of_alist xs) = set (List.map fst xs)" |
532 |
by transfer (simp_all add: dom_map_of_conv_image_fst) |
|
533 |
||
63462 | 534 |
lemma keys_bulkload [simp]: "keys (bulkload xs) = {0..<length xs}" |
56528 | 535 |
by (simp add: bulkload_tabulate) |
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset
|
536 |
|
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
537 |
lemma finite_keys_update[simp]: |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
538 |
"finite (keys (update k v m)) = finite (keys m)" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
539 |
by transfer simp |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
540 |
|
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
541 |
lemma set_ordered_keys[simp]: |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
542 |
"finite (Mapping.keys m) \<Longrightarrow> set (Mapping.ordered_keys m) = Mapping.keys m" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
543 |
unfolding ordered_keys_def by transfer auto |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
544 |
|
63462 | 545 |
lemma distinct_ordered_keys [simp]: "distinct (ordered_keys m)" |
37052 | 546 |
by (simp add: ordered_keys_def) |
547 |
||
63462 | 548 |
lemma ordered_keys_infinite [simp]: "\<not> finite (keys m) \<Longrightarrow> ordered_keys m = []" |
37052 | 549 |
by (simp add: ordered_keys_def) |
550 |
||
63462 | 551 |
lemma ordered_keys_empty [simp]: "ordered_keys empty = []" |
37052 | 552 |
by (simp add: ordered_keys_def) |
553 |
||
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
554 |
lemma sorted_ordered_keys[simp]: "sorted (ordered_keys m)" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
555 |
unfolding ordered_keys_def by simp |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
556 |
|
37052 | 557 |
lemma ordered_keys_update [simp]: |
558 |
"k \<in> keys m \<Longrightarrow> ordered_keys (update k v m) = ordered_keys m" |
|
63462 | 559 |
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> |
560 |
ordered_keys (update k v m) = insort k (ordered_keys m)" |
|
561 |
by (simp_all add: ordered_keys_def) |
|
73832 | 562 |
(auto simp only: sorted_list_of_set_insert_remove[symmetric] insert_absorb) |
37052 | 563 |
|
63462 | 564 |
lemma ordered_keys_delete [simp]: "ordered_keys (delete k m) = remove1 k (ordered_keys m)" |
37052 | 565 |
proof (cases "finite (keys m)") |
63462 | 566 |
case False |
567 |
then show ?thesis by simp |
|
37052 | 568 |
next |
63462 | 569 |
case fin: True |
37052 | 570 |
show ?thesis |
571 |
proof (cases "k \<in> keys m") |
|
63462 | 572 |
case False |
573 |
with fin have "k \<notin> set (sorted_list_of_set (keys m))" |
|
574 |
by simp |
|
575 |
with False show ?thesis |
|
576 |
by (simp add: ordered_keys_def remove1_idem) |
|
37052 | 577 |
next |
63462 | 578 |
case True |
579 |
with fin show ?thesis |
|
580 |
by (simp add: ordered_keys_def sorted_list_of_set_remove) |
|
37052 | 581 |
qed |
582 |
qed |
|
583 |
||
63462 | 584 |
lemma ordered_keys_replace [simp]: "ordered_keys (replace k v m) = ordered_keys m" |
37052 | 585 |
by (simp add: replace_def) |
586 |
||
587 |
lemma ordered_keys_default [simp]: |
|
588 |
"k \<in> keys m \<Longrightarrow> ordered_keys (default k v m) = ordered_keys m" |
|
589 |
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (default k v m) = insort k (ordered_keys m)" |
|
590 |
by (simp_all add: default_def) |
|
591 |
||
63462 | 592 |
lemma ordered_keys_map_entry [simp]: "ordered_keys (map_entry k f m) = ordered_keys m" |
37052 | 593 |
by (simp add: ordered_keys_def) |
594 |
||
595 |
lemma ordered_keys_map_default [simp]: |
|
596 |
"k \<in> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = ordered_keys m" |
|
597 |
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = insort k (ordered_keys m)" |
|
598 |
by (simp_all add: map_default_def) |
|
599 |
||
63462 | 600 |
lemma ordered_keys_tabulate [simp]: "ordered_keys (tabulate ks f) = sort (remdups ks)" |
37052 | 601 |
by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups) |
602 |
||
63462 | 603 |
lemma ordered_keys_bulkload [simp]: "ordered_keys (bulkload ks) = [0..<length ks]" |
37052 | 604 |
by (simp add: ordered_keys_def) |
36110 | 605 |
|
73832 | 606 |
lemma tabulate_fold: "tabulate xs f = List.fold (\<lambda>k m. update k (f k) m) xs empty" |
56528 | 607 |
proof transfer |
608 |
fix f :: "'a \<Rightarrow> 'b" and xs |
|
56529
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
609 |
have "map_of (List.map (\<lambda>k. (k, f k)) xs) = foldr (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty" |
aff193f53a64
restoring notion of primitive vs. derived operations in terms of generated code;
haftmann
parents:
56528
diff
changeset
|
610 |
by (simp add: foldr_map comp_def map_of_foldr) |
73832 | 611 |
also have "foldr (\<lambda>k m. m(k \<mapsto> f k)) xs = List.fold (\<lambda>k m. m(k \<mapsto> f k)) xs" |
56528 | 612 |
by (rule foldr_fold) (simp add: fun_eq_iff) |
73832 | 613 |
ultimately show "map_of (List.map (\<lambda>k. (k, f k)) xs) = List.fold (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty" |
56528 | 614 |
by simp |
615 |
qed |
|
616 |
||
63194 | 617 |
lemma All_mapping_mono: |
618 |
"(\<And>k v. k \<in> keys m \<Longrightarrow> P k v \<Longrightarrow> Q k v) \<Longrightarrow> All_mapping m P \<Longrightarrow> All_mapping m Q" |
|
619 |
unfolding All_mapping_def by transfer (auto simp: All_mapping_def dom_def split: option.splits) |
|
31459 | 620 |
|
63194 | 621 |
lemma All_mapping_empty [simp]: "All_mapping Mapping.empty P" |
622 |
by (auto simp: All_mapping_def lookup_empty) |
|
63462 | 623 |
|
624 |
lemma All_mapping_update_iff: |
|
63194 | 625 |
"All_mapping (Mapping.update k v m) P \<longleftrightarrow> P k v \<and> All_mapping m (\<lambda>k' v'. k = k' \<or> P k' v')" |
63462 | 626 |
unfolding All_mapping_def |
63194 | 627 |
proof safe |
628 |
assume "\<forall>x. case Mapping.lookup (Mapping.update k v m) x of None \<Rightarrow> True | Some y \<Rightarrow> P x y" |
|
63462 | 629 |
then have *: "case Mapping.lookup (Mapping.update k v m) x of None \<Rightarrow> True | Some y \<Rightarrow> P x y" for x |
63194 | 630 |
by blast |
63462 | 631 |
from *[of k] show "P k v" |
632 |
by (simp add: lookup_update) |
|
63194 | 633 |
show "case Mapping.lookup m x of None \<Rightarrow> True | Some v' \<Rightarrow> k = x \<or> P x v'" for x |
63462 | 634 |
using *[of x] by (auto simp add: lookup_update' split: if_splits option.splits) |
63194 | 635 |
next |
636 |
assume "P k v" |
|
637 |
assume "\<forall>x. case Mapping.lookup m x of None \<Rightarrow> True | Some v' \<Rightarrow> k = x \<or> P x v'" |
|
63462 | 638 |
then have A: "case Mapping.lookup m x of None \<Rightarrow> True | Some v' \<Rightarrow> k = x \<or> P x v'" for x |
639 |
by blast |
|
63194 | 640 |
show "case Mapping.lookup (Mapping.update k v m) x of None \<Rightarrow> True | Some xa \<Rightarrow> P x xa" for x |
641 |
using \<open>P k v\<close> A[of x] by (auto simp: lookup_update' split: option.splits) |
|
642 |
qed |
|
643 |
||
644 |
lemma All_mapping_update: |
|
645 |
"P k v \<Longrightarrow> All_mapping m (\<lambda>k' v'. k = k' \<or> P k' v') \<Longrightarrow> All_mapping (Mapping.update k v m) P" |
|
646 |
by (simp add: All_mapping_update_iff) |
|
647 |
||
63462 | 648 |
lemma All_mapping_filter_iff: "All_mapping (filter P m) Q \<longleftrightarrow> All_mapping m (\<lambda>k v. P k v \<longrightarrow> Q k v)" |
63194 | 649 |
by (auto simp: All_mapping_def lookup_filter split: option.splits) |
650 |
||
63462 | 651 |
lemma All_mapping_filter: "All_mapping m Q \<Longrightarrow> All_mapping (filter P m) Q" |
63194 | 652 |
by (auto simp: All_mapping_filter_iff intro: All_mapping_mono) |
31459 | 653 |
|
63462 | 654 |
lemma All_mapping_map_values: "All_mapping (map_values f m) P \<longleftrightarrow> All_mapping m (\<lambda>k v. P k (f k v))" |
63194 | 655 |
by (auto simp: All_mapping_def lookup_map_values split: option.splits) |
656 |
||
63462 | 657 |
lemma All_mapping_tabulate: "(\<forall>x\<in>set xs. P x (f x)) \<Longrightarrow> All_mapping (Mapping.tabulate xs f) P" |
658 |
unfolding All_mapping_def |
|
659 |
apply (intro allI) |
|
660 |
apply transfer |
|
661 |
apply (auto split: option.split dest!: map_of_SomeD) |
|
662 |
done |
|
63194 | 663 |
|
664 |
lemma All_mapping_alist: |
|
665 |
"(\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v) \<Longrightarrow> All_mapping (Mapping.of_alist xs) P" |
|
666 |
by (auto simp: All_mapping_def lookup_of_alist dest!: map_of_SomeD split: option.splits) |
|
667 |
||
63462 | 668 |
lemma combine_empty [simp]: "combine f Mapping.empty y = y" "combine f y Mapping.empty = y" |
669 |
by (transfer; force)+ |
|
63194 | 670 |
|
671 |
lemma (in abel_semigroup) comm_monoid_set_combine: "comm_monoid_set (combine f) Mapping.empty" |
|
672 |
by standard (transfer fixing: f, simp add: combine_options_ac[of f] ac_simps)+ |
|
673 |
||
674 |
locale combine_mapping_abel_semigroup = abel_semigroup |
|
675 |
begin |
|
676 |
||
677 |
sublocale combine: comm_monoid_set "combine f" Mapping.empty |
|
678 |
by (rule comm_monoid_set_combine) |
|
679 |
||
680 |
lemma fold_combine_code: |
|
681 |
"combine.F g (set xs) = foldr (\<lambda>x. combine f (g x)) (remdups xs) Mapping.empty" |
|
682 |
proof - |
|
683 |
have "combine.F g (set xs) = foldr (\<lambda>x. combine f (g x)) xs Mapping.empty" |
|
684 |
if "distinct xs" for xs |
|
685 |
using that by (induction xs) simp_all |
|
686 |
from this[of "remdups xs"] show ?thesis by simp |
|
687 |
qed |
|
63462 | 688 |
|
689 |
lemma keys_fold_combine: "finite A \<Longrightarrow> Mapping.keys (combine.F g A) = (\<Union>x\<in>A. Mapping.keys (g x))" |
|
690 |
by (induct A rule: finite_induct) simp_all |
|
35157 | 691 |
|
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
49973
diff
changeset
|
692 |
end |
59485 | 693 |
|
73832 | 694 |
subsubsection \<open>@{term [source] entries}, @{term [source] ordered_entries}, |
695 |
and @{term [source] fold}\<close> |
|
696 |
||
697 |
context linorder |
|
698 |
begin |
|
699 |
||
700 |
sublocale folding_Map_graph: folding_insort_key "(\<le>)" "(<)" "Map.graph m" fst for m |
|
701 |
by unfold_locales (fact inj_on_fst_graph) |
|
702 |
||
703 |
end |
|
704 |
||
705 |
lemma sorted_fst_list_of_set_insort_Map_graph[simp]: |
|
706 |
assumes "finite (dom m)" "fst x \<notin> dom m" |
|
707 |
shows "sorted_key_list_of_set fst (insert x (Map.graph m)) |
|
708 |
= insort_key fst x (sorted_key_list_of_set fst (Map.graph m))" |
|
709 |
proof(cases x) |
|
710 |
case (Pair k v) |
|
711 |
with \<open>fst x \<notin> dom m\<close> have "Map.graph m \<subseteq> Map.graph (m(k \<mapsto> v))" |
|
712 |
by(auto simp: graph_def) |
|
713 |
moreover from Pair \<open>fst x \<notin> dom m\<close> have "(k, v) \<notin> Map.graph m" |
|
714 |
using graph_domD by fastforce |
|
715 |
ultimately show ?thesis |
|
716 |
using Pair assms folding_Map_graph.sorted_key_list_of_set_insert[where ?m="m(k \<mapsto> v)"] |
|
717 |
by auto |
|
718 |
qed |
|
719 |
||
720 |
lemma sorted_fst_list_of_set_insort_insert_Map_graph[simp]: |
|
721 |
assumes "finite (dom m)" "fst x \<notin> dom m" |
|
722 |
shows "sorted_key_list_of_set fst (insert x (Map.graph m)) |
|
723 |
= insort_insert_key fst x (sorted_key_list_of_set fst (Map.graph m))" |
|
724 |
proof(cases x) |
|
725 |
case (Pair k v) |
|
726 |
with \<open>fst x \<notin> dom m\<close> have "Map.graph m \<subseteq> Map.graph (m(k \<mapsto> v))" |
|
727 |
by(auto simp: graph_def) |
|
728 |
with assms Pair show ?thesis |
|
729 |
unfolding sorted_fst_list_of_set_insort_Map_graph[OF assms] insort_insert_key_def |
|
730 |
using folding_Map_graph.set_sorted_key_list_of_set in_graphD by (fastforce split: if_splits) |
|
731 |
qed |
|
732 |
||
733 |
lemma linorder_finite_Map_induct[consumes 1, case_names empty update]: |
|
734 |
fixes m :: "'a::linorder \<rightharpoonup> 'b" |
|
735 |
assumes "finite (dom m)" |
|
736 |
assumes "P Map.empty" |
|
737 |
assumes "\<And>k v m. \<lbrakk> finite (dom m); k \<notin> dom m; (\<And>k'. k' \<in> dom m \<Longrightarrow> k' \<le> k); P m \<rbrakk> |
|
738 |
\<Longrightarrow> P (m(k \<mapsto> v))" |
|
739 |
shows "P m" |
|
740 |
proof - |
|
741 |
let ?key_list = "\<lambda>m. sorted_list_of_set (dom m)" |
|
742 |
from assms(1,2) show ?thesis |
|
743 |
proof(induction "length (?key_list m)" arbitrary: m) |
|
744 |
case 0 |
|
745 |
then have "sorted_list_of_set (dom m) = []" |
|
746 |
by auto |
|
747 |
with \<open>finite (dom m)\<close> have "m = Map.empty" |
|
748 |
by auto |
|
749 |
with \<open>P Map.empty\<close> show ?case by simp |
|
750 |
next |
|
751 |
case (Suc n) |
|
752 |
then obtain x xs where x_xs: "sorted_list_of_set (dom m) = xs @ [x]" |
|
753 |
by (metis append_butlast_last_id length_greater_0_conv zero_less_Suc) |
|
754 |
have "sorted_list_of_set (dom (m(x := None))) = xs" |
|
755 |
proof - |
|
756 |
have "distinct (xs @ [x])" |
|
757 |
by (metis sorted_list_of_set.distinct_sorted_key_list_of_set x_xs) |
|
758 |
then have "remove1 x (xs @ [x]) = xs" |
|
759 |
by (simp add: remove1_append) |
|
760 |
with \<open>finite (dom m)\<close> x_xs show ?thesis |
|
761 |
by (simp add: sorted_list_of_set_remove) |
|
762 |
qed |
|
763 |
moreover have "k \<le> x" if "k \<in> dom (m(x := None))" for k |
|
764 |
proof - |
|
765 |
from x_xs have "sorted (xs @ [x])" |
|
766 |
by (metis sorted_list_of_set.sorted_sorted_key_list_of_set) |
|
767 |
moreover from \<open>k \<in> dom (m(x := None))\<close> have "k \<in> set xs" |
|
768 |
using \<open>finite (dom m)\<close> \<open>sorted_list_of_set (dom (m(x := None))) = xs\<close> |
|
769 |
by auto |
|
770 |
ultimately show "k \<le> x" |
|
771 |
by (simp add: sorted_append) |
|
772 |
qed |
|
773 |
moreover from \<open>finite (dom m)\<close> have "finite (dom (m(x := None)))" "x \<notin> dom (m(x := None))" |
|
774 |
by simp_all |
|
775 |
moreover have "P (m(x := None))" |
|
776 |
using Suc \<open>sorted_list_of_set (dom (m(x := None))) = xs\<close> x_xs by auto |
|
777 |
ultimately show ?case |
|
778 |
using assms(3)[where ?m="m(x := None)"] by (metis fun_upd_triv fun_upd_upd not_Some_eq) |
|
779 |
qed |
|
780 |
qed |
|
781 |
||
782 |
lemma delete_insort_fst[simp]: "AList.delete k (insort_key fst (k, v) xs) = AList.delete k xs" |
|
783 |
by (induction xs) simp_all |
|
784 |
||
785 |
lemma insort_fst_delete: "\<lbrakk> fst x \<noteq> k2; sorted (List.map fst xs) \<rbrakk> |
|
786 |
\<Longrightarrow> insort_key fst x (AList.delete k2 xs) = AList.delete k2 (insort_key fst x xs)" |
|
787 |
by (induction xs) (fastforce simp add: insort_is_Cons order_trans)+ |
|
788 |
||
789 |
lemma sorted_fst_list_of_set_Map_graph_fun_upd_None[simp]: |
|
790 |
"sorted_key_list_of_set fst (Map.graph (m(k := None))) |
|
791 |
= AList.delete k (sorted_key_list_of_set fst (Map.graph m))" |
|
792 |
proof(cases "finite (Map.graph m)") |
|
793 |
assume "finite (Map.graph m)" |
|
794 |
from this[unfolded finite_graph_iff_finite_dom] show ?thesis |
|
795 |
proof(induction rule: finite_Map_induct) |
|
796 |
let ?list_of="sorted_key_list_of_set fst" |
|
797 |
case (update k2 v2 m) |
|
798 |
note [simp] = \<open>k2 \<notin> dom m\<close> \<open>finite (dom m)\<close> |
|
799 |
||
800 |
have right_eq: "AList.delete k (?list_of (Map.graph (m(k2 \<mapsto> v2)))) |
|
801 |
= AList.delete k (insort_key fst (k2, v2) (?list_of (Map.graph m)))" |
|
802 |
by simp |
|
803 |
||
804 |
show ?case |
|
805 |
proof(cases "k = k2") |
|
806 |
case True |
|
807 |
then have "?list_of (Map.graph ((m(k2 \<mapsto> v2))(k := None))) |
|
808 |
= AList.delete k (insort_key fst (k2, v2) (?list_of (Map.graph m)))" |
|
809 |
using fst_graph_eq_dom update.IH by auto |
|
810 |
then show ?thesis |
|
811 |
using right_eq by metis |
|
812 |
next |
|
813 |
case False |
|
814 |
then have "AList.delete k (insort_key fst (k2, v2) (?list_of (Map.graph m))) |
|
815 |
= insort_key fst (k2, v2) (?list_of (Map.graph (m(k := None))))" |
|
816 |
by (auto simp add: insort_fst_delete update.IH |
|
817 |
folding_Map_graph.sorted_sorted_key_list_of_set[OF subset_refl]) |
|
818 |
also have "\<dots> = ?list_of (insert (k2, v2) (Map.graph (m(k := None))))" |
|
819 |
by auto |
|
820 |
also from False \<open>k2 \<notin> dom m\<close> have "\<dots> = ?list_of (Map.graph ((m(k2 \<mapsto> v2))(k := None)))" |
|
821 |
by (metis graph_map_upd domIff fun_upd_triv fun_upd_twist) |
|
822 |
finally show ?thesis using right_eq by metis |
|
823 |
qed |
|
824 |
qed simp |
|
825 |
qed simp |
|
826 |
||
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
827 |
lemma entries_empty[simp]: "entries empty = {}" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
828 |
by transfer (fact graph_empty) |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
829 |
|
73832 | 830 |
lemma entries_lookup: "entries m = Map.graph (lookup m)" |
831 |
by transfer rule |
|
832 |
||
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
833 |
lemma in_entriesI: "lookup m k = Some v \<Longrightarrow> (k, v) \<in> entries m" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
834 |
by transfer (fact in_graphI) |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
835 |
|
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
836 |
lemma in_entriesD: "(k, v) \<in> entries m \<Longrightarrow> lookup m k = Some v" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
837 |
by transfer (fact in_graphD) |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
838 |
|
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
839 |
lemma fst_image_entries_eq_keys[simp]: "fst ` Mapping.entries m = Mapping.keys m" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
840 |
by transfer (fact fst_graph_eq_dom) |
73832 | 841 |
|
842 |
lemma finite_entries_iff_finite_keys[simp]: |
|
843 |
"finite (entries m) = finite (keys m)" |
|
844 |
by transfer (fact finite_graph_iff_finite_dom) |
|
845 |
||
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
846 |
lemma entries_update: |
73832 | 847 |
"entries (update k v m) = insert (k, v) (entries (delete k m))" |
848 |
by transfer (fact graph_map_upd) |
|
849 |
||
850 |
lemma entries_delete: |
|
851 |
"entries (delete k m) = {e \<in> entries m. fst e \<noteq> k}" |
|
852 |
by transfer (fact graph_fun_upd_None) |
|
853 |
||
854 |
lemma entries_of_alist[simp]: |
|
855 |
"distinct (List.map fst xs) \<Longrightarrow> entries (of_alist xs) = set xs" |
|
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
856 |
by transfer (fact graph_map_of_if_distinct_dom) |
73832 | 857 |
|
858 |
lemma entries_keysD: |
|
859 |
"x \<in> entries m \<Longrightarrow> fst x \<in> keys m" |
|
860 |
by transfer (fact graph_domD) |
|
861 |
||
862 |
lemma set_ordered_entries[simp]: |
|
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
863 |
"finite (keys m) \<Longrightarrow> set (ordered_entries m) = entries m" |
73832 | 864 |
unfolding ordered_entries_def |
865 |
by transfer (auto simp: folding_Map_graph.set_sorted_key_list_of_set[OF subset_refl]) |
|
866 |
||
867 |
lemma distinct_ordered_entries[simp]: "distinct (List.map fst (ordered_entries m))" |
|
868 |
unfolding ordered_entries_def |
|
869 |
by transfer (simp add: folding_Map_graph.distinct_sorted_key_list_of_set[OF subset_refl]) |
|
870 |
||
871 |
lemma sorted_ordered_entries[simp]: "sorted (List.map fst (ordered_entries m))" |
|
872 |
unfolding ordered_entries_def |
|
873 |
by transfer (auto intro: folding_Map_graph.sorted_sorted_key_list_of_set) |
|
874 |
||
875 |
lemma ordered_entries_infinite[simp]: |
|
876 |
"\<not> finite (Mapping.keys m) \<Longrightarrow> ordered_entries m = []" |
|
877 |
by (simp add: ordered_entries_def) |
|
878 |
||
879 |
lemma ordered_entries_empty[simp]: "ordered_entries empty = []" |
|
880 |
by (simp add: ordered_entries_def) |
|
881 |
||
882 |
lemma ordered_entries_update[simp]: |
|
883 |
assumes "finite (keys m)" |
|
884 |
shows "ordered_entries (update k v m) |
|
885 |
= insort_insert_key fst (k, v) (AList.delete k (ordered_entries m))" |
|
886 |
proof - |
|
887 |
let ?list_of="sorted_key_list_of_set fst" and ?insort="insort_insert_key fst" |
|
888 |
||
889 |
have *: "?list_of (insert (k, v) (Map.graph (m(k := None)))) |
|
890 |
= ?insort (k, v) (AList.delete k (?list_of (Map.graph m)))" if "finite (dom m)" for m |
|
891 |
proof - |
|
892 |
from \<open>finite (dom m)\<close> have "?list_of (insert (k, v) (Map.graph (m(k := None)))) |
|
893 |
= ?insort (k, v) (?list_of (Map.graph (m(k := None))))" |
|
894 |
by (intro sorted_fst_list_of_set_insort_insert_Map_graph) (simp_all add: subset_insertI) |
|
895 |
then show ?thesis by simp |
|
896 |
qed |
|
897 |
from assms show ?thesis |
|
898 |
unfolding ordered_entries_def |
|
899 |
apply (transfer fixing: k v) using "*" by auto |
|
900 |
qed |
|
901 |
||
902 |
lemma ordered_entries_delete[simp]: |
|
903 |
"ordered_entries (delete k m) = AList.delete k (ordered_entries m)" |
|
904 |
unfolding ordered_entries_def by transfer auto |
|
905 |
||
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
906 |
lemma map_fst_ordered_entries[simp]: |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
907 |
"List.map fst (ordered_entries m) = ordered_keys m" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
908 |
proof(cases "finite (Mapping.keys m)") |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
909 |
case True |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
910 |
then have "set (List.map fst (Mapping.ordered_entries m)) = set (Mapping.ordered_keys m)" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
911 |
unfolding ordered_entries_def ordered_keys_def |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
912 |
by (transfer) (simp add: folding_Map_graph.set_sorted_key_list_of_set[OF subset_refl] fst_graph_eq_dom) |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
913 |
with True show "List.map fst (Mapping.ordered_entries m) = Mapping.ordered_keys m" |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
914 |
by (metis distinct_ordered_entries ordered_keys_def sorted_list_of_set.idem_if_sorted_distinct |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
915 |
sorted_list_of_set.set_sorted_key_list_of_set sorted_ordered_entries) |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
916 |
next |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
917 |
case False |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
918 |
then show ?thesis |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
919 |
unfolding ordered_entries_def ordered_keys_def by simp |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
920 |
qed |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
921 |
|
73832 | 922 |
lemma fold_empty[simp]: "fold f empty a = a" |
923 |
unfolding fold_def by simp |
|
924 |
||
925 |
lemma insort_key_is_snoc_if_sorted_and_distinct: |
|
926 |
assumes "sorted (List.map f xs)" "f y \<notin> f ` set xs" "\<forall>x \<in> set xs. f x \<le> f y" |
|
927 |
shows "insort_key f y xs = xs @ [y]" |
|
928 |
using assms by (induction xs) (auto dest!: insort_is_Cons) |
|
929 |
||
930 |
lemma fold_update: |
|
931 |
assumes "finite (keys m)" |
|
932 |
assumes "k \<notin> keys m" "\<And>k'. k' \<in> keys m \<Longrightarrow> k' \<le> k" |
|
933 |
shows "fold f (update k v m) a = f k v (fold f m a)" |
|
934 |
proof - |
|
935 |
from assms have k_notin_entries: "k \<notin> fst ` set (ordered_entries m)" |
|
936 |
using entries_keysD by fastforce |
|
937 |
with assms have "ordered_entries (update k v m) |
|
938 |
= insort_insert_key fst (k, v) (ordered_entries m)" |
|
939 |
by simp |
|
940 |
also from k_notin_entries have "\<dots> = ordered_entries m @ [(k, v)]" |
|
941 |
proof - |
|
942 |
from assms have "\<forall>x \<in> set (ordered_entries m). fst x \<le> fst (k, v)" |
|
943 |
unfolding ordered_entries_def |
|
944 |
by transfer (fastforce simp: folding_Map_graph.set_sorted_key_list_of_set[OF order_refl] |
|
945 |
dest: graph_domD) |
|
74157
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
946 |
from insort_key_is_snoc_if_sorted_and_distinct[OF _ _ this] k_notin_entries \<open>finite (keys m)\<close> |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
947 |
show ?thesis |
8e2355ddce1b
add/rename some theorems about Map(pings)
Lukas Stevens <mail@lukas-stevens.de>
parents:
73832
diff
changeset
|
948 |
using sorted_ordered_keys |
73832 | 949 |
unfolding insort_insert_key_def by auto |
950 |
qed |
|
951 |
finally show ?thesis unfolding fold_def by simp |
|
952 |
qed |
|
953 |
||
954 |
lemma linorder_finite_Mapping_induct[consumes 1, case_names empty update]: |
|
955 |
fixes m :: "('a::linorder, 'b) mapping" |
|
956 |
assumes "finite (keys m)" |
|
957 |
assumes "P empty" |
|
958 |
assumes "\<And>k v m. |
|
959 |
\<lbrakk> finite (keys m); k \<notin> keys m; (\<And>k'. k' \<in> keys m \<Longrightarrow> k' \<le> k); P m \<rbrakk> |
|
960 |
\<Longrightarrow> P (update k v m)" |
|
961 |
shows "P m" |
|
962 |
using assms by transfer (simp add: linorder_finite_Map_induct) |
|
963 |
||
63462 | 964 |
|
63194 | 965 |
subsection \<open>Code generator setup\<close> |
966 |
||
967 |
hide_const (open) empty is_empty rep lookup lookup_default filter update delete ordered_keys |
|
968 |
keys size replace default map_entry map_default tabulate bulkload map map_values combine of_alist |
|
73832 | 969 |
entries ordered_entries fold |
63194 | 970 |
|
971 |
end |