theory Basic_Assn
  imports
    "Refine_Imperative_HOL.Sepref_HOL_Bindings"
    "Refine_Imperative_HOL.Sepref_Basic"
begin

section "Auxilary imperative assumptions"

text "The following auxiliary assertion types and lemmas were provided by Peter Lammich"

subsection ‹List-Assn›



lemma list_assn_cong[fundef_cong]:
  "[ xs=xs'; ys=ys'; ∧x y. [ x∈set xs; y∈set ys ] ==> A x y = A' x y ] ==> list_assn A xs ys = list_assn A' xs' ys'"
  by (induction xs ys arbitrary: xs' ys' rule: list_assn.induct) auto


lemma list_assn_app_one: "list_assn P (l1@[x]) (l1'@[y]) = list_assn P l1 l1' * P x y"
  by simp

(* ------------------ ADDED by NM in course of btree_imp -------- *)


lemma list_assn_len: "h ⊨ list_assn A xs ys ==> length xs = length ys"
  using list_assn_aux_ineq_len by fastforce


lemma list_assn_append_Cons_left: "list_assn A (xs@x#ys) zs = (∃_A zs1 z zs2. list_assn A xs zs1 * A x z * list_assn A ys zs2 * ↑(zs1@z#zs2 = zs))"
  by (sep_auto simp add: list_assn_aux_cons_conv list_assn_aux_append_conv1 intro!: ent_iffI)


lemma list_assn_aux_append_Cons: 
  shows "length xs = length zsl ==> list_assn A (xs@x#ys) (zsl@z#zsr) = (list_assn A xs zsl * A x z * list_assn A ys zsr) "
  by (sep_auto simp add: mult.assoc)

lemma list_assn_prod_split: "list_assn (λx y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs"
proof(cases "length as = length bs")
  case True
  then show ?thesis
  proof (induction rule: list_induct2)
    case Nil
    then show ?case by sep_auto
  next
    case (Cons x xs y ys)
    show ?case
    proof (rule ent_iffI, goal_cases)
      case 1
      then show ?case
      using Cons by sep_auto
    next
      case 2
      then show ?case
      using Cons by sep_auto
    qed
  qed
next
  case False
  then show ?thesis
    by (simp add: list_assn_aux_ineq_len)
qed

(* -------------------------------------------- *)

subsection ‹Prod-Assn›


lemma prod_assn_cong[fundef_cong]:
  "[ p=p'; pi=pi'; A (fst p) (fst pi) = A' (fst p) (fst pi); B (snd p) (snd pi) = B' (snd p) (snd pi) ]
    ==> (A×_aB) p pi = (A'×_aB') p' pi'" 
  apply (cases p; cases pi)
  by auto

subsection ‹Assertions and Magic Wand›

lemma entails_preI: "(∧h. h ⊨ P ==> P ==>_A Q) ==> P ==>_A Q"
  unfolding entails_def
  by auto

lemma ent_true_drop_true: 
  "P*true==>_AQ*true ==> P*R*true==>_AQ*true"
  using assn_aci(10) ent_true_drop(1) by presburger

(* TODO *)
lemma rem_true: "P*true ==>_A Q*true ==> P ==>_AQ*true"
  using enttD enttI_true by blast

lemma assn_eq_split:
  assumes "B = C"
  shows "B ==>_A C"
  and "C ==>_A B"
  by (simp_all add: assms)

lemma ent_ex_inst: "∃_Ax. P x ==>_A Q ==> P y ==>_A Q"
  using ent_trans by blast

lemma ent_ex_inst2: "∃_Ax y. P x y ==>_A Q ==> P x y ==>_A Q"
  using ent_trans by blast

lemma ent_wandI2:
  assumes IMP: "P ==>_A (Q -* R)"
  shows "Q*P ==>_A R"
  using assms
  unfolding entails_def 
