Theory Refine_Foreach

theory Refine_Foreach
imports Sepreftime 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 *}
thm vcg_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)
      subgoal by (metis append.assoc append.simps(2) append_Nil hd_Cons_tl)
      subgoal by (metis remove1_tl set_remove1_eq) 
      subgoal by (simp add: diff_mult_distrib)
      done
  subgoal using time_ub II1 apply (auto simp: Some_le_mm3_Some_conv Some_le_emb'_conv Some_eq_emb'_conv
               ) 
    subgoal by (simp add: 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 distinct_append distinct_card dual_order.trans enat_ord_simps(1) length_append order_mono_setup.refl set_append)  
    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"


(*lemma list_set_rel_finite: "(succl, succ) ∈ ⟨Id⟩list_set_rel ⟹ finite succ"
  sorry *)

(* ... *)



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"
  apply (intro fun_relI)
proof 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
    apply (auto simp add: nfoldliIE_def)
    subgoal 
      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])
      unfolding Some_eq_emb'_conv Some_le_emb'_conv
      using Cons(2,3) by auto
    subgoal 
      apply(simp add: RETURNT_def le_fun_def Some_le_emb'_conv)
      apply(rule FNC) using Cons(2,3) by auto
    done      
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))" 
     apply(rule nfoldliIE_rule'[where lr="[]"]) using assms by auto
  also have "… ≤ SPECT (emb P t)"
    apply(rule SPECT_ub) using T by (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    


thm nfoldliIE_rule[THEN T_specifies_rev, THEN T_conseq4,no_vars]


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 
     apply (subst whileT_unfold) by (auto simp: FOREACH_cond_def)
next
  case (Cons x ls)
  show ?case 
  proof (cases "c σ")
    case False thus ?thesis
    unfolding whileIET_def 
     apply (subst whileT_unfold)
      unfolding FOREACH_cond_def
      by simp
  next
    case [simp]: True
    from Cons show ?thesis
    unfolding whileIET_def 
     apply (subst whileT_unfold)
      unfolding FOREACH_cond_def FOREACH_body_def
      apply clarsimp
      apply (rule  bindT_mono)
      apply simp_all
      done
  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›)
  subgoal  using I0 by auto
  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    
      apply(auto simp add: Some_le_mm3_Some_conv emb_eq_Some_conv left_diff_distrib')
      apply(rule exI[where x="l1@[hd a]"]) by simp        
    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
(*
 
lemma LFO_pre_refine: (* TODO: Generalize! *)
  assumes "(li,l)∈⟨A⟩list_set_rel"
  assumes "(ci,c)∈R → bool_rel"
  assumes "(fi,f)∈A→R→⟨R⟩nrest_rel"
  assumes "(s0i,s0)∈R"
  shows "LIST_FOREACH' (RETURNT li) ci fi s0i ≤ ⇓R (FOREACHci I l c f s0 0 body_time)"
proof -
  from assms(1) have [simp]: "finite l" by (auto simp: list_set_rel_def br_def)
  show ?thesis
    unfolding   FOREACHci_def unfolding FOREACHoci_by_LIST_FOREACH 
    apply simp
    apply (rule LIST_FOREACH_autoref[param_fo, THEN nres_relD])
    using assms
    apply auto
    apply (auto simp: it_to_sorted_list_def nres_rel_def pw_le_iff refine_pw_simps
      list_set_rel_def br_def)
    done
qed    
    *)

(*
lemma LFOci_refine: (* TODO: Generalize! *)
  assumes "(li,l)∈⟨A⟩list_set_rel"
  assumes "⋀s si. (si,s)∈R ⟹ ci si ⟷ c s"
  assumes "⋀x xi s si. ⟦(xi,x)∈A; (si,s)∈R⟧ ⟹ fi xi si ≤ ⇓R (f x s)"
  assumes "(s0i,s0)∈R"
  shows "nfoldli li ci fi s0i ≤ ⇓R (FOREACHci I l c f s0 init_time body_time)"
(*
proof -
  from assms LFO_pre_refine[of li l A ci c R fi f s0i s0] show ?thesis
    unfolding fun_rel_def nres_rel_def LIST_FOREACH'_def
    apply (simp add: pw_le_iff refine_pw_simps)
    apply blast+
    done
qed    
*)sorry
*)



end