Theory ArrayMapImpl
section ‹\isaheader{Maps from Naturals by Arrays}›
theory ArrayMapImpl
imports
"../spec/MapSpec"
"../gen_algo/MapGA"
"../../Lib/Diff_Array"
begin
text_raw ‹\label{thy:ArrayMapImpl}›
type_synonym 'v iam = "'v option array"
subsection ‹Definitions›
definition iam_α :: "'v iam ⇒ nat ⇀ 'v" where
"iam_α a i ≡ if i < array_length a then array_get a i else None"
lemma [code]: "iam_α a i ≡ array_get_oo None a i"
unfolding iam_α_def array_get_oo_def .
abbreviation (input) iam_invar :: "'v iam ⇒ bool"
where "iam_invar ≡ λ_. True"
definition iam_empty :: "unit ⇒ 'v iam"
where "iam_empty ≡ λ_::unit. array_of_list []"
definition iam_lookup :: "nat ⇒ 'v iam ⇀ 'v"
where [code_unfold]: "iam_lookup k a ≡ iam_α a k"
definition "iam_increment (l::nat) idx ≡
max (idx + 1 - l) (2 * l + 3)"
lemma incr_correct: "¬ idx < l ⟹ idx < l + iam_increment l idx"
unfolding iam_increment_def by auto
definition iam_update :: "nat ⇒ 'v ⇒ 'v iam ⇒ 'v iam"
where "iam_update k v a ≡ let
l = array_length a;
a = if k < l then a else array_grow a (iam_increment l k) None
in
array_set a k (Some v)
"
lemma [code]: "iam_update k v a ≡ array_set_oo
(λ_. array_set
(array_grow a (iam_increment (array_length a) k) None) k (Some v))
a k (Some v)
"
unfolding iam_update_def array_set_oo_def
apply (rule eq_reflection)
apply (auto simp add: Let_def)
done
definition "iam_update_dj ≡ iam_update"
definition iam_delete :: "nat ⇒ 'v iam ⇒ 'v iam"
where "iam_delete k a ≡
if k<array_length a then array_set a k None else a"
lemma [code]: "iam_delete k a ≡ array_set_oo (λ_. a) a k None"
unfolding iam_delete_def array_set_oo_def by auto
fun iam_rev_iterateoi_aux
:: "nat ⇒ ('v iam) ⇒ ('σ⇒bool) ⇒ (nat × 'v⇒'σ⇒'σ) ⇒ 'σ ⇒ 'σ"
where
"iam_rev_iterateoi_aux 0 a c f σ = σ"
| "iam_rev_iterateoi_aux i a c f σ = (
if c σ then
iam_rev_iterateoi_aux (i - 1) a c f (
case array_get a (i - 1) of None ⇒ σ | Some x ⇒ f (i - 1, x) σ
)
else σ)"
definition iam_rev_iterateoi :: "'v iam ⇒ (nat × 'v,'σ) set_iterator" where
"iam_rev_iterateoi a ≡ iam_rev_iterateoi_aux (array_length a) a"
function iam_iterateoi_aux
:: "nat ⇒ nat ⇒ ('v iam) ⇒ ('σ⇒bool) ⇒ (nat × 'v⇒'σ⇒'σ) ⇒ 'σ ⇒ 'σ"
where
"iam_iterateoi_aux i len a c f σ =
(if i ≥ len ∨ ¬ c σ then σ else let
σ' = (case array_get a i of
None ⇒ σ
| Some x ⇒ f (i,x) σ)
in iam_iterateoi_aux (i + 1) len a c f σ')"
by pat_completeness auto
termination
by (relation "measure (λ(i,l,_). l - i)") auto
declare iam_iterateoi_aux.simps[simp del]
lemma iam_iterateoi_aux_csimps:
"i ≥ len ⟹ iam_iterateoi_aux i len a c f σ = σ"
"¬ c σ ⟹ iam_iterateoi_aux i len a c f σ = σ"
"⟦ i< len; c σ ⟧ ⟹ iam_iterateoi_aux i len a c f σ =
(case array_get a i of
None ⇒ iam_iterateoi_aux (i + 1) len a c f σ
| Some x ⇒ iam_iterateoi_aux (i + 1) len a c f (f (i,x) σ))"
apply (subst iam_iterateoi_aux.simps, simp)
apply (subst iam_iterateoi_aux.simps, simp)
apply (subst iam_iterateoi_aux.simps)
apply (auto split: option.split_asm option.split)
done
definition iam_iterateoi :: "'v iam ⇒ (nat × 'v,'σ) set_iterator" where
"iam_iterateoi a = iam_iterateoi_aux 0 (array_length a) a"
lemma iam_empty_impl: "map_empty iam_α iam_invar iam_empty"
apply unfold_locales
unfolding iam_α_def[abs_def] iam_empty_def
by auto
lemma iam_lookup_impl: "map_lookup iam_α iam_invar iam_lookup"
apply unfold_locales
unfolding iam_α_def[abs_def] iam_lookup_def
by auto
lemma array_get_set_iff: "i<array_length a ⟹
array_get (array_set a i x) j = (if i=j then x else array_get a j)"
by (auto simp: array_get_array_set_other)
lemma iam_update_impl: "map_update iam_α iam_invar iam_update"
apply unfold_locales
unfolding iam_α_def[abs_def] iam_update_def
apply (rule ext)
apply (auto simp: Let_def array_get_set_iff incr_correct)
done
lemma iam_update_dj_impl: "map_update_dj iam_α iam_invar iam_update_dj"
apply (unfold iam_update_dj_def)
apply (rule update_dj_by_update)
apply (rule iam_update_impl)
done
lemma iam_delete_impl: "map_delete iam_α iam_invar iam_delete"
apply unfold_locales
unfolding iam_α_def[abs_def] iam_delete_def
apply (rule ext)
apply (auto simp: Let_def array_get_set_iff)
done
lemma iam_rev_iterateoi_aux_foldli_conv :
"iam_rev_iterateoi_aux n a =
foldli (List.map_filter (λn. map_option (λv. (n, v)) (array_get a n)) (rev [0..<n]))"
by (induct n) (auto simp add: List.map_filter_def fun_eq_iff)
lemma iam_rev_iterateoi_foldli_conv :
"iam_rev_iterateoi a =
foldli (List.map_filter
(λn. map_option (λv. (n, v)) (array_get a n))
(rev [0..<(array_length a)]))"
unfolding iam_rev_iterateoi_def iam_rev_iterateoi_aux_foldli_conv by simp
lemma iam_rev_iterateoi_correct :
fixes m::"'a option array"
defines "kvs ≡ List.map_filter
(λn. map_option (λv. (n, v)) (array_get m n)) (rev [0..<(array_length m)])"
shows "map_iterator_rev_linord (iam_rev_iterateoi m) (iam_α m)"
proof (rule map_iterator_rev_linord_I [of kvs])
show "iam_rev_iterateoi m = foldli kvs"
unfolding iam_rev_iterateoi_foldli_conv kvs_def by simp
next
define al where "al = array_length m"
show dist_kvs: "distinct (map fst kvs)" and "sorted (rev (map fst kvs))"
unfolding kvs_def al_def[symmetric]
apply (induct al)
apply (simp_all
add: List.map_filter_simps set_map_filter image_iff sorted_append
split: option.split)
done
from dist_kvs
have "⋀i. map_of kvs i = iam_α m i"
unfolding kvs_def
apply (case_tac "array_get m i")
apply (simp_all
add: iam_α_def map_of_eq_None_iff set_map_filter image_iff)
done
thus "iam_α m = map_of kvs" by auto
qed
lemma iam_rev_iterateoi_impl:
"poly_map_rev_iterateoi iam_α iam_invar iam_rev_iterateoi"
apply unfold_locales
apply (simp add: iam_α_def[abs_def] dom_def)
apply (simp add: iam_rev_iterateoi_correct)
done
lemma iam_iteratei_impl:
"poly_map_iteratei iam_α iam_invar iam_rev_iterateoi"
proof -
interpret aux: poly_map_rev_iterateoi iam_α iam_invar iam_rev_iterateoi
by (rule iam_rev_iterateoi_impl)
show ?thesis
apply unfold_locales
apply (rule map_rev_iterator_linord_is_it)
by (rule aux.list_rev_it_correct)
qed
lemma iam_iterateoi_aux_foldli_conv :
"iam_iterateoi_aux n (array_length a) a c f σ =
foldli (List.map_filter (λn. map_option (λv. (n, v)) (array_get a n))
([n..<array_length a])) c f σ"
thm iam_iterateoi_aux.induct
apply (induct n "array_length a" a c f σ rule: iam_iterateoi_aux.induct)
apply (subst iam_iterateoi_aux.simps)
apply (auto split: option.split simp: map_filter_simps)
apply (subst (2) upt_conv_Cons)
apply simp
apply (simp add: map_filter_simps)
apply (subst (2) upt_conv_Cons)
apply simp
apply (simp add: map_filter_simps)
done
lemma iam_iterateoi_foldli_conv :
"iam_iterateoi a =
foldli (List.map_filter
(λn. map_option (λv. (n, v)) (array_get a n))
([0..<(array_length a)]))"
apply (intro ext)
unfolding iam_iterateoi_def iam_iterateoi_aux_foldli_conv
by simp
lemmas [simp] = map_filter_simps
lemma map_filter_append[simp]: "List.map_filter f (la@lb)
= List.map_filter f la @ List.map_filter f lb"
by (induct la) (auto split: option.split)
lemma iam_iterateoi_correct:
fixes m::"'a option array"
defines "kvs ≡ List.map_filter
(λn. map_option (λv. (n, v)) (array_get m n)) ([0..<(array_length m)])"
shows "map_iterator_linord (iam_iterateoi m) (iam_α m)"
proof (rule map_iterator_linord_I [of kvs])
show "iam_iterateoi m = foldli kvs"
unfolding iam_iterateoi_foldli_conv kvs_def by simp
next
define al where "al = array_length m"
show dist_kvs: "distinct (map fst kvs)" and "sorted (map fst kvs)"
unfolding kvs_def al_def[symmetric]
apply (induct al)
apply (simp_all
add: set_map_filter image_iff sorted_append
split: option.split)
done
from dist_kvs
have "⋀i. map_of kvs i = iam_α m i"
unfolding kvs_def
apply (case_tac "array_get m i")
apply (simp_all
add: iam_α_def map_of_eq_None_iff set_map_filter image_iff)
done
thus "iam_α m = map_of kvs" by auto
qed
lemma iam_iterateoi_impl:
"poly_map_iterateoi iam_α iam_invar iam_iterateoi"
apply unfold_locales
apply (simp add: iam_α_def[abs_def] dom_def)
apply (simp add: iam_iterateoi_correct)
done
definition iam_basic_ops :: "(nat,'a,'a iam) omap_basic_ops"
where [icf_rec_def]: "iam_basic_ops ≡ ⦇
bmap_op_α = iam_α,
bmap_op_invar = λ_. True,
bmap_op_empty = iam_empty,
bmap_op_lookup = iam_lookup,
bmap_op_update = iam_update,
bmap_op_update_dj = iam_update_dj,
bmap_op_delete = iam_delete,
bmap_op_list_it = iam_rev_iterateoi,
bmap_op_ordered_list_it = iam_iterateoi,
bmap_op_rev_list_it = iam_rev_iterateoi
⦈"
setup Locale_Code.open_block
interpretation iam_basic: StdBasicOMap iam_basic_ops
apply (rule StdBasicOMap.intro)
apply (rule StdBasicMap.intro)
apply (simp_all add: icf_rec_unf)
apply (rule iam_empty_impl iam_lookup_impl iam_update_impl
iam_update_dj_impl iam_delete_impl iam_iteratei_impl
iam_iterateoi_impl iam_rev_iterateoi_impl)+
done
setup Locale_Code.close_block
definition [icf_rec_def]: "iam_ops ≡ iam_basic.dflt_oops"
setup Locale_Code.open_block