# Theory MapSpec

(*  Title:       Isabelle Collections Library
Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
theory MapSpec
imports ICF_Spec_Base
begin
text_raw‹\label{thy:MapSpec}›

(*@intf Map
@abstype 'k⇀'v
This interface specifies maps from keys to values.
*)

text ‹
This theory specifies map operations by means of mapping to
HOL's map type, i.e. @{typ "'k ⇀ 'v"}.
›

type_synonym ('k,'v,'s) map_α = "'s ⇒ 'k ⇀ 'v"
type_synonym ('k,'v,'s) map_invar = "'s ⇒ bool"
locale map =
fixes α :: "'s ⇒ 'u ⇀ '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 ⇀ '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 ⇀ '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 ⇀ 'v"
fixes update :: "'u ⇒ 'v ⇒ 's ⇒ 's"
assumes update_correct:
"invar m ⟹ α (update k v m) = (α m)(k ↦ 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 ⇀ 'v"
fixes update_dj :: "'u ⇒ 'v ⇒ 's ⇒ 's"
assumes update_dj_correct:
"⟦invar m; k∉dom (α m)⟧ ⟹ α (update_dj k v m) = (α m)(k ↦ 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 ⇀ 'v"
fixes delete :: "'u ⇒ 's ⇒ 's"
assumes delete_correct:
"invar m ⟹ α (delete k m) = (α m) | (-{k})"
"invar m ⟹ invar (delete k m)"

type_synonym ('k,'v,'s) map_add = "'s ⇒ 's ⇒ 's"
constrains α :: "'s ⇒ 'u ⇀ 'v"
fixes add :: "'s ⇒ 's ⇒ 's"
"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"
constrains α :: "'s ⇒ 'u ⇀ 'v"
fixes add_dj :: "'s ⇒ 's ⇒ 's"
"⟦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 ⇀ '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 ⇀ 'v"
fixes sng :: "'u ⇒ 'v ⇒ 's"
assumes sng_correct :
"α (sng k v) = [k ↦ v]"
"invar (sng k v)"

type_synonym ('k,'v,'s) map_isSng = "'s ⇒ bool"
locale map_isSng = map +
constrains α :: "'s ⇒ 'k ⇀ 'v"
fixes isSng :: "'s ⇒ bool"
assumes isSng_correct:
"invar s ⟹ isSng s ⟷ (∃k v. α s = [k ↦ v])"
begin
lemma isSng_correct_exists1 :
"invar s ⟹ (isSng s ⟷ (∃!k. ∃v. (α s k = Some v)))"
apply (auto simp add: isSng_correct split: if_split_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 ⇀ '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 ⇀ '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.
›

(* Deprecated *)
(*locale map_iteratei = finite_map +
constrains α :: "'s ⇒ 'u ⇀ '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]

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]

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
*)

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 ⇀ '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 ⇀ '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 ⇀ '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 ⇀ '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 ⇀ '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 ⇀ '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 ⇀ '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 ⇀ 'v1) ⇒ ('u1 × 'v1 ⇀ ('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 ⇀ 'v1" and invar1
and α2 :: "'m2 ⇒ 'u2 ⇀ '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

(*Let's use a definition for the precondition *)

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 ⇀ 'v1" and invar1
and α2 :: "'m2 ⇒ 'u ⇀ '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 ⇀ 'v" and invar1
and α2 :: "'m2 ⇒ 'u ⇀ '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}"
qed

lemmas restrict_correct =
restrict_correct_aux1
restrict_correct_aux2
end

subsection "Ordered Maps"
locale ordered_map = map α invar
for α :: "'s ⇒ ('u::linorder) ⇀ 'v" and invar

locale ordered_finite_map = finite_map α invar + ordered_map α invar
for α :: "'s ⇒ ('u::linorder) ⇀ 'v" and invar

subsubsection ‹Ordered Iteration›
(* Deprecated *)
(*
locale map_iterateoi = ordered_finite_map α invar
for α :: "'s ⇒ ('u::linorder) ⇀ '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) ⇀ '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
*)

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) ⇀ '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) ⇀ '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 ⇀ '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›])
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 ⇀ '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›])
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 ⇀ '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 ⇀ '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_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 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_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
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