Theory Foreach_Refine

section ‹\isaheader{Example for Foreach-Loops}›
theory Foreach_Refine
imports 
  Collections.Refine_Dflt_Only_ICF 
begin

text ‹
  This example presents the usage of the foreach loop.
  We define a simple foreach loop that looks for the largest element with
  a given property. Ordered loops are used to be sure to find the largest one.
›

subsection ‹Definition›

definition find_max_invar where
  "find_max_invar P S it σ = 
     (case σ of None ⇒ (∀x ∈ S - it. ¬(P x))
             | Some y ⇒ (P y ∧ y ∈ S-it ∧ (∀x ∈ S - it - {y}. ¬(P x))))"

definition find_max :: "('a::{linorder} ⇒ bool) ⇒ 'a set ⇒ ('a option) nres" where
  "find_max P S ≡ 
   FOREACHoci ((≥)) (find_max_invar P S) S
     (λσ. σ = None) (λx _. RETURN (if P x then Some x else None)) None"

subsection ‹Correctness›
text ‹As simple correctness property, we show:
  If the algorithm returns the maximal element satisfying ‹P›.
›
lemma find_max_correct:
  fixes S:: "'a::{linorder} set"
  assumes "finite S"
  shows "find_max P S ≤ SPEC (λσ. case σ of None ⇒ ∀x∈S. ¬(P x)
                                          | Some y ⇒ (P y ∧ y ∈ S ∧ (∀x∈S. P x ⟶ y ≥ x)))"
  unfolding find_max_def
proof (rule FOREACHoci_rule)
  show "finite S" by fact
next
  show "find_max_invar P S S None" 
  unfolding find_max_invar_def by simp
next
  fix x it σ
  assume "σ = None"
         "x ∈ it"
         "it ⊆ S"
         "find_max_invar P S it σ"
         "∀y∈it - {x}. y ≤ x"
         "∀y∈S - it. x ≤ y"

  from ‹find_max_invar P S it σ› ‹σ = None› 
  have not_P_others: "∀x∈S - it. ¬ P x"
    by (simp add: find_max_invar_def)

  from ‹x ∈ it› ‹it ⊆ S› have "x ∈ S" by blast

  show "RETURN (if P x then Some x else None) ≤ SPEC (find_max_invar P S (it - {x}))"
    using not_P_others ‹x ∈ S›
    by (auto simp add: find_max_invar_def)
next
  fix σ
  assume "find_max_invar P S {} σ"
  thus "case σ of None ⇒ ∀x∈S. ¬ P x
        | Some y ⇒ P y ∧ y ∈ S ∧ (∀x∈S. P x ⟶ x ≤ y)"
    by (cases σ, auto simp add: find_max_invar_def)
next
  fix it σ
  assume "it ≠ {}"
         "it ⊆ S"
         "find_max_invar P S it σ"
         "σ ≠ None"
         "∀x∈it. ∀y∈S - it. x ≤ y"

  from ‹σ ≠ None› obtain y where σ_eq[simp]: "σ = Some y" by auto
  from ‹find_max_invar P S it σ› 
    have y_props[simp]: "P y" "y ∈ S" "y ∉ it" and not_P: "∀x∈S - it - {y}. ¬ P x"
    by (simp_all add: find_max_invar_def)
 
  { fix x
    assume "x ∈ S" "P x"
    with not_P have "x ∈ it ∨ x = y" by auto
    with ‹∀x∈it. ∀y∈S - it. x ≤ y› y_props have "x ≤ y" by auto
  } note less_eq_y = this

  show "case σ of None ⇒ ∀x∈S. ¬ P x
        | Some y ⇒ P y ∧ y ∈ S ∧ (∀x∈S. P x ⟶ x ≤ y)" 
   by (simp add: find_max_invar_def Ball_def less_eq_y)
qed

subsection ‹Data Refinement and Determinization›
text ‹
  Next, we use automatic data refinement and transfer to generate an
  executable algorithm using a red-black-tree. 
›
schematic_goal find_max_impl_refine_aux:
  assumes invar_S: "rs.invar S"
  shows "RETURN (?f) ≤ (find_max P (rs.α S))"
  unfolding find_max_def
  by (refine_transfer 
    RBTSetImpl.rs.rev_iterateoi_correct[unfolded set_iterator_rev_linord_def,
    OF invar_S])

concrete_definition find_max_impl for P S uses find_max_impl_refine_aux

lemma find_max_impl_refine:
  assumes invar_S: "rs.invar S"
  shows "RETURN (find_max_impl P S) ≤ (find_max P (rs.α S))"
  using assms by (rule find_max_impl.refine)

subsubsection ‹Executable Code›

lemma find_max_impl_correct :
assumes invar_S: "rs.invar S"
shows "case find_max_impl P S of None ⇒ ∀x∈rs.α S. ¬(P x)
                               | Some y ⇒ (P y ∧ y ∈ (rs.α S) 
                                 ∧ (∀x∈rs.α S. P x ⟶ y ≥ x))"
proof -
  note find_max_impl_refine [of S P, OF invar_S]
  also note find_max_correct [OF RBTSetImpl.rs.finite[of S, OF invar_S], of P]
  finally show ?thesis by simp
qed

text ‹Finally, we can generate code›
export_code find_max_impl checking SML
export_code find_max_impl checking OCaml?
export_code find_max_impl checking Haskell?
export_code find_max_impl checking Scala
  
end