Theory Refine_Foreach (Isabelle repository snapshot 408271602165 12-Mar-2013)

header {* \isaheader{Foreach Loops} *}
theory Refine_Foreach
imports Refine_While "../Collections/iterator/SetIterator"
begin

text {*
  A common pattern for loop usage is iteration over the elements of a set.
  This theory provides the @{text "FOREACH"}-combinator, that iterates over 
  each element of a set.
*}

subsection {* Auxilliary Lemmas *}
text {* The following lemma is commonly used when reasoning about iterator
  invariants.
  It helps converting the set of elements that remain to be iterated over to
  the set of elements already iterated over. *}
lemma it_step_insert_iff: 
  "it ⊆ S ==> x∈it ==> S-(it-{x}) = insert x (S-it)" by auto

subsection {* Definition *}

text {*
  Foreach-loops come in different versions, depending on whether they have an 
  annotated invariant (I), a termination condition (C), and an order (O).

  Note that asserting that the set is finite is not necessary to guarantee
  termination. However, we currently provide only iteration over finite sets,
  as this also matches the ICF concept of iterators.
*}
   
definition "FOREACH_body f ≡ λ(xs, σ). do {
  let x = hd xs; σ'\<leftarrow>f x σ; RETURN (tl xs,σ')
  }"

definition FOREACH_cond where "FOREACH_cond c ≡ (λ(xs,σ). xs≠[] ∧ c σ)"

text {* Foreach with continuation condition, order and annotated invariant: *}

definition FOREACHoci ("FOREACH⇣_O⇣_C⇗^_⇖") where "FOREACHoci Φ S R c f σ0 ≡ do {
  ASSERT (finite S);
  xs \<leftarrow> SPEC (λxs. distinct xs ∧ S = set xs ∧ sorted_by_rel R xs);
  (_,σ) \<leftarrow> WHILEIT 
    (λ(it,σ). ∃xs'. xs = xs' @ it ∧ Φ (set it) σ) (FOREACH_cond c) (FOREACH_body f) (xs,σ0); 
  RETURN σ }"

text {* Foreach with continuation condition and annotated invariant: *}
definition FOREACHci ("FOREACH⇣_C⇗^_⇖") where "FOREACHci Φ S ≡ FOREACHoci Φ S (λ_ _. True)"

text {* Foreach with continuation condition: *}
definition FOREACHc ("FOREACH⇣_C") where "FOREACHc ≡ FOREACHci (λ_ _. True)"

text {* Foreach with annotated invariant: *}
definition FOREACHi ("FOREACH⇗^_⇖") where 
  "FOREACHi Φ S f σ0 ≡ FOREACHci Φ S (λ_. True) f σ0"

text {* Foreach with annotated invariant and order: *}
definition FOREACHoi ("FOREACH⇣_O⇗^_⇖") where 
  "FOREACHoi Φ S R f σ0 ≡ FOREACHoci Φ S R (λ_. True) f σ0"

text {* Basic foreach *}
definition "FOREACH S f σ0 ≡ FOREACHc S (λ_. True) f σ0"

subsection {* Proof Rules *}

