Theory WB_More_IICF_LLVM

theory WB_More_IICF_LLVM
imports
  Isabelle_LLVM.IICF
  Isabelle_LLVM.Sepref_HOL_Bindings
  More_Sepref.WB_More_Refinement
begin

paragraph ‹This is not part of the multiset setup›

(*
definition "list_mset_assn A ≡ pure (list_mset_rel O ⟨the_pure A⟩mset_rel)"
declare list_mset_assn_def[symmetric,fcomp_norm_unfold]
lemma [safe_constraint_rules]: "is_pure (list_mset_assn A)" unfolding list_mset_assn_def by simp
*)

lemma prod_assn_id_assn_destroy:
  fixes R :: ‹_ ⇒ _ ⇒ _ ⇒ bool›
  shows ‹Rd *a id_assnd = (R ×a id_assn)d›
  apply (auto simp: hfprod_def prod_assn_def[abs_def] invalid_assn_def pure_def intro!: ext)
  apply (metis (full_types) pred_lift_extract_simps(2) pure_true_conv sep.add.right_neutral)
  by (metis Sep_Algebra_Add.pure_part_pure pred_lift_extract_simps(1) pred_lift_extract_simps(2)
    pure_part_split_conj)


(*lemma
 shows list_mset_assn_add_mset_Nil:
     ‹list_mset_assn R (add_mset q Q) [] = (λ_. False)› and
   list_mset_assn_empty_Cons:
    ‹list_mset_assn R {#} (x # xs) = (λ_. False)› and
   list_mset_assn_empty_nil:
    ‹list_mset_assn R {#} [] = □›
  unfolding list_mset_assn_def list_mset_rel_def mset_rel_def pure_def p2rel_def
    rel2p_def rel_mset_def br_def
  by (sep_auto simp: Collect_eq_comp pure_true_conv)+
*)

lemma Exists_eq_simp: ‹(∃x. (P x ∧* ↑ (x = b)) s) ⟷ P b s›
  apply (auto)
  apply (metis (full_types) Sep_Algebra_Add.pure_part_pure pure_partI pure_part_split_conj pure_true_conv sep.add.right_neutral)
  by (metis (full_types)pure_true_conv sep_conj_sep_emptyE)

lemma ‹(↑(x = b)) s ⟷ x = b ∧ □ s›
  by (auto simp: pred_lift_def)
lemma split_conj_is_pure:
  assumes ‹Sepref_Basic.is_pure B›
  shows ‹(B b bi ∧* R) s = ((bi, b) ∈ the_pure B ∧ R s)› (is ?A)
proof -
  obtain B' where R: ‹B = pure B'› using assms unfolding is_pure_conv ..
  then have R': ‹B' = the_pure B› by simp
  show A: ?A
    unfolding R'[symmetric] unfolding R pure_def pred_lift_extract_simps
    by auto
qed
lemma split_conj_is_pure2:
  assumes ‹Sepref_Basic.is_pure B›
  shows
      ‹(R1 ∧* B b bi ∧* R) s = ((bi, b) ∈ the_pure B ∧ (R1 ∧* R) s)› (is ?B)
  apply (subst sep_algebra_class.sep_conj_left_commute)
  apply (subst split_conj_is_pure[OF assms])
  apply simp
  done

(*
lemma snd_hnr_pure:
   ‹CONSTRAINT is_pure B ⟹ (return ∘ snd, RETURN ∘ snd) ∈ Ad *a Bk →a B›
  apply sepref_to_hoare
  apply (sep_auto simp: htriple_def wp_def mwp_def Monad.return_def pure_true_conv split_conj_is_pure
    split_conj_is_pure2 pred_lift_def)
  oops
*)

(*
lemma list_mset_assn_pure_conv:
  ‹list_mset_assn (pure R) = pure (⟨R⟩list_rel_mset_rel)›
proof -
  have [iff]: ‹(∀x x'. ((x', x) ∈ R) = ((x', x) ∈ P')) ⟷ R = P'› for P'
    by auto
  have [simp]: ‹the_pure (λa c. ↑((c, a) ∈ R)) = R›
    by (auto simp: the_pure_def)

  show ?thesis
    apply (intro ext)
    using list_all2_reorder_left_invariance[of ‹(λx x'. (x, x') ∈ R)›]
    by (fastforce
      simp: list_rel_mset_rel_def list_mset_assn_def
      mset_rel_def rel2p_def[abs_def] rel_mset_def p2rel_def
      list_mset_rel_def[abs_def] Collect_eq_comp br_def pred_lift_def
      list_rel_def Collect_eq_comp_right Sepref_Basic.pure_def
    intro!: arg_cong[of _ _ ‹λb. pure b _ _›])
qed
*)


