Theory DBM_Imperative_Loops

theory DBM_Imperative_Loops
  imports 
    Refine_Imperative_HOL.IICF
begin

subsection ‹Additional proof rules for typical looping constructs›

subsubsection ‹@{term Heap_Monad.fold_map}›

lemma fold_map_ht:
  assumes "list_all (λx. <A * true> f x <λr. ↑(Q x r) * A>⇩t) xs"
  shows "<A * true> Heap_Monad.fold_map f xs <λrs. ↑(list_all2 (λx r. Q x r) xs rs) * A>⇩t"
  using assms by (induction xs; sep_auto)

lemma fold_map_ht':
  assumes "list_all (λx. <true> f x <λr. ↑(Q x r)>⇩t) xs"
  shows "<true> Heap_Monad.fold_map f xs <λrs. ↑(list_all2 (λx r. Q x r) xs rs)>⇩t"
  using assms by (induction xs; sep_auto)

lemma fold_map_ht1:
  assumes "⋀x xi. <A * R x xi * true> f xi <λr. A * ↑(Q x r)>⇩t"
  shows "
  <A * list_assn R xs xsi * true>
    Heap_Monad.fold_map f xsi
  <λrs. A * ↑(list_all2 (λx r. Q x r) xs rs)>⇩t"
  apply (induction xs arbitrary: xsi)
   apply (sep_auto; fail)
  subgoal for x xs xsi
    by (cases xsi; sep_auto heap: assms)
  done

lemma fold_map_ht2:
  assumes "⋀x xi. <A * R x xi * true> f xi <λr. A * R x xi * ↑(Q x r)>⇩t"
  shows "
  <A * list_assn R xs xsi * true>
    Heap_Monad.fold_map f xsi
  <λrs. A * list_assn R xs xsi * ↑(list_all2 (λx r. Q x r) xs rs)>⇩t"
  apply (induction xs arbitrary: xsi)
   apply (sep_auto; fail)
  subgoal for x xs xsi
    apply (cases xsi; sep_auto heap: assms)
     apply (rule cons_rule[rotated 2], rule frame_rule, rprems)
      apply frame_inference
     apply frame_inference
    apply sep_auto
    done
  done

lemma fold_map_ht3:
  assumes "⋀x xi. <A * R x xi * true> f xi <λr. A * Q x r>⇩t"
  shows "<A * list_assn R xs xsi * true> Heap_Monad.fold_map f xsi <λrs. A * list_assn Q xs rs>⇩t"
  apply (induction xs arbitrary: xsi)
   apply (sep_auto; fail)
  subgoal for x xs xsi
    apply (cases xsi; sep_auto heap: assms)
     apply (rule Hoare_Triple.cons_pre_rule[rotated], rule frame_rule, rprems, frame_inference)
    apply sep_auto
    done
  done

