Theory Refine_Foreach

theory Refine_Foreach
imports NREST RefineMonadicVCG SepLogic_Misc
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 {
  x ← RETURNT( hd xs); σ'←f x σ; RETURNT (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 R Φ S c f σ0 inittime body_time ≡ do {
  ASSERT (finite S);
  xs ← SPECT (emb (λxs. distinct xs ∧ S = set xs ∧ sorted_wrt R xs) inittime);
  (_,σ) ← whileIET 
    (λ(it,σ). ∃xs'. xs = xs' @ it ∧ Φ (set it) σ) (λ(it,_). length it * body_time) (FOREACH_cond c) (FOREACH_body f) (xs,σ0); 
  RETURNT σ }"

text ‹Foreach with continuation condition and annotated invariant:›
definition FOREACHci (‹FOREACH⇩C⇗_⇖›) where "FOREACHci ≡ FOREACHoci (λ_ _. True)"


subsection ‹Proof Rules›

lemma FOREACHoci_rule:
  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 σ ≤ SPECT (emb (I (it-{x})) (enat body_time))"
  assumes FIN: "finite S"
  assumes I0: "I S σ0"
  assumes II1: "⋀σ. ⟦I {} σ⟧ ⟹ P σ"
  assumes II2: "⋀it σ. ⟦ it≠{}; it⊆S; I it σ; ¬c σ;
                         ∀x∈it. ∀y∈S - it. R y x ⟧ ⟹ P σ"
  assumes time_ub: "inittime + enat ((card S) * body_time) ≤ enat overall_time" 
  assumes progress_f[progress_rules]: "⋀a b. progress (f a b)"
  shows "FOREACHoci R I S c f σ0 inittime body_time ≤ SPECT (emb P (enat overall_time))"
  unfolding FOREACHoci_def
  apply(rule T_specifies_I)
  unfolding FOREACH_body_def FOREACH_cond_def  
  apply(vcg'‹-› rules:  IP[THEN T_specifies_rev, THEN T_conseq4])

  prefer 5 apply auto []
  subgoal using I0 by blast
  subgoal by blast  
  subgoal by simp  
  subgoal by auto 
  subgoal by (metis distinct_append hd_Cons_tl remove1_tl set_remove1_eq sorted_wrt.simps(2) sorted_wrt_append)  
  subgoal by (metis DiffD1 DiffD2 UnE list.set_sel(1) set_append sorted_wrt_append)  
  subgoal apply (auto simp: Some_le_mm3_Some_conv Some_le_emb'_conv Some_eq_emb'_conv diff_mult_distrib)
    subgoal by (metis append.assoc append.simps(2) append_Nil hd_Cons_tl)
    subgoal by (metis remove1_tl set_remove1_eq)
    done
  subgoal using time_ub II1 apply (auto simp: Some_le_mm3_Some_conv Some_le_emb'_conv Some_eq_emb'_conv distinct_card) 
    subgoal by (metis DiffD1 DiffD2 II2 Un_iff Un_upper2 sorted_wrt_append) 
    subgoal by (metis DiffD1 DiffD2 II2 Un_iff sorted_wrt_append sup_ge2) 
    subgoal by (metis add_mono diff_le_self dual_order.trans enat_ord_simps(1) length_append order_mono_setup.refl)  
    done
  subgoal by (fact FIN)
  done


lemma FOREACHci_rule :
  assumes IP: 
    "⋀x it σ. ⟦ x∈it; it⊆S; I it σ; c σ ⟧ ⟹ f x σ ≤ SPECT (emb (I (it-{x})) (enat body_time))"
  assumes II1: "⋀σ. ⟦I {} σ⟧ ⟹ P σ"
  assumes II2: "⋀it σ. ⟦ it≠{}; it⊆S; I it σ; ¬c σ ⟧ ⟹ P σ"
  assumes FIN: "finite S"
  assumes I0: "I S σ0"
  assumes progress_f: "⋀a b. progress (f a b)"
  assumes "inittime + enat (card S * body_time) ≤ enat overall_time"
  shows "FOREACHci I S c f σ0 inittime body_time  ≤ SPECT (emb P (enat overall_time))"
  unfolding FOREACHci_def
  by (rule FOREACHoci_rule) (simp_all add: assms)

text ‹We define a relation between distinct lists and sets.›  
definition [to_relAPP]: "list_set_rel R ≡ ⟨R⟩list_rel O br set distinct"

subsection ‹Nres-Fold with Interruption (nfoldli)›
text ‹
  A foreach-loop can be conveniently expressed as an operation that converts
  the set to a list, followed by folding over the list.
  
  This representation is handy for automatic refinement, as the complex 
  foreach-operation is expressed by two relatively simple operations.
›

text ‹We first define a fold-function in the nrest-monad›
definition nfoldli where
  "nfoldli l c f s = RECT (λD (l,s). (case l of 
    [] ⇒ RETURNT s 
    | x#ls ⇒ if c s then do { s←f x s; D (ls, s)} else RETURNT s
  )) (l, s)"