lemma nempty_list_mset_rel_iff: ‹M ≠ {#} ⟹
  (xs, M) ∈ list_mset_rel ⟷ (xs ≠ [] ∧ hd xs ∈# M ∧
         (tl xs, remove1_mset (hd xs) M) ∈ list_mset_rel)›
  by (cases xs) (auto simp: list_mset_rel_def br_def dest!: multi_member_split)

(*abbreviation ghost_assn where
  ‹ghost_assn ≡ hr_comp unit_assn virtual_copy_rel›
*)

text ‹This function does not change the size of the underlying array.›
definition take1 where
  ‹take1 xs = take 1 xs›


text ‹The following two abbreviation are variants from term‹uncurry4› and
   term‹uncurry6›. The problem is that term‹uncurry2 (uncurry2 f)› and
   term‹uncurry (uncurry3 f)› are the same term, but only the latter is folded
   to term‹uncurry4›.›
abbreviation uncurry4' where
  "uncurry4' f ≡ uncurry2 (uncurry2 f)"

abbreviation uncurry6' where
  "uncurry6' f ≡ uncurry2 (uncurry4' f)"


lemma hrp_comp_Id2[simp]: ‹hrp_comp A Id = A›
  unfolding hrp_comp_def by auto

(*
lemma norm_RETURN_o[to_hnr_post]:
  "⋀f. (RETURN oooo f)$x$y$z$a = (RETURN$(f$x$y$z$a))"
  "⋀f. (RETURN ooooo f)$x$y$z$a$b = (RETURN$(f$x$y$z$a$b))"
  "⋀f. (RETURN oooooo f)$x$y$z$a$b$c = (RETURN$(f$x$y$z$a$b$c))"
  "⋀f. (RETURN ooooooo f)$x$y$z$a$b$c$d = (RETURN$(f$x$y$z$a$b$c$d))"
  "⋀f. (RETURN oooooooo f)$x$y$z$a$b$c$d$e = (RETURN$(f$x$y$z$a$b$c$d$e))"
  "⋀f. (RETURN ooooooooo f)$x$y$z$a$b$c$d$e$g = (RETURN$(f$x$y$z$a$b$c$d$e$g))"
  "⋀f. (RETURN oooooooooo f)$x$y$z$a$b$c$d$e$g$h= (RETURN$(f$x$y$z$a$b$c$d$e$g$h))"
  "⋀f. (RETURN ∘11 f)$x$y$z$a$b$c$d$e$g$h$i= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i))"
  "⋀f. (RETURN ∘12 f)$x$y$z$a$b$c$d$e$g$h$i$j= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j))"
  "⋀f. (RETURN ∘13 f)$x$y$z$a$b$c$d$e$g$h$i$j$l= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l))"
  "⋀f. (RETURN ∘14 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m))"
  "⋀f. (RETURN ∘15 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n))"
  "⋀f. (RETURN ∘16 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p))"
  "⋀f. (RETURN ∘17 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r=
    (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r))"
  "⋀f. (RETURN ∘18 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s=
    (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s))"
  "⋀f. (RETURN ∘19 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t=
    (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t))"
  "⋀f. (RETURN ∘20 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t$u=
    (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t$u))"
  by auto

lemma norm_return_o[to_hnr_post]:
  "⋀f. (return oooo f)$x$y$z$a = (return$(f$x$y$z$a))"
  "⋀f. (return ooooo f)$x$y$z$a$b = (return$(f$x$y$z$a$b))"
  "⋀f. (return oooooo f)$x$y$z$a$b$c = (return$(f$x$y$z$a$b$c))"
  "⋀f. (return ooooooo f)$x$y$z$a$b$c$d = (return$(f$x$y$z$a$b$c$d))"
  "⋀f. (return oooooooo f)$x$y$z$a$b$c$d$e = (return$(f$x$y$z$a$b$c$d$e))"
  "⋀f. (return ooooooooo f)$x$y$z$a$b$c$d$e$g = (return$(f$x$y$z$a$b$c$d$e$g))"
  "⋀f. (return oooooooooo f)$x$y$z$a$b$c$d$e$g$h= (return$(f$x$y$z$a$b$c$d$e$g$h))"
  "⋀f. (return ∘11 f)$x$y$z$a$b$c$d$e$g$h$i= (return$(f$x$y$z$a$b$c$d$e$g$h$i))"
  "⋀f. (return ∘12 f)$x$y$z$a$b$c$d$e$g$h$i$j= (return$(f$x$y$z$a$b$c$d$e$g$h$i$j))"
  "⋀f. (return ∘13 f)$x$y$z$a$b$c$d$e$g$h$i$j$l= (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l))"
  "⋀f. (return ∘14 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m= (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m))"
  "⋀f. (return ∘15 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n= (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n))"
  "⋀f. (return ∘16 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p= (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p))"
  "⋀f. (return ∘17 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r=
    (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r))"
  "⋀f. (return ∘18 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s=
    (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s))"
  "⋀f. (return ∘19 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t=
    (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t))"
  "⋀f. (return ∘20 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t$u=
    (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t$u))"
    by auto
*)

(*This is rather different from the SML version*)
lemma list_rel_update:
  assumes rel: ‹(xs, ys) ∈ ⟨the_pure R⟩list_rel› and
   h: ‹R b bi s› and
   p: ‹is_pure R›
  shows ‹(list_update xs ba bi, list_update ys ba b) ∈ ⟨the_pure R⟩list_rel›
proof -
  obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
    using p by fastforce
  have [simp]: ‹(bi, b) ∈ the_pure R›
    using h p by (auto simp: R R' pure_app_eq pred_lift_extract_simps)
  have ‹length xs = length ys›
    using assms list_rel_imp_same_length by blast

  then show ?thesis
    using rel
    by (induction xs ys arbitrary: ba rule: list_induct2) (auto split: nat.splits)
qed

end