Theory SetIterator

(*  Title:       Iterators over Finite Sets
    Author:      Thomas Tuerk <tuerk@in.tum.de>
    Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
section ‹\isaheader{Iterators over Finite Sets}›
theory SetIterator
imports 
  Automatic_Refinement.Misc 
  Automatic_Refinement.Foldi 
  (*"../../Refine_Monadic/Refine_Monadic"*)
begin

text ‹When reasoning about finite sets, it is often handy to be able to iterate over the elements
  of the set. If the finite set is represented by a list, the @{term fold} operation can be used.
  For general finite sets, the order of elements is not fixed though. Therefore, nondeterministic
  iterators are introduced in this theory.›

subsection ‹General Iterators›

type_synonym ('x,'σ) set_iterator = "('σ⇒bool) ⇒ ('x⇒'σ⇒'σ) ⇒ 'σ ⇒ 'σ"

locale set_iterator_genord =
  fixes iti::"('x,'σ) set_iterator" 
    and S0::"'x set" 
    and R::"'x ⇒ 'x ⇒ bool"
  assumes foldli_transform:
    "∃l0. distinct l0 ∧ S0 = set l0 ∧ sorted_wrt R l0 ∧ iti = foldli l0"
begin
  text ‹Let's prove some trivial lemmata to show that the formalisation agrees with
          the view of iterators described above.›
  lemma set_iterator_weaken_R :
    "(⋀x y. ⟦x ∈ S0; y ∈ S0; R x y⟧ ⟹ R' x y) ⟹ 
             set_iterator_genord iti S0 R'"
    by (metis set_iterator_genord.intro foldli_transform sorted_wrt_mono_rel)

  lemma finite_S0 :
    shows "finite S0"
    by (metis finite_set foldli_transform)

  lemma iti_stop_rule_cond :
    assumes not_c: "¬(c σ)"
    shows "iti c f σ = σ"
  proof -
    from foldli_transform obtain l0 where l0_props:
      "iti c = foldli l0 c" by blast
    with foldli_not_cond [of c σ l0 f, OF not_c]
    show ?thesis by simp
  qed

  lemma iti_stop_rule_emp :
    assumes S0_emp: "S0 = {}"
    shows "iti c f σ = σ"
  proof -
    from foldli_transform obtain l0 where l0_props:
      "S0 = set l0" "iti c = foldli l0 c" by blast
    with foldli.simps(1) [of c f σ] S0_emp
    show ?thesis by simp
  qed

  text ‹Reducing everything to folding is cumbersome. Let's
          define a few high-level inference rules.›

  lemma iteratei_rule_P:
    assumes 
      "I S0 σ0"
      "⋀S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0; 
                 ∀y∈S - {x}. R x y; ∀y∈S0 - S. R y x⟧ 
                 ⟹ I (S - {x}) (f x σ)"
      "⋀σ. I {} σ ⟹ P σ"
      "⋀σ S. ⟦ S ⊆ S0; S ≠ {}; ¬ c σ; I S σ;
               ∀x∈S. ∀y∈S0-S. R y x ⟧ ⟹ P σ"
    shows "P (iti c f σ0)"
  proof -
    { fix P I σ0 f
      assume
        I: "I S0 σ0" and 
        R: "⋀S σ x. ⟦c σ; x ∈ S; I S σ; S ⊆ S0; ∀y∈S-{x}. R x y⟧ ⟹ I (S - {x}) (f x σ)" and
        C1: "I {} (iti c f σ0) ⟹ P" and
        C2:"⋀S. ⟦S ⊆ S0; S ≠ {}; ¬ c (iti c f σ0); I S (iti c f σ0)⟧ ⟹ P"

      from foldli_transform obtain l0 where l0_props:
         "distinct l0" "S0 = set l0" "sorted_wrt R l0"  "iti c = foldli l0 c" by auto

      from I R  
      have "I {} (iti c f σ0) ∨ 
          (∃S. S ⊆ S0 ∧ S ≠ {} ∧ 
               ¬ (c (iti c f σ0)) ∧ 
               I S (iti c f σ0))" 
        unfolding l0_props using l0_props(1,3)
      proof (induct l0 arbitrary: σ0)
        case Nil thus ?case by simp
      next
        case (Cons x l0)
        note ind_hyp = Cons(1)
        note I_x_l0 = Cons(2)
        note step = Cons(3)
        from Cons(4) have dist_l0: "distinct l0" and x_nin_l0: "x ∉ set l0" by simp_all
        from Cons(5) have R_l0: "∀y∈set l0. R x y" and 
                          sort_l0: "sorted_wrt R l0" by simp_all

        show ?case
        proof (cases "c σ0")
          case False
          with I_x_l0 show ?thesis
            apply (rule_tac disjI2)
            apply (rule_tac exI[where x="set (x # l0)"])
            apply (simp)
          done
        next
          case True note c_σ0 = this

          from step[of σ0 x "set (x # l0)"] I_x_l0 R_l0 c_σ0 x_nin_l0
          have step': "I (set l0) (f x σ0)"
            by (simp_all add: Ball_def)

          from ind_hyp [OF step' step dist_l0 sort_l0]
          have "I {} (foldli l0 c f (f x σ0)) ∨ 
                (∃S. S ⊆ set l0 ∧ S ≠ {} ∧
                ¬ c (foldli l0 c f (f x σ0)) ∧ I S (foldli l0 c f (f x σ0)))" 
            by (fastforce)
          thus ?thesis
            by (simp add: c_σ0 subset_iff) metis
        qed
      qed
      with C1 C2 have "P" by blast
    } note aux = this

    from assms
    show ?thesis 
      apply (rule_tac aux [of "λS σ. I S σ ∧ (∀x∈S. ∀y∈S0-S. R y x)" σ0 f])
      apply auto
    done
  qed

  text ‹Instead of removing elements one by one from the invariant, adding them is sometimes more natural.›
  lemma iteratei_rule_insert_P:
  assumes pre :
      "I {} σ0"
      "⋀S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0; ∀y∈(S0 - S) - {x}. R x y;
                 ∀y∈S. R y x⟧ 
                  ⟹ I (insert x S) (f x σ)"
      "⋀σ. I S0 σ ⟹ P σ"
      "⋀σ S. ⟦ S ⊆ S0; S ≠ S0; 
              ¬ (c σ); I S σ; ∀x∈S0-S. ∀y∈S. R y x ⟧ ⟹ P σ"
  shows "P (iti c f σ0)"
  proof -
    let ?I' = "λS σ. I (S0 - S) σ"

    have pre1: 
      "!!σ S. ⟦ S ⊆ S0; S ≠ {}; ¬ (c σ); ?I' S σ;
             ∀x∈S. ∀y∈S0-S. R y x⟧ ⟹ P σ"
    proof -
      fix S σ
      assume AA: 
        "S ⊆ S0" "S ≠ {}"
        "¬ (c σ)" 
        "?I' S σ" "∀x∈S. ∀y∈S0-S. R y x"
      with pre(4) [of "S0 - S"]
      show "P σ" by auto
    qed

    have pre2 :"⋀x S σ. ⟦c σ; x ∈ S; S ⊆ S0; ?I' S σ; ∀y∈S - {x}. R x y; ∀y∈S0-S. R y x ⟧ ⟹ ?I' (S - {x}) (f x σ)"
    proof -
      fix x S σ
      assume AA : "c σ" "x ∈ S" "S ⊆ S0" "?I' S σ" "∀y∈S - {x}. R x y" "∀y∈S0 - S. R y x" 

      from AA(2) AA(3) have "S0 - (S - {x}) = insert x (S0 - S)" "S0 - (S0 - S) = S" by auto
      moreover 
      note pre(2) [of σ x "S0 - S"] AA
      ultimately show "?I' (S - {x}) (f x σ)"
        by auto
    qed

    show "P (iti c f σ0)" 
      apply (rule iteratei_rule_P [of ?I' σ0 c f P])
      apply (simp add: pre)
      apply (rule pre2) apply simp_all
      apply (simp add: pre(3))
      apply (simp add: pre1)
    done
  qed

  text ‹Show that iti without interruption is related to fold›
  lemma iti_fold: 
  assumes lc_f: "comp_fun_commute f"
    shows "iti (λ_. True) f σ0 = Finite_Set.fold f σ0 S0"
  proof (rule iteratei_rule_insert_P [where I = "λX σ'. σ' = Finite_Set.fold f σ0 X"])
    fix S σ x
    assume "x ∈ S0 - S" "S ⊆ S0" and σ_eq: "σ = Finite_Set.fold f σ0 S"
    from finite_S0 ‹S ⊆ S0› have fin_S: "finite S" by (metis finite_subset)
    from ‹x ∈ S0 - S› have x_nin_S: "x ∉ S" by simp

    interpret comp_fun_commute: comp_fun_commute f
      by (fact lc_f)
    note fold_eq = comp_fun_commute.fold_insert [OF fin_S x_nin_S]
    show "f x σ = Finite_Set.fold f σ0 (insert x S)"
      by (simp add: fold_eq σ_eq)
  qed simp_all
end


subsection ‹Iterators over Maps›

type_synonym ('k,'v,'σ) map_iterator = "('k×'v,'σ) set_iterator"

text ‹Iterator over the key-value pairs of a finite map are called iterators over maps.›
abbreviation "map_iterator_genord it m R ≡ set_iterator_genord it (map_to_set m) R"

subsection ‹Unordered Iterators›

text ‹Often one does not care about the order in which the elements are processed. 
        Therefore, the selection function can be set to not impose any further restrictings.
        This leads to considerably simpler theorems.›

definition "set_iterator it S0 ≡ set_iterator_genord it S0 (λ_ _. True)"
abbreviation "map_iterator it m ≡ set_iterator it (map_to_set m)"

lemma set_iterator_intro :
    "set_iterator_genord it S0 R ⟹ set_iterator it S0"
unfolding set_iterator_def
apply (rule set_iterator_genord.set_iterator_weaken_R [where R = R])
apply simp_all
done

lemma set_iterator_no_cond_rule_P:
"⟦ set_iterator it S0;
   I S0 σ0;
   !!S σ x. ⟦ x ∈ S; I S σ; S ⊆ S0 ⟧ ⟹ I (S - {x}) (f x σ);
   !!σ. I {} σ ⟹ P σ
 ⟧ ⟹ P (it (λ_. True) f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_P [of it S0 "λ_ _. True" I σ0 "λ_. True" f P]
by simp 

lemma set_iterator_no_cond_rule_insert_P:
"⟦ set_iterator it S0;
   I {} σ0;
   !!S σ x. ⟦ x ∈ S0 - S; I S σ; S ⊆ S0 ⟧  ⟹ I (insert x S) (f x σ);
   !!σ. I S0 σ ⟹ P σ
 ⟧ ⟹ P (it (λ_. True) f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_insert_P [of it S0 "λ_ _. True" I σ0 "λ_. True" f P]
by simp 

lemma set_iterator_rule_P:
"⟦ set_iterator it S0;
   I S0 σ0;
   !!S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0 ⟧ ⟹ I (S - {x}) (f x σ);
   !!σ. I {} σ ⟹ P σ;
   !!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
 ⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_P [of it S0 "λ_ _. True" I σ0 c f P]
by simp 

lemma set_iterator_rule_insert_P:
"⟦ set_iterator it S0;
   I {} σ0;
   !!S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0 ⟧  ⟹ I (insert x S) (f x σ);
   !!σ. I S0 σ ⟹ P σ;
   !!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
 ⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_insert_P [of it S0 "λ_ _. True" I σ0 c f P]
by simp  


text‹The following rules is adapted for maps. Instead of a set of key-value pairs the invariant
       now only sees the keys.›
lemma map_iterator_genord_rule_P:
  assumes "map_iterator_genord it m R"
      and I0: "I (dom m) σ0"
      and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ; 
                             ∀k' v'. k' ∈ it-{k} ∧ m k' = Some v' ⟶ R (k, v) (k', v');
                             ∀k' v'. k' ∉ it ∧ m k' = Some v' ⟶ R (k', v') (k, v)⟧ ⟹ 
                            I (it - {k}) (f (k, v) σ)"
      and IF: "!!σ. I {} σ ⟹ P σ"
      and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ;
                         ∀k v k' v'. k ∉ it ∧ m k = Some v ∧ k' ∈ it ∧ m k' = Some v' ⟶ 
                                     R (k, v) (k', v') ⟧ ⟹ P σ"
  shows "P (it c f σ0)"
proof (rule set_iterator_genord.iteratei_rule_P [of it "map_to_set m" R "λS σ. I (fst ` S) σ" σ0 c f P])
  show "map_iterator_genord it m R" by fact
next
  show "I (fst ` map_to_set m) σ0" using I0 by (simp add: map_to_set_dom[symmetric])
next
  fix σ
  assume "I (fst ` {}) σ"
  with IF show "P σ" by simp
next
  fix σ S
  assume "S ⊆ map_to_set m" "S ≠ {}" "¬ c σ" "I (fst ` S) σ"  
         and R_prop: "∀x∈S. ∀y∈map_to_set m - S. R y x"
  let ?S' = "fst ` S"

  show "P σ"
  proof (rule II [where it = ?S'])
    from ‹S ⊆ map_to_set m›
    show "?S' ⊆ dom m"
      unfolding map_to_set_dom
      by auto
  next
    from ‹S ≠ {}› show "?S' ≠ {}" by auto
  next
    show "¬ (c σ)" by fact
  next
    show "I (fst ` S) σ" by fact
  next
    show "∀k v k' v'.
       k ∉ fst ` S ∧
       m k = Some v ∧
       k' ∈ fst ` S ∧ m k' = Some v' ⟶
       R (k, v) (k', v')" 
    proof (intro allI impI, elim conjE )
      fix k v k' v'
      assume pre_k: "k ∉ fst ` S" "m k = Some v"
      assume pre_k': "k' ∈ fst ` S" "m k' = Some v'"

      from ‹S ⊆ map_to_set m› pre_k' 
      have kv'_in: "(k', v') ∈ S"
        unfolding map_to_set_def by auto

      from ‹S ⊆ map_to_set m› pre_k
      have kv_in: "(k, v) ∈ map_to_set m - S"
        unfolding map_to_set_def 
        by (auto simp add: image_iff)

      from R_prop kv_in kv'_in
      show "R (k, v) (k',v')" by simp
    qed
  qed
next
  fix σ S kv
  assume "S ⊆ map_to_set m" "kv ∈ S" "c σ" and I_S': "I (fst ` S) σ" and 
         R_S: "∀kv'∈S - {kv}. R kv kv'" and
         R_not_S: "∀kv'∈map_to_set m - S. R kv' kv"
  let ?S' = "fst ` S" 
  obtain k v where kv_eq[simp]: "kv = (k, v)" by (rule prod.exhaust)

  have "I (fst ` S - {k}) (f (k, v) σ)"
  proof (rule IP)
    show "c σ" by fact
  next
    from ‹kv ∈ S› show "k ∈ ?S'" by (auto simp add: image_iff Bex_def)
  next
    from ‹kv ∈ S› ‹S ⊆ map_to_set m› 
    have "kv ∈ map_to_set m" by auto
    thus m_k_eq: "m k = Some v" unfolding map_to_set_def by simp
  next
    from ‹S ⊆ map_to_set m›
    show S'_subset: "?S' ⊆ dom m"
      unfolding map_to_set_dom
      by auto
  next
    show "I (fst ` S) σ" by fact
  next
    from ‹S ⊆ map_to_set m› ‹kv ∈ S›
    have S_simp: "{(k', v'). k' ∈ (fst ` S) - {k} ∧ m k' = Some v'} = S - {kv}"
      unfolding map_to_set_def subset_iff
      apply (auto simp add: image_iff Bex_def)
      apply (metis option.inject)
    done

    from R_S[unfolded S_simp[symmetric]] R_not_S
    show "∀k' v'. k' ∈ fst ` S - {k} ∧ m k' = Some v' ⟶
                  R (k, v) (k', v') " 
      by simp
  next
    from ‹S ⊆ map_to_set m› R_not_S
    show "∀k' v'. k' ∉ fst ` S ∧ m k' = Some v' ⟶ R (k', v') (k, v)" 
      apply (simp add: Ball_def map_to_set_def subset_iff image_iff)
      apply metis
    done
  qed

  moreover 
    from ‹S ⊆ map_to_set m› ‹kv ∈ S›
    have "fst ` (S - {kv}) = fst ` S - {k}"
      apply (simp add: set_eq_iff image_iff Bex_def map_to_set_def subset_iff)
      apply (metis option.inject)
    done

  ultimately show "I (fst ` (S - {kv})) (f kv σ)" by simp
qed

lemma map_iterator_genord_rule_insert_P:
  assumes "map_iterator_genord it m R"
      and I0: "I {} σ0"
      and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ; 
                             ∀k' v'. k' ∈ (dom m - it) - {k} ∧ m k' = Some v' ⟶ R (k, v) (k', v');
                             ∀k' v'. k' ∈ it ∧ m k' = Some v' ⟶ 
                               R (k', v') (k, v)⟧ ⟹ I (insert k it) (f (k, v) σ)"
      and IF: "!!σ. I (dom m) σ ⟹ P σ"
      and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ;
                         ∀k v k' v'. k ∈ it ∧ m k = Some v ∧ k' ∉ it ∧ m k' = Some v' ⟶ 
                                     R (k, v) (k', v') ⟧ ⟹ P σ"
  shows "P (it c f σ0)"
proof (rule map_iterator_genord_rule_P [of it m R "λS σ. I (dom m - S) σ"])
  show "map_iterator_genord it m R" by fact
next
  show "I (dom m - dom m) σ0" using I0 by simp
next
  fix σ
  assume "I (dom m - {}) σ"
  with IF show "P σ" by simp
next
  fix σ it
  assume assms: "it ⊆ dom m" "it ≠ {}" "¬ c σ" "I (dom m - it) σ"
                "∀k v k' v'. k ∉ it ∧ m k = Some v ∧ k' ∈ it ∧ m k' = Some v' ⟶
                             R (k, v) (k', v')"
  from assms have "dom m - it ≠ dom m" by auto
  with II[of "dom m - it" σ] assms
  show "P σ" 
    apply (simp add: subset_iff dom_def)
    apply (metis option.simps(2))
  done
next
  fix k v it σ
  assume assms: "c σ" "k ∈ it" "m k = Some v" "it ⊆ dom m" "I (dom m - it) σ"
                "∀k' v'. k' ∈ it - {k} ∧ m k' = Some v' ⟶ R (k, v) (k', v')"
                "∀k' v'. k' ∉ it ∧ m k' = Some v' ⟶ R (k', v') (k, v)"

  hence "insert k (dom m - it) = (dom m - (it - {k}))" "dom m - (dom m - it) = it" by auto
  with assms IP[of σ k "dom m - it" v]
  show "I (dom m - (it - {k})) (f (k, v) σ)" by (simp_all add: subset_iff)
qed

lemma map_iterator_rule_P:
  assumes "map_iterator it 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 (it c f σ0)"
using assms map_iterator_genord_rule_P[of it m "λ_ _. True" I σ0 c f P]
unfolding set_iterator_def
by simp

lemma map_iterator_rule_insert_P:
  assumes "map_iterator it m"
      and I0: "I {} σ0"
      and IP: "!!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 IF: "!!σ. I (dom m) σ ⟹ P σ"
      and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ ⟧ ⟹ P σ"
  shows "P (it c f σ0)"
using assms map_iterator_genord_rule_insert_P[of it m "λ_ _. True" I σ0 c f P]
unfolding set_iterator_def
by simp

lemma map_iterator_no_cond_rule_P:
  assumes "map_iterator it m"
      and I0: "I (dom m) σ0"
      and IP: "!!k v it σ. ⟦ k ∈ it; m k = Some v; it ⊆ dom m; I it σ ⟧ ⟹ I (it - {k}) (f (k, v) σ)"
      and IF: "!!σ. I {} σ ⟹ P σ"
  shows "P (it (λ_. True) f σ0)"
using assms map_iterator_genord_rule_P[of it m "λ_ _. True" I σ0 "λ_. True" f P]
unfolding set_iterator_def
by simp

lemma map_iterator_no_cond_rule_insert_P:
  assumes "map_iterator it m"
      and I0: "I {} σ0"
      and IP: "!!k v it σ. ⟦ k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ ⟧ ⟹ I (insert k it) (f (k, v) σ)"
      and IF: "!!σ. I (dom m) σ ⟹ P σ"
  shows "P (it (λ_. True) f σ0)"
using assms map_iterator_genord_rule_insert_P[of it m "λ_ _. True" I σ0 "λ_. True" f P]
unfolding set_iterator_def
by simp


subsection ‹Ordered Iterators›

text ‹Selecting according to a linear order is another case that is interesting. 
 Ordered iterators over maps, i.\,e.\ iterators over key-value pairs,
 use an order on the keys.›

context linorder begin
  definition "set_iterator_linord it S0 
    ≡ set_iterator_genord it S0 (≤)"
  definition "set_iterator_rev_linord it S0 
    ≡ set_iterator_genord it S0 (≥)"
  definition "set_iterator_map_linord it S0 ≡ 
     set_iterator_genord it S0 (λ(k,_) (k',_). k≤k')"
  definition "set_iterator_map_rev_linord it S0 ≡ 
     set_iterator_genord it S0 (λ(k,_) (k',_). k≥k')"
  abbreviation "map_iterator_linord it m ≡ 
    set_iterator_map_linord it (map_to_set m)"
  abbreviation "map_iterator_rev_linord it m ≡ 
    set_iterator_map_rev_linord it (map_to_set m)"

  lemma set_iterator_linord_rule_P:
  "⟦ set_iterator_linord it S0;
     I S0 σ0;
     !!S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S0-S ⟹ x' ≤ x; ⋀x'. x' ∈ S ⟹ x ≤ x'⟧ ⟹ I (S - {x}) (f x σ);
     !!σ. I {} σ ⟹ P σ;
     !!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀x x'. ⟦x ∈ S; x' ∈ S0-S⟧ ⟹ x' ≤ x) ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
   ⟧ ⟹ P (it c f σ0)"
  unfolding set_iterator_linord_def
  apply (rule set_iterator_genord.iteratei_rule_P [of it S0 "(≤)" I σ0 c f P])
  apply (simp_all add: Ball_def)
  apply (metis order_refl)
  done

  lemma set_iterator_linord_rule_insert_P:
  "⟦ set_iterator_linord it S0;
     I {} σ0;
     !!S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S ⟹ x' ≤ x; ⋀x'. x' ∈ S0 - S ⟹ x ≤ x'⟧  ⟹ I (insert x S) (f x σ);
     !!σ. I S0 σ ⟹ P σ;
     !!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ (⋀x x'. ⟦x ∈ S0-S; x' ∈ S⟧ ⟹ x' ≤ x) ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
   ⟧ ⟹ P (it c f σ0)"
  unfolding set_iterator_linord_def
  apply (rule set_iterator_genord.iteratei_rule_insert_P [of it S0 "(≤)" I σ0 c f P])
  apply (simp_all add: Ball_def)
  apply (metis order_refl)
  done

  lemma set_iterator_rev_linord_rule_P:
  "⟦ set_iterator_rev_linord it S0;
     I S0 σ0;
     !!S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S0-S ⟹ x ≤ x'; ⋀x'. x' ∈ S ⟹ x' ≤ x⟧ ⟹ I (S - {x}) (f x σ);
     !!σ. I {} σ ⟹ P σ;
     !!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀x x'. ⟦x ∈ S; x' ∈ S0-S⟧ ⟹ x ≤ x') ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
   ⟧ ⟹ P (it c f σ0)"
  unfolding set_iterator_rev_linord_def
  apply (rule set_iterator_genord.iteratei_rule_P [of it S0 "(≥)" I σ0 c f P])
  apply (simp_all add: Ball_def)
  apply (metis order_refl)
  done

  lemma set_iterator_rev_linord_rule_insert_P:
  "⟦ set_iterator_rev_linord it S0;
     I {} σ0;
     !!S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S ⟹ x ≤ x'; ⋀x'. x' ∈ S0 - S ⟹ x' ≤ x⟧  ⟹ I (insert x S) (f x σ);
     !!σ. I S0 σ ⟹ P σ;
     !!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹  (⋀x x'. ⟦x ∈ S0-S; x' ∈ S⟧ ⟹ x ≤ x') ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
   ⟧ ⟹ P (it c f σ0)"
  unfolding set_iterator_rev_linord_def
  apply (rule set_iterator_genord.iteratei_rule_insert_P [of it S0 "(≥)" I σ0 c f P])
  apply (simp_all add: Ball_def)
  apply (metis order_refl)
  done


  lemma set_iterator_map_linord_rule_P:
  "⟦ set_iterator_map_linord it S0;
     I S0 σ0;
     !!S σ k v. ⟦ c σ; (k, v) ∈ S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S0-S ⟹ k' ≤ k;
                  ⋀k' v'. (k', v') ∈ S ⟹ k ≤ k'⟧ ⟹ I (S - {(k,v)}) (f (k,v) σ);
     !!σ. I {} σ ⟹ P σ;
     !!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S0-S; (k', v') ∈ S⟧ ⟹ k ≤ k') ⟹
         ¬ c σ ⟹ I S σ ⟹ P σ
   ⟧ ⟹ P (it c f σ0)"
  unfolding set_iterator_map_linord_def
  apply (rule set_iterator_genord.iteratei_rule_P 
    [of it S0 "(λ(k,_) (k',_). k ≤ k')" I σ0 c f P])
  apply simp_all
  apply (auto simp add: Ball_def)
  apply (metis order_refl)
  apply metis
  done

  lemma set_iterator_map_linord_rule_insert_P:
  "⟦ set_iterator_map_linord it S0;
     I {} σ0;
     !!S σ k v. ⟦ c σ; (k, v) ∈ S0 - S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S ⟹ k' ≤ k;
                  ⋀k' v'. (k',v') ∈ S0 - S ⟹ k ≤ k'⟧  ⟹ I (insert (k,v) S) (f (k,v) σ);
     !!σ. I S0 σ ⟹ P σ;
     !!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S; (k', v') ∈ S0-S⟧ ⟹ k ≤ k') ⟹
            ¬ c σ ⟹ I S σ ⟹ P σ
   ⟧ ⟹ P (it c f σ0)"
  unfolding set_iterator_map_linord_def
  apply (rule set_iterator_genord.iteratei_rule_insert_P 
    [of it S0 "(λ(k,_) (k',_). k ≤ k')" I σ0 c f P])
  apply simp_all
  apply (auto simp add: Ball_def)
  apply (metis order_refl)
  apply metis
  done

  lemma set_iterator_map_rev_linord_rule_P:
  "⟦ set_iterator_map_rev_linord it S0;
     I S0 σ0;
     !!S σ k v. ⟦ c σ; (k, v) ∈ S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S0-S ⟹ k ≤ k';
                  ⋀k' v'. (k', v') ∈ S ⟹ k' ≤ k⟧ ⟹ I (S - {(k,v)}) (f (k,v) σ);
     !!σ. I {} σ ⟹ P σ;
     !!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S0-S; (k', v') ∈ S⟧ ⟹ k' ≤ k) ⟹ 
            ¬ c σ ⟹ I S σ ⟹ P σ
   ⟧ ⟹ P (it c f σ0)"
  unfolding set_iterator_map_rev_linord_def
  apply (rule set_iterator_genord.iteratei_rule_P 
    [of it S0 "(λ(k,_) (k',_). k ≥ k')" I σ0 c f P])
  apply simp_all
  apply (auto simp add: Ball_def)
  apply (metis order_refl)
  apply metis
  done

  lemma set_iterator_map_rev_linord_rule_insert_P:
  "⟦ set_iterator_map_rev_linord it S0;
     I {} σ0;
     !!S σ k v. ⟦ c σ; (k, v) ∈ S0 - S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S ⟹ k ≤ k';
                 ⋀k' v'. (k',v') ∈ S0 - S ⟹ k' ≤ k⟧  ⟹ I (insert (k,v) S) (f (k,v) σ);
     !!σ. I S0 σ ⟹ P σ;
     !!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S; (k', v') ∈ S0-S⟧ ⟹ k' ≤ k) ⟹ 
            ¬ c σ ⟹ I S σ ⟹ P σ
   ⟧ ⟹ P (it c f σ0)"
  unfolding set_iterator_map_rev_linord_def
  apply (rule set_iterator_genord.iteratei_rule_insert_P 
    [of it S0 "(λ(k,_) (k',_). k ≥ k')" I σ0 c f P])
  apply simp_all
  apply (auto simp add: Ball_def)
  apply (metis order_refl)
  apply metis
  done


  lemma map_iterator_linord_rule_P:
    assumes "map_iterator_linord it m"
        and I0: "I (dom m) σ0"
        and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ;
                 ⋀k'. k' ∈ it ⟹ k ≤ k'; 
                 ⋀k'. k' ∈ (dom m)-it ⟹ k' ≤ k⟧ ⟹ I (it - {k}) (f (k, v) σ)"
        and IF: "!!σ. I {} σ ⟹ P σ"
        and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ;
                  ⋀k k'. ⟦k ∈ (dom m)-it; k' ∈ it⟧ ⟹ k ≤ k'⟧ ⟹ P σ"
    shows "P (it c f σ0)"
  using assms
  unfolding set_iterator_map_linord_def
  by (rule map_iterator_genord_rule_P) auto

  lemma map_iterator_linord_rule_insert_P:
    assumes "map_iterator_linord it m"
        and I0: "I {} σ0"
        and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ;
                 ⋀k'. k' ∈ (dom m - it) ⟹ k ≤ k'; 
                 ⋀k'. k' ∈ it ⟹ k' ≤ k ⟧ ⟹ I (insert k it) (f (k, v) σ)"
        and IF: "!!σ. I (dom m) σ ⟹ P σ"
        and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ;
                  ⋀k k'. ⟦k ∈ it; k' ∈ (dom m)-it⟧ ⟹ k ≤ k'⟧ ⟹ P σ"
    shows "P (it c f σ0)"
  using assms
  unfolding set_iterator_map_linord_def
  by (rule map_iterator_genord_rule_insert_P) auto

  lemma map_iterator_rev_linord_rule_P:
    assumes "map_iterator_rev_linord it m"
        and I0: "I (dom m) σ0"
        and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ;
                 ⋀k'. k' ∈ it ⟹ k' ≤ k; 
                 ⋀k'. k' ∈ (dom m)-it ⟹ k ≤ k'⟧ ⟹ I (it - {k}) (f (k, v) σ)"
        and IF: "!!σ. I {} σ ⟹ P σ"
        and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ;
                  ⋀k k'. ⟦k ∈ (dom m)-it; k' ∈ it⟧ ⟹ k' ≤ k⟧ ⟹ P σ"
    shows "P (it c f σ0)"
  using assms
  unfolding set_iterator_map_rev_linord_def
  by (rule map_iterator_genord_rule_P) auto

  lemma map_iterator_rev_linord_rule_insert_P:
    assumes "map_iterator_rev_linord it m"
        and I0: "I {} σ0"
        and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ;
                 ⋀k'. k' ∈ (dom m - it) ⟹ k' ≤ k; 
                 ⋀k'. k' ∈ it ⟹ k ≤ k'⟧ ⟹ I (insert k it) (f (k, v) σ)"
        and IF: "!!σ. I (dom m) σ ⟹ P σ"
        and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ;
                  ⋀k k'. ⟦k ∈ it; k' ∈ (dom m)-it⟧ ⟹ k' ≤ k⟧ ⟹ P σ"
    shows "P (it c f σ0)"
  using assms
  unfolding set_iterator_map_rev_linord_def
  by (rule map_iterator_genord_rule_insert_P) auto
end

subsection ‹Conversions to foldli›

lemma set_iterator_genord_foldli_conv :
  "set_iterator_genord iti S R ⟷
   (∃l0. distinct l0 ∧ S = set l0 ∧ sorted_wrt R l0 ∧ iti = foldli l0)"
unfolding set_iterator_genord_def by simp

lemma set_iterator_genord_I [intro] :
  "⟦distinct l0; S = set l0; sorted_wrt R l0; iti = foldli l0⟧ ⟹
   set_iterator_genord iti S R" unfolding set_iterator_genord_foldli_conv
   by blast

lemma set_iterator_foldli_conv :
  "set_iterator iti S ⟷
   (∃l0. distinct l0 ∧ S = set l0 ∧ iti = foldli l0)"
unfolding set_iterator_def set_iterator_genord_def by simp

lemma set_iterator_I [intro] :
  "⟦distinct l0; S = set l0; iti = foldli l0⟧ ⟹
   set_iterator iti S" 
   unfolding set_iterator_foldli_conv
   by blast

context linorder begin
  lemma set_iterator_linord_foldli_conv :
    "set_iterator_linord iti S ⟷
     (∃l0. distinct l0 ∧ S = set l0 ∧ sorted l0 ∧ iti = foldli l0)"
  unfolding set_iterator_linord_def set_iterator_genord_def by simp

  lemma set_iterator_linord_I [intro] :
    "⟦distinct l0; S = set l0; sorted l0; iti = foldli l0⟧ ⟹
     set_iterator_linord iti S" 
     unfolding set_iterator_linord_foldli_conv
     by blast

  lemma set_iterator_rev_linord_foldli_conv :
    "set_iterator_rev_linord iti S ⟷
     (∃l0. distinct l0 ∧ S = set l0 ∧ sorted (rev l0) ∧ iti = foldli l0)"
  unfolding set_iterator_rev_linord_def set_iterator_genord_def by simp

  lemma set_iterator_rev_linord_I [intro] :
    "⟦distinct l0; S = set l0; sorted (rev l0); iti = foldli l0⟧ ⟹
     set_iterator_rev_linord iti S" 
     unfolding set_iterator_rev_linord_foldli_conv
     by blast
end


lemma map_iterator_genord_foldli_conv :
  "map_iterator_genord iti m R ⟷
   (∃(l0::('k × 'v) list). distinct (map fst l0) ∧ m = map_of l0 ∧ sorted_wrt R l0 ∧ iti = foldli l0)"
proof -
  { fix l0 :: "('k × 'v) list"
    assume dist: "distinct l0"
    have "(map_to_set m = set l0) ⟷
          (distinct (map fst l0) ∧
           m = map_of l0)"
    proof (cases "distinct (map fst l0)")
      case True thus ?thesis by (metis map_of_map_to_set)
    next
      case False note not_dist_fst = this

      with dist have "~(inj_on fst (set l0))" by (simp add: distinct_map)
      hence "set l0 ≠ map_to_set m"
        by (rule_tac notI) (simp add: map_to_set_def inj_on_def)
      with not_dist_fst show ?thesis by simp
    qed
  } 
  thus ?thesis
    unfolding set_iterator_genord_def distinct_map
    by metis
qed

lemma map_iterator_genord_I [intro] :
  "⟦distinct (map fst l0); m = map_of l0; sorted_wrt R l0; iti = foldli l0⟧ ⟹
   map_iterator_genord iti m R" 
   unfolding map_iterator_genord_foldli_conv
   by blast

lemma map_iterator_foldli_conv :
  "map_iterator iti m ⟷
   (∃l0. distinct (map fst l0) ∧ m = map_of l0 ∧ iti = foldli l0)"
unfolding set_iterator_def map_iterator_genord_foldli_conv 
by simp

lemma map_iterator_I [intro] :
  "⟦distinct (map fst l0); m = map_of l0; iti = foldli l0⟧ ⟹
   map_iterator iti m" 
   unfolding map_iterator_foldli_conv
   by blast

context linorder begin

  lemma sorted_wrt_keys_map_fst:
    "sorted_wrt (λ(k,_) (k',_). R k k') l = sorted_wrt R (map fst l)"
    by (induct l) auto

  lemma map_iterator_linord_foldli_conv :
    "map_iterator_linord iti m ⟷
     (∃l0. distinct (map fst l0) ∧ m = map_of l0 ∧ sorted (map fst l0) ∧ iti = foldli l0)"
  unfolding set_iterator_map_linord_def map_iterator_genord_foldli_conv
  by (simp add: sorted_wrt_keys_map_fst)

  lemma map_iterator_linord_I [intro] :
    "⟦distinct (map fst l0); m = map_of l0; sorted (map fst l0); iti = foldli l0⟧ ⟹
     map_iterator_linord iti m" 
     unfolding map_iterator_linord_foldli_conv
     by blast

  lemma map_iterator_rev_linord_foldli_conv :
    "map_iterator_rev_linord iti m ⟷
     (∃l0. distinct (map fst l0) ∧ m = map_of l0 ∧ sorted (rev (map fst l0)) ∧ iti = foldli l0)"
  unfolding set_iterator_map_rev_linord_def map_iterator_genord_foldli_conv 
  by (simp add: sorted_wrt_keys_map_fst)

  lemma map_iterator_rev_linord_I [intro] :
    "⟦distinct (map fst l0); m = map_of l0; sorted (rev (map fst l0)); iti = foldli l0⟧ ⟹
     map_iterator_rev_linord iti m" 
     unfolding map_iterator_rev_linord_foldli_conv
     by blast

end

end