Theory MapGA

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

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

*)

header {* \isaheader{Generic Algorithms for Maps} *}
theory MapGA
imports 
  "../spec/MapSpec"
  "../common/Misc" 
  "../iterator/SetIteratorGA" 
  "../iterator/SetIteratorGACollections"
begin

text_raw {*\label{thy:MapGA}*}

subsection {*Disjoint Update (by update)*}
lemma (in map_update) update_dj_by_update: 
  "map_update_dj α invar update"
  apply (unfold_locales)
  apply (auto simp add: update_correct)
  done

subsection {*Disjoint Add (by add)*}
lemma (in map_add) add_dj_by_add: 
  "map_add_dj α invar add"
  apply (unfold_locales)
  apply (auto simp add: add_correct)
  done

subsection {*Add (by iterate)*}

definition it_add where 
  "it_add update iti = (λm1 m2. iterate_add_to_map m1 update (iti m2))"

lemma it_add_code[code]:
  "it_add update iti m1 m2 = iti m2 (λ_. True) (λ(x, y). update x y) m1"
unfolding it_add_def iterate_add_to_map_def by simp

lemma it_add_correct:
  fixes α :: "'s => 'u \<rightharpoonup> 'v"
  assumes iti: "map_iteratei α invar iti"
  assumes upd_OK: "map_update α invar update"
  shows "map_add α invar (it_add update iti)"
unfolding it_add_def
proof 
  fix m1 m2
  assume "invar m1" "invar m2"
  with map_iteratei.iteratei_rule[OF iti, of m2] 
  have iti_m2: "map_iterator (iti m2) (α m2)" by simp

  from iterate_add_to_map_correct [OF upd_OK, OF `invar m1` iti_m2 ]
  show "α (iterate_add_to_map m1 update (iti m2)) = α m1 ++ α m2"
       "invar (iterate_add_to_map m1 update (iti m2))"
    by simp_all
qed


subsection {*Disjoint Add (by iterate)*}
lemma it_add_dj_correct:
  fixes α :: "'s => 'u \<rightharpoonup> 'v"
  assumes iti: "map_iteratei α invar iti"
  assumes upd_dj_OK: "map_update_dj α invar update"
  shows "map_add_dj α invar (it_add update iti)"
unfolding it_add_def
proof 
  fix m1 m2
  assume "invar m1" "invar m2" and dom_dj: "dom (α m1) ∩ dom (α m2) = {}"
  with map_iteratei.iteratei_rule[OF iti, OF `invar m2`] 
  have iti_m2: "map_iterator (iti m2) (α m2)" by simp

  from iterate_add_to_map_dj_correct [OF upd_dj_OK, OF `invar m1` iti_m2 ] dom_dj
  show "α (iterate_add_to_map m1 update (iti m2)) = α m1 ++ α m2"
       "invar (iterate_add_to_map m1 update (iti m2))"
    by auto
qed

subsection {*Emptiness check (by iteratei)*}

definition iti_isEmpty where
  "iti_isEmpty iti = (λm. iterate_is_empty (iti m))"

lemma iti_isEmpty[code] :
  "iti_isEmpty iti m = iti m (λc. c) (λ_ _. False) True"
unfolding iti_isEmpty_def iterate_is_empty_def by simp

lemma iti_isEmpty_correct:
  assumes iti: "map_iteratei α invar iti"
  shows "map_isEmpty α invar (iti_isEmpty iti)"