lemma nfoldli_simps[simp]:
  "nfoldli [] c f s = RETURNT s"
  "nfoldli (x#ls) c f s = 
    (if c s then do { s←f x s; nfoldli ls c f s} else RETURNT s)"
  unfolding nfoldli_def by (subst RECT_unfold, refine_mono, auto split: nat.split)+

lemma param_nfoldli[param]:
  shows "(nfoldli,nfoldli) ∈ 
    ⟨Ra⟩list_rel → (Rb→Id) → (Ra→Rb→⟨Rb⟩nrest_rel) → Rb → ⟨Rb⟩nrest_rel"
proof (intro fun_relI, goal_cases)
  case (1 l l' c c' f f' s s')
  thus ?case
    apply (induct arbitrary: s s')
    apply (simp only: nfoldli_simps True_implies_equals)
    apply parametricity
    apply (simp only: nfoldli_simps True_implies_equals)
    apply (parametricity)
    done
qed

lemma nfoldli_no_ctd[simp]: "¬ctd s ⟹ nfoldli l ctd f s = RETURNT s"
  by (cases l) auto

lemma nfoldli_append: "nfoldli (l1@l2) ctd f s = nfoldli l1 ctd f s ⤜ nfoldli l2 ctd f"
  by (induction l1 arbitrary: s) simp_all

lemma nfoldli_assert:
  assumes "set l ⊆ S"
  shows "nfoldli l c (λ x s. ASSERT (x ∈ S) ⪢ f x s) s = nfoldli l c f s"
  using assms by (induction l arbitrary: s) (auto simp: pw_eq_iff refine_pw_simps)

lemmas nfoldli_assert' = nfoldli_assert[OF order.refl]

definition nfoldliIE :: "('d list ⇒ 'd list ⇒ 'a ⇒  bool) ⇒ nat ⇒ 'd list ⇒ ('a ⇒ bool) ⇒ ('d ⇒ 'a ⇒ 'a nrest) ⇒ 'a ⇒ 'a nrest" where
  "nfoldliIE I E l c f s = nfoldli l c f s"

lemma nfoldliIE_rule':
  assumes IS: "⋀x l1 l2 σ. ⟦ l0=l1@x#l2; I l1 (x#l2) σ; c σ ⟧ ⟹ f x σ ≤ SPECT (emb (I (l1@[x]) l2) (enat body_time))"
  assumes FNC: "⋀l1 l2 σ. ⟦ l0=l1@l2; I l1 l2 σ; ¬c σ ⟧ ⟹ P σ"  
  assumes FC: "⋀σ. ⟦ I l0 [] σ ⟧ ⟹ P σ"  
  shows "lr@l = l0 ⟹ I lr l σ ⟹ nfoldliIE I body_time l c f σ ≤ SPECT (emb P (body_time * length l))"
proof (induct l arbitrary: lr σ)
  case Nil
  then show ?case by (auto simp: nfoldliIE_def RETURNT_def le_fun_def  Some_le_emb'_conv dest!: FC)
next
  case (Cons a l)
  show ?case
  proof(cases "c σ")
    case True
    have "f a σ ⤜ nfoldli l c f ≤ SPECT (emb P (enat (body_time + body_time * length l)))"
      apply (rule T_specifies_I) 
      apply (vcg'‹-› rules: IS[THEN T_specifies_rev  , THEN T_conseq4] 
                            Cons(1)[unfolded nfoldliIE_def, THEN T_specifies_rev  , THEN T_conseq4])
      using True Cons(2,3) by (auto simp add: Some_eq_emb'_conv Some_le_emb'_conv)
    with True show ?thesis 
      by (auto simp add: nfoldliIE_def)
  next
    case False
    hence "P σ"
      by (rule FNC[OF Cons(2)[symmetric] Cons(3)])
    with False show ?thesis 
      by (auto simp add: nfoldliIE_def RETURNT_def le_fun_def Some_le_emb'_conv)
  qed
qed

lemma nfoldliIE_rule:
  assumes I0: "I [] l0 σ0"
  assumes IS: "⋀x l1 l2 σ. ⟦ l0=l1@x#l2; I l1 (x#l2) σ; c σ ⟧ ⟹ f x σ ≤ SPECT (emb (I (l1@[x]) l2) (enat body_time))"
  assumes FNC: "⋀l1 l2 σ. ⟦ l0=l1@l2; I l1 l2 σ; ¬c σ ⟧ ⟹ P σ"  
  assumes FC: "⋀σ. ⟦ I l0 [] σ ⟧ ⟹ P σ"  
  assumes T: "(body_time * length l0) ≤ t"
  shows "nfoldliIE I body_time l0 c f σ0 ≤ SPECT (emb P t)"
proof -
  have "nfoldliIE I body_time l0 c f σ0 ≤ SPECT (emb P (body_time * length l0))" 
    by (rule nfoldliIE_rule'[where lr="[]"]) (use assms in auto)
  also have "… ≤ SPECT (emb P t)"
    by (rule SPECT_ub) (use T in ‹auto simp: le_fun_def›)
  finally show ?thesis .
qed


lemma nfoldli_refine[refine]:
  assumes "(li, l) ∈ ⟨S⟩list_rel"
    and "(si, s) ∈ R"
    and CR: "(ci, c) ∈ R → bool_rel"
    and [refine]: "⋀xi x si s. ⟦ (xi,x)∈S; (si,s)∈R; c s ⟧ ⟹ fi xi si ≤ ⇓R (f x s)"
  shows "nfoldli li ci fi si ≤ ⇓ R (nfoldli l c f s)"
  using assms(1,2)
proof (induction arbitrary: si s rule: list_rel_induct)
  case Nil thus ?case by (simp add: RETURNT_refine)
next
  case (Cons xi x li l) 
  note [refine] = Cons

  show ?case
    apply (simp add: RETURNT_refine  split del: if_split)
    apply refine_rcg
    using CR Cons.prems by (auto simp: RETURNT_refine  dest: fun_relD)
qed

definition "nfoldliIE' I bt l0 f s0 = nfoldliIE I bt l0 (λ_. True) f s0"

lemma nfoldliIE'_rule:
  assumes 
"⋀x l1 l2 σ.
    l0 = l1 @ x # l2 ⟹
    I l1 (x # l2) σ ⟹ Some 0 ≤ lst (f x σ) (emb (I (l1 @ [x]) l2) (enat body_time))"
"I [] l0 σ0"
"(⋀σ. I l0 [] σ ⟹ Some (t + enat (body_time * length l0)) ≤ Q σ)"
shows "Some t ≤ lst (nfoldliIE' I body_time l0 f σ0) Q"
  unfolding nfoldliIE'_def
  apply(rule nfoldliIE_rule[where P="I l0 []" and c="λ_. True" and t="body_time * length l0",
        THEN T_specifies_rev, THEN T_conseq4])
       apply fact
      subgoal apply(rule T_specifies_I) using assms(1) by auto 
     subgoal by auto
    apply simp
   apply simp
  subgoal  
    unfolding Some_eq_emb'_conv 
    using assms(3) by auto
  done




text ‹We relate our fold-function to the while-loop that we used in
  the original definition of the foreach-loop›
lemma nfoldli_while: "nfoldli l c f σ
          ≤
         (whileIET I E 
           (FOREACH_cond c) (FOREACH_body f) (l, σ) ⤜
          (λ(_, σ). RETURNT σ))"
proof (induct l arbitrary: σ)
  case Nil thus ?case 
    unfolding whileIET_def 
    by (subst whileT_unfold) (auto simp: FOREACH_cond_def)
next
  case (Cons x ls)
  show ?case 
  proof (cases "c σ")
    case False thus ?thesis
      unfolding whileIET_def by (subst whileT_unfold) (simp add: FOREACH_cond_def)
  next
    case [simp]: True
    from Cons show ?thesis
      unfolding whileIET_def by (subst whileT_unfold)
        (auto simp add: FOREACH_cond_def FOREACH_body_def intro: bindT_mono)
  qed    
qed

lemma rr: "l0 = l1 @ a ⟹ a ≠ [] ⟹ l0 = l1 @ hd a # tl a" by auto 

lemma nfoldli_rule:
  assumes I0: "I [] l0 σ0"
  assumes IS: "⋀x l1 l2 σ. ⟦ l0=l1@x#l2; I l1 (x#l2) σ; c σ ⟧ ⟹ f x σ ≤ SPECT (emb (I (l1@[x]) l2) (enat body_time))"
  assumes FNC: "⋀l1 l2 σ. ⟦ l0=l1@l2; I l1 l2 σ; ¬c σ ⟧ ⟹ P σ"
  assumes FC: "⋀σ. ⟦ I l0 [] σ; c σ ⟧ ⟹ P σ"
  assumes progressf: "⋀x y. progress (f x y)"
  shows "nfoldli l0 c f σ0 ≤ SPECT (emb P (body_time * length l0))"
  apply (rule order_trans[OF nfoldli_while[
          where I="λ(l2,σ). ∃l1. l0=l1@l2 ∧ I l1 l2 σ" and E="λ(l2,σ). (length l2) * body_time"]])  
  unfolding FOREACH_cond_def FOREACH_body_def 
  apply(rule T_specifies_I)
  apply(vcg'_step ‹clarsimp›)
     apply simp subgoal using I0 by auto 
    apply simp subgoal 
      apply(vcg'_step ‹clarsimp›)
      apply (elim exE conjE)
      subgoal for a b l1      
        apply(vcg'_step ‹clarsimp› rules: IS[THEN T_specifies_rev , THEN T_conseq4 ])
           apply(rule rr) 
            apply simp_all 
        by(auto simp add: Some_le_mm3_Some_conv emb_eq_Some_conv left_diff_distrib'
                   intro:  exI[where x="l1@[hd a]"])
      done
  subgoal (* progress *)
    supply progressf [progress_rules] by (progress ‹clarsimp›)  
  subgoal
    apply(vcg' ‹clarsimp›) 
    subgoal for a σ
      apply(cases "c σ")       
        using FC FNC by(auto simp add: Some_le_emb'_conv  mult.commute)         
    done
  done

definition "LIST_FOREACH' tsl c f σ ≡ do {xs ← tsl; nfoldli xs c f σ}"

text ‹This constant is a placeholder to be converted to
  custom operations by pattern rules› 
definition "it_to_sorted_list R s to_sorted_list_time
  ≡ SPECT (emb (λl. distinct l ∧ s = set l ∧ sorted_wrt R l) to_sorted_list_time)"

definition "LIST_FOREACH Φ tsl c f σ0 bodytime ≡ do {
  xs ← tsl;
  (_,σ) ← whileIET (λ(it, σ). ∃xs'. xs = xs' @ it ∧ Φ (set it) σ) (λ(it, σ). length it * bodytime)
    (FOREACH_cond c) (FOREACH_body f) (xs, σ0);
    RETURNT σ}"

lemma FOREACHoci_by_LIST_FOREACH:
  "FOREACHoci R Φ S c f σ0 to_sorted_list_time bodytime = do {
    ASSERT (finite S);
    LIST_FOREACH Φ (it_to_sorted_list R S to_sorted_list_time) c f σ0 bodytime
  }"
  unfolding OP_def FOREACHoci_def LIST_FOREACH_def it_to_sorted_list_def 
  by simp



end