Theory SetIteratorOperations

(*  Title:       Operations on Iterators over Finite Sets
    Author:      Thomas Tuerk <tuerk@in.tum.de>
    Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
section ‹Operations on Set Iterators›
theory SetIteratorOperations
imports Main SetIterator
begin

text‹Many operations on sets can be lifted to iterators over sets. This theory tries to introduce
the most useful such operations.›

subsection ‹Empty set›

text ‹Iterators over empty sets and singleton sets are very easy to define.›
definition set_iterator_emp :: "('a,'σ) set_iterator" where
  "set_iterator_emp c f σ0 = σ0"

lemma set_iterator_emp_foldli_conv :
  "set_iterator_emp = foldli []"
by (simp add: fun_eq_iff set_iterator_emp_def)

lemma set_iterator_genord_emp_correct :
  "set_iterator_genord set_iterator_emp {} R"
apply (rule set_iterator_genord.intro)
apply (rule exI[where x="[]"])
apply (simp add: set_iterator_emp_foldli_conv)
done

lemma set_iterator_emp_correct :
  "set_iterator set_iterator_emp {}"
using set_iterator_intro [OF set_iterator_genord_emp_correct] .

lemma (in linorder) set_iterator_linord_emp_correct :
  "set_iterator_linord set_iterator_emp {}"
unfolding set_iterator_linord_def
by (fact set_iterator_genord_emp_correct) 

lemma (in linorder) set_iterator_rev_linord_emp_correct :
  "set_iterator_rev_linord set_iterator_emp {}"
unfolding set_iterator_rev_linord_def
by (fact set_iterator_genord_emp_correct) 

lemma (in linorder) map_iterator_linord_emp_correct :
  "map_iterator_linord set_iterator_emp Map.empty"
  "set_iterator_map_linord set_iterator_emp {}"
unfolding set_iterator_map_linord_def
by (simp_all add: set_iterator_genord_emp_correct map_to_set_def) 

lemma (in linorder) map_iterator_rev_linord_emp_correct :
  "map_iterator_rev_linord set_iterator_emp Map.empty"
  "set_iterator_map_rev_linord set_iterator_emp {}"
unfolding set_iterator_map_rev_linord_def
by (simp_all add: set_iterator_genord_emp_correct map_to_set_def) 


subsection‹Singleton Sets›

definition set_iterator_sng :: "'a ⇒ ('a,'σ) set_iterator" where
  "set_iterator_sng x c f σ0 = (if c σ0 then f x σ0 else σ0)"

lemma set_iterator_sng_foldli_conv :
  "set_iterator_sng x = foldli [x]"
by (simp add: fun_eq_iff set_iterator_sng_def)

lemma set_iterator_genord_sng_correct :
  "set_iterator_genord (set_iterator_sng (x::'a)) {x} R"
apply (rule set_iterator_genord.intro)
apply (rule exI[where x="[x]"])
apply (simp add: set_iterator_sng_foldli_conv)
done

lemma set_iterator_sng_correct :
  "set_iterator (set_iterator_sng x) {x}"
unfolding set_iterator_def
by (rule set_iterator_genord_sng_correct)

lemma (in linorder) set_iterator_linord_sng_correct :
  "set_iterator_linord (set_iterator_sng x) {x}"
unfolding set_iterator_linord_def
by (simp add: set_iterator_genord_sng_correct) 

lemma (in linorder) set_iterator_rev_linord_sng_correct :
  "set_iterator_rev_linord (set_iterator_sng x) {x}"
unfolding set_iterator_rev_linord_def
by (simp add: set_iterator_genord_sng_correct) 

lemma (in linorder) map_iterator_linord_sng_correct :
  "map_iterator_linord (set_iterator_sng (k,v)) (Map.empty (k ↦ v))"
unfolding set_iterator_map_linord_def
by (simp add: set_iterator_genord_sng_correct) 

lemma (in linorder) map_iterator_rev_linord_sng_correct :
  "map_iterator_rev_linord (set_iterator_sng (k,v)) (Map.empty (k ↦ v))"
unfolding set_iterator_map_rev_linord_def
by (simp add: set_iterator_genord_sng_correct) 


subsection ‹Union›

text ‹Iterators over disjoint sets can be combined by first iterating over one and then the
other set. The result is an iterator over the union of the original sets.›

definition set_iterator_union ::
    "('a,'σ) set_iterator ⇒ ('a, 'σ) set_iterator ⇒ ('a,'σ) set_iterator" where
  "set_iterator_union it_a it_b ≡ λc f σ0. (it_b c f (it_a c f σ0))"

lemma set_iterator_union_foldli_conv :
  "set_iterator_union (foldli as) (foldli bs) = foldli (as @ bs)"
by (simp add: fun_eq_iff set_iterator_union_def foldli_append)

lemma set_iterator_genord_union_correct :
  fixes it_a :: "('a,'σ) set_iterator"
  fixes it_b :: "('a,'σ) set_iterator"
  fixes R S_a S_b
  assumes it_a: "set_iterator_genord it_a S_a R"
  assumes it_b: "set_iterator_genord it_b S_b R"
  assumes dist_Sab: "S_a ∩ S_b = {}"
  assumes R_OK: "⋀a b. ⟦a ∈ S_a; b ∈ S_b⟧ ⟹ R a b"
  shows "set_iterator_genord (set_iterator_union it_a it_b) (S_a ∪ S_b) R"
proof -
  from it_a obtain as where 
    dist_as: "distinct as" and S_a_eq: "S_a = set as" and 
    sorted_as: "sorted_wrt R as" and it_a_eq: "it_a = foldli as"
  unfolding set_iterator_genord_foldli_conv by blast

  from it_b obtain bs where 
    dist_bs: "distinct bs" and S_b_eq: "S_b = set bs" and 
    sorted_bs: "sorted_wrt R bs" and it_b_eq: "it_b = foldli bs"
  unfolding set_iterator_genord_foldli_conv by blast

  show ?thesis
  proof (rule set_iterator_genord_I [of "as @ bs"])
    from dist_Sab S_a_eq S_b_eq dist_as dist_bs
    show "distinct (as @ bs)" by simp
  next
    from S_a_eq S_b_eq 
    show "S_a ∪ S_b = set (as @ bs)" by simp
  next
    from sorted_as sorted_bs R_OK S_a_eq S_b_eq
    show "sorted_wrt R (as @ bs)"
      by (simp add: sorted_wrt_append Ball_def)
  next
    show "set_iterator_union it_a it_b = (foldli (as @ bs))"
      unfolding it_a_eq it_b_eq set_iterator_union_foldli_conv by simp
  qed
qed

lemma set_iterator_union_emp [simp] :
  "set_iterator_union (set_iterator_emp) it = it"
  "set_iterator_union it (set_iterator_emp) = it"
unfolding set_iterator_emp_def set_iterator_union_def
by simp_all

lemma set_iterator_union_correct :
  assumes it_a: "set_iterator it_a S_a"
  assumes it_b: "set_iterator it_b S_b"
  assumes dist_Sab: "S_a ∩ S_b = {}"
  shows "set_iterator (set_iterator_union it_a it_b) (S_a ∪ S_b)"
proof -
  note res' = set_iterator_genord_union_correct [OF it_a[unfolded set_iterator_def] 
                                                    it_b[unfolded set_iterator_def] dist_Sab]
  from set_iterator_intro [OF res']
  show ?thesis by simp
qed

lemma (in linorder) set_iterator_linord_union_correct :
  assumes it_a: "set_iterator_linord it_a S_a"
  assumes it_b: "set_iterator_linord it_b S_b"
  assumes ord_Sab: "⋀a b. ⟦a ∈ S_a; b ∈ S_b⟧ ⟹ a < b"
  shows "set_iterator_linord (set_iterator_union it_a it_b) (S_a ∪ S_b)"
unfolding set_iterator_linord_def
apply (rule_tac set_iterator_genord_union_correct[
   OF it_a[unfolded set_iterator_linord_def] it_b[unfolded set_iterator_linord_def]])
apply (insert ord_Sab)
apply auto
apply (metis less_le_not_le ord_Sab)
done

lemma (in linorder) set_iterator_rev_linord_union_correct :
  assumes it_a: "set_iterator_rev_linord it_a S_a"
  assumes it_b: "set_iterator_rev_linord it_b S_b"
  assumes ord_Sab: "⋀a b. ⟦a ∈ S_a; b ∈ S_b⟧ ⟹ a > b"
  shows "set_iterator_rev_linord (set_iterator_union it_a it_b) (S_a ∪ S_b)"
unfolding set_iterator_rev_linord_def
apply (rule_tac set_iterator_genord_union_correct[
   OF it_a[unfolded set_iterator_rev_linord_def] it_b[unfolded set_iterator_rev_linord_def]])
apply (insert ord_Sab)
apply auto
apply (metis less_le_not_le ord_Sab)
done

lemma (in linorder) map_iterator_linord_union_correct :
  assumes it_a: "set_iterator_map_linord it_a S_a"
  assumes it_b: "set_iterator_map_linord it_b S_b"
  assumes ord_Sab: "⋀kv kv'. ⟦kv ∈ S_a; kv' ∈ S_b⟧ ⟹ fst kv < fst kv'"
  shows "set_iterator_map_linord (set_iterator_union it_a it_b) (S_a ∪ S_b)"
  unfolding set_iterator_map_linord_def
  apply (rule set_iterator_genord_union_correct [OF 
    it_a[unfolded set_iterator_map_linord_def] 
    it_b[unfolded set_iterator_map_linord_def]])
  apply (insert ord_Sab)
  apply auto
  apply (metis less_le_not_le)
done

lemma (in linorder) map_iterator_rev_linord_union_correct :
  assumes it_a: "set_iterator_map_rev_linord it_a S_a"
  assumes it_b: "set_iterator_map_rev_linord it_b S_b"
  assumes ord_Sab: "⋀kv kv'. ⟦kv ∈ S_a; kv' ∈ S_b⟧ ⟹ fst kv > fst kv'"
  shows "set_iterator_map_rev_linord (set_iterator_union it_a it_b) (S_a ∪ S_b)"
  unfolding set_iterator_map_rev_linord_def
  apply (rule set_iterator_genord_union_correct [OF 
    it_a[unfolded set_iterator_map_rev_linord_def] 
    it_b[unfolded set_iterator_map_rev_linord_def]])
  apply (insert ord_Sab)
  apply auto
  apply (metis less_le_not_le)
done


subsection ‹Product›

definition set_iterator_product :: 
    "('a,'σ) set_iterator ⇒ ('a ⇒ ('b,'σ) set_iterator) ⇒ ('a × 'b ,'σ) set_iterator" where
  "set_iterator_product it_a it_b ≡ λc f σ0.
    it_a c (
      λa σ. it_b a c (λb σ. f (a,b) σ) σ
    ) σ0"


lemma set_iterator_product_foldli_conv: 
  "set_iterator_product (foldli as) (λa. foldli (bs a)) =
   foldli (concat (map (λa. map (λb. (a, b)) (bs a)) as))"
apply (induct as)
  apply (simp add: set_iterator_product_def)
apply (simp add: set_iterator_product_def foldli_append foldli_map o_def fun_eq_iff)
done

lemma set_iterator_product_it_b_cong: 
assumes it_a_OK: "set_iterator it_a S_a"
    and it_b_b': "⋀a. a ∈ S_a ⟹ it_b a = it_b' a"
shows "set_iterator_product it_a it_b =
       set_iterator_product it_a it_b'"
proof -
  from it_a_OK obtain as where 
    dist_as: "distinct as" and S_a_eq: "S_a = set as" and 
    it_a_eq: "it_a = foldli as"
  unfolding set_iterator_foldli_conv by blast
  
  from it_b_b'[unfolded S_a_eq]
  show ?thesis unfolding it_a_eq
    by (induct as) 
       (simp_all add: set_iterator_product_def it_b_b' fun_eq_iff)
qed

definition set_iterator_product_order ::
  "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'b ⇒ 'b ⇒ bool) ⇒
   ('a × 'b) ⇒ ('a × 'b) ⇒ bool" where
  "set_iterator_product_order R_a R_b ab ab' ⟷
   (if (fst ab = fst ab') then R_b (fst ab) (snd ab) (snd ab') else
                               R_a (fst ab) (fst ab'))"

lemma set_iterator_genord_product_correct :
  fixes it_a :: "('a,'σ) set_iterator"
  fixes it_b :: "'a ⇒ ('b,'σ) set_iterator" 
  assumes it_a: "set_iterator_genord it_a S_a R_a"
  assumes it_b: "⋀a. a ∈ S_a ⟹ set_iterator_genord (it_b a) (S_b a) (R_b a)"
  shows "set_iterator_genord (set_iterator_product it_a it_b) (Sigma S_a S_b) 
             (set_iterator_product_order R_a R_b)"
proof -
  from it_a obtain as where 
    dist_as: "distinct as" and S_a_eq: "S_a = set as" and 
    sorted_as: "sorted_wrt R_a as" and it_a_eq: "it_a = foldli as"
  unfolding set_iterator_genord_foldli_conv by blast

  from it_b obtain bs where 
    dist_bs: "⋀a. a ∈ set as ⟹ distinct (bs a)" and S_b_eq: "⋀a. a ∈ set as ⟹  S_b a = set (bs a)" and 
    sorted_bs: "⋀a. a ∈ set as ⟹ sorted_wrt (R_b a) (bs a)" and 
    it_b_eq: "⋀a. a ∈ set as ⟹ it_b a = foldli (bs a)"
  unfolding set_iterator_genord_foldli_conv by (metis S_a_eq)

  let ?abs = "concat (map (λa. map (λb. (a, b)) (bs a)) as)"

  show ?thesis
  proof (rule set_iterator_genord_I[of ?abs])
    from set_iterator_product_it_b_cong[of it_a S_a it_b, 
       OF set_iterator_intro[OF it_a] it_b_eq] it_a_eq S_a_eq
    have "set_iterator_product it_a it_b =
          set_iterator_product (foldli as) (λa. foldli (bs a))" by simp
    thus "set_iterator_product it_a it_b = foldli ?abs"
      by (simp add: set_iterator_product_foldli_conv)
  next
    show "distinct ?abs"
    using dist_as dist_bs[unfolded S_a_eq]
    by (induct as) 
       (simp_all add: distinct_map inj_on_def dist_bs set_eq_iff image_iff)
  next
    show "Sigma S_a S_b = set ?abs" 
      unfolding S_a_eq using S_b_eq
      by (induct as) auto  
  next
    from sorted_as sorted_bs dist_as     
    show "sorted_wrt
           (set_iterator_product_order R_a R_b)
           (concat (map (λa. map (Pair a) (bs a)) as))"
    proof (induct as rule: list.induct)
      case Nil thus ?case by simp
    next
      case (Cons a as)
      from Cons(2) have R_a_as: "⋀a'. a' ∈ set as ⟹ R_a a a'" and
                        sorted_as: "sorted_wrt R_a as" by simp_all
      from Cons(3) have sorted_bs_a: "sorted_wrt (R_b a) (bs a)" 
                    and sorted_bs_as: "⋀a. a ∈ set as ⟹ sorted_wrt (R_b a) (bs a)" by simp_all
      from Cons(4) have dist_as: "distinct as" and a_nin_as: "a ∉ set as" by simp_all
      note ind_hyp = Cons(1)[OF sorted_as sorted_bs_as dist_as]
      
      define bs_a where "bs_a = bs a"
      from sorted_bs_a
      have sorted_prod_a : "sorted_wrt (set_iterator_product_order R_a R_b) (map (Pair a) (bs a))"
        unfolding bs_a_def[symmetric]
        apply (induct bs_a rule: list.induct) 
        apply (simp_all add: set_iterator_product_order_def Ball_def image_iff)
      done

      show ?case
        apply (simp add: sorted_wrt_append ind_hyp sorted_prod_a)
        apply (simp add: set_iterator_product_order_def R_a_as a_nin_as)
      done
    qed
  qed
qed

lemma set_iterator_product_correct :
  assumes it_a: "set_iterator it_a S_a"
  assumes it_b: "⋀a. a ∈ S_a ⟹ set_iterator (it_b a) (S_b a)"
  shows "set_iterator (set_iterator_product it_a it_b) (Sigma S_a S_b)"
proof -
  note res' = set_iterator_genord_product_correct [OF it_a[unfolded set_iterator_def], 
     of it_b S_b "λ_ _ _. True", OF it_b[unfolded set_iterator_def]]
  note res = set_iterator_intro [OF res']
  thus ?thesis by simp
qed


subsection ‹Filter and Image›

text ‹Filtering and applying an injective function on iterators is easily defineable as well.
  In contrast to sets the function really has to be injective, because an iterator guarentees to
  visit each element only once.›

definition set_iterator_image_filter ::
    "('a ⇒ 'b option) ⇒ ('a,'σ) set_iterator ⇒ ('b,'σ) set_iterator" where
  "set_iterator_image_filter g it ≡ λc f σ0. (it c
     (λx σ. (case (g x) of Some x' ⇒ f x' σ | None ⇒ σ)) σ0)"

lemma set_iterator_image_filter_foldli_conv :
  "set_iterator_image_filter g (foldli xs) =
   foldli (List.map_filter g xs)"
by (induct xs) (auto simp add: List.map_filter_def set_iterator_image_filter_def fun_eq_iff)  

lemma set_iterator_genord_image_filter_correct :
  fixes it :: "('a,'σ) set_iterator"
  fixes g :: "'a ⇒ 'b option"
  assumes it_OK: "set_iterator_genord it S R"
  assumes g_inj_on: "inj_on g (S ∩ dom g)"
  assumes R'_prop: "⋀x y x' y'. ⟦x ∈ S; g x = Some x'; y ∈ S; g y = Some y'; R x y⟧ ⟹ R' x' y'"
  shows "set_iterator_genord (set_iterator_image_filter g it) {y. ∃x. x ∈ S ∧ g x = Some y} R'"
proof -
  from it_OK obtain xs where 
    dist_xs: "distinct xs" and S_eq: "S = set xs" and 
    sorted_xs: "sorted_wrt R xs" and it_eq: "it = foldli xs"
  unfolding set_iterator_genord_foldli_conv by blast

  show ?thesis
  proof (rule set_iterator_genord_I [of "List.map_filter g xs"])
    show "set_iterator_image_filter g it =
          foldli (List.map_filter g xs)"
      unfolding it_eq  set_iterator_image_filter_foldli_conv by simp
  next
    from dist_xs g_inj_on[unfolded S_eq]
    show "distinct (List.map_filter g xs)"
      apply (induct xs)
      apply (simp add: List.map_filter_simps) 
      apply (simp add: List.map_filter_def image_iff inj_on_def Ball_def dom_def)
      apply (metis not_Some_eq option.sel)
    done
  next
    show "{y. ∃x. x ∈ S ∧ g x = Some y} =
          set (List.map_filter g xs)"
      unfolding S_eq set_map_filter by simp
  next
    from sorted_xs R'_prop[unfolded S_eq]
    show "sorted_wrt R' (List.map_filter g xs)"
    proof (induct xs rule: list.induct)
      case Nil thus ?case by (simp add: List.map_filter_simps) 
    next
      case (Cons x xs)
      note sort_x_xs = Cons(2)
      note R'_x_xs = Cons(3)

      from Cons have ind_hyp: "sorted_wrt R' (List.map_filter g xs)" by auto

      show ?case
        apply (cases "g x")  
        apply (simp add: List.map_filter_simps ind_hyp)
        apply (simp add: List.map_filter_simps set_map_filter Ball_def ind_hyp)
        apply (insert R'_x_xs[of x] sort_x_xs)
        apply (simp add: Ball_def)
        apply metis
      done
    qed
  qed
qed


lemma set_iterator_image_filter_correct :
  fixes it :: "('a,'σ) set_iterator"
  fixes g :: "'a ⇒ 'b option"
  assumes it_OK: "set_iterator it S"
  assumes g_inj_on: "inj_on g (S ∩ dom g)"
  shows "set_iterator (set_iterator_image_filter g it) {y. ∃x. x ∈ S ∧ g x = Some y}"
proof -
  note res' = set_iterator_genord_image_filter_correct [OF it_OK[unfolded set_iterator_def], 
     of g "λ_ _. True"]
  note res = set_iterator_intro [OF res']
  with g_inj_on show ?thesis by simp 
qed


text ‹Special definitions for only filtering or only appling a function are handy.›
definition set_iterator_filter ::
    "('a ⇒ bool) ⇒ ('a,'σ) set_iterator ⇒ ('a,'σ) set_iterator" where
  "set_iterator_filter P ≡ set_iterator_image_filter (λx. if P x then Some x else None)"

lemma set_iterator_filter_foldli_conv :
  "set_iterator_filter P (foldli xs) = foldli (filter P xs)"
  apply (simp add: set_iterator_filter_def set_iterator_image_filter_foldli_conv)
  apply (rule cong) apply simp
  apply (induct xs)
  apply (simp_all add: List.map_filter_def)
done

lemma set_iterator_filter_alt_def [code] : 
  "set_iterator_filter P it = (λc f. it c (λ(x::'a) (σ::'b). if P x then f x σ else σ))"
proof -
  have "⋀f. (λ(x::'a) (σ::'b).
             case if P x then Some x else None of None ⇒ σ
             | Some x' ⇒ f x' σ) =
            (λx σ. if P x then f x σ else σ)"
     by auto
  thus ?thesis 
    unfolding set_iterator_filter_def
              set_iterator_image_filter_def[abs_def]
    by simp
qed

lemma set_iterator_genord_filter_correct :
  fixes it :: "('a,'σ) set_iterator"
  assumes it_OK: "set_iterator_genord it S R"
  shows "set_iterator_genord (set_iterator_filter P it) {x. x ∈ S ∧ P x} R"
proof -
  let ?g = "λx. if P x then Some x else None"
  have in_dom_g: "⋀x. x ∈ dom ?g ⟷ P x" unfolding dom_def by auto

  from set_iterator_genord_image_filter_correct [OF it_OK, of ?g R, folded set_iterator_filter_def]
  show ?thesis
    by (simp add: if_split_eq1 inj_on_def Ball_def in_dom_g)
qed

lemma set_iterator_filter_correct :
  assumes it_OK: "set_iterator it S"
  shows "set_iterator (set_iterator_filter P it) {x. x ∈ S ∧ P x}"
proof -
  note res' = set_iterator_genord_filter_correct [OF it_OK[unfolded set_iterator_def], 
    of P]
  note res = set_iterator_intro [OF res']
  thus ?thesis by simp
qed

lemma (in linorder) set_iterator_linord_filter_correct :
  assumes it_OK: "set_iterator_linord it S"
  shows "set_iterator_linord (set_iterator_filter P it) {x. x ∈ S ∧ P x}"
using assms
unfolding set_iterator_linord_def
by (rule set_iterator_genord_filter_correct)

lemma (in linorder) set_iterator_rev_linord_filter_correct :
  assumes it_OK: "set_iterator_rev_linord it S"
  shows "set_iterator_rev_linord (set_iterator_filter P it) {x. x ∈ S ∧ P x}"
using assms
unfolding set_iterator_rev_linord_def
by (rule set_iterator_genord_filter_correct)

definition set_iterator_image ::
    "('a ⇒ 'b) ⇒ ('a,'σ) set_iterator ⇒ ('b,'σ) set_iterator" where
  "set_iterator_image g ≡ set_iterator_image_filter (λx. Some (g x))"

lemma set_iterator_image_foldli_conv :
  "set_iterator_image g (foldli xs) = foldli (map g xs)"
  apply (simp add: set_iterator_image_def set_iterator_image_filter_foldli_conv)
  apply (rule cong) apply simp
  apply (induct xs)
  apply (simp_all add: List.map_filter_def)
done

lemma set_iterator_image_alt_def [code] : 
  "set_iterator_image g it = (λc f. it c (λx. f (g x)))"
unfolding set_iterator_image_def
          set_iterator_image_filter_def[abs_def]
by simp

lemma set_iterator_genord_image_correct :
  fixes it :: "('a,'σ) set_iterator"
  assumes it_OK: "set_iterator_genord it S R"
  assumes g_inj: "inj_on g S"
  assumes R'_prop: "⋀x y. ⟦x ∈ S; y ∈ S; R x y⟧ ⟹ R' (g x) (g y)"
  shows "set_iterator_genord (set_iterator_image g it) (g ` S) R'"
proof -
  let ?g = "λx. Some (g x)"
  have set_eq: "⋀S. {y . ∃x. x ∈ S ∧ ?g x = Some y} = g ` S" by auto

  show ?thesis
    apply (rule set_iterator_genord_image_filter_correct [OF it_OK, of ?g R', 
     folded set_iterator_image_def set_eq[symmetric]])
    apply (insert g_inj, simp add: inj_on_def) []
    apply (insert R'_prop, auto)
  done
qed

lemma set_iterator_image_correct :
  assumes it_OK: "set_iterator it S"
  assumes g_inj: "inj_on g S"
  assumes S'_OK: "S' = g ` S"
  shows "set_iterator (set_iterator_image g it) S'"
proof -
  note res' = set_iterator_genord_image_correct [OF it_OK[unfolded set_iterator_def] g_inj, 
    of "λ_ _. True"]
  note res = set_iterator_intro [OF res', folded S'_OK]
  thus ?thesis by simp
qed



subsection ‹Construction from list (foldli)›

text ‹Iterators correspond by definition to iteration over distinct lists. They fix an order 
 in which the elements are visited. Therefore, it is trivial to construct an iterator from a 
 distinct list.›

lemma set_iterator_genord_foldli_correct :
"distinct xs ⟹ sorted_wrt R xs ⟹ set_iterator_genord (foldli xs) (set xs) R"
by (rule set_iterator_genord_I[of xs]) (simp_all)

lemma set_iterator_foldli_correct :
"distinct xs ⟹ set_iterator (foldli xs) (set xs)"
by (rule set_iterator_I[of xs]) (simp_all)

lemma (in linorder) set_iterator_linord_foldli_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted xs"
shows "set_iterator_linord (foldli xs) (set xs)"
using assms
by (rule_tac set_iterator_linord_I[of xs]) (simp_all)


lemma (in linorder) set_iterator_rev_linord_foldli_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted (rev xs)"
shows "set_iterator_rev_linord (foldli xs) (set xs)"
using assms
by (rule_tac set_iterator_rev_linord_I[of xs]) (simp_all)


lemma map_iterator_genord_foldli_correct :
"distinct (map fst xs) ⟹ sorted_wrt R xs ⟹ map_iterator_genord (foldli xs) (map_of xs) R"
by (rule map_iterator_genord_I[of xs]) simp_all

lemma map_iterator_foldli_correct :
"distinct (map fst xs) ⟹ map_iterator (foldli xs) (map_of xs)"
by (rule map_iterator_I[of xs]) (simp_all)

lemma (in linorder) map_iterator_linord_foldli_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (map fst xs)"
shows "map_iterator_linord (foldli xs) (map_of xs)"
using assms
by (rule_tac map_iterator_linord_I[of xs]) (simp_all)


lemma (in linorder) map_iterator_rev_linord_foldli_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (rev (map fst xs))"
shows "map_iterator_rev_linord (foldli xs) (map_of xs)"
using assms
by (rule_tac map_iterator_rev_linord_I[of xs]) (simp_all)


subsection ‹Construction from list (foldri)›

lemma set_iterator_genord_foldri_correct :
"distinct xs ⟹ sorted_wrt R (rev xs) ⟹ set_iterator_genord (foldri xs) (set xs) R"
by (rule set_iterator_genord_I[of "rev xs"]) (simp_all add: foldri_def)

lemma set_iterator_foldri_correct :
"distinct xs ⟹ set_iterator (foldri xs) (set xs)"
by (rule set_iterator_I[of "rev xs"]) (simp_all add: foldri_def)

lemma (in linorder) set_iterator_linord_foldri_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted (rev xs)"
shows "set_iterator_linord (foldri xs) (set xs)"
using assms
by (rule_tac set_iterator_linord_I[of "rev xs"]) (simp_all add: foldri_def)

lemma (in linorder) set_iterator_rev_linord_foldri_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted xs"
shows "set_iterator_rev_linord (foldri xs) (set xs)"
using assms
by (rule_tac set_iterator_rev_linord_I[of "rev xs"]) (simp_all add: foldri_def)

lemma map_iterator_genord_foldri_correct :
"distinct (map fst xs) ⟹ sorted_wrt R (rev xs) ⟹ map_iterator_genord (foldri xs) (map_of xs) R"
by (rule map_iterator_genord_I[of "rev xs"]) 
   (simp_all add: rev_map[symmetric] foldri_def)

lemma map_iterator_foldri_correct :
"distinct (map fst xs) ⟹ map_iterator (foldri xs) (map_of xs)"
by (rule map_iterator_I[of "rev xs"]) 
   (simp_all add: rev_map[symmetric] foldri_def)

lemma (in linorder) map_iterator_linord_foldri_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (rev (map fst xs))"
shows "map_iterator_linord (foldri xs) (map_of xs)"
using assms
by (rule_tac map_iterator_linord_I[of "rev xs"]) 
   (simp_all add: rev_map[symmetric] foldri_def)

lemma (in linorder) map_iterator_rev_linord_foldri_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (map fst xs)"
shows "map_iterator_rev_linord (foldri xs) (map_of xs)"
using assms
by (rule_tac map_iterator_rev_linord_I[of "rev xs"]) 
   (simp_all add: rev_map[symmetric] foldri_def)


subsection ‹Iterators over Maps›

text ‹In the following iterator over the key-value pairs of a finite map are called
 iterators over maps. Operations for such iterators are presented.›

subsubsection‹Domain Iterator›

text ‹One very simple such operation is iterating over only the keys of the map.›

definition map_iterator_dom where
  "map_iterator_dom it = set_iterator_image fst it"

lemma map_iterator_dom_foldli_conv :
  "map_iterator_dom (foldli kvs) = foldli (map fst kvs)"
unfolding map_iterator_dom_def set_iterator_image_foldli_conv by simp

lemma map_iterator_genord_dom_correct :
  assumes it_OK: "map_iterator_genord it m R"
  assumes R'_prop: "⋀k v k' v'. ⟦m k = Some v; m k' = Some v'; R (k, v) (k', v')⟧ ⟹ R' k k'"
  shows "set_iterator_genord (map_iterator_dom it) (dom m) R'"
proof -
  have pre1: "inj_on fst (map_to_set m)" 
     unfolding inj_on_def map_to_set_def by simp

  from set_iterator_genord_image_correct[OF it_OK pre1, of R'] R'_prop
  show ?thesis
    unfolding map_iterator_dom_def map_to_set_dom[symmetric]
    by (auto simp add: map_to_set_def)
qed

lemma map_iterator_dom_correct :
  assumes it_OK: "map_iterator it m"
  shows "set_iterator (map_iterator_dom it) (dom m)"
using assms
unfolding set_iterator_def 
apply (rule_tac map_iterator_genord_dom_correct)
apply simp_all
done

lemma (in linorder) map_iterator_linord_dom_correct :
  assumes it_OK: "map_iterator_linord it m"
  shows "set_iterator_linord (map_iterator_dom it) (dom m)"
using assms
unfolding set_iterator_linord_def set_iterator_map_linord_def  
apply (rule_tac map_iterator_genord_dom_correct)
apply assumption
apply auto
done

lemma (in linorder) map_iterator_rev_linord_dom_correct :
  assumes it_OK: "map_iterator_rev_linord it m"
  shows "set_iterator_rev_linord (map_iterator_dom it) (dom m)"
using assms
unfolding set_iterator_rev_linord_def set_iterator_map_rev_linord_def
apply (rule_tac map_iterator_genord_dom_correct)
apply assumption
apply auto
done


subsubsection‹Domain Iterator with Filter›

text ‹More complex is iterating over only the keys such that the key-value pairs satisfy some
        property.›

definition map_iterator_dom_filter ::
    "('a × 'b ⇒ bool) ⇒ ('a × 'b,'σ) set_iterator ⇒ ('a,'σ) set_iterator" where
  "map_iterator_dom_filter P it ≡ set_iterator_image_filter 
     (λxy. if P xy then Some (fst xy) else None) it"

lemma map_iterator_dom_filter_alt_def [code] :
  "map_iterator_dom_filter P it = 
   (λc f. it c (λkv σ. if P kv then f (fst kv) σ else σ))"
unfolding map_iterator_dom_filter_def set_iterator_image_filter_def
apply (rule ext)
apply (rule ext)
apply (rule arg_cong2[where f="it"])
apply (simp)
apply (simp add: fun_eq_iff split: option.splits)
done

lemma map_iterator_genord_dom_filter_correct :
  fixes it :: "('a × 'b, 'σ) set_iterator"
  assumes it_OK: "set_iterator_genord it (map_to_set m) R"
  assumes R'_prop: "⋀k1 v1 k2 v2.
      ⟦m k1 = Some v1; P (k1, v1);
       m k2 = Some v2; P (k2, v2); R (k1, v1) (k2, v2)⟧ ⟹ R' k1 k2"
  shows "set_iterator_genord (map_iterator_dom_filter P it) {k . ∃v. m k = Some v ∧ P (k, v)} R'"
proof - 
  define g where "g xy = (if P xy then Some (fst xy) else None)" for xy :: "'a × 'b"

  note set_iterator_genord_image_filter_correct [OF it_OK, of g R']

  have g_eq_Some: "⋀kv k. g kv = Some k ⟷ ((k = fst kv) ∧ P kv)"
    unfolding g_def by (auto split: prod.splits option.splits)

  have "⋀x1 x2 y. x1 ∈ map_to_set m ⟹ x2 ∈ map_to_set m ⟹
                  g x1 = Some y ⟹ g x2 = Some y ⟹ x1 = x2"
  proof -
    fix x1 x2 y
    assume x1_in: "x1 ∈ map_to_set m"
       and x2_in: "x2 ∈ map_to_set m"
       and g1_eq: "g x1 = Some y" 
       and g2_eq: "g x2 = Some y"

    obtain k1 v1 where x1_eq[simp] : "x1 = (k1, v1)" by (rule prod.exhaust)
    obtain k2 v2 where x2_eq[simp] : "x2 = (k2, v2)" by (rule prod.exhaust)

    from g1_eq g2_eq g_eq_Some have k1_eq: "k1 = k2" by simp 
    with x1_in x2_in have v1_eq: "v1 = v2"
      unfolding map_to_set_def by simp
    from k1_eq v1_eq show "x1 = x2" by simp
  qed
  hence g_inj_on: "inj_on g (map_to_set m ∩ dom g)"
    unfolding inj_on_def dom_def by auto

  have g_eq_Some: "⋀x y. (g x = Some y) ⟷ (P x ∧ y = (fst x))"
    unfolding g_def by auto

  have "set_iterator_genord (set_iterator_image_filter g it)
            {y. ∃x. x ∈ map_to_set m ∧ g x = Some y} R'" 
    apply (rule set_iterator_genord_image_filter_correct [OF it_OK, of g R', OF g_inj_on])
    apply (insert R'_prop) 
    apply (auto simp add: g_eq_Some map_to_set_def)
  done
  thus ?thesis
    unfolding map_iterator_dom_filter_def g_def[symmetric]
    by (simp add: g_eq_Some map_to_set_def)
qed

lemma map_iterator_dom_filter_correct :
  assumes it_OK: "map_iterator it m"
  shows "set_iterator (map_iterator_dom_filter P it) {k. ∃v. m k = Some v ∧ P (k, v)}"
using assms
unfolding set_iterator_def
apply (rule_tac map_iterator_genord_dom_filter_correct)
apply simp_all
done

lemma (in linorder) map_iterator_linord_dom_filter_correct :
  assumes it_OK: "map_iterator_linord it m"
  shows "set_iterator_linord (map_iterator_dom_filter P it) {k. ∃v. m k = Some v ∧ P (k, v)}"
using assms
unfolding set_iterator_map_linord_def set_iterator_linord_def 
apply (rule_tac map_iterator_genord_dom_filter_correct 
  [where R = "λ(k,_) (k',_). k≤k'"])
apply (simp_all add: set_iterator_def)
done

lemma (in linorder) set_iterator_rev_linord_map_filter_correct :
  assumes it_OK: "map_iterator_rev_linord it m"
  shows "set_iterator_rev_linord (map_iterator_dom_filter P it) 
  {k. ∃v. m k = Some v ∧ P (k, v)}"
using assms
unfolding set_iterator_map_rev_linord_def set_iterator_rev_linord_def 
apply (rule_tac map_iterator_genord_dom_filter_correct 
  [where R = "λ(k,_) (k',_). k≥k'"])
apply (simp_all add: set_iterator_def)
done


subsubsection‹Product for Maps›

definition map_iterator_product where
  "map_iterator_product it_a it_b =
   set_iterator_image (λkvv'. (fst (fst kvv'), snd kvv')) 
    (set_iterator_product it_a (λkv. it_b (snd kv)))"

lemma map_iterator_product_foldli_conv :
"map_iterator_product (foldli as) (λa. foldli (bs a)) = 
 foldli (concat (map (λ(k, v). map (Pair k) (bs v)) as))"
unfolding map_iterator_product_def set_iterator_product_foldli_conv set_iterator_image_foldli_conv
by (simp add: map_concat o_def split_def) 

lemma map_iterator_product_alt_def [code] :
  "map_iterator_product it_a it_b = 
   (λc f. it_a c (λa. it_b (snd a) c (λb. f (fst a, b))))"
unfolding map_iterator_product_def set_iterator_product_def set_iterator_image_alt_def
by simp

lemma map_iterator_genord_product_correct :
  fixes it_a :: "(('k × 'v),'σ) set_iterator"
  fixes it_b :: "'v ⇒ ('e,'σ) set_iterator" 
  fixes S_a S_b R_a R_b m
  assumes it_a: "map_iterator_genord it_a m R_a"
  assumes it_b: "⋀k v. m k = Some v ⟹ set_iterator_genord (it_b v) (S_b v) (R_b v)"
  assumes R'_prop: "⋀k v u k' v' u'.
       m k = Some v ⟹
       u ∈ S_b v ⟹
       m k' = Some v' ⟹
       u' ∈ S_b v' ⟹
       if k = k' then R_b v u u'
       else R_a (k, v) (k', v') ⟹
       R_ab (k, u) (k', u')"
  shows "set_iterator_genord (map_iterator_product it_a it_b) 
     {(k, e) . (∃v. m k = Some v ∧ e ∈ S_b v)} R_ab"
proof -
  from it_b have it_b': "⋀kv. kv ∈ map_to_set m ⟹
       set_iterator_genord (it_b (snd kv)) (S_b (snd kv)) (R_b (snd kv))"
    unfolding map_to_set_def by (case_tac kv, simp)

  have "(⋃x∈{(k, v). m k = Some v}. ⋃y∈S_b (snd x). {(x, y)}) = {((k,v), e) . 
          (m k = Some v) ∧ e ∈ S_b v}" by (auto)
  with set_iterator_genord_product_correct [OF it_a, of "λkv. it_b (snd kv)" 
    "λkv. S_b (snd kv)" "λkv. R_b (snd kv)", OF it_b']
  have it_ab': "set_iterator_genord (set_iterator_product it_a (λkv. it_b (snd kv)))
      {((k,v), e) . (m k = Some v) ∧ e ∈ S_b v}
      (set_iterator_product_order R_a
        (λkv. R_b (snd kv)))"
     (is "set_iterator_genord ?it_ab' ?S_ab' ?R_ab'")
    unfolding map_to_set_def
    by (simp add: Sigma_def)

  let ?g = "λkvv'. (fst (fst kvv'), snd kvv')"
  have inj_g: "inj_on ?g ?S_ab'"
    unfolding inj_on_def by simp

  have R_ab_OK: "⋀x y.
      x ∈ {((k, v), e). m k = Some v ∧ e ∈ S_b v} ⟹
      y ∈ {((k, v), e). m k = Some v ∧ e ∈ S_b v} ⟹
      set_iterator_product_order R_a (λkv. R_b (snd kv)) x y ⟹
      R_ab (fst (fst x), snd x) (fst (fst y), snd y)"
    apply (simp add: set_iterator_product_order_def)
    apply clarify
    apply (simp)
    apply (unfold fst_conv snd_conv)
    apply (metis R'_prop option.inject)
  done

  have "(?g ` {((k, v), e). m k = Some v ∧ e ∈ S_b v}) = {(k, e). ∃v. m k = Some v ∧ e ∈ S_b v}" 
    by (simp add: image_iff set_eq_iff)
  with set_iterator_genord_image_correct [OF it_ab' inj_g, of R_ab, OF R_ab_OK]
  show ?thesis 
    by (simp add: map_iterator_product_def)
qed

lemma map_iterator_product_correct :
  assumes it_a: "map_iterator it_a m"
  assumes it_b: "⋀k v. m k = Some v ⟹ set_iterator (it_b v) (S_b v)"
  shows "set_iterator (map_iterator_product it_a it_b) 
         {(k, e) . (∃v. m k = Some v ∧ e ∈ S_b v)}"
proof -
  note res' = map_iterator_genord_product_correct [OF it_a[unfolded set_iterator_def], 
     of it_b S_b "λ_ _ _. True"]
  note res = set_iterator_intro [OF res']
  with it_b show ?thesis unfolding set_iterator_def by simp
qed

  
subsubsection‹Key Filter›

definition map_iterator_key_filter ::
    "('a ⇒ bool) ⇒ ('a × 'b,'σ) set_iterator ⇒ ('a × 'b,'σ) set_iterator" where
  "map_iterator_key_filter P ≡ set_iterator_filter (P ∘ fst)"

lemma map_iterator_key_filter_foldli_conv :
  "map_iterator_key_filter P (foldli kvs) =  foldli (filter (λ(k, v). P k) kvs)"
unfolding map_iterator_key_filter_def set_iterator_filter_foldli_conv o_def split_def 
by simp

lemma map_iterator_key_filter_alt_def [code] :
  "map_iterator_key_filter P it = (λc f. it c (λx σ. if P (fst x) then f x σ else σ))"
unfolding map_iterator_key_filter_def set_iterator_filter_alt_def
  set_iterator_image_filter_def by simp

lemma map_iterator_genord_key_filter_correct :
  fixes it :: "('a × 'b, 'σ) set_iterator"
  assumes it_OK: "map_iterator_genord it m R"
  shows "map_iterator_genord (map_iterator_key_filter P it) (m |` {k . P k}) R"
proof - 
  from set_iterator_genord_filter_correct [OF it_OK, of "P ∘ fst", 
    folded map_iterator_key_filter_def] 
  have step1: "set_iterator_genord (map_iterator_key_filter P it)
                  {x ∈ map_to_set m. (P ∘ fst) x} R" 
    by simp

  have "{x ∈ map_to_set m. (P ∘ fst) x} = map_to_set (m |` {k . P k})"
    unfolding map_to_set_def restrict_map_def
    by (auto split: if_splits)
  with step1 show ?thesis by simp
qed

lemma map_iterator_key_filter_correct :
  assumes it_OK: "map_iterator it m"
  shows "set_iterator (map_iterator_key_filter P it) (map_to_set (m |` {k . P k}))"
using assms
unfolding set_iterator_def
apply (rule_tac map_iterator_genord_key_filter_correct)
apply simp_all
done

end