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>
*)
section ‹\isaheader{Specification of Maps}›
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)"

subsubsection "Add"
type_synonym ('k,'v,'s) map_add = "'s ⇒ 's ⇒ 's"
locale map_add = map +
  constrains α :: "'s ⇒ 'u ⇀ '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 ⇀ '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 ⇀ '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]
    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
*)

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