Theory MapGA

(*  Title:       Isabelle Collections Library
Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
(*
Changes since submission on 2009-11-26:

2009-12-10: OrderedMap, algorithms for iterators, min, max, to_sorted_list

*)

theory MapGA
imports SetIteratorCollectionsGA
begin

text_raw ‹\label{thy:MapGA}›

record ('k,'v,'s) map_basic_ops =
bmap_op_α :: "('k,'v,'s) map_α"
bmap_op_invar :: "('k,'v,'s) map_invar"
bmap_op_empty :: "('k,'v,'s) map_empty"
bmap_op_lookup :: "('k,'v,'s) map_lookup"
bmap_op_update :: "('k,'v,'s) map_update"
bmap_op_update_dj :: "('k,'v,'s) map_update_dj"
bmap_op_delete :: "('k,'v,'s) map_delete"
bmap_op_list_it :: "('k,'v,'s) map_list_it"

record ('k,'v,'s) omap_basic_ops = "('k,'v,'s) map_basic_ops" +
bmap_op_ordered_list_it :: "'s ⇒ ('k,'v,('k×'v) list) map_iterator"
bmap_op_rev_list_it :: "'s ⇒ ('k,'v,('k×'v) list) map_iterator"

locale StdBasicMapDefs =
poly_map_iteratei_defs "bmap_op_list_it ops"
for ops :: "('k,'v,'s,'more) map_basic_ops_scheme"
begin
abbreviation α where "α == bmap_op_α ops"
abbreviation invar where "invar == bmap_op_invar ops"
abbreviation empty where "empty == bmap_op_empty ops"
abbreviation lookup where "lookup == bmap_op_lookup ops"
abbreviation update where "update == bmap_op_update ops"
abbreviation update_dj where "update_dj == bmap_op_update_dj ops"
abbreviation delete where "delete == bmap_op_delete ops"
abbreviation list_it where "list_it == bmap_op_list_it ops"
end

locale StdBasicOMapDefs = StdBasicMapDefs ops
+ poly_map_iterateoi_defs "bmap_op_ordered_list_it ops"
+ poly_map_rev_iterateoi_defs "bmap_op_rev_list_it ops"
for ops :: "('k::linorder,'v,'s,'more) omap_basic_ops_scheme"
begin
abbreviation ordered_list_it where "ordered_list_it
≡ bmap_op_ordered_list_it ops"
abbreviation rev_list_it where "rev_list_it
≡ bmap_op_rev_list_it ops"
end

locale StdBasicMap = StdBasicMapDefs ops +
map α invar +
map_empty α invar empty +
map_lookup α invar lookup  +
map_update α invar update  +
map_update_dj α invar update_dj +
map_delete α invar delete  +
poly_map_iteratei α invar list_it
for ops :: "('k,'v,'s,'more) map_basic_ops_scheme"
begin
lemmas correct[simp] = empty_correct lookup_correct update_correct
update_dj_correct delete_correct
end

locale StdBasicOMap =
StdBasicOMapDefs ops +
StdBasicMap ops +
poly_map_iterateoi α invar ordered_list_it +
poly_map_rev_iterateoi α invar rev_list_it
for ops :: "('k::linorder,'v,'s,'more) omap_basic_ops_scheme"
begin
end

context StdBasicMapDefs begin
definition "g_sng k v ≡ update k v (empty ())"
definition "g_add m1 m2 ≡ iterate m2 (λ(k,v) σ. update k v σ) m1"

definition
"g_sel m P ≡
iteratei m (λσ. σ = None) (λx σ. if P x then Some x else None) None"

definition "g_bex m P ≡ iteratei m (λx. ¬x) (λkv σ. P kv) False"
definition "g_ball m P ≡ iteratei m id (λkv σ. P kv) True"

definition "g_size m ≡ iterate m (λ_. Suc) (0::nat)"
definition "g_size_abort b m ≡ iteratei m (λs. s<b) (λ_. Suc) (0::nat)"

definition "g_isEmpty m ≡ g_size_abort 1 m = 0"
definition "g_isSng m ≡ g_size_abort 2 m = 1"

definition "g_to_list m ≡ iterate m (#) []"

definition "g_list_to_map l ≡ foldl (λm (k,v). update k v m) (empty ())
(rev l)"

definition "g_add_dj m1 m2 ≡ iterate m2 (λ(k,v) σ. update_dj k v σ) m1"

definition "g_restrict P m ≡ iterate m
(λ(k,v) σ. if P (k,v) then update_dj k v σ else σ) (empty ())"

definition dflt_ops :: "('k,'v,'s) map_ops"
where [icf_rec_def]:
"dflt_ops ≡
⦇
map_op_α = α,
map_op_invar = invar,
map_op_empty = empty,
map_op_lookup = lookup,
map_op_update = update,
map_op_update_dj = update_dj,
map_op_delete = delete,
map_op_list_it = list_it,
map_op_sng = g_sng,
map_op_restrict = g_restrict,
map_op_isEmpty = g_isEmpty,
map_op_isSng = g_isSng,
map_op_ball = g_ball,
map_op_bex = g_bex,
map_op_size = g_size,
map_op_size_abort = g_size_abort,
map_op_sel = g_sel,
map_op_to_list = g_to_list,
map_op_to_map = g_list_to_map
⦈"

local_setup ‹Locale_Code.lc_decl_del @{term dflt_ops}›

end

lemma update_dj_by_update:
assumes "map_update α invar update"
shows "map_update_dj α invar update"
proof -
interpret map_update α invar update by fact
show ?thesis
apply (unfold_locales)
done
qed

lemma map_iterator_linord_is_it:
"map_iterator_linord m it ⟹ map_iterator m it"
unfolding set_iterator_def set_iterator_map_linord_def
apply (erule set_iterator_genord.set_iterator_weaken_R)
..

lemma map_rev_iterator_linord_is_it:
"map_iterator_rev_linord m it ⟹ map_iterator m it"
unfolding set_iterator_def set_iterator_map_rev_linord_def
apply (erule set_iterator_genord.set_iterator_weaken_R)
..

context StdBasicMap
begin
lemma g_sng_impl: "map_sng α invar g_sng"
apply unfold_locales
apply (simp_all add: update_correct empty_correct g_sng_def)
done

proof
fix m1 m2
assume "invar m1" "invar m2"

have "α (g_add m1 m2) = α m1 ++ α m2 ∧ invar (g_add m1 m2)"
unfolding A
apply (rule
iterate_add_to_map_correct[of α invar update m1 "iteratei m2" "α m2"])
apply unfold_locales []
apply fact
apply (rule iteratei_correct, fact)
done
thus "α (g_add m1 m2) = α m1 ++ α m2" "invar (g_add m1 m2)" by auto
qed

lemma g_sel_impl: "map_sel' α invar g_sel"
proof -
have A: "⋀m P. g_sel m P = iterate_sel_no_map (iteratei m) P"
unfolding g_sel_def iterate_sel_no_map_def iterate_sel_def by simp

{ fix m P
assume I: "invar m"
note iterate_sel_no_map_correct[OF iteratei_correct[OF I], of P]
}
thus ?thesis
apply unfold_locales
unfolding A
apply (simp add: Bex_def Ball_def image_iff map_to_set_def)
apply clarify
apply (metis option.exhaust prod.exhaust)
apply (simp add: Bex_def Ball_def image_iff map_to_set_def)
done
qed

lemma g_bex_impl: "map_bex α invar g_bex"
apply unfold_locales
unfolding g_bex_def
apply (rule_tac I="λit σ. σ ⟷ (∃kv∈it. P kv)"
in iteratei_rule_insert_P)
by (auto simp: map_to_set_def)

lemma g_ball_impl: "map_ball α invar g_ball"
apply unfold_locales
unfolding g_ball_def
apply (rule_tac I="λit σ. σ ⟷ (∀kv∈it. P kv)"
in iteratei_rule_insert_P)
apply (auto simp: map_to_set_def)
done

lemma g_size_impl: "map_size α invar g_size"
proof
fix m
assume I: "invar m"
have A: "g_size m ≡ iterate_size (iteratei m)"
unfolding g_size_def iterate_size_def by simp

from iterate_size_correct [OF iteratei_correct[OF I]]
show "g_size m = card (dom (α m))"
unfolding A
qed

lemma g_size_abort_impl: "map_size_abort α invar g_size_abort"
proof
fix s m
assume I: "invar m"
have A: "g_size_abort s m ≡ iterate_size_abort (iteratei m) s"
unfolding g_size_abort_def iterate_size_abort_def by simp

from iterate_size_abort_correct [OF iteratei_correct[OF I]]
show "g_size_abort s m = min s (card (dom (α m)))"
unfolding A
qed

lemma g_isEmpty_impl: "map_isEmpty α invar g_isEmpty"
proof
fix m
assume I: "invar m"
interpret map_size_abort α invar g_size_abort by (rule g_size_abort_impl)
from size_abort_correct[OF I] have
"g_size_abort 1 m = min 1 (card (dom (α m)))" .
thus "g_isEmpty m = (α m = Map.empty)" unfolding g_isEmpty_def
by (auto simp: min_def card_0_eq[OF finite] I)
qed

lemma g_isSng_impl: "map_isSng α invar g_isSng"
proof
fix m
assume I: "invar m"
interpret map_size_abort α invar g_size_abort by (rule g_size_abort_impl)
from size_abort_correct[OF I] have
"g_size_abort 2 m = min 2 (card (dom (α m)))" .
thus "g_isSng m = (∃k v. α m = [k ↦ v])" unfolding g_isSng_def
by (auto simp: min_def I card_Suc_eq dom_eq_singleton_conv)
qed

lemma g_to_list_impl: "map_to_list α invar g_to_list"
proof
fix m
assume I: "invar m"

have A: "g_to_list m = iterate_to_list (iteratei m)"
unfolding g_to_list_def iterate_to_list_def by simp

from iterate_to_list_correct [OF iteratei_correct[OF I]]
have set_l_eq: "set (g_to_list m) = map_to_set (α m)" and
dist_l: "distinct (g_to_list m)" unfolding A by simp_all

from dist_l show dist_fst_l: "distinct (map fst (g_to_list m))"
by (simp add: distinct_map set_l_eq map_to_set_def inj_on_def)

from map_of_map_to_set[of "(g_to_list m)" "α m", OF dist_fst_l] set_l_eq
show "map_of (g_to_list m) = α m" by simp
qed

lemma g_list_to_map_impl: "list_to_map α invar g_list_to_map"
proof -
{
fix m0 l
assume "invar m0"
hence "invar (foldl (λs (k,v). update k v s) m0 l) ∧
α (foldl (λs (k,v). update k v s) m0 l) = α m0 ++ map_of (rev l)"
proof (induction l arbitrary: m0)
case Nil thus ?case by simp
next
case (Cons kv l)
obtain k v where [simp]: "kv=(k,v)" by (cases kv) auto
have "invar (foldl (λs (k, v). update k v s) m0 (kv # l))"
apply simp
apply (rule conjunct1[OF Cons.IH])
done
moreover have "α (foldl (λs (k, v). update k v s) m0 (kv # l)) =
α m0 ++ map_of (rev (kv # l))"
apply simp
apply (rule trans[OF conjunct2[OF Cons.IH]])
apply (auto
split: option.split
)
done
ultimately show ?case
by simp
qed
} thus ?thesis
apply unfold_locales
unfolding g_list_to_map_def
apply (auto simp: empty_correct)
done
qed

proof
fix m1 m2
assume "invar m1" "invar m2" and DJ: "dom (α m1) ∩ dom (α m2) = {}"

have "α (g_add_dj m1 m2) = α m1 ++ α m2 ∧ invar (g_add_dj m1 m2)"
unfolding A
apply (rule
of α invar update_dj m1 "iteratei m2" "α m2"])
apply unfold_locales []
apply fact
apply (rule iteratei_correct, fact)
using DJ apply (simp add: Int_ac)
done
thus "α (g_add_dj m1 m2) = α m1 ++ α m2" "invar (g_add_dj m1 m2)" by auto
qed

lemma g_restrict_impl: "map_restrict α invar α invar g_restrict"
proof
fix m P
assume I: "invar m"

have AUX: "⋀k v it σ.
⟦it ⊆ {(k, v). α m k = Some v}; α m k = Some v; (k, v) ∉ it;
{(k, v). α σ k = Some v} = it ∩ Collect P⟧
⟹ k ∉ dom (α σ)"
proof (rule ccontr, simp)
fix k v it σ
assume "k∈dom (α σ)"
then obtain v' where "α σ k = Some v'" by auto
moreover assume "{(k, v). α σ k = Some v} = it ∩ Collect P"
ultimately have MEM: "(k,v')∈it" by auto
moreover assume "it ⊆ {(k, v). α m k = Some v}" and "α m k = Some v"
ultimately have "v'=v" by auto
moreover assume "(k,v)∉it"
moreover note MEM
ultimately show False by simp
qed

have "α (g_restrict P m) = α m | {k. ∃v. α m k = Some v ∧ P (k, v)} ∧
invar (g_restrict P m)"
unfolding g_restrict_def
apply (rule_tac I="λit σ. invar σ
∧ map_to_set (α σ) = it ∩ Collect P"
in iterate_rule_insert_P)
apply (auto simp: I empty_correct update_dj_correct map_to_set_def AUX)
apply (auto split: if_split_asm)
apply (rule ext)
apply (auto simp: Map.restrict_map_def)
apply force
apply (rule ccontr)
apply force
done
thus "α (g_restrict P m) = α m | {k. ∃v. α m k = Some v ∧ P (k, v)}"
"invar (g_restrict P m)" by auto
qed

lemma dflt_ops_impl: "StdMap dflt_ops"
apply (rule StdMap_intro)
apply icf_locales
g_isEmpty_impl g_isSng_impl g_ball_impl g_bex_impl g_size_impl
g_size_abort_impl g_sel_impl g_to_list_impl g_list_to_map_impl)+
done
end

context StdBasicOMapDefs
begin
definition
"g_min m P ≡
iterateoi m (λσ. σ = None) (λx σ. if P x then Some x else None) None"

definition
"g_max m P ≡
rev_iterateoi m (λσ. σ = None) (λx σ. if P x then Some x else None) None"

definition "g_to_sorted_list m ≡ rev_iterateo m (#) []"
definition "g_to_rev_list m ≡ iterateo m (#) []"

definition dflt_oops :: "('k,'v,'s) omap_ops"
where [icf_rec_def]:
"dflt_oops ≡ map_ops.extend dflt_ops
⦇
map_op_ordered_list_it = ordered_list_it,
map_op_rev_list_it = rev_list_it,
map_op_min = g_min,
map_op_max = g_max,
map_op_to_sorted_list = g_to_sorted_list,
map_op_to_rev_list = g_to_rev_list
⦈"
local_setup ‹Locale_Code.lc_decl_del @{term dflt_oops}›

end

context StdBasicOMap
begin
lemma g_min_impl: "map_min α invar g_min"
proof
fix m P

assume I: "invar m"

from iterateoi_correct[OF I]
have iti': "map_iterator_linord (iterateoi m) (α m)" by simp
note sel_correct = iterate_sel_no_map_map_linord_correct[OF iti', of P]

have A: "g_min m P = iterate_sel_no_map (iterateoi m) P"
unfolding g_min_def iterate_sel_no_map_def iterate_sel_def by simp

{ assume "rel_of (α m) P ≠ {}"
with sel_correct
show "g_min m P ∈ Some  rel_of (α m) P"
unfolding A
by (auto simp add: image_iff rel_of_def)
}

{ assume "rel_of (α m) P = {}"
with sel_correct show "g_min m P = None"
unfolding A
by (auto simp add: image_iff rel_of_def)
}

{ fix k v
assume "(k, v) ∈ rel_of (α m) P"
with sel_correct show "fst (the (g_min m P)) ≤ k"
unfolding A
by (auto simp add: image_iff rel_of_def)
}
qed

lemma g_max_impl: "map_max α invar g_max"
proof
fix m P

assume I: "invar m"

from rev_iterateoi_correct[OF I]
have iti': "map_iterator_rev_linord (rev_iterateoi m) (α m)" by simp
note sel_correct = iterate_sel_no_map_map_rev_linord_correct[OF iti', of P]

have A: "g_max m P = iterate_sel_no_map (rev_iterateoi m) P"
unfolding g_max_def iterate_sel_no_map_def iterate_sel_def by simp

{ assume "rel_of (α m) P ≠ {}"
with sel_correct
show "g_max m P ∈ Some  rel_of (α m) P"
unfolding A
by (auto simp add: image_iff rel_of_def)
}

{ assume "rel_of (α m) P = {}"
with sel_correct show "g_max m P = None"
unfolding A
by (auto simp add: image_iff rel_of_def)
}

{ fix k v
assume "(k, v) ∈ rel_of (α m) P"
with sel_correct show "fst (the (g_max m P)) ≥ k"
unfolding A
by (auto simp add: image_iff rel_of_def)
}
qed

lemma g_to_sorted_list_impl: "map_to_sorted_list α invar g_to_sorted_list"
proof
fix m
assume I: "invar m"
note iti = rev_iterateoi_correct[OF I]
from iterate_to_list_map_rev_linord_correct[OF iti]
show "sorted (map fst (g_to_sorted_list m))"
"distinct (map fst (g_to_sorted_list m))"
"map_of (g_to_sorted_list m) = α m"
unfolding g_to_sorted_list_def iterate_to_list_def by simp_all
qed

lemma g_to_rev_list_impl: "map_to_rev_list α invar g_to_rev_list"
proof
fix m
assume I: "invar m"
note iti = iterateoi_correct[OF I]
from iterate_to_list_map_linord_correct[OF iti]
show "sorted (rev (map fst (g_to_rev_list m)))"
"distinct (map fst (g_to_rev_list m))"
"map_of (g_to_rev_list m) = α m"
unfolding g_to_rev_list_def iterate_to_list_def
qed

lemma dflt_oops_impl: "StdOMap dflt_oops"
proof -
interpret aux: StdMap dflt_ops by (rule dflt_ops_impl)

show ?thesis
apply (rule StdOMap_intro)
apply icf_locales
apply (rule g_min_impl)
apply (rule g_max_impl)
apply (rule g_to_sorted_list_impl)
apply (rule g_to_rev_list_impl)
done
qed

end

locale g_image_filter_defs_loc =
m1: StdMapDefs ops1 +
m2: StdMapDefs ops2
for ops1 :: "('k1,'v1,'s1,'m1) map_ops_scheme"
and ops2 :: "('k2,'v2,'s2,'m2) map_ops_scheme"
begin
definition "g_image_filter f m1 ≡ m1.iterate m1 (λkv σ. case f kv of
None => σ
| Some (k',v') => m2.update_dj k' v' σ
) (m2.empty ())"
end

locale g_image_filter_loc = g_image_filter_defs_loc ops1 ops2 +
m1: StdMap ops1 +
m2: StdMap ops2
for ops1 :: "('k1,'v1,'s1,'m1) map_ops_scheme"
and ops2 :: "('k2,'v2,'s2,'m2) map_ops_scheme"
begin
lemma g_image_filter_impl:
"map_image_filter m1.α m1.invar m2.α m2.invar g_image_filter"
proof
fix m k' v' and f :: "('k1 × 'v1) ⇒ ('k2 × 'v2) option"
assume invar_m: "m1.invar m" and
unique_f: "transforms_to_unique_keys (m1.α m) f"

have A: "g_image_filter f m =
iterate_to_map m2.empty m2.update_dj (
set_iterator_image_filter f (m1.iteratei m))"
unfolding g_image_filter_def iterate_to_map_alt_def
set_iterator_image_filter_def case_prod_beta
by simp

from m1.iteratei_correct[OF invar_m]
have iti_m: "map_iterator (m1.iteratei m) (m1.α m)" by simp

from unique_f have inj_on_f: "inj_on f (map_to_set (m1.α m) ∩ dom f)"
unfolding transforms_to_unique_keys_def inj_on_def Ball_def map_to_set_def
by auto (metis option.inject)

define vP where "vP k v ⟷ (∃k' v'. m1.α m k' = Some v' ∧ f (k', v') = Some (k, v))" for k v
have vP_intro: "⋀k v. (∃k' v'. m1.α m k' = Some v'
∧ f (k', v') = Some (k, v)) ⟷ vP k v"
unfolding vP_def by simp
{ fix k v
have "Eps_Opt (vP k) = Some v ⟷ vP k v"
using unique_f unfolding vP_def transforms_to_unique_keys_def
apply (rule_tac Eps_Opt_eq_Some)
apply (metis prod.inject option.inject)
done
} note Eps_vP_elim[simp] = this
have map_intro: "{y. ∃x. x ∈ map_to_set (m1.α m) ∧ f x = Some y}
= map_to_set (λk. Eps_Opt (vP k))"
by (simp add: map_to_set_def vP_intro set_eq_iff split: prod.splits)

from set_iterator_image_filter_correct [OF iti_m, OF inj_on_f,
unfolded map_intro]
have iti_filter: "map_iterator (set_iterator_image_filter f (m1.iteratei m))
(λk. Eps_Opt (vP k))" by auto

have upd: "map_update_dj m2.α m2.invar m2.update_dj" by unfold_locales
have emp: "map_empty m2.α m2.invar m2.empty" by unfold_locales

from iterate_to_map_correct[OF upd emp iti_filter] show
"map_op_invar ops2 (g_image_filter f m) ∧
(map_op_α ops2 (g_image_filter f m) k' = Some v') =
(∃k v. map_op_α ops1 m k = Some v ∧ f (k, v) = Some (k', v'))"
unfolding A vP_def[symmetric]

qed
end

sublocale g_image_filter_loc
< map_image_filter m1.α m1.invar m2.α m2.invar g_image_filter
by (rule g_image_filter_impl)

locale g_value_image_filter_defs_loc =
m1: StdMapDefs ops1 +
m2: StdMapDefs ops2
for ops1 :: "('k,'v1,'s1,'m1) map_ops_scheme"
and ops2 :: "('k,'v2,'s2,'m2) map_ops_scheme"
begin
definition "g_value_image_filter f m1 ≡ m1.iterate m1 (λ(k,v) σ.
case f k v of
None => σ
| Some v' => m2.update_dj k v' σ
) (m2.empty ())"

end

(* TODO: Move to Misc *)
lemma restrict_map_dom_subset: "⟦ dom m ⊆ R⟧ ⟹ m|R = m"
apply (rule ext)
apply (auto simp: restrict_map_def)
apply (case_tac "m x")
apply auto
done

locale g_value_image_filter_loc = g_value_image_filter_defs_loc ops1 ops2 +
m1: StdMap ops1 +
m2: StdMap ops2
for ops1 :: "('k,'v1,'s1,'m1) map_ops_scheme"
and ops2 :: "('k,'v2,'s2,'m2) map_ops_scheme"
begin
lemma g_value_image_filter_impl:
"map_value_image_filter m1.α m1.invar m2.α m2.invar g_value_image_filter"
apply unfold_locales
unfolding g_value_image_filter_def
apply (rule_tac I="λit σ. m2.invar σ
∧ m2.α σ = (λk. Option.bind (map_op_α ops1 m k) (f k)) | it"
in m1.old_iterate_rule_insert_P)

apply auto []
apply (auto simp: m2.empty_correct) []
defer
apply simp []
apply (rule restrict_map_dom_subset)
apply (auto) []
apply (case_tac "m1.α m x")
apply (auto) [2]

apply (auto split: option.split simp: m2.update_dj_correct intro!: ext)
apply (auto simp: restrict_map_def)
done
end

sublocale g_value_image_filter_loc
< map_value_image_filter m1.α m1.invar m2.α m2.invar g_value_image_filter
by (rule g_value_image_filter_impl)

end