unfolding iti_isEmpty_def
proof 
  fix m
  assume "invar m"
  with map_iteratei.iteratei_rule[OF iti, of m] 
  have iti': "map_iterator (iti m) (α m)" by simp

  from iterate_is_empty_correct[OF iti']
  show "iterate_is_empty (iti m) = (α m = Map.empty)"
    by (simp add: map_to_set_empty_iff)
qed


subsection {* Iterators *}

subsubsection {* Iteratei (by iterateoi) *}
lemma iti_by_itoi: 
  assumes "map_iterateoi α invar it"
  shows "map_iteratei α invar it"
using assms
unfolding map_iterateoi_def map_iteratei_def map_iteratei_axioms_def
          map_iterateoi_axioms_def set_iterator_map_linord_def 
          finite_map_def ordered_finite_map_def
by (metis set_iterator_intro)

subsubsection {* Iteratei (by reverse\_iterateoi) *}
lemma iti_by_ritoi: 
  assumes "map_reverse_iterateoi α invar it"
  shows "map_iteratei α invar it"
using assms
unfolding map_reverse_iterateoi_def map_iteratei_def map_iteratei_axioms_def
          map_reverse_iterateoi_axioms_def set_iterator_map_rev_linord_def 
          finite_map_def ordered_finite_map_def
by (metis set_iterator_intro)


subsection {*Selection (by iteratei)*}

definition iti_sel where
  "iti_sel iti = (λm f. iterate_sel (iti m) f)"

lemma iti_sel_code[code] :
  "iti_sel iti m f = iti m (λσ. σ = None) (λx σ. f x) None"
unfolding iti_sel_def iterate_sel_def by simp

lemma iti_sel_correct:
  assumes iti: "map_iteratei α invar iti"
  shows "map_sel α invar (iti_sel iti)"
proof -
  { fix m f
    assume "invar m"
    with map_iteratei.iteratei_rule [OF iti, of m]
    have iti': "map_iterator (iti m) (α m)" by simp
    note iterate_sel_genord_correct[OF iti'[unfolded set_iterator_def], of f]
  }
  thus ?thesis
    unfolding map_sel_def iti_sel_def
    apply (simp add: Bex_def Ball_def image_iff map_to_set_def)
    apply (metis option.exhaust)
  done
qed


subsection {* Map-free selection by selection *}

definition iti_sel_no_map where
  "iti_sel_no_map iti = (λm P. iterate_sel_no_map (iti m) P)"

lemma iti_sel_no_map_code[code] :
  "iti_sel_no_map iti m P = iti m (λσ. σ = None) (λx σ. if P x then Some x else None) None"
unfolding iti_sel_no_map_def iterate_sel_no_map_alt_def by simp

lemma iti_sel'_correct:
  assumes iti: "map_iteratei α invar iti"
  shows "map_sel' α invar (iti_sel_no_map iti)"
proof -
  { fix m P
    assume "invar m"
    with map_iteratei.iteratei_rule [OF iti, of m]
    have iti': "map_iterator (iti m) (α m)" by simp
    note iterate_sel_no_map_correct[OF iti', of P]
  }
  thus ?thesis
    unfolding map_sel'_def iti_sel_no_map_def
    apply (simp add: Bex_def Ball_def image_iff map_to_set_def)
    apply clarify
    apply (metis option.exhaust PairE)
  done
qed

subsection {* Map-free selection by selection *}

definition sel_sel'
  :: "('s => ('k × 'v => _ option) => _ option) => 's => ('k × 'v => bool) => ('k×'v) option"
where "sel_sel' sel s P = sel s (λkv. if P kv then Some kv else None)"

lemma sel_sel'_correct: 
  assumes "map_sel α invar sel"
  shows "map_sel' α invar (sel_sel' sel)"
proof -
  interpret map_sel α invar sel by fact

  show ?thesis
  proof
    case goal1 show ?case
      apply (rule selE[OF goal1(1,2), where f="(λkv. if P kv then Some kv else None)"])
      apply (simp add: goal1)
      apply (simp split: split_if_asm)
      apply (fold sel_sel'_def)
      apply (blast intro: goal1(4))
      done
  next
    case goal2 thus ?case
      apply (auto simp add: sel_sel'_def)
      apply (drule selI[where f="(λkv. if P kv then Some kv else None)"])
      apply auto
      done
  qed
qed


subsection {*Bounded Quantification (by sel)*}
definition sel_ball 
  :: "('s => ('k × 'v => unit option) \<rightharpoonup> unit) => 's => ('k × 'v => bool) => bool"
  where "sel_ball sel s P == sel s (λkv. if ¬P kv then Some () else None) = None"

lemma sel_ball_correct:
  assumes "map_sel α invar sel"
  shows "map_ball α invar (sel_ball sel)"
proof -
  interpret map_sel α invar sel by fact
  
  show ?thesis
    apply unfold_locales
    apply (unfold sel_ball_def)
    apply (auto elim: sel_someE dest: sel_noneD split: split_if_asm)
    done
qed

definition sel_bexists
  :: "('s => ('k × 'v => unit option) \<rightharpoonup> unit) => 's => ('k × 'v => bool) => bool"
  where "sel_bexists sel s P == sel s (λkv. if P kv then Some () else None) = Some ()"

lemma sel_bexists_correct:
  assumes "map_sel α invar sel"
  shows "map_bexists α invar (sel_bexists sel)"
proof -
  interpret map_sel α invar sel by fact
  
  show ?thesis
    apply unfold_locales
    apply (unfold sel_bexists_def)
    apply auto
    apply (force elim!: sel_someE split: split_if_asm) []
    apply (erule_tac f="(λkv. if P kv then Some () else None)" in selE)
    apply assumption
    apply simp
    apply simp
    done
qed

definition neg_ball_bexists
  :: "('s => ('k × 'v => bool) => bool) => 's => ('k × 'v => bool) => bool"
  where "neg_ball_bexists ball s P == ¬ (ball s (λkv. ¬(P kv)))"

lemma neg_ball_bexists_correct:
  fixes ball
  assumes "map_ball α invar ball"
  shows "map_bexists α invar (neg_ball_bexists ball)"
proof -
  interpret map_ball α invar ball by fact
  show ?thesis
    apply (unfold_locales)
    apply (unfold neg_ball_bexists_def)
    apply (simp add: ball_correct)
  done
qed



subsection {*Bounded Quantification (by iterate)*}

definition iti_ball where
  "iti_ball iti = (λm. iterate_ball (iti m))"

lemma iti_ball_code[code] :
  "iti_ball iti m P = iti m (λc. c) (λx σ. P x) True"
unfolding iti_ball_def iterate_ball_def[abs_def] id_def by simp

lemma iti_ball_correct:
  assumes iti: "map_iteratei α invar iti"
  shows "map_ball α invar (iti_ball iti)"
unfolding iti_ball_def
proof 
  fix m P
  assume "invar m"
  with map_iteratei.iteratei_rule[OF iti, of m] 
  have iti': "map_iterator (iti m) (α m)" by simp

  from iterate_ball_correct[OF iti', of P]
  show "iterate_ball (iti m) P = (∀u v. α m u = Some v --> P (u, v))"
    by (simp add: map_to_set_def)
qed

definition iti_bexists where
  "iti_bexists iti = (λm. iterate_bex (iti m))"

lemma iti_bexists_code[code] :
  "iti_bexists iti m P = iti m (λc. ¬c) (λx σ. P x) False"
unfolding iti_bexists_def iterate_bex_def[abs_def] by simp

lemma iti_bexists_correct:
  assumes iti: "map_iteratei α invar iti"
  shows "map_bexists α invar (iti_bexists iti)"
unfolding iti_bexists_def
proof 
  fix m P
  assume "invar m"
  with map_iteratei.iteratei_rule[OF iti, of m] 
  have iti': "map_iterator (iti m) (α m)" by simp

  from iterate_bex_correct[OF iti', of P]
  show "iterate_bex (iti m) P = (∃u v. α m u = Some v ∧ P (u, v)) "
    by (simp add: map_to_set_def)
qed


subsection {* Size (by iterate)*}

definition it_size where
  "it_size iti = (λm. iterate_size (iti m))"

lemma it_size_code[code] :
  "it_size iti m = iti m (λ_. True) (λx n . Suc n) 0"
unfolding it_size_def iterate_size_def by simp

lemma it_size_correct:
  assumes iti: "map_iteratei α invar iti"
  shows "map_size α invar (it_size iti)"
unfolding it_size_def
proof 
  fix m
  assume "invar m"
  with map_iteratei.iteratei_rule[OF iti, of m] 
  have iti': "map_iterator (iti m) (α m)" by simp

  from iterate_size_correct [OF iti']
  show "finite (dom (α m))"
       "iterate_size (iti m) = card (dom (α m))"
    by (simp_all add: finite_map_to_set card_map_to_set) 
qed 

subsection {* Size with abort (by iterate) *}

definition iti_size_abort where
  "iti_size_abort iti = (λn m. iterate_size_abort (iti m) n)"

lemma iti_size_abort_code[code] :
  "iti_size_abort iti n m = iti m (λσ. σ < n) (λx. Suc) 0"
unfolding iti_size_abort_def iterate_size_abort_def by simp

lemma iti_size_abort_correct:
  assumes iti: "map_iteratei α invar iti"
  shows "map_size_abort α invar (iti_size_abort iti)"
unfolding iti_size_abort_def
proof 
  fix m n
  assume "invar m"
  with map_iteratei.iteratei_rule[OF iti, of m] 
  have iti': "map_iterator (iti m) (α m)" by simp

  from iterate_size_abort_correct [OF iti']
  show "finite (dom (α m))"
       "iterate_size_abort (iti m) n = min n (card (dom (α m)))"
    by (simp_all add: finite_map_to_set card_map_to_set) 
qed 

subsection {* Singleton check (by size-abort) *}

definition sza_isSng where
  "sza_isSng iti = (λm. iterate_is_sng (iti m))"

lemma sza_isSng_code[code] :
  "sza_isSng iti m = (iti m (λσ. σ < 2) (λx. Suc) 0 = 1)"
unfolding sza_isSng_def iterate_is_sng_def iterate_size_abort_def by simp

lemma sza_isSng_correct:
  assumes iti: "map_iteratei α invar iti"
  shows "map_isSng α invar (sza_isSng iti)"
unfolding sza_isSng_def
proof 
  fix m 
  assume "invar m"
  with map_iteratei.iteratei_rule[OF iti, of m] 
  have iti': "map_iterator (iti m) (α m)" by simp

  have "card (map_to_set (α m)) = (Suc 0) <-> (∃kv. map_to_set (α m) = {kv})" by (simp add: card_Suc_eq)
  also have "… <-> (∃kv. α m = [fst kv \<mapsto> snd kv])" unfolding map_to_set_def
     apply (rule iff_exI)
     apply (simp add: set_eq_iff fun_eq_iff all_conj_distrib)
     apply auto
     apply (metis option.exhaust)
     apply (metis option.simps(1,2))
  done
  finally have "card (map_to_set (α m)) = (Suc 0) <-> (∃k v. α m = [k \<mapsto> v])" by simp

  with iterate_is_sng_correct [OF iti']
  show "iterate_is_sng (iti m) = (∃k v. α m = [k \<mapsto> v])"
    by simp
qed 

subsection {*Map to List (by iterate)*}

definition it_map_to_list where
  "it_map_to_list iti = (λm. iterate_to_list (iti m))"

lemma it_map_to_list_code[code] :
  "it_map_to_list iti m = iti m (λ_. True) op # []"
unfolding it_map_to_list_def iterate_to_list_def by simp

lemma it_map_to_list_correct:
  assumes iti: "map_iteratei α invar iti"
  shows "map_to_list α invar (it_map_to_list iti)"
unfolding it_map_to_list_def
proof 
  fix m
  assume "invar m"
  with map_iteratei.iteratei_rule[OF iti, of m] 
  have iti': "map_iterator (iti m) (α m)" by simp
  let ?l = "iterate_to_list (iti m)"

  from iterate_to_list_correct [OF iti']
  have set_l_eq: "set ?l = map_to_set (α m)" and dist_l: "distinct ?l" by simp_all

  from dist_l show dist_fst_l: "distinct (map fst ?l)"
    by (simp add: distinct_map set_l_eq map_to_set_def inj_on_def)
    
  from map_of_map_to_set[of ?l "α m", OF dist_fst_l] set_l_eq
  show "map_of (iterate_to_list (iti m)) = α m" by simp
qed


subsection {*List to Map*}

(* Tail recursive version *)
fun gen_list_to_map_aux
  :: "('k => 'v => 'm => 'm) => 'm => ('k×'v) list => 'm"
  where
  "gen_list_to_map_aux upd accs [] = accs" |
  "gen_list_to_map_aux upd accs ((k,v)#l) = gen_list_to_map_aux upd (upd k v accs) l"

definition "gen_list_to_map empt upd l == gen_list_to_map_aux upd (empt ()) (rev l)"

lemma gen_list_to_map_correct:
  assumes "map_empty α invar empt"
  assumes "map_update α invar upd"
  shows "list_to_map α invar (gen_list_to_map empt upd)"
proof -
  interpret map_empty α invar empt by fact
  interpret map_update α invar upd by fact

  { -- "Show a generalized lemma"
    fix l accs
    have "invar accs ==> α (gen_list_to_map_aux upd accs l) = α accs ++ map_of (rev l)
          ∧ invar (gen_list_to_map_aux upd accs l)"
     apply (induct l arbitrary: accs)
     apply simp
     apply (case_tac a)
     apply (simp add: update_correct)
     done
  } thus ?thesis
    apply (unfold_locales)
    apply (unfold gen_list_to_map_def)
    apply (auto simp add: empty_correct)
    done
qed

subsection {* Singleton (by empty, update) *}
definition eu_sng
  :: "(unit => 'm) => ('k => 'v => 'm => 'm) => 'k => 'v => 'm"
  where "eu_sng empt update k v == update k v (empt ())"

lemma eu_sng_correct:
  fixes empty
  assumes "map_empty α invar empty"
  assumes "map_update α invar update"
  shows "map_sng α invar (eu_sng empty update)"
proof -
  interpret map_empty α invar empty by fact
  interpret map_update α invar update by fact

  show ?thesis
    apply (unfold_locales)
    apply (simp_all add: update_correct empty_correct eu_sng_def)
  done
qed


subsection {* Min (by iterateoi) *}

lemma itoi_min_correct:
  assumes iti: "map_iterateoi α invar iti"
  shows "map_min α invar (iti_sel_no_map iti)"
unfolding iti_sel_no_map_def
proof 
  fix m P

  assume "invar m"
  with map_iterateoi.iterateoi_rule [OF iti, of m]
  have iti': "map_iterator_linord (iti m) (α m)" by simp
  note sel_correct = iterate_sel_no_map_map_linord_correct[OF iti', of P]
 
  { assume "rel_of (α m) P ≠ {}"
    with sel_correct show "iterate_sel_no_map (iti m) P ∈ Some ` rel_of (α m) P"
      by (auto simp add: image_iff rel_of_def)
  }

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

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

subsection {* Max (by reverse\_iterateoi) *}

lemma ritoi_max_correct:
  assumes iti: "map_reverse_iterateoi α invar iti"
  shows "map_max α invar (iti_sel_no_map iti)"
unfolding iti_sel_no_map_def
proof 
  fix m P

  assume "invar m"
  with map_reverse_iterateoi.reverse_iterateoi_rule [OF iti, of m]
  have iti': "map_iterator_rev_linord (iti m) (α m)" by simp
  note sel_correct = iterate_sel_no_map_map_rev_linord_correct[OF iti', of P]
 
  { assume "rel_of (α m) P ≠ {}"
    with sel_correct show "iterate_sel_no_map (iti m) P ∈ Some ` rel_of (α m) P"
      by (auto simp add: image_iff rel_of_def)
  }

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

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


subsection {* Conversion to sorted list (by reverse\_iterateo) *}

lemma rito_map_to_sorted_list_correct:
  assumes iti: "map_reverse_iterateoi α invar iti"
  shows "map_to_sorted_list α invar (it_map_to_list iti)"
unfolding it_map_to_list_def
proof 
  fix m
  assume "invar m"
  with map_reverse_iterateoi.reverse_iterateoi_rule[OF iti, of m] 
  have iti': "map_iterator_rev_linord (iti m) (α m)" by simp
  let ?l = "iterate_to_list (iti m)"

  from iterate_to_list_map_rev_linord_correct [OF iti']
  show "sorted (map fst ?l)" 
       "distinct (map fst ?l)"
       "map_of (iterate_to_list (iti m)) = α m" by simp_all
qed


subsection {* image restrict *}

definition it_map_image_filter ::
  "('s1 => ('u1 × 'v1,'s2) set_iterator) => (unit => 's2) => ('u2 => 'v2 => 's2 => 's2) => ('u1 × 'v1 => ('u2 × 'v2) option) => 's1 => 's2"
  where "it_map_image_filter map_it map_emp map_up_dj f m ≡
         iterate_to_map map_emp map_up_dj (set_iterator_image_filter f (map_it m))"

lemma it_map_image_filter_alt_def[code]:
  "it_map_image_filter map_it map_emp map_up_dj f m ≡
   map_it m (λ_. True) (λkv σ. case (f kv) of None => σ | Some (k', v') => (map_up_dj k' v' σ)) (map_emp ())"
unfolding it_map_image_filter_def iterate_to_map_alt_def set_iterator_image_filter_def prod_case_beta
by simp

lemma it_map_image_filter_correct:
  fixes α1 :: "'s1 => 'u1 \<rightharpoonup> 'v1"
  fixes α2 :: "'s2 => 'u2 \<rightharpoonup> 'v2" 
  assumes it: "map_iteratei α1 invar1 map_it"
  assumes emp: "map_empty α2 invar2 map_emp"
  assumes up: "map_update_dj α2 invar2 map_up_dj"
  shows "map_image_filter α1 invar1 α2 invar2 (it_map_image_filter map_it map_emp map_up_dj)"
proof 
  fix m k' v' and f :: "('u1 × 'v1) => ('u2 × 'v2) option"
  assume invar_m: "invar1 m" and
         unique_f: "transforms_to_unique_keys (α1 m) f"

  from map_iteratei.iteratei_rule[OF it, OF invar_m] 
  have iti_m: "map_iterator (map_it m) (α1 m)" by simp

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

  def vP ≡ "λk v. ∃k' v'. α1 m k' = Some v' ∧ f (k', v') = Some (k, v)"
  have vP_intro: "!!k v. (∃k' v'. α1 m k' = Some v' ∧ f (k', v') = Some (k, v)) <-> vP k v"
    unfolding vP_def by simp
  { fix k v
    have "Eps_Opt (vP k) = Some v <-> vP k v"
      using unique_f unfolding vP_def transforms_to_unique_keys_def 
      apply (rule_tac Eps_Opt_eq_Some)
      apply (metis Pair_eq option.inject)
    done
  } note Eps_vP_elim[simp] = this
  have map_intro: "{y. ∃x. x ∈ map_to_set (α1 m) ∧ f x = Some y} = map_to_set (λk. Eps_Opt (vP k))"
    by (simp add: map_to_set_def vP_intro set_eq_iff split: prod.splits)

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

  from iterate_to_map_correct [OF up emp iti_filter]
  show "invar2 (it_map_image_filter map_it map_emp map_up_dj f m) ∧
       (α2 (it_map_image_filter map_it map_emp map_up_dj f m) k' = Some v') =
       (∃k v. α1 m k = Some v ∧ f (k, v) = Some (k', v'))"
    unfolding it_map_image_filter_def vP_def[symmetric]
    by (simp add: vP_intro)
qed


definition mif_map_value_image_filter :: 
  "(('u × 'v1 => ('u × 'v2) option) => 's1 => 's2) =>
    ('u => 'v1 => 'v2 option) => 's1 => 's2"
where
    "mif_map_value_image_filter mif f ≡
     mif (λ(k, v). case (f k v) of Some v' => Some (k, v') | None => None)"

lemma mif_map_value_image_filter_correct :
  fixes α1 :: "'s1 => 'u \<rightharpoonup> 'v1"
  fixes α2 :: "'s2 => 'u \<rightharpoonup> 'v2" 
shows "map_image_filter α1 invar1 α2 invar2 mif ==>
       map_value_image_filter α1 invar1 α2 invar2 (mif_map_value_image_filter mif)"
proof -
  assume "map_image_filter α1 invar1 α2 invar2 mif"
  then interpret map_image_filter α1 invar1 α2 invar2 mif . 

  show "map_value_image_filter α1 invar1 α2 invar2 (mif_map_value_image_filter mif)"
  proof (intro map_value_image_filter.intro conjI)
    fix m 
    fix f :: "'u => 'v1 => 'v2 option"
    assume invar: "invar1 m"

    let ?f = "λ(k, v). case (f k v) of Some v' => Some (k, v') | None => None"
    have unique_f: "transforms_to_unique_keys (α1 m) ?f"
      unfolding transforms_to_unique_keys_def
      by (auto split: option.split)

    note correct' = map_image_filter_correct [OF invar unique_f, folded mif_map_value_image_filter_def]

    from correct' show "invar2 (mif_map_value_image_filter mif f m)"
      by simp

    have "!!k. α2 (mif_map_value_image_filter mif f m) k = Option.bind (α1 m k) (f k)"
    proof -
      fix k
      show "α2 (mif_map_value_image_filter mif f m) k = Option.bind (α1 m k) (f k)"
      using correct'
      apply (cases "Option.bind (α1 m k) (f k)")
      apply (auto split: option.split)
      apply (case_tac "α1 m k")
      apply (auto split: option.split)
      apply (metis option.inject)
      done
    qed
    thus "α2 (mif_map_value_image_filter mif f m) = (λk. Option.bind (α1 m k) (f k))"
      by (simp add: fun_eq_iff)
  qed
qed

definition it_map_value_image_filter ::
  "('s1 => ('u × 'v1,'s2) set_iterator) => (unit => 's2) => ('u => 'v2 => 's2 => 's2) => 
   ('u => 'v1 => 'v2 option) => 's1 => 's2" where
  "it_map_value_image_filter map_it map_emp map_up_dj f ≡
   it_map_image_filter map_it map_emp map_up_dj
     (λ(k, v). case (f k v) of Some v' => Some (k, v') | None => None)"

lemma it_map_value_image_filter_alt_def :
  "it_map_value_image_filter map_it map_emp map_up_dj =
   mif_map_value_image_filter (it_map_image_filter map_it map_emp map_up_dj)"
apply (simp add: fun_eq_iff)
unfolding it_map_image_filter_def mif_map_value_image_filter_def
  it_map_value_image_filter_def
by fast

lemma it_map_value_image_filter_correct:
  fixes α1 :: "'s1 => 'u \<rightharpoonup> 'v1"
  fixes α2 :: "'s2 => 'u \<rightharpoonup> 'v2" 
  assumes it: "map_iteratei α1 invar1 map_it"
  assumes emp: "map_empty α2 invar2 map_emp"
  assumes up: "map_update_dj α2 invar2 map_up_dj"
  shows "map_value_image_filter α1 invar1 α2 invar2 
    (it_map_value_image_filter map_it map_emp map_up_dj)"
proof -
  note mif_OK = it_map_image_filter_correct [OF it emp up]
  note mif_map_value_image_filter_correct [OF mif_OK]
  thus ?thesis
    unfolding it_map_value_image_filter_alt_def
    by fast
qed


definition mif_map_restrict :: 
  "(('u × 'v => ('u × 'v) option) => 's1 => 's2) =>
   ('u × 'v => bool) => 's1 => 's2"
where
    "mif_map_restrict mif P ≡
     mif (λ(k, v). if (P (k, v)) then Some (k, v) else None)"

lemma mif_map_restrict_alt_def :
  "mif_map_restrict mif P =
   mif_map_value_image_filter mif (λk v. if (P (k, v)) then Some v else None)"
proof -
  have "(λk v. if P (k, v) then Some (k, v) else None) =
        (λk v. case if P (k, v) then Some v else None of None => None
               | Some v' => Some (k, v'))" 
    by (simp add: fun_eq_iff)
  thus ?thesis
    unfolding mif_map_restrict_def mif_map_value_image_filter_def
    by simp
qed

lemma mif_map_restrict_correct :
  fixes α1 :: "'s1 => 'u \<rightharpoonup> 'v"
  fixes α2 :: "'s2 => 'u \<rightharpoonup> 'v" 
shows "map_image_filter α1 invar1 α2 invar2 mif ==>
       map_restrict α1 invar1 α2 invar2 (mif_map_restrict mif)"
proof -
  assume "map_image_filter α1 invar1 α2 invar2 mif"
  then interpret map_value_image_filter α1 invar1 α2 invar2 
                "mif_map_value_image_filter mif"
    by (rule mif_map_value_image_filter_correct) 

  show ?thesis
    unfolding mif_map_restrict_alt_def map_restrict_def
    apply (auto simp add: map_value_image_filter_correct fun_eq_iff
              restrict_map_def)
    apply (case_tac "α1 m x")
    apply auto
  done
qed

definition it_map_restrict ::
  "('s1 => ('u × 'v,'s2) set_iterator) => (unit => 's2) => ('u => 'v => 's2 => 's2) => 
   ('u × 'v => bool) => 's1 => 's2" where
  "it_map_restrict map_it map_emp map_up_dj P ≡
   it_map_image_filter map_it map_emp map_up_dj
     (λ(k, v). if (P (k, v)) then Some (k, v) else None)"

lemma it_map_restrict_alt_def :
  "it_map_restrict map_it map_emp map_up_dj =
   mif_map_restrict (it_map_image_filter map_it map_emp map_up_dj)"
apply (simp add: fun_eq_iff)
unfolding it_map_image_filter_def mif_map_restrict_def
  it_map_restrict_def
by fast

lemma it_map_restrict_correct:
  fixes α1 :: "'s1 => 'u \<rightharpoonup> 'v"
  fixes α2 :: "'s2 => 'u \<rightharpoonup> 'v" 
  assumes it: "map_iteratei α1 invar1 map_it"
  assumes emp: "map_empty α2 invar2 map_emp"
  assumes up: "map_update_dj α2 invar2 map_up_dj"
  shows "map_restrict α1 invar1 α2 invar2 
    (it_map_restrict map_it map_emp map_up_dj)"
proof -
  note mif_OK = it_map_image_filter_correct [OF it emp up]
  note mif_map_restrict_correct [OF mif_OK]
  thus ?thesis
    unfolding it_map_restrict_alt_def
    by fast
qed

end