header {* \isaheader{Specification of Maps} *}
theory MapSpec
imports Main "../iterator/SetIterator"
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"}.
*}
locale map =
fixes α :: "'s => 'u \<rightharpoonup> 'v" -- "Abstraction to map datatype"
fixes invar :: "'s => bool" -- "Invariant"
subsection "Basic Map Functions"
subsubsection "Empty Map"
locale map_empty = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes empty :: "unit => 's"
assumes empty_correct:
"α (empty ()) = Map.empty"
"invar (empty ())"
subsubsection "Lookup"
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"
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"
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"
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"
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)"
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"
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"
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)"
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"
locale map_size = finite_map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes size :: "'s => nat"
assumes size_correct: "invar s ==> size s = card (dom (α s))"
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.
*}
locale map_iteratei = finite_map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes iteratei :: "'s => ('u × 'v,'σ) set_iterator"
assumes iteratei_rule: "invar m ==> map_iterator (iteratei m) (α m)"
begin
lemma 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 map_iterator_rule_P [OF iteratei_rule, of m I σ0 c f P]
by (simp_all add: assms)
lemma iteratei_rule_insert_P:
assumes
"invar m"
"I {} σ0"
"!!k v it σ. [| c σ; k ∈ (dom (α m) - it); α m k = Some v; it ⊆ dom (α m); I it σ |]
==> I (insert k it) (f (k, v) σ)"
"!!σ. I (dom (α m)) σ ==> P σ"
"!!σ it. [| it ⊆ dom (α m); it ≠ dom (α m);
¬ (c σ);
I it σ |] ==> P σ"
shows "P (iteratei m c f σ0)"
using map_iterator_rule_insert_P [OF iteratei_rule, of m I σ0 c f P]
by (simp_all add: assms)
lemma 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 (iteratei m (λ_. True) f σ0)"
using iteratei_rule_P [of m I σ0 "λ_. True" f P]
by fast
lemma 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 iteratei_rule_insert_P [of m I σ0 "λ_. True" f P]
by fast
end
lemma map_iteratei_I :
assumes "!!m. invar m ==> map_iterator (iti m) (α m)"
shows "map_iteratei α invar iti"
proof
fix m
assume invar_m: "invar m"
from assms(1)[OF invar_m] show it_OK: "map_iterator (iti m) (α m)" .
from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_def]]
show "finite (dom (α m))" by (simp add: finite_map_to_set)
qed
subsubsection "Bounded Quantification"
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))"
locale map_bexists = map +
constrains α :: "'s => 'u \<rightharpoonup> 'v"
fixes bexists :: "'s => ('u × 'v => bool) => bool"
assumes bexists_correct: "invar m ==> bexists m P <-> (∃u v. α m u = Some v ∧ P (u, v))"
subsubsection "Selection of Entry"
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)"
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"
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"
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))"
locale map_image_filter = map α1 invar1 + 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.*}
locale map_value_image_filter = map α1 invar1 + 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 :
"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
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 [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
locale map_restrict = map α1 invar1 + 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 map_iterateoi = ordered_finite_map α invar
for α :: "'s => ('u::linorder) \<rightharpoonup> 'v" and invar
+
fixes iterateoi :: "'s => ('u × 'v,'σ) set_iterator"
assumes iterateoi_rule: "
invar m ==> map_iterator_linord (iterateoi m) (α m)"
begin
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;
∀j∈it. k≤j;
∀j∈dom (α m) - it. j≤k;
α m k = Some v;
it ⊆ dom (α m);
I it σ
|] ==> I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ==> P σ"
assumes II: "!!σ it. [|
it ⊆ dom (α m);
it ≠ {};
¬ c σ;
I it σ;
∀k∈it. ∀j∈dom (α m) - it. j≤k
|] ==> P σ"
shows "P (iterateoi m c f σ0)"
using map_iterator_linord_rule_P [OF iterateoi_rule, of m I σ0 c f P] assms
by simp
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; ∀j∈it. k≤j; ∀j∈dom (α m) - it. j≤k; α m k = Some v; it ⊆ dom (α m); I it σ |]
==> I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ==> P σ"
shows "P (iterateoi m (λ_. True) f σ0)"
using map_iterator_linord_rule_P [OF iterateoi_rule, of m I σ0 "λ_. True" f P] assms
by simp
end
lemma map_iterateoi_I :
assumes "!!m. invar m ==> map_iterator_linord (itoi m) (α m)"
shows "map_iterateoi α invar itoi"
proof
fix m
assume invar_m: "invar m"
from assms(1)[OF invar_m] show it_OK: "map_iterator_linord (itoi m) (α m)" .
from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_map_linord_def]]
show "finite (dom (α m))" by (simp add: finite_map_to_set)
qed
locale map_reverse_iterateoi = ordered_finite_map α invar
for α :: "'s => ('u::linorder) \<rightharpoonup> 'v" and invar
+
fixes reverse_iterateoi :: "'s => ('u × 'v,'σ) set_iterator"
assumes reverse_iterateoi_rule: "
invar m ==> map_iterator_rev_linord (reverse_iterateoi m) (α m)"
begin
lemma reverse_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;
∀j∈it. k≥j;
∀j∈dom (α m) - it. j≥k;
α m k = Some v;
it ⊆ dom (α m);
I it σ
|] ==> I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ==> P σ"
assumes II: "!!σ it. [|
it ⊆ dom (α m);
it ≠ {};
¬ c σ;
I it σ;
∀k∈it. ∀j∈dom (α m) - it. j≥k
|] ==> P σ"
shows "P (reverse_iterateoi m c f σ0)"
using map_iterator_rev_linord_rule_P [OF reverse_iterateoi_rule, of m I σ0 c f P] assms
by simp
lemma reverse_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;
∀j∈it. k≥j;
∀j∈dom (α m) - it. j≥k;
α m k = Some v;
it ⊆ dom (α m);
I it σ
|] ==> I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ==> P σ"
shows "P (reverse_iterateoi m (λ_. True) f σ0)"
using map_iterator_rev_linord_rule_P[OF reverse_iterateoi_rule, of m I σ0 "λ_. True" f P] assms
by simp
end
lemma map_reverse_iterateoi_I :
assumes "!!m. invar m ==> map_iterator_rev_linord (ritoi m) (α m)"
shows "map_reverse_iterateoi α invar ritoi"
proof
fix m
assume invar_m: "invar m"
from assms(1)[OF invar_m] show it_OK: "map_iterator_rev_linord (ritoi m) (α m)" .
from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_map_rev_linord_def]]
show "finite (dom (α m))" by (simp add: finite_map_to_set)
qed
subsubsection {* Minimal and Maximal Elements *}
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
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"
locale map_to_sorted_list = ordered_map α invar + map_to_list α invar to_list
for α :: "'s => 'u::linorder \<rightharpoonup> 'v" and invar to_list +
assumes to_list_sorted:
"invar m ==> sorted (map fst (to_list m))"
subsection "Record Based Interface"
record ('k,'v,'s) map_ops =
map_op_α :: "'s => 'k \<rightharpoonup> 'v"
map_op_invar :: "'s => bool"
map_op_empty :: "unit => 's"
map_op_sng :: "'k => 'v => 's"
map_op_lookup :: "'k => 's => 'v option"
map_op_update :: "'k => 'v => 's => 's"
map_op_update_dj :: "'k => 'v => 's => 's"
map_op_delete :: "'k => 's => 's"
map_op_restrict :: "('k × 'v => bool) => 's => 's"
map_op_add :: "'s => 's => 's"
map_op_add_dj :: "'s => 's => 's"
map_op_isEmpty :: "'s => bool"
map_op_isSng :: "'s => bool"
map_op_ball :: "'s => ('k × 'v => bool) => bool"
map_op_bexists :: "'s => ('k × 'v => bool) => bool"
map_op_size :: "'s => nat"
map_op_size_abort :: "nat => 's => nat"
map_op_sel :: "'s => ('k × 'v => bool) => ('k×'v) option" -- "Version without mapping"
map_op_to_list :: "'s => ('k×'v) list"
map_op_to_map :: "('k×'v) list => 's"
locale StdMapDefs =
fixes 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 sng where "sng == map_op_sng 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 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 bexists where "bexists == map_op_bexists 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_sng α invar sng +
map_lookup α invar lookup +
map_update α invar update +
map_update_dj α invar update_dj +
map_delete α invar delete +
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_bexists α invar bexists +
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
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
bexists_correct
size_correct
size_abort_correct
to_list_correct
to_map_correct
end
record ('k,'v,'s) omap_ops = "('k,'v,'s) map_ops" +
map_op_min :: "'s => ('k × 'v => bool) => ('k × 'v) option"
map_op_max :: "'s => ('k × 'v => bool) => ('k × 'v) option"
locale StdOMapDefs = StdMapDefs ops
for ops :: "('k::linorder,'v,'s,'more) omap_ops_scheme"
begin
abbreviation min where "min == map_op_min ops"
abbreviation max where "max == map_op_max ops"
end
locale StdOMap =
StdOMapDefs ops +
StdMap ops +
map_min α invar min +
map_max α invar max
for ops
begin
end
end