lemma FOREACHoci_rule[refine_vcg]:
  assumes FIN: "finite S"
  assumes I0: "I S σ0"
  assumes IP: 
    "!!x it σ. [| c σ; x∈it; it⊆S; I it σ; ∀y∈it - {x}. R x y;
                ∀y∈S - it. R y x |] ==> f x σ ≤ SPEC (I (it-{x}))"
  assumes II1: "!!σ. [|I {} σ|] ==> P σ"
  assumes II2: "!!it σ. [| it≠{}; it⊆S; I it σ; ¬c σ;
                         ∀x∈it. ∀y∈S - it. R y x |] ==> P σ"
  shows "FOREACHoci I S R c f σ0 ≤ SPEC P"
  unfolding FOREACHoci_def
  apply (intro refine_vcg)

  apply (rule FIN)

  apply (subgoal_tac "wf (measure (λ(xs, _). length xs))")
    apply assumption
    apply simp

  apply (insert I0, simp add: I0) []
  unfolding FOREACH_body_def FOREACH_cond_def
  apply (rule refine_vcg)+
  apply (simp, elim conjE exE)+
  apply (rename_tac xs'' s xs' σ xs)
defer
  apply (simp, elim conjE exE)+
  apply (rename_tac x s xs' σ σ' xs)
defer
proof -
  fix xs' σ xs

  assume I_xs': "I (set xs') σ"
     and sorted_xs_xs': "sorted_by_rel R (xs @ xs')"
     and dist: "distinct xs" "distinct xs'" "set xs ∩ set xs' = {}"
     and S_eq: "S = set xs ∪ set xs'" 

  from S_eq have "set xs' ⊆ S" by simp
  from dist S_eq have S_diff: "S - set xs' = set xs" by blast

  { assume "xs' ≠ []" "c σ"
    from `xs' ≠ []` obtain x xs'' where xs'_eq: "xs' = x # xs''" by (cases xs', auto)

    have x_in_xs': "x ∈ set xs'" and x_nin_xs'': "x ∉ set xs''" 
       using `distinct xs'` unfolding xs'_eq by simp_all
  
    from IP[of σ x "set xs'", OF `c σ` x_in_xs' `set xs' ⊆ S` `I (set xs') σ`] x_nin_xs''
         sorted_xs_xs' S_diff
    show "f (hd xs') σ ≤ SPEC
            (λx. (∃xs'a. xs @ xs' = xs'a @ tl xs') ∧
                 I (set (tl xs')) x)"
      apply (simp add: xs'_eq)
      apply (simp add: sorted_by_rel_append)
    done
  }

  { assume "xs' = [] ∨ ¬(c σ)"
    show "P σ" 
    proof (cases "xs' = []")
      case True thus "P σ" using `I (set xs') σ` by (simp add: II1)
    next
      case False note xs'_neq_nil = this
      with `xs' = [] ∨ ¬ c σ` have "¬ c σ" by simp
 
      from II2 [of "set xs'" σ] S_diff sorted_xs_xs'
      show "P σ" 
        apply (simp add: xs'_neq_nil S_eq `¬ c σ` I_xs')
        apply (simp add: sorted_by_rel_append)
      done
    qed
  }
qed

lemma FOREACHoi_rule[refine_vcg]:
  assumes FIN: "finite S"
  assumes I0: "I S σ0"
  assumes IP: 
    "!!x it σ. [| x∈it; it⊆S; I it σ; ∀y∈it - {x}. R x y;
                ∀y∈S - it. R y x |] ==> f x σ ≤ SPEC (I (it-{x}))"
  assumes II1: "!!σ. [|I {} σ|] ==> P σ"
  shows "FOREACHoi I S R f σ0 ≤ SPEC P"
  unfolding FOREACHoi_def 
  by (rule FOREACHoci_rule) (simp_all add: assms)

lemma FOREACHci_rule[refine_vcg]:
  assumes FIN: "finite S"
  assumes I0: "I S σ0"
  assumes IP: 
    "!!x it σ. [| x∈it; it⊆S; I it σ; c σ |] ==> f x σ ≤ SPEC (I (it-{x}))"
  assumes II1: "!!σ. [|I {} σ|] ==> P σ"
  assumes II2: "!!it σ. [| it≠{}; it⊆S; I it σ; ¬c σ |] ==> P σ"
  shows "FOREACHci I S c f σ0 ≤ SPEC P"
  unfolding FOREACHci_def
  by (rule FOREACHoci_rule) (simp_all add: assms)

lemma FOREACHoci_refine:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes RR_OK: "!!x y. [|x ∈ S; y ∈ S; RR x y|] ==> RR' (α x) (α y)"
  assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
  assumes REFC: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ';  Φ'' it σ it' σ'; Φ it σ; (σ,σ')∈R
  |] ==> c σ <-> c' σ'"
  assumes REFPHI: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ'' it σ it' σ'; (σ,σ')∈R
  |] ==> Φ it σ"
  assumes REFSTEP: "!!x it σ x' it' σ'. [|∀y∈it-{x}. RR x y; 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ it σ; Φ' it' σ';  Φ'' it σ it' σ'; c σ; c' σ';
    (σ,σ')∈R
  |] ==> f x σ 
    ≤ \<Down>({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
  shows "FOREACHoci Φ S RR c f σ0 ≤ \<Down>R (FOREACHoci Φ' S' RR' c' f' σ0')"
  unfolding FOREACHoci_def
  apply (rule ASSERT_refine_right ASSERT_refine_left)+
  using REFS INJ apply (auto dest: finite_imageD) []

  apply (rule bind_refine)
  apply (subgoal_tac 
     "SPEC (λxs. distinct xs ∧ S = set xs ∧ sorted_by_rel RR xs) ≤ 
        \<Down> {(xs, xsa). xsa = map α xs ∧ sorted_by_rel RR xs ∧ distinct xs ∧ distinct xsa ∧ set xs = S ∧ set xsa = S'}
      (SPEC (λxs. distinct xs ∧ S' = set xs ∧ sorted_by_rel RR' xs))")
  apply assumption
  apply (rule SPEC_refine_sv)
  apply (simp add: single_valued_def)
  apply (rule SPEC_rule)
  apply (insert INJ, simp add: REFS distinct_map sorted_by_rel_map)[]
  apply (rule sorted_by_rel_weaken[of _ RR])
  apply (simp add: RR_OK)
  apply (simp)

  apply (rule bind_refine)
  apply (rule_tac WHILEIT_refine)
  apply (subgoal_tac "((x, σ0), x', σ0')∈{((xs,σ),(xs',σ')). sorted_by_rel RR xs ∧ 
    xs'=map α xs ∧ set xs ⊆ S ∧ set xs' ⊆ S' ∧ (σ,σ')∈R ∧ Φ'' (set xs) σ (set xs') σ'}", assumption)
  apply (simp add: REFS REF0 REFPHI0)

  apply (auto intro: single_valuedI single_valuedD[OF SV]) []

  using REFPHI 
  apply (simp) 
  apply (clarify)
  apply (rule conjI)  
  prefer 2
  apply auto[]
defer
  using REFC apply (clarify) apply (auto simp add: FOREACH_cond_def) []

  apply (simp add: FOREACH_body_def Let_def split: prod.splits) []
  apply (rule bind_refine)
    apply (case_tac a, simp add: FOREACH_cond_def) []
    apply (rule REFSTEP)
      apply (subgoal_tac "∀y∈set a-{hd a}. RR (hd a) y", assumption)
      apply simp
      apply simp
      apply simp
      apply (subgoal_tac "hd (map α a)∈set aa", assumption)
      apply simp_all[3]
      apply fast
      apply simp
      apply simp
      apply fast
      apply (simp add: FOREACH_cond_def)
      apply (simp add: FOREACH_cond_def)
      apply simp
    apply (rule RETURN_refine_sv)
    apply (rule single_valuedI)
    apply (auto simp add: single_valuedD[OF SV]) []
    apply (case_tac a, simp)
    apply (clarify, simp)

  apply (split prod.split, intro allI impI)+
  apply (rule RETURN_refine_sv[OF SV])
  apply (auto)[]
proof -
  fix xs axs' xs''
  assume map_eq: "map α xs = axs' @ map α xs''"
     and xs''_subset: "set xs'' ⊆ set xs"
     and dist_xs: "distinct (map α xs)"
  hence "axs' = take (length axs') (map α xs)" by (metis append_eq_conv_conj)
  hence axs'_eq: "axs' = map α (take (length axs') xs)" by (simp add: take_map)

  from map_eq axs'_eq have map_eq: "map α xs = map α ((take (length axs') xs) @ xs'')"
    by (metis map_append)

  have inj_α: "inj_on α (set xs ∪ set ((take (length axs') xs) @ xs''))"
  proof -
    from xs''_subset
    have "(set xs ∪ set ((take (length axs') xs) @ xs'')) = set xs"
      by (auto elim: in_set_takeD)

    with dist_xs show ?thesis
      by (simp add: distinct_map)
  qed
  
  from inj_on_map_eq_map [OF inj_α] map_eq
  have "xs = (take (length axs') xs) @ xs''" by blast
  thus "∃xs'. xs = xs' @ xs''" by blast
qed 
 
lemma FOREACHoci_refine_rcg[refine]:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes RR_OK: "!!x y. [|x ∈ S; y ∈ S; RR x y|] ==> RR' (α x) (α y)"
  assumes SV: "single_valued R"
  assumes REFC: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ it σ; (σ,σ')∈R
  |] ==> c σ <-> c' σ'"
  assumes REFPHI: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; (σ,σ')∈R
  |] ==> Φ it σ"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| ∀y∈it-{x}. RR x y;
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ it σ; Φ' it' σ'; c σ; c' σ';
    (σ,σ')∈R
  |] ==> f x σ ≤ \<Down>R (f' x' σ')"
  shows "FOREACHoci Φ S RR c f σ0 ≤ \<Down>R (FOREACHoci Φ' S' RR' c' f' σ0')"
  apply (rule FOREACHoci_refine[where Φ''="λ_ _ _ _. True"])
  apply (rule assms)+
  using assms by simp_all

lemma FOREACHoci_weaken:
  assumes IREF: "!!it σ. it⊆S ==> I it σ ==> I' it σ"
  shows "FOREACHoci I' S RR c f σ0 ≤ FOREACHoci I S RR c f σ0"
  apply (rule FOREACHoci_refine_rcg[where α=id and R=Id, simplified])
  apply (auto intro: IREF)
  done

lemma FOREACHoci_weaken_order:
  assumes RRREF: "!!x y. x ∈ S ==> y ∈ S ==> RR x y ==> RR' x y"
  shows "FOREACHoci I S RR c f σ0 ≤ FOREACHoci I S RR' c f σ0"
  apply (rule FOREACHoci_refine_rcg[where α=id and R=Id, simplified])
  apply (auto intro: RRREF)
  done


subsubsection {* Rules for Derived Constructs *}

lemma FOREACHoi_refine:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes RR_OK: "!!x y. [|x ∈ S; y ∈ S; RR x y|] ==> RR' (α x) (α y)"
  assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
  assumes REFPHI: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ'' it σ it' σ'; (σ,σ')∈R
  |] ==> Φ it σ"
  assumes REFSTEP: "!!x it σ x' it' σ'. [|∀y∈it-{x}. RR x y; 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ it σ; Φ' it' σ';  Φ'' it σ it' σ'; (σ,σ')∈R
  |] ==> f x σ 
    ≤ \<Down>({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
  shows "FOREACHoi Φ S RR f σ0 ≤ \<Down>R (FOREACHoi Φ' S' RR' f' σ0')"
  unfolding FOREACHoi_def
  apply (rule FOREACHoci_refine [of α _ _ _ _ _ _ _ Φ''])
  apply (simp_all add: assms)
done

lemma FOREACHoi_refine_rcg[refine]:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes RR_OK: "!!x y. [|x ∈ S; y ∈ S; RR x y|] ==> RR' (α x) (α y)"
  assumes SV: "single_valued R"
  assumes REFPHI: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; (σ,σ')∈R
  |] ==> Φ it σ"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| ∀y∈it-{x}. RR x y;
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ it σ; Φ' it' σ'; (σ,σ')∈R
  |] ==> f x σ ≤ \<Down>R (f' x' σ')"
  shows "FOREACHoi Φ S RR f σ0 ≤ \<Down>R (FOREACHoi Φ' S' RR' f' σ0')"
  apply (rule FOREACHoi_refine[where Φ''="λ_ _ _ _. True"])
  apply (rule assms)+
  using assms by simp_all

lemma FOREACHci_refine:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
  assumes REFC: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ';  Φ'' it σ it' σ'; Φ it σ; (σ,σ')∈R
  |] ==> c σ <-> c' σ'"
  assumes REFPHI: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ'' it σ it' σ'; (σ,σ')∈R
  |] ==> Φ it σ"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ it σ; Φ' it' σ';  Φ'' it σ it' σ'; c σ; c' σ';
    (σ,σ')∈R
  |] ==> f x σ 
    ≤ \<Down>({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
  shows "FOREACHci Φ S c f σ0 ≤ \<Down>R (FOREACHci Φ' S' c' f' σ0')"
  unfolding FOREACHci_def
  apply (rule FOREACHoci_refine [of α _ _ _ _ _ _ _ Φ''])
  apply (simp_all add: assms)
done

lemma FOREACHci_refine_rcg[refine]:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes REFC: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ it σ; (σ,σ')∈R
  |] ==> c σ <-> c' σ'"
  assumes REFPHI: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; (σ,σ')∈R
  |] ==> Φ it σ"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ it σ; Φ' it' σ'; c σ; c' σ';
    (σ,σ')∈R
  |] ==> f x σ ≤ \<Down>R (f' x' σ')"
  shows "FOREACHci Φ S c f σ0 ≤ \<Down>R (FOREACHci Φ' S' c' f' σ0')"
  apply (rule FOREACHci_refine[where Φ''="λ_ _ _ _. True"])
  apply (rule assms)+
  using assms by auto

lemma FOREACHci_weaken:
  assumes IREF: "!!it σ. it⊆S ==> I it σ ==> I' it σ"
  shows "FOREACHci I' S c f σ0 ≤ FOREACHci I S c f σ0"
  apply (rule FOREACHci_refine_rcg[where α=id and R=Id, simplified])
  apply (auto intro: IREF)
  done

lemma FOREACHi_rule[refine_vcg]:
  assumes FIN: "finite S"
  assumes I0: "I S σ0"
  assumes IP: 
    "!!x it σ. [| x∈it; it⊆S; I it σ |] ==> f x σ ≤ SPEC (I (it-{x}))"
  assumes II: "!!σ. [|I {} σ|] ==> P σ"
  shows "FOREACHi I S f σ0 ≤ SPEC P"
  unfolding FOREACHi_def
  apply (rule FOREACHci_rule[of S I])
  using assms by auto

lemma FOREACHc_rule:
  assumes FIN: "finite S"
  assumes I0: "I S σ0"
  assumes IP: 
    "!!x it σ. [| x∈it; it⊆S; I it σ |] ==> f x σ ≤ SPEC (I (it-{x}))"
  assumes II1: "!!σ. [|I {} σ|] ==> P σ"
  assumes II2: "!!it σ. [| it≠{}; it⊆S; I it σ; ¬c σ |] ==> P σ"
  shows "FOREACHc S c f σ0 ≤ SPEC P"
  unfolding FOREACHc_def
  apply (rule order_trans[OF FOREACHci_weaken], rule TrueI)
  apply (rule FOREACHci_rule[where I=I])
  using assms by auto

lemma FOREACH_rule:
  assumes FIN: "finite S"
  assumes I0: "I S σ0"
  assumes IP: 
    "!!x it σ. [| x∈it; it⊆S; I it σ |] ==> f x σ ≤ SPEC (I (it-{x}))"
  assumes II: "!!σ. [|I {} σ|] ==> P σ"
  shows "FOREACH S f σ0 ≤ SPEC P"
  unfolding FOREACH_def FOREACHc_def
  apply (rule order_trans[OF FOREACHci_weaken], rule TrueI)
  apply (rule FOREACHci_rule[where I=I])
  using assms by auto

lemma FOREACHc_refine:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
  assumes REFC: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ'' it σ it' σ'; (σ,σ')∈R
  |] ==> c σ <-> c' σ'"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ'' it σ it' σ'; c σ; c' σ'; (σ,σ')∈R
  |] ==> f x σ 
    ≤ \<Down>({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
  shows "FOREACHc S c f σ0 ≤ \<Down>R (FOREACHc S' c' f' σ0')"
  unfolding FOREACHc_def
  apply (rule FOREACHci_refine[where Φ''=Φ'', OF INJ REFS REF0 SV REFPHI0])
  apply (erule (4) REFC)
  apply (rule TrueI)
  apply (erule (9) REFSTEP)
  done

lemma FOREACHc_refine_rcg[refine]:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes REFC: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; (σ,σ')∈R
  |] ==> c σ <-> c' σ'"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S'; c σ; c' σ';
    (σ,σ')∈R
  |] ==> f x σ ≤ \<Down>R (f' x' σ')"
  shows "FOREACHc S c f σ0 ≤ \<Down>R (FOREACHc S' c' f' σ0')"
  unfolding FOREACHc_def
  apply (rule FOREACHci_refine_rcg)
  apply (rule assms)+
  using assms by auto

lemma FOREACHi_refine:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
  assumes REFPHI: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ'' it σ it' σ'; (σ,σ')∈R
  |] ==> Φ it σ"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ it σ; Φ' it' σ';  Φ'' it σ it' σ';
    (σ,σ')∈R
  |] ==> f x σ 
    ≤ \<Down>({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
  shows "FOREACHi Φ S f σ0 ≤ \<Down>R (FOREACHi Φ' S' f' σ0')"
  unfolding FOREACHi_def
  apply (rule FOREACHci_refine[where Φ''=Φ'', OF INJ REFS REF0 SV REFPHI0])
  apply (rule refl)
  apply (erule (5) REFPHI)
  apply (erule (9) REFSTEP)
  done

lemma FOREACHi_refine_rcg[refine]:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes REFPHI: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; (σ,σ')∈R
  |] ==> Φ it σ"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ it σ; Φ' it' σ';
    (σ,σ')∈R
  |] ==> f x σ ≤ \<Down>R (f' x' σ')"
  shows "FOREACHi Φ S f σ0 ≤ \<Down>R (FOREACHi Φ' S' f' σ0')"
  unfolding FOREACHi_def
  apply (rule FOREACHci_refine_rcg)
  apply (rule assms)+
  using assms apply auto
  done

lemma FOREACH_refine:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ'' it σ it' σ'; (σ,σ')∈R
  |] ==> f x σ 
    ≤ \<Down>({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
  shows "FOREACH S f σ0 ≤ \<Down>R (FOREACH S' f' σ0')"
  unfolding FOREACH_def
  apply (rule FOREACHc_refine[where Φ''=Φ'', OF INJ REFS REF0 SV REFPHI0])
  apply (rule refl)
  apply (erule (7) REFSTEP)
  done

lemma FOREACH_refine_rcg[refine]:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    (σ,σ')∈R
  |] ==> f x σ ≤ \<Down>R (f' x' σ')"
  shows "FOREACH S f σ0 ≤ \<Down>R (FOREACH S' f' σ0')"
  unfolding FOREACH_def
  apply (rule FOREACHc_refine_rcg)
  apply (rule assms)+
  using assms by auto

lemma FOREACHci_refine_rcg'[refine]:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes REFC: "!!it σ it' σ'. [| 
    it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; (σ,σ')∈R
  |] ==> c σ <-> c' σ'"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ' it' σ'; c σ; c' σ';
    (σ,σ')∈R
  |] ==> f x σ ≤ \<Down>R (f' x' σ')"
  shows "FOREACHc S c f σ0 ≤ \<Down>R (FOREACHci Φ' S' c' f' σ0')"
  unfolding FOREACHc_def
  apply (rule FOREACHci_refine_rcg) 
  apply (rule assms)
  apply (rule assms)
  apply (rule assms)
  apply (rule assms)
  apply (erule (4) REFC)
  apply (rule TrueI)
  apply (rule REFSTEP, assumption+)
  done

lemma FOREACHi_refine_rcg'[refine]:
  fixes α :: "'S => 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on α S"
  assumes REFS: "S' = α`S"
  assumes REF0: "(σ0,σ0')∈R"
  assumes SV: "single_valued R"
  assumes REFSTEP: "!!x it σ x' it' σ'. [| 
    x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
    Φ' it' σ';
    (σ,σ')∈R
  |] ==> f x σ ≤ \<Down>R (f' x' σ')"
  shows "FOREACH S f σ0 ≤ \<Down>R (FOREACHi Φ' S' f' σ0')"
  unfolding FOREACH_def FOREACHi_def
  apply (rule FOREACHci_refine_rcg') 
  apply (rule assms)+
  apply simp
  apply (rule REFSTEP, assumption+)
  done

subsection {* FOREACH with empty sets *}

lemma FOREACHoci_emp [simp] :
  "FOREACHoci Φ {} R c f σ = do {ASSERT (Φ {} σ); RETURN σ}"
apply (simp add: FOREACHoci_def bind_RES image_def)
apply (simp add: WHILEIT_unfold FOREACH_cond_def)
done

lemma FOREACHoi_emp [simp] :
  "FOREACHoi Φ {} R f σ = do {ASSERT (Φ {} σ); RETURN σ}"
by (simp add: FOREACHoi_def)

lemma FOREACHci_emp [simp] :
  "FOREACHci Φ {} c f σ = do {ASSERT (Φ {} σ); RETURN σ}"
by (simp add: FOREACHci_def)

lemma FOREACHc_emp [simp] :
  "FOREACHc {} c f σ = RETURN σ"
by (simp add: FOREACHc_def)

lemma FOREACH_emp [simp] :
  "FOREACH {} f σ = RETURN σ"
by (simp add: FOREACH_def)

lemma FOREACHi_emp [simp] :
  "FOREACHi Φ {} f σ = do {ASSERT (Φ {} σ); RETURN σ}"
by (simp add: FOREACHi_def)


locale transfer_FOREACH = transfer +
  constrains α :: "'mc => 's nres"
  fixes creturn :: "'s => 'mc"
  and cbind :: "'mc => ('s=>'mc) => 'mc"
  and liftc :: "('s => bool) => 'mc => bool"

  assumes transfer_bind: "[|α m ≤ M; !!x. α (f x) ≤ F x |] 
    ==> α (cbind m f) ≤ bind M F"
  assumes transfer_return: "α (creturn x) ≤ RETURN x"

  assumes liftc: "[|RETURN x ≤ α m; α m ≠ FAIL|] ==> liftc c m <-> c x"
begin

abbreviation lift_it :: "('x,'mc) set_iterator => 
  ('s=>bool) => ('x => 's => 'mc) => 's => 'mc"
  where
  "lift_it it c f s0 ≡ it 
    (liftc c) 
    (λx s. cbind s (f x)) 
    (creturn s0)"

lemma transfer_FOREACHoci[refine_transfer]:
  fixes X :: "'x set" and s0 :: "'s"
  assumes IT: "set_iterator_genord iterate X R"
  assumes RS: "!!x s. α (f x s) ≤ F x s"
  shows "α (lift_it iterate c f s0) ≤ FOREACHoci I X R c F s0"
proof -
  from IT obtain xs where xs_props: 
    "distinct xs" "X = set xs" "sorted_by_rel R xs" "iterate = foldli xs"
    unfolding set_iterator_genord_def by blast

  def RL≡"λ(it,s). WHILE (FOREACH_cond c) (FOREACH_body F) (it, s) »=
      (λ(_, σ). RETURN σ)"
  hence RL_def': 
    "!!it s. RL (it,s) = WHILE (FOREACH_cond c) (FOREACH_body F) (it, s) »=
    (λ(_, σ). RETURN σ)" by auto

  {
    fix it s
    have "RL (it, s) = (
      if (FOREACH_cond c (it,s)) then 
        (FOREACH_body F (it,s) »= RL)
      else 
        RETURN s)"
      unfolding RL_def
      apply (subst WHILE_unfold)
      apply (auto simp: pw_eq_iff refine_pw_simps)
      done
  } note RL_unfold = this

  {
    fix it::"'x list" and x and s :: "'s"
    assume C: "c s"
    have "do{ s'\<leftarrow>F x s; RL (it, s')} ≤ RL (x # it,s)"
      apply (subst (2) RL_unfold)
      unfolding FOREACH_cond_def FOREACH_body_def
      apply (rule pw_leI)
      using C apply (simp add: refine_pw_simps)
      done
  } note RL_unfold_step=this

  have RL_le: "RL (xs,s0) ≤ FOREACHoci I X R c F s0"
    unfolding FOREACHoci_def
    apply (rule le_ASSERTI)
    apply (rule bind2let_refine [of xs Id _ "λ_. RL(xs,s0)" Id, simplified])
    apply (simp add: xs_props)
    apply (rule order_trans[OF _ monoD[OF bind_mono1 WHILEI_le_WHILEIT]])
    apply (rule order_trans[OF _ monoD[OF bind_mono1 WHILEI_weaken[OF TrueI]]])
    apply (fold WHILE_def)
    apply (fold RL_def')
    by simp

  { fix S xs'
    have "do { s\<leftarrow>α S; RL (xs',s) } ≤ RL (xs,s0) ==>
          α (foldli xs' (liftc c) (λx s. cbind s (f x)) S) ≤ 
          RL (xs, s0)"
    proof (induct xs' arbitrary: S)
      case (Nil S) thus ?case 
        by (simp add: RL_unfold FOREACH_cond_def)
      next
        case (Cons x xs' S) 
        note ind_hyp = Cons(1)
        note pre = Cons(2)

        show ?case
        proof (cases "α S")
          case FAIL with pre have "RL (xs, s0) = FAIL" by simp
          thus ?thesis by simp
        next
          case (RES S') note α_S_eq[simp] = this 

          from transfer_bind [of S "RES S'" "f x" "F x", OF _ RS]
          have α_bind: "α (cbind S (f x)) ≤ RES S' »= F x" by simp

          { fix s
            assume "s ∈ S'"
            with liftc [of s S c]
            have "c s = liftc c S" by simp
          } note liftc_intro = this

          show ?thesis
          proof (cases "liftc c S")
            case False note not_liftc = this
            with liftc_intro have "!!s. c s ==> s ∉ S'" by auto

            hence "RES S' »= (λs. RL (x # xs', s)) = RES S'"
              apply (simp add: bind_def Sup_nres_def image_iff RL_unfold
                               FOREACH_cond_def Ball_def Bex_def) 
              apply (auto)
            done
            with pre not_liftc show ?thesis by simp
          next
            case True note liftc = this

            with liftc_intro have S'_simps: "S' ∩ {s. c s} = S'" "S' ∩ {s. ¬ c s} = {}"
               by auto
            have "((α (cbind S (f x))) »= (λs. RL (xs', s))) ≤ 
                  ((RES S' »= F x) »= (λs. RL (xs', s)))"
              by (rule bind_mono) (simp_all add: α_bind)
            also have "... =  RES S' »= (λs. F x s »= (λs. RL (xs', s)))" by simp
            also have "… ≤ α S »= (λs. RL (x # xs', s))"
              apply (simp add: RL_unfold[of "x # xs'"] FOREACH_cond_def bind_RES S'_simps)
              apply (simp add: FOREACH_body_def)
              done
            also note pre
            finally have pre': "α (cbind S (f x)) »= (λs. RL (xs', s)) ≤ RL (xs, s0)" by simp

            from ind_hyp[OF pre'] liftc
            show ?thesis by simp
          qed
        qed
      qed
  }
  moreover
  have "α (creturn s0) »= (λs. RL (xs, s)) ≤ RL (xs, s0)"
  proof -
    have "α (creturn s0) »= (λs. RL (xs, s)) ≤
          RETURN s0 »= (λs. RL (xs, s))"
      apply (rule bind_mono)
      apply (simp_all add: transfer_return)
    done
    thus ?thesis by simp
  qed
  ultimately have lift_le: "α (lift_it (foldli xs) c f s0) ≤ RL (xs, s0)" by simp
  
  
  from order_trans[OF lift_le RL_le, folded xs_props(4)]
  show ?thesis .
qed

lemma transfer_FOREACHoi[refine_transfer]:
  fixes X :: "'x set" and s0 :: "'s"
  assumes IT: "set_iterator_genord iterate X R"
  assumes RS: "!!x s. α (f x s) ≤ F x s"
  shows "α (lift_it iterate (λ_. True) f s0) ≤ FOREACHoi I X R F s0"
unfolding FOREACHoi_def
by (rule transfer_FOREACHoci [OF IT RS])

lemma transfer_FOREACHci[refine_transfer]:
  fixes X :: "'x set" and s0 :: "'s"
  assumes IT: "set_iterator iterate X"
  assumes RS: "!!x s. α (f x s) ≤ F x s"
  shows "α (lift_it iterate c f s0) ≤ FOREACHci I X c F s0"
unfolding FOREACHci_def
by (rule transfer_FOREACHoci [OF IT[unfolded set_iterator_def] RS])

lemma transfer_FOREACHc[refine_transfer]:
  fixes X :: "'x set" and s0 :: "'s"
  assumes IT: "set_iterator iterate X"
  assumes RS: "!!x s. α (f x s) ≤ F x s"
  shows "α (lift_it iterate c f s0) ≤ FOREACHc X c F s0"
  unfolding FOREACHc_def using assms by (rule transfer_FOREACHci)

lemma transfer_FOREACHI[refine_transfer]:
  fixes X :: "'x set" and s0 :: "'s"
  assumes IT: "set_iterator iterate X"
  assumes RS: "!!x s. α (f x s) ≤ F x s"
  shows "α (lift_it iterate (λ_. True) f s0) ≤ FOREACHi I X F s0"
  unfolding FOREACHi_def 
  using assms by (rule transfer_FOREACHci)

lemma det_FOREACH[refine_transfer]:
  fixes X :: "'x set" and s0 :: "'s"
  assumes IT: "set_iterator iterate X"
  assumes RS: "!!x s. α (f x s) ≤ F x s"
  shows "α (lift_it iterate (λ_. True) f s0) ≤ FOREACH X F s0"
  unfolding FOREACH_def
  using assms by (rule transfer_FOREACHc)

end

lemma FOREACHoci_mono[refine_mono]:
  assumes "!!x. f x ≤ f' x"
  shows "FOREACHoci I S R c f s0 ≤ FOREACHoci I S R c f' s0"
  using assms apply -
  unfolding FOREACHoci_def FOREACH_body_def
  apply (refine_mono)
  done
lemma FOREACHoi_mono[refine_mono]:
  assumes "!!x. f x ≤ f' x"
  shows "FOREACHoi I S R f s0 ≤ FOREACHoi I S R f' s0"
  using assms apply -
  unfolding FOREACHoi_def FOREACH_body_def
  apply (refine_mono)
  done
lemma FOREACHci_mono[refine_mono]:
  assumes "!!x. f x ≤ f' x"
  shows "FOREACHci I S c f s0 ≤ FOREACHci I S c f' s0"
  using assms apply -
  unfolding FOREACHci_def FOREACH_body_def
  apply (refine_mono)
  done
lemma FOREACHc_mono[refine_mono]:
  assumes "!!x. f x ≤ f' x"
  shows "FOREACHc S c f s0 ≤ FOREACHc S c f' s0"
  using assms apply -
  unfolding FOREACHc_def 
  apply (refine_mono)
  done
lemma FOREACHi_mono[refine_mono]:
  assumes "!!x. f x ≤ f' x"
  shows "FOREACHi I S f s0 ≤ FOREACHi I S f' s0"
  using assms apply -
  unfolding FOREACHi_def 
  apply (refine_mono)
  done
lemma FOREACH_mono[refine_mono]:
  assumes "!!x. f x ≤ f' x"
  shows "FOREACH S f s0 ≤ FOREACH S f' s0"
  using assms apply -
  unfolding FOREACH_def 
  apply (refine_mono)
  done

end