header {* \isaheader{Specification of Maps} *}
theory MapSpec
imports ICF_Spec_Base
begin
text_raw{*\label{thy:MapSpec}*}
text {*
This theory specifies map operations by means of mapping to
HOL's map type, i.e. @{typ "'k \<rightharpoonup> 'v"}.
*}
type_synonym ('k,'v,'s) map_α = "'s => 'k \<rightharpoonup> 'v"
type_synonym ('k,'v,'s) map_invar = "'s => bool"
locale map =
fixes α :: "'s => 'u \<rightharpoonup> 'v" -- "Abstraction to map datatype"
fixes invar :: "'s => bool" -- "Invariant"
locale map_no_invar = map +
assumes invar[simp, intro!]: "!!s. invar s"
subsection "Basic Map Functions"
subsubsection "Empty Map"
type_synonym ('k,'v,'s) map_empty = "unit => 's"
locale map_empty = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes empty :: "unit => 's"
assumes empty_correct:
"α (empty ()) = Map.empty"
"invar (empty ())"
subsubsection "Lookup"
type_synonym ('k,'v,'s) map_lookup = "'k => 's => 'v option"
locale map_lookup = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes lookup :: "'u => 's => 'v option"
assumes lookup_correct:
"invar m ==> lookup k m = α m k"
subsubsection "Update"
type_synonym ('k,'v,'s) map_update = "'k => 'v => 's => 's"
locale map_update = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes update :: "'u => 'v => 's => 's"
assumes update_correct:
"invar m ==> α (update k v m) = (α m)(k \<mapsto> v)"
"invar m ==> invar (update k v m)"
subsubsection "Disjoint Update"
type_synonym ('k,'v,'s) map_update_dj = "'k => 'v => 's => 's"
locale map_update_dj = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes update_dj :: "'u => 'v => 's => 's"
assumes update_dj_correct:
"[|invar m; k∉dom (α m)|] ==> α (update_dj k v m) = (α m)(k \<mapsto> v)"
"[|invar m; k∉dom (α m)|] ==> invar (update_dj k v m)"
subsubsection "Delete"
type_synonym ('k,'v,'s) map_delete = "'k => 's => 's"
locale map_delete = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes delete :: "'u => 's => 's"
assumes delete_correct:
"invar m ==> α (delete k m) = (α m) |` (-{k})"
"invar m ==> invar (delete k m)"
subsubsection "Add"
type_synonym ('k,'v,'s) map_add = "'s => 's => 's"
locale map_add = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes add :: "'s => 's => 's"
assumes add_correct:
"invar m1 ==> invar m2 ==> α (add m1 m2) = α m1 ++ α m2"
"invar m1 ==> invar m2 ==> invar (add m1 m2)"
type_synonym ('k,'v,'s) map_add_dj = "'s => 's => 's"
locale map_add_dj = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes add_dj :: "'s => 's => 's"
assumes add_dj_correct:
"[|invar m1; invar m2; dom (α m1) ∩ dom (α m2) = {}|] ==> α (add_dj m1 m2) = α m1 ++ α m2"
"[|invar m1; invar m2; dom (α m1) ∩ dom (α m2) = {} |] ==> invar (add_dj m1 m2)"
subsubsection "Emptiness Check"
type_synonym ('k,'v,'s) map_isEmpty = "'s => bool"
locale map_isEmpty = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes isEmpty :: "'s => bool"
assumes isEmpty_correct : "invar m ==> isEmpty m <-> α m = Map.empty"
subsubsection "Singleton Maps"
type_synonym ('k,'v,'s) map_sng = "'k => 'v => 's"
locale map_sng = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes sng :: "'u => 'v => 's"
assumes sng_correct :
"α (sng k v) = [k \<mapsto> v]"
"invar (sng k v)"
type_synonym ('k,'v,'s) map_isSng = "'s => bool"
locale map_isSng = map +
constrains α :: "'s => 'k \<rightharpoonup> 'v"
fixes isSng :: "'s => bool"
assumes isSng_correct:
"invar s ==> isSng s <-> (∃k v. α s = [k \<mapsto> v])"
begin
lemma isSng_correct_exists1 :
"invar s ==> (isSng s <-> (∃!k. ∃v. (α s k = Some v)))"
apply (auto simp add: isSng_correct split: split_if_asm)
apply (rule_tac x=k in exI)
apply (rule_tac x=v in exI)
apply (rule ext)
apply (case_tac "α s x")
apply auto
apply force
done
lemma isSng_correct_card :
"invar s ==> (isSng s <-> (card (dom (α s)) = 1))"
by (auto simp add: isSng_correct card_Suc_eq dom_eq_singleton_conv)
end
subsubsection "Finite Maps"
locale finite_map = map +
assumes finite[simp, intro!]: "invar m ==> finite (dom (α m))"
subsubsection "Size"
type_synonym ('k,'v,'s) map_size = "'s => nat"
locale map_size = finite_map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes size :: "'s => nat"
assumes size_correct: "invar s ==> size s = card (dom (α s))"
type_synonym ('k,'v,'s) map_size_abort = "nat => 's => nat"
locale map_size_abort = finite_map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes size_abort :: "nat => 's => nat"
assumes size_abort_correct: "invar s ==> size_abort m s = min m (card (dom (α s)))"
subsubsection "Iterators"
text {*
An iteration combinator over a map applies a function to a state for each
map entry, in arbitrary order.
Proving of properties is done by invariant reasoning.
An iterator can also contain a continuation condition. Iteration is
interrupted if the condition becomes false.
*}
type_synonym ('k,'v,'s) map_list_it
= "'s => ('k×'v,('k×'v) list) set_iterator"
locale poly_map_iteratei_defs =
fixes list_it :: "'s => ('u×'v,('u×'v) list) set_iterator"
begin
definition iteratei :: "'s => ('u×'v,'σ) set_iterator"
where "iteratei S ≡ it_to_it (list_it S)"
abbreviation "iterate m ≡ iteratei m (λ_. True)"
end
locale poly_map_iteratei =
finite_map + poly_map_iteratei_defs list_it
for list_it :: "'s => ('u×'v,('u×'v) list) set_iterator" +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
assumes list_it_correct: "invar m ==> map_iterator (list_it m) (α m)"
begin
lemma iteratei_correct: "invar S ==> map_iterator (iteratei S) (α S)"
unfolding iteratei_def
apply (rule it_to_it_correct)
by (rule list_it_correct)
lemma pi_iteratei[icf_proper_iteratorI]:
"proper_it (iteratei S) (iteratei S)"
unfolding iteratei_def
by (intro icf_proper_iteratorI)
lemma iteratei_rule_P:
assumes "invar m"
and I0: "I (map_to_set (α m)) σ0"
and IP: "!!k v it σ. [| c σ; (k,v) ∈ it; it ⊆ map_to_set (α m); I it σ |]
==> I (it - {(k,v)}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ==> P σ"
and II: "!!σ it. [| it ⊆ map_to_set (α m); it ≠ {}; ¬ c σ; I it σ |] ==> P σ"
shows "P (iteratei m c f σ0)"
apply (rule set_iterator_rule_P[OF iteratei_correct])
apply fact
apply fact
apply (case_tac x, simp add: IP)
apply fact
apply fact
done
lemma iteratei_rule_insert_P:
assumes "invar m"
and "I {} σ0"
and "!!k v it σ. [| c σ; (k,v) ∈ (map_to_set (α m) - it);
it ⊆ map_to_set (α m); I it σ |]
==> I (insert (k,v) it) (f (k, v) σ)"
and "!!σ. I (map_to_set (α m)) σ ==> P σ"
and "!!σ it. [| it ⊆ map_to_set (α m); it ≠ map_to_set (α m);
¬ (c σ);
I it σ |] ==> P σ"
shows "P (iteratei m c f σ0)"
apply (rule set_iterator_rule_insert_P[OF iteratei_correct])
apply fact
apply fact
apply (case_tac x, simp add: assms)
apply fact
apply fact
done
lemma iterate_rule_P:
assumes "invar m"
and I0: "I (map_to_set (α m)) σ0"
and IP: "!!k v it σ. [| (k,v) ∈ it; it ⊆ map_to_set (α m); I it σ |]
==> I (it - {(k,v)}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ==> P σ"
shows "P (iterate m f σ0)"
apply (rule iteratei_rule_P)
apply fact
apply (rule I0)
apply (rule IP, assumption+) []
apply (rule IF, assumption)
apply simp
done
lemma iterate_rule_insert_P:
assumes "invar m"
and I0: "I {} σ0"
and "!!k v it σ. [| (k,v) ∈ (map_to_set (α m) - it);
it ⊆ map_to_set (α m); I it σ |]
==> I (insert (k,v) it) (f (k, v) σ)"
and "!!σ. I (map_to_set (α m)) σ ==> P σ"
shows "P (iterate m f σ0)"
apply (rule iteratei_rule_insert_P)
apply fact
apply (rule I0)
apply (rule assms, assumption+) []
apply (rule assms, assumption)
apply simp
done
lemma old_iteratei_rule_P:
assumes "invar m"
and I0: "I (dom (α m)) σ0"
and IP: "!!k v it σ. [| c σ; k ∈ it; α m k = Some v; it ⊆ dom (α m); I it σ |]
==> I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ==> P σ"
and II: "!!σ it. [| it ⊆ dom (α m); it ≠ {}; ¬ c σ; I it σ |] ==> P σ"
shows "P (iteratei m c f σ0)"
using assms
by (rule map_iterator_rule_P[OF iteratei_correct])
lemma old_iteratei_rule_insert_P:
assumes "invar m"
and "I {} σ0"
and "!!k v it σ. [| c σ; k ∈ (dom (α m) - it); α m k = Some v;
it ⊆ dom (α m); I it σ |]
==> I (insert k it) (f (k, v) σ)"
and "!!σ. I (dom (α m)) σ ==> P σ"
and "!!σ it. [| it ⊆ dom (α m); it ≠ dom (α m);
¬ (c σ);
I it σ |] ==> P σ"
shows "P (iteratei m c f σ0)"
using assms by (rule map_iterator_rule_insert_P[OF iteratei_correct])
lemma old_iterate_rule_P:
"[|
invar m;
I (dom (α m)) σ0;
!!k v it σ. [| k ∈ it; α m k = Some v; it ⊆ dom (α m); I it σ |]
==> I (it - {k}) (f (k, v) σ);
!!σ. I {} σ ==> P σ
|] ==> P (iterate m f σ0)"
using old_iteratei_rule_P [of m I σ0 "λ_. True" f P]
by blast
lemma old_iterate_rule_insert_P:
"[|
invar m;
I {} σ0;
!!k v it σ. [| k ∈ (dom (α m) - it); α m k = Some v;
it ⊆ dom (α m); I it σ |]
==> I (insert k it) (f (k, v) σ);
!!σ. I (dom (α m)) σ ==> P σ
|] ==> P (iteratei m (λ_. True) f σ0)"
using old_iteratei_rule_insert_P [of m I σ0 "λ_. True" f P]
by blast
end
subsubsection "Bounded Quantification"
type_synonym ('k,'v,'s) map_ball = "'s => ('k × 'v => bool) => bool"
locale map_ball = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes ball :: "'s => ('u × 'v => bool) => bool"
assumes ball_correct: "invar m ==> ball m P <-> (∀u v. α m u = Some v --> P (u, v))"
type_synonym ('k,'v,'s) map_bex = "'s => ('k × 'v => bool) => bool"
locale map_bex = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes bex :: "'s => ('u × 'v => bool) => bool"
assumes bex_correct:
"invar m ==> bex m P <-> (∃u v. α m u = Some v ∧ P (u, v))"
subsubsection "Selection of Entry"
type_synonym ('k,'v,'s,'r) map_sel = "'s => ('k × 'v => 'r option) => 'r option"
locale map_sel = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes sel :: "'s => ('u × 'v => 'r option) => 'r option"
assumes selE:
"[| invar m; α m u = Some v; f (u, v) = Some r;
!!u v r. [| sel m f = Some r; α m u = Some v; f (u, v) = Some r |] ==> Q
|] ==> Q"
assumes selI:
"[| invar m; ∀u v. α m u = Some v --> f (u, v) = None |] ==> sel m f = None"
begin
lemma sel_someE:
"[| invar m; sel m f = Some r;
!!u v. [| α m u = Some v; f (u, v) = Some r |] ==> P
|] ==> P"
apply (cases "∃u v r. α m u = Some v ∧ f (u, v) = Some r")
apply safe
apply (erule_tac u=u and v=v and r=ra in selE)
apply assumption
apply assumption
apply simp
apply (auto)
apply (drule (1) selI)
apply simp
done
lemma sel_noneD: "[|invar m; sel m f = None; α m u = Some v|] ==> f (u, v) = None"
apply (rule ccontr)
apply simp
apply (erule exE)
apply (erule_tac f=f and u=u and v=v and r=y in selE)
apply auto
done
end
-- "Equivalent description of sel-map properties"
lemma map_sel_altI:
assumes S1:
"!!s f r P. [| invar s; sel s f = Some r;
!!u v. [|α s u = Some v; f (u, v) = Some r|] ==> P
|] ==> P"
assumes S2:
"!!s f u v. [|invar s; sel s f = None; α s u = Some v|] ==> f (u, v) = None"
shows "map_sel α invar sel"
proof -
show ?thesis
apply (unfold_locales)
apply (case_tac "sel m f")
apply (force dest: S2)
apply (force elim: S1)
apply (case_tac "sel m f")
apply assumption
apply (force elim: S1)
done
qed
subsubsection "Selection of Entry (without mapping)"
type_synonym ('k,'v,'s) map_sel' = "'s => ('k × 'v => bool) => ('k×'v) option"
locale map_sel' = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes sel' :: "'s => ('u × 'v => bool) => ('u×'v) option"
assumes sel'E:
"[| invar m; α m u = Some v; P (u, v);
!!u v. [| sel' m P = Some (u,v); α m u = Some v; P (u, v)|] ==> Q
|] ==> Q"
assumes sel'I:
"[| invar m; ∀u v. α m u = Some v --> ¬ P (u, v) |] ==> sel' m P = None"
begin
lemma sel'_someE:
"[| invar m; sel' m P = Some (u,v);
!!u v. [| α m u = Some v; P (u, v) |] ==> thesis
|] ==> thesis"
apply (cases "∃u v. α m u = Some v ∧ P (u, v)")
apply safe
apply (erule_tac u=ua and v=va in sel'E)
apply assumption
apply assumption
apply simp
apply (auto)
apply (drule (1) sel'I)
apply simp
done
lemma sel'_noneD: "[|invar m; sel' m P = None; α m u = Some v|] ==> ¬ P (u, v)"
apply (rule ccontr)
apply simp
apply (erule (2) sel'E[where P=P])
apply auto
done
lemma sel'_SomeD:
"[| sel' m P = Some (u, v); invar m |] ==> α m u = Some v ∧ P (u, v)"
apply(cases "∃u' v'. α m u' = Some v' ∧ P (u', v')")
apply clarsimp
apply(erule (2) sel'E[where P=P])
apply simp
apply(clarsimp)
apply(drule (1) sel'I)
apply simp
done
end
subsubsection "Map to List Conversion"
type_synonym ('k,'v,'s) map_to_list = "'s => ('k×'v) list"
locale map_to_list = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes to_list :: "'s => ('u×'v) list"
assumes to_list_correct:
"invar m ==> map_of (to_list m) = α m"
"invar m ==> distinct (map fst (to_list m))"
subsubsection "List to Map Conversion"
type_synonym ('k,'v,'s) list_to_map = "('k×'v) list => 's"
locale list_to_map = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes to_map :: "('u×'v) list => 's"
assumes to_map_correct:
"α (to_map l) = map_of l"
"invar (to_map l)"
subsubsection "Image of a Map"
text {* This locale allows to apply a function to both the keys and
the values of a map while at the same time filtering entries. *}
definition transforms_to_unique_keys ::
"('u1 \<rightharpoonup> 'v1) => ('u1 × 'v1 \<rightharpoonup> ('u2 × 'v2)) => bool"
where
"transforms_to_unique_keys m f ≡ (∀k1 k2 v1 v2 k' v1' v2'. (
m k1 = Some v1 ∧
m k2 = Some v2 ∧
f (k1, v1) = Some (k', v1') ∧
f (k2, v2) = Some (k', v2')) -->
(k1 = k2))"
type_synonym ('k1,'v1,'m1,'k2,'v2,'m2) map_image_filter
= "('k1 × 'v1 => ('k2 × 'v2) option) => 'm1 => 'm2"
locale map_image_filter = m1!: map α1 invar1 + m2!: map α2 invar2
for α1 :: "'m1 => 'u1 \<rightharpoonup> 'v1" and invar1
and α2 :: "'m2 => 'u2 \<rightharpoonup> 'v2" and invar2
+
fixes map_image_filter :: "('u1 × 'v1 => ('u2 × 'v2) option) => 'm1 => 'm2"
assumes map_image_filter_correct_aux1:
"!!k' v'.
[|invar1 m; transforms_to_unique_keys (α1 m) f|] ==>
(invar2 (map_image_filter f m) ∧
((α2 (map_image_filter f m) k' = Some v') <->
(∃k v. (α1 m k = Some v) ∧ f (k, v) = Some (k', v'))))"
begin
lemma map_image_filter_correct_aux2 :
assumes "invar1 m"
and "transforms_to_unique_keys (α1 m) f"
shows "(α2 (map_image_filter f m) k' = None) <->
(∀k v v'. α1 m k = Some v --> f (k, v) ≠ Some (k', v'))"
proof -
note map_image_filter_correct_aux1 [OF assms]
have Some_eq: "!!v'. (α2 (map_image_filter f m) k' = Some v') =
(∃k v. α1 m k = Some v ∧ f (k, v) = Some (k', v'))"
by (simp add: map_image_filter_correct_aux1 [OF assms])
have intro_some: "(α2 (map_image_filter f m) k' = None) <->
(∀v'. α2 (map_image_filter f m) k' ≠ Some v')" by auto
from intro_some Some_eq show ?thesis by auto
qed
lemmas map_image_filter_correct =
conjunct1 [OF map_image_filter_correct_aux1]
conjunct2 [OF map_image_filter_correct_aux1]
map_image_filter_correct_aux2
end
text {* Most of the time the mapping function is only applied to values. Then,
the precondition disapears.*}
type_synonym ('k,'v1,'m1,'k2,'v2,'m2) map_value_image_filter
= "('k => 'v1 => 'v2 option) => 'm1 => 'm2"
locale map_value_image_filter = m1!: map α1 invar1 + m2!: map α2 invar2
for α1 :: "'m1 => 'u \<rightharpoonup> 'v1" and invar1
and α2 :: "'m2 => 'u \<rightharpoonup> 'v2" and invar2
+
fixes map_value_image_filter :: "('u => 'v1 => 'v2 option) => 'm1 => 'm2"
assumes map_value_image_filter_correct_aux:
"invar1 m ==>
invar2 (map_value_image_filter f m) ∧
(α2 (map_value_image_filter f m) =
(λk. Option.bind (α1 m k) (f k)))"
begin
lemmas map_value_image_filter_correct =
conjunct1[OF map_value_image_filter_correct_aux]
conjunct2[OF map_value_image_filter_correct_aux]
lemma map_value_image_filter_correct_alt :
"invar1 m ==>
invar2 (map_value_image_filter f m)"
"invar1 m ==>
(α2 (map_value_image_filter f m) k = Some v') <->
(∃v. (α1 m k = Some v) ∧ f k v = Some v')"
"invar1 m ==>
(α2 (map_value_image_filter f m) k = None) <->
(∀v. (α1 m k = Some v) --> f k v = None)"
proof -
assume invar_m : "invar1 m"
note aux = map_value_image_filter_correct_aux [OF invar_m]
from aux show "invar2 (map_value_image_filter f m)" by simp
from aux show "(α2 (map_value_image_filter f m) k = Some v') <->
(∃v. (α1 m k = Some v) ∧ f k v = Some v')"
by (cases "α1 m k", simp_all)
from aux show "(α2 (map_value_image_filter f m) k = None) <->
(∀v. (α1 m k = Some v) --> f k v = None)"
by (cases "α1 m k", simp_all)
qed
end
type_synonym ('k,'v,'m1,'m2) map_restrict = "('k × 'v => bool) => 'm1 => 'm2"
locale map_restrict = m1!: map α1 invar1 + m2!: map α2 invar2
for α1 :: "'m1 => 'u \<rightharpoonup> 'v" and invar1
and α2 :: "'m2 => 'u \<rightharpoonup> 'v" and invar2
+
fixes restrict :: "('u × 'v => bool) => 'm1 => 'm2"
assumes restrict_correct_aux1 :
"invar1 m ==> α2 (restrict P m) = α1 m |` {k. ∃v. α1 m k = Some v ∧ P (k, v)}"
"invar1 m ==> invar2 (restrict P m)"
begin
lemma restrict_correct_aux2 :
"invar1 m ==> α2 (restrict (λ(k,_). P k) m) = α1 m |` {k. P k}"
proof -
assume invar_m : "invar1 m"
have "α1 m |` {k. (∃v. α1 m k = Some v) ∧ P k} = α1 m |` {k. P k}"
(is "α1 m |` ?A1 = α1 m |` ?A2")
proof
fix k
show "(α1 m |` ?A1) k = (α1 m |` ?A2) k"
proof (cases "k ∈ ?A2")
case False thus ?thesis by simp
next
case True
hence P_k : "P k" by simp
show ?thesis
by (cases "α1 m k", simp_all add: P_k)
qed
qed
with invar_m show "α2 (restrict (λ(k, _). P k) m) = α1 m |` {k. P k}"
by (simp add: restrict_correct_aux1)
qed
lemmas restrict_correct =
restrict_correct_aux1
restrict_correct_aux2
end
subsection "Ordered Maps"
locale ordered_map = map α invar
for α :: "'s => ('u::linorder) \<rightharpoonup> 'v" and invar
locale ordered_finite_map = finite_map α invar + ordered_map α invar
for α :: "'s => ('u::linorder) \<rightharpoonup> 'v" and invar
subsubsection {* Ordered Iteration *}
locale poly_map_iterateoi_defs =
fixes olist_it :: "'s => ('u×'v,('u×'v) list) set_iterator"
begin
definition iterateoi :: "'s => ('u×'v,'σ) set_iterator"
where "iterateoi S ≡ it_to_it (olist_it S)"
abbreviation "iterateo m ≡ iterateoi m (λ_. True)"
end
locale poly_map_iterateoi =
finite_map α invar + poly_map_iterateoi_defs list_ordered_it
for α :: "'s => ('u::linorder) \<rightharpoonup> 'v"
and invar
and list_ordered_it :: "'s => ('u×'v,('u×'v) list) set_iterator" +
assumes list_ordered_it_correct: "invar m
==> map_iterator_linord (list_ordered_it m) (α m)"
begin
lemma iterateoi_correct: "invar S ==> map_iterator_linord (iterateoi S) (α S)"
unfolding iterateoi_def
apply (rule it_to_it_map_linord_correct)
by (rule list_ordered_it_correct)
lemma pi_iterateoi[icf_proper_iteratorI]:
"proper_it (iterateoi S) (iterateoi S)"
unfolding iterateoi_def
by (intro icf_proper_iteratorI)
lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
assumes MINV: "invar m"
assumes I0: "I (dom (α m)) σ0"
assumes IP: "!!k v it σ. [|
c σ;
k ∈ it;
α m k = Some v;
it ⊆ dom (α m);
I it σ;
!!j. j∈it ==> k≤j;
!!j. j∈dom (α m) - it ==> j≤k
|] ==> I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ==> P σ"
assumes II: "!!σ it. [|
it ⊆ dom (α m);
it ≠ {};
¬ c σ;
I it σ;
!!k j. [|k∈it; j∈dom (α m) - it|] ==> j≤k
|] ==> P σ"
shows "P (iterateoi m c f σ0)"
using assms by (rule map_iterator_linord_rule_P[OF iterateoi_correct])
lemma iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
assumes MINV: "invar m"
assumes I0: "I (dom (α m)) σ0"
assumes IP: "!!k v it σ. [|
k ∈ it;
α m k = Some v;
it ⊆ dom (α m);
I it σ;
!!j. j∈it ==> k≤j;
!!j. j∈dom (α m) - it ==> j≤k
|] ==> I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ==> P σ"
shows "P (iterateo m f σ0)"
using assms
map_iterator_linord_rule_P[OF iterateoi_correct, of m I σ0 "λ_. True" f P]
by blast
end
type_synonym ('k,'v,'s) map_list_rev_it
= "'s => ('k×'v,('k×'v) list) set_iterator"
locale poly_map_rev_iterateoi_defs =
fixes list_rev_it :: "'s => ('u×'v,('u×'v) list) set_iterator"
begin
definition rev_iterateoi :: "'s => ('u×'v,'σ) set_iterator"
where "rev_iterateoi S ≡ it_to_it (list_rev_it S)"
abbreviation "rev_iterateo m ≡ rev_iterateoi m (λ_. True)"
abbreviation "reverse_iterateoi ≡ rev_iterateoi"
abbreviation "reverse_iterateo ≡ rev_iterateo"
end
locale poly_map_rev_iterateoi =
finite_map α invar + poly_map_rev_iterateoi_defs list_rev_it
for α :: "'s => ('u::linorder) \<rightharpoonup> 'v"
and invar
and list_rev_it :: "'s => ('u×'v,('u×'v) list) set_iterator" +
assumes list_rev_it_correct:
"invar m ==> map_iterator_rev_linord (list_rev_it m) (α m)"
begin
lemma rev_iterateoi_correct:
"invar S ==> map_iterator_rev_linord (rev_iterateoi S) (α S)"
unfolding rev_iterateoi_def
apply (rule it_to_it_map_rev_linord_correct)
by (rule list_rev_it_correct)
lemma pi_rev_iterateoi[icf_proper_iteratorI]:
"proper_it (rev_iterateoi S) (rev_iterateoi S)"
unfolding rev_iterateoi_def
by (intro icf_proper_iteratorI)
lemma rev_iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
assumes MINV: "invar m"
assumes I0: "I (dom (α m)) σ0"
assumes IP: "!!k v it σ. [|
c σ;
k ∈ it;
α m k = Some v;
it ⊆ dom (α m);
I it σ;
!!j. j∈it ==> k≥j;
!!j. j∈dom (α m) - it ==> j≥k
|] ==> I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ==> P σ"
assumes II: "!!σ it. [|
it ⊆ dom (α m);
it ≠ {};
¬ c σ;
I it σ;
!!k j. [|k∈it; j∈dom (α m) - it|] ==> j≥k
|] ==> P σ"
shows "P (rev_iterateoi m c f σ0)"
using assms by (rule map_iterator_rev_linord_rule_P[OF rev_iterateoi_correct])
lemma rev_iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
assumes MINV: "invar m"
assumes I0: "I (dom (α m)) σ0"
assumes IP: "!!k v it σ. [|
k ∈ it;
α m k = Some v;
it ⊆ dom (α m);
I it σ;
!!j. j∈it ==> k≥j;
!!j. j∈dom (α m) - it ==> j≥k
|] ==> I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ==> P σ"
shows "P (rev_iterateo m f σ0)"
using assms
map_iterator_rev_linord_rule_P[OF rev_iterateoi_correct,
of m I σ0 "λ_. True" f P]
by blast
end
subsubsection {* Minimal and Maximal Elements *}
type_synonym ('k,'v,'s) map_min
= "'s => ('k × 'v => bool) => ('k × 'v) option"
locale map_min = ordered_map +
constrains α :: "'s => 'u::linorder \<rightharpoonup> 'v"
fixes min :: "'s => ('u × 'v => bool) => ('u × 'v) option"
assumes min_correct:
"[| invar s; rel_of (α s) P ≠ {} |] ==> min s P ∈ Some ` rel_of (α s) P"
"[| invar s; (k,v) ∈ rel_of (α s) P |] ==> fst (the (min s P)) ≤ k"
"[| invar s; rel_of (α s) P = {} |] ==> min s P = None"
begin
lemma minE:
assumes A: "invar s" "rel_of (α s) P ≠ {}"
obtains k v where
"min s P = Some (k,v)" "(k,v)∈rel_of (α s) P" "∀(k',v')∈rel_of (α s) P. k ≤ k'"
proof -
from min_correct(1)[OF A] have MIS: "min s P ∈ Some ` rel_of (α s) P" .
then obtain k v where KV: "min s P = Some (k,v)" "(k,v)∈rel_of (α s) P"
by auto
show thesis
apply (rule that[OF KV])
apply (clarify)
apply (drule min_correct(2)[OF `invar s`])
apply (simp add: KV(1))
done
qed
lemmas minI = min_correct(3)
lemma min_Some:
"[| invar s; min s P = Some (k,v) |] ==> (k,v)∈rel_of (α s) P"
"[| invar s; min s P = Some (k,v); (k',v')∈rel_of (α s) P |] ==> k≤k'"
apply -
apply (cases "rel_of (α s) P = {}")
apply (drule (1) min_correct(3))
apply simp
apply (erule (1) minE)
apply auto [1]
apply (drule (1) min_correct(2))
apply auto
done
lemma min_None:
"[| invar s; min s P = None |] ==> rel_of (α s) P = {}"
apply (cases "rel_of (α s) P = {}")
apply simp
apply (drule (1) min_correct(1))
apply auto
done
end
type_synonym ('k,'v,'s) map_max
= "'s => ('k × 'v => bool) => ('k × 'v) option"
locale map_max = ordered_map +
constrains α :: "'s => 'u::linorder \<rightharpoonup> 'v"
fixes max :: "'s => ('u × 'v => bool) => ('u × 'v) option"
assumes max_correct:
"[| invar s; rel_of (α s) P ≠ {} |] ==> max s P ∈ Some ` rel_of (α s) P"
"[| invar s; (k,v) ∈ rel_of (α s) P |] ==> fst (the (max s P)) ≥ k"
"[| invar s; rel_of (α s) P = {} |] ==> max s P = None"
begin
lemma maxE:
assumes A: "invar s" "rel_of (α s) P ≠ {}"
obtains k v where
"max s P = Some (k,v)" "(k,v)∈rel_of (α s) P" "∀(k',v')∈rel_of (α s) P. k ≥ k'"
proof -
from max_correct(1)[OF A] have MIS: "max s P ∈ Some ` rel_of (α s) P" .
then obtain k v where KV: "max s P = Some (k,v)" "(k,v)∈rel_of (α s) P"
by auto
show thesis
apply (rule that[OF KV])
apply (clarify)
apply (drule max_correct(2)[OF `invar s`])
apply (simp add: KV(1))
done
qed
lemmas maxI = max_correct(3)
lemma max_Some:
"[| invar s; max s P = Some (k,v) |] ==> (k,v)∈rel_of (α s) P"
"[| invar s; max s P = Some (k,v); (k',v')∈rel_of (α s) P |] ==> k≥k'"
apply -
apply (cases "rel_of (α s) P = {}")
apply (drule (1) max_correct(3))
apply simp
apply (erule (1) maxE)
apply auto [1]
apply (drule (1) max_correct(2))
apply auto
done
lemma max_None:
"[| invar s; max s P = None |] ==> rel_of (α s) P = {}"
apply (cases "rel_of (α s) P = {}")
apply simp
apply (drule (1) max_correct(1))
apply auto
done
end
subsubsection "Conversion to List"
type_synonym ('k,'v,'s) map_to_sorted_list
= "'s => ('k × 'v) list"
locale map_to_sorted_list = ordered_map +
constrains α :: "'s => 'u::linorder \<rightharpoonup> 'v"
fixes to_sorted_list :: "'s => ('u×'v) list"
assumes to_sorted_list_correct:
"invar m ==> map_of (to_sorted_list m) = α m"
"invar m ==> distinct (map fst (to_sorted_list m))"
"invar m ==> sorted (map fst (to_sorted_list m))"
type_synonym ('k,'v,'s) map_to_rev_list
= "'s => ('k × 'v) list"
locale map_to_rev_list = ordered_map +
constrains α :: "'s => 'u::linorder \<rightharpoonup> 'v"
fixes to_rev_list :: "'s => ('u×'v) list"
assumes to_rev_list_correct:
"invar m ==> map_of (to_rev_list m) = α m"
"invar m ==> distinct (map fst (to_rev_list m))"
"invar m ==> sorted (rev (map fst (to_rev_list m)))"
subsection "Record Based Interface"
record ('k,'v,'s) map_ops =
map_op_α :: "('k,'v,'s) map_α"
map_op_invar :: "('k,'v,'s) map_invar"
map_op_empty :: "('k,'v,'s) map_empty"
map_op_lookup :: "('k,'v,'s) map_lookup"
map_op_update :: "('k,'v,'s) map_update"
map_op_update_dj :: "('k,'v,'s) map_update_dj"
map_op_delete :: "('k,'v,'s) map_delete"
map_op_list_it :: "('k,'v,'s) map_list_it"
map_op_sng :: "('k,'v,'s) map_sng"
map_op_restrict :: "('k,'v,'s,'s) map_restrict"
map_op_add :: "('k,'v,'s) map_add"
map_op_add_dj :: "('k,'v,'s) map_add_dj"
map_op_isEmpty :: "('k,'v,'s) map_isEmpty"
map_op_isSng :: "('k,'v,'s) map_isSng"
map_op_ball :: "('k,'v,'s) map_ball"
map_op_bex :: "('k,'v,'s) map_bex"
map_op_size :: "('k,'v,'s) map_size"
map_op_size_abort :: "('k,'v,'s) map_size_abort"
map_op_sel :: "('k,'v,'s) map_sel'"
map_op_to_list :: "('k,'v,'s) map_to_list"
map_op_to_map :: "('k,'v,'s) list_to_map"
locale StdMapDefs = poly_map_iteratei_defs "map_op_list_it ops"
for ops :: "('k,'v,'s,'more) map_ops_scheme"
begin
abbreviation α where "α == map_op_α ops"
abbreviation invar where "invar == map_op_invar ops"
abbreviation empty where "empty == map_op_empty ops"
abbreviation lookup where "lookup == map_op_lookup ops"
abbreviation update where "update == map_op_update ops"
abbreviation update_dj where "update_dj == map_op_update_dj ops"
abbreviation delete where "delete == map_op_delete ops"
abbreviation list_it where "list_it == map_op_list_it ops"
abbreviation sng where "sng == map_op_sng ops"
abbreviation restrict where "restrict == map_op_restrict ops"
abbreviation add where "add == map_op_add ops"
abbreviation add_dj where "add_dj == map_op_add_dj ops"
abbreviation isEmpty where "isEmpty == map_op_isEmpty ops"
abbreviation isSng where "isSng == map_op_isSng ops"
abbreviation ball where "ball == map_op_ball ops"
abbreviation bex where "bex == map_op_bex ops"
abbreviation size where "size == map_op_size ops"
abbreviation size_abort where "size_abort == map_op_size_abort ops"
abbreviation sel where "sel == map_op_sel ops"
abbreviation to_list where "to_list == map_op_to_list ops"
abbreviation to_map where "to_map == map_op_to_map ops"
end
locale StdMap = StdMapDefs 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 +
map_sng α invar sng +
map_restrict α invar α invar restrict +
map_add α invar add +
map_add_dj α invar add_dj +
map_isEmpty α invar isEmpty +
map_isSng α invar isSng +
map_ball α invar ball +
map_bex α invar bex +
map_size α invar size +
map_size_abort α invar size_abort +
map_sel' α invar sel +
map_to_list α invar to_list +
list_to_map α invar to_map
for ops :: "('k,'v,'s,'more) map_ops_scheme"
begin
lemmas correct =
empty_correct
sng_correct
lookup_correct
update_correct
update_dj_correct
delete_correct
restrict_correct
add_correct
add_dj_correct
isEmpty_correct
isSng_correct
ball_correct
bex_correct
size_correct
size_abort_correct
to_list_correct
to_map_correct
end
lemmas StdMap_intro = StdMap.intro[rem_dup_prems]
locale StdMap_no_invar = StdMap + map_no_invar α invar
record ('k,'v,'s) omap_ops = "('k,'v,'s) map_ops" +
map_op_ordered_list_it :: "'s => ('k,'v,('k×'v) list) map_iterator"
map_op_rev_list_it :: "'s => ('k,'v,('k×'v) list) map_iterator"
map_op_min :: "'s => ('k × 'v => bool) => ('k × 'v) option"
map_op_max :: "'s => ('k × 'v => bool) => ('k × 'v) option"
map_op_to_sorted_list :: "'s => ('k × 'v) list"
map_op_to_rev_list :: "'s => ('k × 'v) list"
locale StdOMapDefs = StdMapDefs ops
+ poly_map_iterateoi_defs "map_op_ordered_list_it ops"
+ poly_map_rev_iterateoi_defs "map_op_rev_list_it ops"
for ops :: "('k::linorder,'v,'s,'more) omap_ops_scheme"
begin
abbreviation ordered_list_it where "ordered_list_it
≡ map_op_ordered_list_it ops"
abbreviation rev_list_it where "rev_list_it
≡ map_op_rev_list_it ops"
abbreviation min where "min == map_op_min ops"
abbreviation max where "max == map_op_max ops"
abbreviation to_sorted_list where
"to_sorted_list ≡ map_op_to_sorted_list ops"
abbreviation to_rev_list where "to_rev_list ≡ map_op_to_rev_list ops"
end
locale StdOMap =
StdOMapDefs ops +
StdMap ops +
poly_map_iterateoi α invar ordered_list_it +
poly_map_rev_iterateoi α invar rev_list_it +
map_min α invar min +
map_max α invar max +
map_to_sorted_list α invar to_sorted_list +
map_to_rev_list α invar to_rev_list
for ops :: "('k::linorder,'v,'s,'more) omap_ops_scheme"
begin
end
lemmas StdOMap_intro =
StdOMap.intro[OF StdMap_intro, rem_dup_prems]
end