Theory SetAbstractionIterator

(*  Title:       Iterators over Representations of Finite Sets
    Author:      Thomas Tuerk <tuerk@in.tum.de>
    Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
section ‹\isaheader{Iterators over Representations of Finite Sets}›
theory SetAbstractionIterator
imports Main SetIterator 
begin

text ‹Sometimes, an iterator does not iterate over an abstract set directly. 
 Especialy, if datastructures that are composed of several concrete datastructures 
 for maps or sets are involved, it might be interesting to iterate over 
 representations of values instead of the abstract values. This leads to the following construct.› 

locale set_iterator_abs_genord =
  fixes α :: "'xc ⇒ 'xa"
    and invar :: "'xc ⇒ bool"  
    and iti::"('xc,'σ) set_iterator"
    and S0::"'xa set" 
    and R::"'xa ⇒ 'xa ⇒ bool"
  assumes foldli_transform:
    "∃lc. (∀xc ∈ set lc. invar xc) ∧ 
          distinct (map α lc) ∧ S0 = set (map α lc) ∧ 
          sorted_wrt R (map α lc) ∧ iti = foldli lc"
begin
  text ‹In the simplest case, the function used for iteration does not depend on
    the representation, but just the abstract values. In this case, the \emph{normal} iterators
    can be used with an adapted function.› 
  lemma remove_abs :
    assumes f_OK: "⋀xc. invar xc ⟹ α xc ∈ S0 ⟹ fc xc = fa (α xc)"
        and it_OK: "⋀iti. set_iterator_genord iti S0 R ⟹ P (iti c fa σ0)"
    shows "P (iti c fc σ0)"
  proof -
    from foldli_transform obtain lc where 
          lc_invar: "⋀xc. xc ∈ set lc ⟹ invar xc" 
      and α_props: "distinct (map α lc)" "S0 = set (map α lc)" 
                   "sorted_wrt R (map α lc)" 
      and iti_eq: "iti = foldli lc" by blast

    from α_props have "set_iterator_genord (foldli (map α lc)) S0 R"
      by (rule_tac set_iterator_genord_I [of "map α lc"]) simp_all
    with it_OK have P_OK: "P (foldli (map α lc) c fa σ0)" by blast

    from lc_invar f_OK[unfolded α_props(2)]
    have "foldli (map α lc) c fa σ0 = foldli lc c fc σ0"
      by (induct lc arbitrary: σ0) simp_all
 
    with P_OK iti_eq show ?thesis by simp
  qed

  text ‹In general, one needs the representation, though. Even in this case,
    the construct can be reduced to standard iterators.›
  lemma remove_abs2 :
    "∃S0'. set_iterator_genord iti S0' (λx y. R (α x) (α y)) ∧
           inj_on α S0' ∧ α ` S0' = S0 ∧ (∀x ∈ S0'. invar x)"
  proof -
    from foldli_transform obtain lc where 
          lc_invar: "⋀xc. xc ∈ set lc ⟹ invar xc" 
      and α_props: "distinct (map α lc)" "S0 = set (map α lc)" 
                   "sorted_wrt R (map α lc)" 
      and iti_eq: "iti = foldli lc" by blast
    from α_props have it': "set_iterator_genord iti (set lc) (λx y. R (α x) (α y))"
      apply (rule_tac set_iterator_genord_I [of lc])  
      apply (simp_all add: distinct_map sorted_wrt_map iti_eq)
    done

    from α_props show ?thesis
      apply (rule_tac exI[where x = "set lc"])
      apply (simp add: lc_invar distinct_map it')
    done
  qed

  text ‹Let's now derive the inference rules for iterators over representations.›

  lemma iteratei_abs_simple_rule_P:
  assumes f_OK: "⋀xc. invar xc ⟹ α xc ∈ S0 ⟹ f xc = f' (α xc)"
  assumes pre :
      "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)"
    apply (rule remove_abs[of f f' P c σ0])
    apply (simp add: f_OK)
    apply (erule set_iterator_genord.iteratei_rule_P [of _ S0 R I])
    apply (simp_all add: pre)
  done

  lemma iteratei_abs_simple_rule_insert_P:
  assumes f_OK: "⋀xc. invar xc ⟹ α xc ∈ S0 ⟹ f xc = f' (α xc)"
  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)"
    apply (rule remove_abs[of f f' P c σ0])
    apply (simp add: f_OK)
    apply (erule set_iterator_genord.iteratei_rule_insert_P [of _ S0 R I])
    apply (simp_all add: pre)
  done

  lemma iteratei_abs_rule_P:
  assumes pre :
      "I S0 σ0"
      "⋀S σ x. ⟦ c σ; invar x; α 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 -
    obtain S0' where S0'_props: "set_iterator_genord iti S0' (λx y. R (α x) (α y))"
       "inj_on α S0'" "S0 = α ` S0'" "⋀x. x ∈ S0' ⟹ invar x" by (metis remove_abs2)
  
    show ?thesis
    proof (rule set_iterator_genord.iteratei_rule_P[OF S0'_props(1), of "λS σ. I (α ` S) σ" σ0 c], goal_cases)
      case 1
      thus ?case using S0'_props pre by simp   
    next
      case 3 thus ?case using S0'_props pre by simp   
    next
      case prems: (2 S σ x)

      from prems S0'_props have inv_x: "invar x" by blast
      from prems(4) have subs_alpha: "α ` S ⊆ α ` S0'" by auto
      from S0'_props prems(2,4)
      have diff_alpha: "α ` S - {α x} = α ` (S - {x})" "α ` S0' - α ` S = α ` (S0' - S)"
       by (auto simp add: inj_on_def subset_iff Ball_def)

      show ?case 
        using pre(2)[of σ x "α ` S"] S0'_props(3)  
        by (simp add: inv_x prems subs_alpha diff_alpha)
    next
      case prems: (4 σ S)
      show ?case
        using pre(4)[of "α ` S" σ] prems S0'_props
        by auto
    qed
  qed

  lemma iteratei_abs_rule_insert_P:
  assumes pre :
      "I {} σ0"
      "⋀S σ x. ⟦ c σ; invar x; α 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 -
    obtain S0' where S0'_props: "set_iterator_genord iti S0' (λx y. R (α x) (α y))"
       "inj_on α S0'" "S0 = α ` S0'" "⋀x. x ∈ S0' ⟹ invar x" by (metis remove_abs2)
  
    show ?thesis
    proof (rule set_iterator_genord.iteratei_rule_insert_P[OF S0'_props(1), of "λS σ. I (α ` S) σ" σ0 c], goal_cases)
      case 1
      thus ?case using S0'_props pre by simp   
    next
      case 3
      thus ?case using S0'_props pre by simp   
    next
      case prems: (2 S σ x)

      from prems S0'_props have inv_x: "invar x" by blast
      from prems(4) have subs_alpha: "α ` S ⊆ α ` S0'" by auto
      from S0'_props prems(2,4)
      have diff_alpha: "α ` (S0' - S) - {α x} = α ` ((S0' - S) - {x})" "α ` S0' - α ` S = α ` (S0' - S)"
       by (auto simp add: inj_on_def subset_iff Ball_def)
      
      show ?case 
        using pre(2)[of σ x "α ` S"] prems S0'_props(3)  
        by (simp add: diff_alpha inv_x subs_alpha)
    next
      case prems: (4 σ S)

      from prems(1) have subs_alpha: "α ` S ⊆ α ` S0'" by auto

      from S0'_props prems
      have diff_alpha: "α ` S0' - α ` S = α ` (S0' - S)"
       by (auto simp add: inj_on_def subset_iff Ball_def)

      from prems(1,2) S0'_props(2,3)
      have alpha_eq: "α ` S ≠ α ` S0'"
        apply (simp add: inj_on_def set_eq_iff image_iff Bex_def subset_iff)
        apply blast
      done

      show ?case
        using pre(4)[of "α ` S" σ] S0'_props prems
        by (auto simp add: subs_alpha diff_alpha alpha_eq)
    qed
  qed
end

lemma set_iterator_abs_genord_trivial:
  "set_iterator_abs_genord id (λ_. True) = set_iterator_genord"
by (simp add: set_iterator_genord_def set_iterator_abs_genord_def fun_eq_iff)

lemma set_iterator_abs_genord_trivial_simp [simp] :
  assumes "∀x. invar x"
      and "∀x. α x = x"
shows "set_iterator_abs_genord α invar = set_iterator_genord"
proof -
  from assms have "invar = (λ_. True)" and "α = id"
    by (simp_all add: fun_eq_iff)
  thus ?thesis by (simp add: set_iterator_abs_genord_trivial)
qed

subsection ‹Introduce iterators over representations›
lemma set_iterator_abs_genord_I2 :
  assumes it_OK: "set_iterator_genord iti S0 Rc"
      and R_OK: "⋀xc1 xc2. ⟦invar xc1; invar xc2; Rc xc1 xc2⟧ ⟹ Ra (α xc1) (α xc2)"
      and dist: "⋀xc1 xc2. ⟦invar xc1; invar xc2; xc1 ∈ S0; xc2 ∈ S0; α xc1 = α xc2⟧ ⟹ xc1 = xc2"
      and invar: "⋀xc. xc ∈ S0 ⟹ invar xc"
      and S0'_eq: "S0' = α ` S0"
  shows "set_iterator_abs_genord α invar iti S0' Ra"
  proof -
    from it_OK obtain l0 where dist_l0: "distinct l0" and 
          S0_eq: "S0 = set l0" and 
          sort_Rc: "sorted_wrt Rc l0"  and iti_eq: "iti = foldli l0" 
      unfolding set_iterator_genord_def by auto

    have "set l0 ⊆ S0" unfolding S0_eq by simp
    with dist_l0 sort_Rc 
    have map_props: "distinct (map α l0) ∧ sorted_wrt Ra (map α l0)"
    proof (induct l0) 
      case Nil thus ?case by simp
    next
      case (Cons x l0)
      hence "distinct l0" and "x ∉ set l0" and "x ∈ S0" and "set l0 ⊆ S0" and
            "distinct (map α l0)" "sorted_wrt Ra (map α l0)" "⋀x'. x' ∈ set l0 ⟹ Rc x x'"
        by (simp_all)
      thus ?case using dist[of x] R_OK[of x] invar 
        apply (simp add: image_iff Ball_def subset_iff)
        apply metis
      done
    qed

    show ?thesis
      unfolding S0'_eq
      apply (rule set_iterator_abs_genord.intro)
      apply (rule_tac exI[where x = l0])
      apply (simp add: iti_eq map_props S0_eq Ball_def invar)
    done
  qed


subsection ‹Map-Iterators›

lemma map_to_set_cong: 
  "map_to_set m1 = map_to_set m2 ⟷ m1 = m2"
apply (simp add: set_eq_iff map_to_set_def)
apply (simp add: fun_eq_iff)
apply (metis not_Some_eq)
done


definition "map_iterator_abs_genord α invar it m R ≡ 
set_iterator_abs_genord (λ(k,v). (k, α v)) (λ(k,v). invar v) it (map_to_set m) R"

lemma map_iterator_abs_genord_I2 :
  assumes it_OK: "map_iterator_genord iti m R'"
      and invar: "⋀k v. m k = Some v ⟹ invar v"
      and R_OK: "⋀k v k' v'. invar v ⟹ invar v' ⟹ R' (k, v) (k', v') ⟹ R (k, α v) (k', α v')"
      and m'_eq: "m' = ((map_option α) o m)"
  shows "map_iterator_abs_genord α invar iti m' R"
proof -
  let ?α' = "λ(k,v). (k, α v)"
  let ?invar' = "λ(k,v). invar v"

  have α_rewr: "?α' ` (map_to_set m) = map_to_set ((map_option α) o m)"
    by (auto simp add: map_to_set_def)
 
  note rule' = set_iterator_abs_genord_I2[OF it_OK[unfolded set_iterator_def], 
    of ?invar' R ?α' "map_to_set (map_option α ∘ m)", unfolded α_rewr map_iterator_abs_genord_def[symmetric]]

  show ?thesis
    unfolding m'_eq
    apply (rule rule')
    apply (auto simp add: map_to_set_def invar R_OK)
  done
qed

lemma map_iterator_abs_genord_remove_abs2 :
  assumes iti: "map_iterator_abs_genord α invar iti m R"
  obtains m' where "map_iterator_genord iti m' (λ(k, v) (k', v'). R (k, α v) (k', α v'))"
       "(map_option α) o m' = m" "⋀k v. m' k = Some v ⟹ invar v"
  proof -
    let ?α' = "λ(k,v). (k, α v)"
    let ?invar' = "λ(k,v). invar v"

    from set_iterator_abs_genord.foldli_transform [OF iti[unfolded map_iterator_abs_genord_def]]
    obtain lc where lc_invar: "⋀k v. (k, v) ∈ set lc ⟹ invar v" 
      and α_props: "distinct (map ?α' lc)" "map_to_set m = set (map ?α' lc)" 
                   "sorted_wrt R (map ?α' lc)" 
      and iti_eq: "iti = foldli lc" by blast

    from α_props(2)[symmetric] have in_lc: "⋀k v. (k, v) ∈ set lc ⟹ m k = Some (α v)" 
      by (auto simp add: set_eq_iff image_iff map_to_set_def Ball_def Bex_def)
    from α_props(1) have inj_on_α': "inj_on ?α' (set lc)" by (simp add: distinct_map)

    from in_lc inj_on_α'
    have inj_on_fst: "inj_on fst (set lc)"
      apply (simp add: inj_on_def Ball_def)
      apply (metis option.inject)
    done

    let ?m' = "map_of lc"

    from α_props have it': "map_iterator_genord iti ?m' (λx y. R (?α' x) (?α' y))"
      apply (rule_tac set_iterator_genord_I [of lc])  
      apply (simp_all add: distinct_map sorted_wrt_map iti_eq map_to_set_map_of inj_on_fst)
    done

    from inj_on_fst α_props(1)
    have "distinct (map fst (map ?α' lc))" 
      by (auto simp add: distinct_map inj_on_def Ball_def)
    hence "map_to_set m = map_to_set (map_of (map ?α' lc))"
      by (simp add: α_props map_to_set_map_of)
    hence m_eq: "map_option α ∘ map_of lc = m"
      by (simp add: map_of_map[symmetric] map_to_set_cong)

    from that[of ?m'] it' lc_invar α_props(1) show ?thesis
      by (simp add: distinct_map split_def inj_on_fst ran_distinct m_eq)
  qed


lemma map_iterator_abs_genord_rule_P:
  assumes iti_OK: "map_iterator_abs_genord α invar iti m R"
      and I0: "I (dom m) σ0"
      and IP: "!!k v it σ. ⟦ c σ; k ∈ it; invar v; m k = Some (α v); it ⊆ dom m; I it σ; 
                             ∀k' v'. k' ∈ it-{k} ∧ invar v' ∧ m k' = Some (α v') ⟶ R (k, α v) (k', α v');
                             ∀k' v'. k' ∉ it ∧ invar v' ∧ 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 ∧ invar v ∧ m k = Some (α v) ∧ 
                                     k' ∈ it ∧ invar v' ∧ m k' = Some (α v') ⟶ 
                                     R (k, α v) (k', α v') ⟧ ⟹ P σ"
  shows "P (iti c f σ0)"
proof -
  let ?α' = "λ(k,v). (k, α v)"
  let ?invar' = "λ(k,v). invar v"

  from map_iterator_abs_genord_remove_abs2 [OF iti_OK]
  obtain m' where m'_props: "map_iterator_genord iti m' (λx y. R (?α' x) (?α' y))"
     "m = map_option α ∘ m'" "⋀k v. m' k = Some v ⟹ invar v" 
     by (auto simp add: split_def) 

  have dom_m'_eq: "dom m' = dom m"
    unfolding m'_props by (simp add: dom_def)

  show ?thesis
  proof (rule map_iterator_genord_rule_P[OF m'_props(1), of I], goal_cases)
    case 1
    thus ?case using I0 by (simp add: dom_m'_eq)   
  next
    case 3
    thus ?case using IF by simp   
  next
    case prems: (2 k v S σ)
    from IP [of σ k S v] prems
    show ?case
      by (simp add: m'_props) metis
  next
    case prems: (4 σ S)
    show ?case
      using II[of S σ] prems
      by (simp add: m'_props) metis
  qed
qed


lemma map_iterator_abs_genord_rule_insert_P:
  assumes iti_OK: "map_iterator_abs_genord α invar iti m R"
      and I0: "I {} σ0"
      and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; invar v; m k = Some (α v); it ⊆ dom m; I it σ; 
                             ∀k' v'. k' ∈ (dom m - it)-{k} ∧ invar v' ∧ m k' = Some (α v') ⟶ R (k, α v) (k', α v');
                             ∀k' v'. k' ∈ it ∧ invar v' ∧ 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 ∧ invar v ∧ m k = Some (α v) ∧ 
                                     k' ∉ it ∧ invar v' ∧ m k' = Some (α v') ⟶ 
                                     R (k, α v) (k', α v') ⟧ ⟹ P σ"
  shows "P (iti c f σ0)"
proof -
  let ?α' = "λ(k,v). (k, α v)"
  let ?invar' = "λ(k,v). invar v"

  from map_iterator_abs_genord_remove_abs2 [OF iti_OK]
  obtain m' where m'_props: "map_iterator_genord iti m' (λx y. R (?α' x) (?α' y))"
     "m = map_option α ∘ m'" "⋀k v. m' k = Some v ⟹ invar v" 
     by (auto simp add: split_def) 

  have dom_m'_eq: "dom m' = dom m"
    unfolding m'_props by (simp add: dom_def)

  show ?thesis
  proof (rule map_iterator_genord_rule_insert_P[OF m'_props(1), of I], goal_cases)
    case 1
    thus ?case using I0 by simp   
  next
    case 3
    thus ?case using IF by (simp add: dom_m'_eq)   
  next
    case prems: (2 k v S σ)
    from IP [of σ k S v] prems
    show ?case 
      by (simp add: m'_props) metis
  next
    case prems: (4 σ S)
    show ?case
      using II[of S σ] prems
      by (simp add: m'_props) metis
  qed
qed


subsection ‹Unsorted Iterators›

definition "set_iterator_abs α invar it S0 ≡ set_iterator_abs_genord α invar it S0 (λ_ _. True)"

lemma set_iterator_abs_trivial:
  "set_iterator_abs id (λ_. True) = set_iterator"
by (simp add: set_iterator_def set_iterator_abs_def fun_eq_iff)

lemma set_iterator_abs_trivial_simp [simp]:
  assumes "∀x. invar x"
      and "∀x. α x = x"
shows "set_iterator_abs α invar = set_iterator"
proof -
  from assms have "invar = (λ_. True)" and "α = id"
    by (simp_all add: fun_eq_iff)
  thus ?thesis by (simp add: set_iterator_abs_trivial)
qed

lemma set_iterator_abs_I2 :
  assumes it_OK: "set_iterator iti S0"
      and dist: "⋀xc1 xc2. ⟦invar xc1; invar xc2; xc1 ∈ S0; xc2 ∈ S0; α xc1 = α xc2⟧ ⟹ xc1 = xc2"
      and invar: "⋀xc. xc ∈ S0 ⟹ invar xc"
      and S0'_OK: "S0' = α ` S0"
  shows "set_iterator_abs α invar iti S0'"
unfolding set_iterator_abs_def S0'_OK
apply (rule set_iterator_abs_genord_I2[OF it_OK[unfolded set_iterator_def], of invar _ α])
apply (simp_all add: dist invar)
done


lemma set_iterator_abs_simple_rule_P:
"⟦ set_iterator_abs α invar it S0;
   (⋀xc. invar xc ⟹ f xc = f' (α xc));
   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_abs_def
using set_iterator_abs_genord.iteratei_abs_simple_rule_P [of α invar it S0 "λ_ _. True" f f' I σ0 c P]
by simp 

lemma set_iterator_abs_simple_no_cond_rule_P:
"⟦ set_iterator_abs α invar it S0;
   (⋀xc. invar xc ⟹ f xc = f' (α xc));
   I S0 σ0;
   !!S σ x. ⟦ x ∈ S; I S σ; S ⊆ S0 ⟧ ⟹ I (S - {x}) (f' x σ);
   !!σ. I {} σ ⟹ P σ
 ⟧ ⟹ P (it (λ_. True) f σ0)"
using set_iterator_abs_simple_rule_P[of α invar it S0 f f' I σ0 "λ_. True" P]
by simp 

lemma set_iterator_abs_simple_rule_insert_P :
"⟦ set_iterator_abs α invar it S0;
   (⋀xc. invar xc ⟹ f xc = f' (α xc));
   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_abs_def
using set_iterator_abs_genord.iteratei_abs_simple_rule_insert_P [of α invar it S0 "λ_ _. True" f f' I σ0 c P]
by simp 

lemma set_iterator_abs_no_cond_simple_rule_insert_P :
"⟦ set_iterator_abs α invar it S0;
   (⋀xc. invar xc ⟹ f xc = f' (α xc));
   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)"
using set_iterator_abs_simple_rule_insert_P[of α invar it S0 f f' I σ0 "λ_. True" P]
by simp 


lemma set_iterator_abs_rule_P:
"⟦ set_iterator_abs α invar it S0;
   I S0 σ0;
   !!S σ x. ⟦ c σ; invar x; α 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_abs_def
using set_iterator_abs_genord.iteratei_abs_rule_P [of α invar it S0 "λ_ _. True" I σ0 c f P]
by simp 

lemma set_iterator_abs_no_cond_rule_P:
"⟦ set_iterator_abs α invar it S0;
   I S0 σ0;
   !!S σ x. ⟦ invar x; α x ∈ S; I S σ; S ⊆ S0 ⟧ ⟹ I (S - {α x}) (f x σ);
   !!σ. I {} σ ⟹ P σ
 ⟧ ⟹ P (it (λ_. True) f σ0)"
using set_iterator_abs_rule_P[of α invar it S0 I σ0 "λ_. True" f P]
by simp 

lemma set_iterator_abs_rule_insert_P :
"⟦ set_iterator_abs α invar it S0;
   I {} σ0;
   !!S σ x. ⟦ c σ; invar x; α 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_abs_def
using set_iterator_abs_genord.iteratei_abs_rule_insert_P [of α invar it S0 "λ_ _. True" I σ0 c f P]
by simp 

lemma set_iterator_abs_no_cond_rule_insert_P :
"⟦ set_iterator_abs α invar it S0;
   I {} σ0;
   !!S σ x. ⟦ invar x; α x ∈ S0 - S; I S σ; S ⊆ S0 ⟧  ⟹ I (insert (α x) S) (f x σ);
   !!σ. I S0 σ ⟹ P σ
 ⟧ ⟹ P (it (λ_. True) f σ0)"
using set_iterator_abs_rule_insert_P[of α invar it S0 I σ0 "λ_. True" f P]
by simp 


subsection ‹Unsorted Map-Iterators›

definition "map_iterator_abs α invar it m ≡ map_iterator_abs_genord α invar it m (λ_ _. True)"

lemma map_iterator_abs_trivial:
  "map_iterator_abs id (λ_. True) = map_iterator"
by (simp add: set_iterator_def map_iterator_abs_def map_iterator_abs_genord_def 
              set_iterator_abs_genord_def set_iterator_genord_def fun_eq_iff)

lemma map_iterator_abs_trivial_simp [simp] :
  assumes "∀x. invar x"
      and "∀x. α x = x"
shows "map_iterator_abs α invar = map_iterator"
proof -
  from assms have "invar = (λ_. True)" and "α = id"
    by (simp_all add: fun_eq_iff)
  thus ?thesis by (simp add: map_iterator_abs_trivial)
qed


lemma map_iterator_abs_I2 :
  assumes it_OK: "map_iterator iti m"
      and invar: "⋀k v. m k = Some v ⟹ invar v"
      and m'_eq: "m' = map_option α ∘ m"
  shows "map_iterator_abs α invar iti m'"
using assms
unfolding map_iterator_abs_def set_iterator_def
by (rule_tac map_iterator_abs_genord_I2 [OF it_OK[unfolded set_iterator_def]]) simp_all

lemma map_iterator_abs_rule_P:
  assumes iti_OK: "map_iterator_abs α invar iti m"
      and I0: "I (dom m) σ0"
      and IP: "!!k v it σ. ⟦ c σ; k ∈ it; invar v; 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 (iti c f σ0)"
apply (rule map_iterator_abs_genord_rule_P [OF iti_OK[unfolded map_iterator_abs_def], of I])
apply (simp_all add: I0 IP IF II)
done

lemma map_iterator_abs_no_cond_rule_P:
  assumes iti_OK: "map_iterator_abs α invar iti m"
      and I0: "I (dom m) σ0"
      and IP: "!!k v it σ. ⟦ k ∈ it; invar v; m k = Some (α v); it ⊆ dom m; I it σ ⟧ ⟹ 
                            I (it - {k}) (f (k, v) σ)"
      and IF: "!!σ. I {} σ ⟹ P σ"
  shows "P (iti (λ_. True) f σ0)"
apply (rule map_iterator_abs_rule_P [OF iti_OK, of I])
apply (simp_all add: I0 IP IF)
done

lemma map_iterator_abs_rule_insert_P:
  assumes iti_OK: "map_iterator_abs α invar iti m"
      and I0: "I {} σ0"
      and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; invar v; 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 (iti c f σ0)"
apply (rule map_iterator_abs_genord_rule_insert_P [OF iti_OK[unfolded map_iterator_abs_def], of I])
apply (simp_all add: I0 IP IF II)
done

lemma map_iterator_abs_no_cond_rule_insert_P:
  assumes iti_OK: "map_iterator_abs α invar iti m"
      and I0: "I {} σ0"
      and IP: "!!k v it σ. ⟦ k ∈ dom m - it; invar v; m k = Some (α v); it ⊆ dom m; I it σ ⟧ ⟹ 
                            I (insert k it) (f (k, v) σ)"
      and IF: "!!σ. I (dom m) σ ⟹ P σ"
  shows "P (iti (λ_. True) f σ0)"
apply (rule map_iterator_abs_genord_rule_insert_P [OF iti_OK[unfolded map_iterator_abs_def], of I])
apply (simp_all add: I0 IP IF)
done

end