(*  by (meson assms ent_fwd ent_mp ent_refl fr_rot mod_frame_fwd)*)
proof (clarsimp, goal_cases)
  case (1 h as)
  then obtain as1 as2 where "as = as1 ∪ as2" "as1 ∩ as2 = {}" "(h,as1) ⊨ Q" "(h,as2) ⊨ P"
    by (metis mod_star_conv prod.inject)
  then have "(h,as2) ⊨ (Q-*R)"
    by (simp add: "1"(1))
  then have "(h,as1∪as2) ⊨ Q * (Q-*R)"
    by (simp add: ‹(h, as1) ⊨ Q› ‹as1 ∩ as2 = {}› star_assnI)
  then show ?case 
    using ‹as = as1 ∪ as2› ent_fwd ent_mp by blast
qed

lemma ent_wand: "(P ==>_A (Q -* R)) = (Q*P ==>_A R)"
  using ent_wandI2 ent_wandI by blast

lemma wand_ent_trans:
  assumes "P' ==>_A P"
      and "Q ==>_A Q'"
    shows "P -* Q ==>_A P' -* Q'"
  by (meson assms(1) assms(2) ent_wand ent_frame_fwd ent_refl ent_trans)

lemma wand_elim: "(P -* Q) * (Q -* R) ==>_A (P -* R)"
  by (metis ent_wand ent_frame_fwd ent_mp ent_refl star_assoc)

lemma emp_wand_same: "emp ==>_A (H -* H)"
  by (simp add: ent_wandI)

lemma emp_wand_equal: "(emp -* H) = H"
  apply(intro ent_iffI)
  apply (metis ent_mp norm_assertion_simps(1))
  by (simp add: ent_wandI)

lemma pure_wand_equal: "P ==> (↑(P) -* H) = H"
  by (simp add: emp_wand_equal)

lemma pure_wand_ent: "(P ==> (H1 ==>_A H2)) ==> H1 ==>_A ↑(P) -* H2"
  by (simp add: ent_wand)

lemma "↑(P ⟶ Q) ==>_A (↑(P) -* ↑(Q))"
  by (simp add: pure_wand_ent)

lemma wand_uncurry: "(P*Q) -* R ==>_A P -* (Q -* R)"
  by (simp add: assn_aci ent_mp ent_wandI fr_rot)

lemma wand_absorb: "(P -* Q) * R ==>_A (P -* (Q * R))"
  by (smt (z3) ent_mp ent_refl ent_star_mono ent_wandI star_aci(2) star_aci(3))

lemma wand_ent_self: "P ==>_A Q -* (Q * P)"
  by (simp add: ent_wandI)

lemma wand_ent_cancel: "P * ((P * Q) -* R) ==>_A Q -* R"
  by (simp add: ent_wandI2 wand_uncurry)


lemma "∃R. Q * R ==>_A P"
  using ent_mp by auto

lemma "P ==>_A Q * true ==> P = Q * (Q -* P)"
  apply(intro ent_iffI)
proof(goal_cases)
  case 2
  then show ?case
    by (simp add: ent_mp)
next
  case test: 1
  show ?case
    unfolding entails_def
    apply clarsimp
  proof (goal_cases)
    case (1 a b)
    then have "(a,b) ⊨ Q * true"
      using test entails_def
      by blast
    then obtain h as1 as2 where *:
        "(a,b) = (h, as1 ∪ as2) ∧ as1 ∩ as2 = {} ∧ (h, as1) ⊨ Q ∧ (h, as2) ⊨ true"
    using mod_star_conv by auto
  then have "(h, as1 ∪ as2) ⊨ P" "(a,b) = (h, as1 ∪ as2)" 
    using "1" by blast+
  then show ?case 
    apply simp
    thm star_assnI
    apply(intro star_assnI)
    apply (simp_all add: *)
    apply(intro wand_assnI)
    apply (meson "*" models_in_range)
    apply auto
    oops

end