Theory More_Loops

(*
  File:         More_Loops.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory More_Loops
imports
  "Refine_Monadic.Refine_While"
  "Refine_Monadic.Refine_Foreach"
  "HOL-Library.Rewrite"
begin

subsection ‹More Theorem about Loops›

text ‹Most theorem below have a counterpart in the Refinement Framework that is weaker (by missing
  assertions for example that are critical for code generation).
›
lemma Down_id_eq:
  ‹⇓Id x = x›
  by auto

lemma while_upt_while_direct1:
  "b ≥ a ⟹
  do {
    (_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
      ([a..<b],σ);
    RETURN σ
  } ≤ do {
    (_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
    RETURN σ
  }"
  apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
  apply (refine_vcg WHILET_refine[where R = ‹{((l, x'), (i::nat, x::'a)). x= x' ∧ i ≤ b ∧ i ≥ a ∧
     l = drop (i-a) [a..<b]}›])
  subgoal by auto
  subgoal by (auto simp: FOREACH_cond_def)
  subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
  subgoal by auto
  done

lemma while_upt_while_direct2:
  "b ≥ a ⟹
  do {
    (_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
      ([a..<b],σ);
    RETURN σ
  } ≥ do {
    (_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
    RETURN σ
  }"
  apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
  apply (refine_vcg WHILET_refine[where R = ‹{((i::nat, x::'a), (l, x')). x= x' ∧ i ≤ b ∧ i ≥ a ∧
    l = drop (i-a) [a..<b]}›])
  subgoal by auto
  subgoal by (auto simp: FOREACH_cond_def)
  subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
  subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
  subgoal by auto
  done

lemma while_upt_while_direct:
  "b ≥ a ⟹
  do {
    (_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
      ([a..<b],σ);
    RETURN σ
  } = do {
    (_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
    RETURN σ
  }"
  using while_upt_while_direct1[of a b] while_upt_while_direct2[of a b]
  unfolding order_eq_iff by fast

lemma while_nfoldli:
  "do {
    (_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
    RETURN σ
  } ≤ nfoldli l c f σ"
  apply (induct l arbitrary: σ)
  apply (subst WHILET_unfold)
  apply (simp add: FOREACH_cond_def)

  apply (subst WHILET_unfold)
  apply (auto
    simp: FOREACH_cond_def FOREACH_body_def
    intro: bind_mono Refine_Basic.bind_mono(1))
 done
lemma nfoldli_while: "nfoldli l c f σ
          ≤
         (WHILE⇩T⇗I⇖
           (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l, σ) ⤜
          (λ(_, σ). RETURN σ))"
proof (induct l arbitrary: σ)
  case Nil thus ?case by (subst WHILEIT_unfold) (auto simp: FOREACH_cond_def)
next
  case (Cons x ls)
  show ?case
  proof (cases "c σ")
    case False thus ?thesis
      apply (subst WHILEIT_unfold)
      unfolding FOREACH_cond_def
      by simp
  next
    case [simp]: True
    from Cons show ?thesis
      apply (subst WHILEIT_unfold)
      unfolding FOREACH_cond_def FOREACH_body_def
      apply clarsimp
      apply (rule Refine_Basic.bind_mono)
      apply simp_all
      done
  qed
qed

lemma while_eq_nfoldli: "do {
    (_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
    RETURN σ
  } = nfoldli l c f σ"
  apply (rule antisym)
  apply (rule while_nfoldli)
  apply (rule order_trans[OF nfoldli_while[where I="λ_. True"]])
  apply (simp add: WHILET_def)
  done

end