subsubsection ‹@{term imp_for'} and @{term imp_for}›

lemma imp_for_rule2:
  assumes
    "emp ⟹⇩A I i a"
    "⋀i a. <A * I i a * true> ci a <λr. A * I i a * ↑(r ⟷ c a)>⇩t"
    "⋀i a. i < j ⟹ c a ⟹ <A * I i a * true> f i a <λr. A * I (i + 1) r>⇩t"
    "⋀a. I j a ⟹⇩A Q a" "⋀i a. i < j ⟹ ¬ c a ⟹ I i a ⟹⇩A Q a"
    "i ≤ j"
  shows "<A * true> imp_for i j ci f a <λr. A * Q r>⇩t"
proof -
  have
    "<A * I i a * true>
      imp_for i j ci f a
    <λr. A * (I j r ∨⇩A (∃⇩A i'. ↑(i' < j ∧ ¬ c r) * I i' r))>⇩t"
    using ‹i ≤ j› assms(2,3)
    apply (induction "j - i" arbitrary: i a; sep_auto)
    subgoal
      apply (rule ent_star_mono, rule ent_star_mono)
        apply (rule ent_refl, rule ent_disjI1_direct, rule ent_refl)
      done
     apply rprems
    apply sep_auto
      apply (rprems)
       apply sep_auto+
    apply (rule ent_star_mono, rule ent_star_mono, rule ent_refl, rule ent_disjI2')
     apply solve_entails
     apply simp+
    done
  then show ?thesis
    apply (rule cons_rule[rotated 2])
    subgoal
      apply (subst merge_true_star[symmetric])
      apply (rule ent_frame_fwd[OF assms(1)])
       apply frame_inference+
      done
    apply (rule ent_star_mono)
     apply (rule ent_star_mono, rule ent_refl)
     apply (solve_entails eintros: assms(5) assms(4) ent_disjE)+
    done
qed

lemma imp_for_rule:
  assumes
    "emp ⟹⇩A I i a"
    "⋀i a. <I i a * true> ci a <λr. I i a * ↑(r ⟷ c a)>⇩t"
    "⋀i a. i < j ⟹ c a ⟹ <I i a * true> f i a <λr. I (i + 1) r>⇩t"
    "⋀a. I j a ⟹⇩A Q a" "⋀i a. i < j ⟹ ¬ c a ⟹ I i a ⟹⇩A Q a"
    "i ≤ j"
  shows "<true> imp_for i j ci f a <λr. Q r>⇩t"
  by (rule cons_rule[rotated 2], rule imp_for_rule2[where A = true])
     (rule assms | sep_auto heap: assms; fail)+

lemma imp_for'_rule2:
  assumes
    "emp ⟹⇩A I i a"
    "⋀i a. i < j ⟹ <A * I i a * true> f i a <λr. A * I (i + 1) r>⇩t"
    "⋀a. I j a ⟹⇩A Q a"
    "i ≤ j"
  shows "<A * true> imp_for' i j f a <λr. A * Q r>⇩t"
  unfolding imp_for_imp_for'[symmetric] using assms(3,4)
  by (sep_auto heap: assms imp_for_rule2[where c = "λ_. True"])

lemma imp_for'_rule:
  assumes
    "emp ⟹⇩A I i a"
    "⋀i a. i < j ⟹ <I i a * true> f i a <λr. I (i + 1) r>⇩t"
    "⋀a. I j a ⟹⇩A Q a"
    "i ≤ j"
  shows "<true> imp_for' i j f a <λr. Q r>⇩t"
  unfolding imp_for_imp_for'[symmetric] using assms(3,4)
  by (sep_auto heap: assms imp_for_rule[where c = "λ_. True"])

lemma nth_rule:
  assumes "is_pure S"
    and "b < length a"
  shows
    "<nat_assn b bi * array_assn S a ai> Array.nth ai bi
     <λr. ∃⇩Ax. nat_assn b bi * array_assn S a ai * S x r * true * ↑ (x = a ! b)>"
  using sepref_fr_rules(165)[unfolded hn_refine_def hn_ctxt_def] assms by force

lemma imp_for_list_all:
  assumes
    "is_pure R" "n ≤ length xs"
    "⋀x xi. <A * R x xi * true> Pi xi <λr. A * ↑ (r ⟷ P x)>⇩t"
  shows "
  <A * array_assn R xs a * true>
    imp_for 0 n Heap_Monad.return
    (λi _. do {
      x ← Array.nth a i; Pi x
    })
    True
  <λr. A *  array_assn R xs a * ↑(r ⟷ list_all P (take n xs))>⇩t"
  apply (rule imp_for_rule2[where I = "λi r. ↑ (r ⟷ list_all P (take i xs))"])
       apply sep_auto
      apply sep_auto
  subgoal for i b
    using assms(2)
    apply (sep_auto heap: nth_rule)
     apply (rule cons_rule[rotated 2], rule frame_rule,
        rule nth_rule[where b = i and a = xs], rule assms)
       apply simp
      apply (simp add: pure_def)
      apply frame_inference
     apply frame_inference
    apply (sep_auto heap: assms(3) simp: pure_def take_Suc_conv_app_nth)
    done
    apply (simp add: take_Suc_conv_app_nth)
   apply simp
  unfolding list_all_iff
   apply clarsimp
   apply (metis le_less set_take_subset_set_take subsetCE)
  ..

lemma imp_for_list_ex:
  assumes
    "is_pure R" "n ≤ length xs"
    "⋀x xi. <A * R x xi * true> Pi xi <λr. A * ↑ (r ⟷ P x)>⇩t"
  shows "
  <A * array_assn R xs a * true>
    imp_for 0 n (λx. Heap_Monad.return (¬ x))
    (λi _. do {
      x ← Array.nth a i; Pi x
    })
    False
  <λr. A *  array_assn R xs a * ↑(r ⟷ list_ex P (take n xs))>⇩t"
  apply (rule imp_for_rule2[where I = "λi r. ↑ (r ⟷ list_ex P (take i xs))"])
       apply sep_auto
      apply sep_auto
  subgoal for i b
    using assms(2)
    apply (sep_auto heap: nth_rule)
     apply (rule cons_rule[rotated 2], rule frame_rule, rule nth_rule[of _ i xs], rule assms)
       apply simp
      apply (simp add: pure_def)
      apply frame_inference
     apply frame_inference
    apply (sep_auto heap: assms(3) simp: pure_def take_Suc_conv_app_nth)
    done
    apply (simp add: take_Suc_conv_app_nth)
   apply simp
  unfolding list_ex_iff
   apply clarsimp
   apply (metis le_less set_take_subset_set_take subsetCE)
  ..

lemma imp_for_list_all2:
  assumes
    "is_pure R" "is_pure S" "n ≤ length xs" "n ≤ length ys"
    "⋀x xi y yi. <A * R x xi * S y yi * true> Pi xi yi <λr. A * ↑ (r ⟷ P x y)>⇩t"
  shows "
  <A * array_assn R xs a  * array_assn S ys b * true>
    imp_for 0 n Heap_Monad.return
    (λi _. do {
      x ← Array.nth a i; y ← Array.nth b i; Pi x y
    })
    True
  <λr. A *  array_assn R xs a  * array_assn S ys b * ↑(r ⟷ list_all2 P (take n xs) (take n ys))>⇩t"
  apply (rule imp_for_rule2[where I = "λi r. ↑ (r ⟷ list_all2 P (take i xs) (take i ys))"])
       apply (sep_auto; fail)
      apply (sep_auto; fail)
  subgoal for i _
    supply [simp] = pure_def
    using assms(3,4)
    apply sep_auto
     apply (rule cons_rule[rotated 2], rule frame_rule, rule nth_rule[of _ i xs], rule assms)
       apply force
      apply (simp, frame_inference; fail)
     apply frame_inference
    apply sep_auto

     apply (rule cons_rule[rotated 2], rule frame_rule, rule nth_rule[of _ i ys], rule assms)
    unfolding pure_def
       apply force
      apply (simp, frame_inference; fail)
     apply frame_inference
    apply sep_auto

    supply [sep_heap_rules] = assms(5)
    apply sep_auto
    subgoal
      unfolding list_all2_conv_all_nth apply clarsimp
      subgoal for i'
        by (cases "i' = i") auto
      done
    subgoal
      unfolding list_all2_conv_all_nth by clarsimp
    apply frame_inference
    done
  unfolding list_all2_conv_all_nth apply auto
  done

lemma imp_for_list_all2':
  assumes
    "is_pure R" "is_pure S" "n ≤ length xs" "n ≤ length ys"
    "⋀x xi y yi. <R x xi * S y yi> Pi xi yi <λr. ↑ (r ⟷ P x y)>⇩t"
  shows "
  <array_assn R xs a  * array_assn S ys b>
    imp_for 0 n Heap_Monad.return
    (λi _. do {
      x ← Array.nth a i; y ← Array.nth b i; Pi x y
    })
    True
  <λr. array_assn R xs a  * array_assn S ys b * ↑(r ⟷ list_all2 P (take n xs) (take n ys))>⇩t"
  by (rule cons_rule[rotated 2], rule imp_for_list_all2[where A = true, rotated 4])
     (sep_auto heap: assms intro: assms)+

end