Theory Auxiliary

section ‹Auxiliary Lemmas›

(*<*)
theory Auxiliary
  imports
    "HOL-Library.Multiset"
    "Nested_Multisets_Ordinals.Signed_Multiset"
    "HOL-Library.Linear_Temporal_Logic_on_Streams"
begin
(*>*)

unbundle multiset.lifting

subsection‹General›

lemma sum_list_hd_tl:
  fixes xs :: "(_ :: group_add) list"
  shows "xs  []  sum_list (tl xs) = (- hd xs) + sum_list xs"
  by (cases xs) simp_all


subsection‹Sums›

lemma Sum_eq_pick_changed_elem:
  assumes "finite M"
    and "m  M" "f m = g m + Δ"
    and "n. n  m  n  M  f n = g n"
  shows "(xM. f x) = (xM. g x) + Δ"
  using assms
proof (induct M arbitrary: m rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert x F)
  then show ?case
  proof (cases "x=m")
    case True
    with insert have "sum f F = sum g F"
      by (intro sum.cong[OF refl]) force
    with insert True show ?thesis
      by (auto simp: add.commute add.left_commute)
  next
    case False
    with insert show ?thesis
      by (auto simp: add.assoc)
  qed
qed

lemma sum_pos_ex_elem_pos: "(0::int) < (mM. f m)  mM. 0 < f m"
  by (meson not_le sum_nonpos)

lemma sum_if_distrib_add: "finite A  b  A  (aA. if a=b then X b + Y a else X a) = (aA. X a) + Y b"
  by (simp add: Sum_eq_pick_changed_elem)

subsection‹Partial Orders›

lemma (in order) order_finite_set_exists_foundation:
  fixes   t :: 'a
  assumes "finite M"
    and   "t  M"
  shows   "sM. s  t  (uM. ¬ u < s)"
  using assms
  by (simp add: dual_order.strict_iff_order finite_has_minimal2)

lemma order_finite_set_obtain_foundation:
  fixes   t :: "_ :: order"
  assumes "finite M"
    and   "t  M"
  obtains s where "s  M" "s  t" "uM. ¬ u < s"
  using assms order_finite_set_exists_foundation by blast

subsection‹Multisets›

lemma finite_nonzero_count: "finite {t. count M t > 0}"
  using count by auto

lemma finite_count[simp]: "finite {t. count M t > i}"
  by (rule finite_subset[OF _ finite_nonzero_count[of M]]) (auto simp only: set_mset_def)

subsection‹Signed Multisets›

lemma zcount_zmset_of_nonneg[simp]: "0  zcount (zmset_of M) t"
  by simp

lemma finite_zcount_pos[simp]: "finite {t. zcount M t > 0}"
  apply transfer
  subgoal for M
    apply (rule finite_subset[OF _ finite_Un[THEN iffD2, OF conjI[OF finite_nonzero_count finite_nonzero_count]], of _ "fst M" "snd M"])
    apply (auto simp only: set_mset_def fst_conv snd_conv split: prod.splits)
    done
  done

lemma finite_zcount_neg[simp]: "finite {t. zcount M t < 0}"
  apply transfer
  subgoal for M
    apply (rule finite_subset[OF _ finite_Un[THEN iffD2, OF conjI[OF finite_nonzero_count finite_nonzero_count]], of _ "fst M" "snd M"])
    apply (auto simp only: set_mset_def fst_conv snd_conv split: prod.splits)
    done
  done

lemma pos_zcount_in_zmset: "0 < zcount M x  x ∈#z M"
  by (simp add: zcount_inI)

lemma zmset_elem_nonneg: "x ∈#z M  (x. x ∈#z M  0  zcount M x)  0 < zcount M x"
  by (simp add: order.order_iff_strict zcount_eq_zero_iff)

lemma zero_le_sum_single: "0  zcount (xM. {#f x#}z) t"
  by (induct M rule: infinite_finite_induct) auto

lemma mem_zmset_of[simp]: "x ∈#z zmset_of M  x ∈# M"
  by (simp add: set_zmset_def)

lemma mset_neg_minus: "mset_neg (abs_zmultiset (Mp,Mn)) = Mn-Mp"
  by (simp add: mset_neg.abs_eq)

lemma mset_pos_minus: "mset_pos (abs_zmultiset (Mp,Mn)) = Mp-Mn"
  by (simp add: mset_pos.abs_eq)

lemma mset_neg_sum_set: "(m. m  M  mset_neg (f m) = {#})  mset_neg (mM. f m) = {#}"
  by (induct M rule: infinite_finite_induct) auto

lemma mset_neg_empty_iff: "mset_neg M = {#}  (t. 0  zcount M t)"
  apply rule
  subgoal
    by (metis add.commute add.right_neutral mset_pos_as_neg zcount_zmset_of_nonneg zmset_of_empty)
  subgoal
    apply (induct rule: zmultiset.abs_induct)
    subgoal for y
      apply (induct y)
      apply (subst mset_neg_minus)
      apply transfer'
      apply (simp add: Diff_eq_empty_iff_mset mset_subset_eqI)
      done
    done
  done

lemma mset_neg_zcount_nonneg: "mset_neg M = {#}  0  zcount M t"
  by (subst (asm) mset_neg_empty_iff) simp

lemma in_zmset_conv_pos_neg_disj: "x ∈#z M  x ∈# mset_pos M  x ∈# mset_neg M"
  by (metis count_mset_pos in_diff_zcount mem_zmset_of mset_pos_neg_partition nat_code(2) not_in_iff zcount_ne_zero_iff)

lemma in_zmset_notin_mset_pos[simp]: "x ∈#z M  x ∉# mset_pos M  x ∈# mset_neg M"
  by (auto simp: in_zmset_conv_pos_neg_disj)

lemma in_zmset_notin_mset_neg[simp]: "x ∈#z M  x ∉# mset_neg M  x ∈# mset_pos M"
  by (auto simp: in_zmset_conv_pos_neg_disj)

lemma in_mset_pos_in_zmset: "x ∈# mset_pos M  x ∈#z M"
  by (auto intro: iffD2[OF in_zmset_conv_pos_neg_disj])

lemma in_mset_neg_in_zmset: "x ∈# mset_neg M  x ∈#z M"
  by (auto intro: iffD2[OF in_zmset_conv_pos_neg_disj])

lemma set_zmset_eq_set_mset_union: "set_zmset M = set_mset (mset_pos M)  set_mset (mset_neg M)"
  by (auto dest: in_mset_pos_in_zmset in_mset_neg_in_zmset)

lemma member_mset_pos_iff_zcount: "x ∈# mset_pos M  0 < zcount M x"
  using not_in_iff pos_zcount_in_zmset by force

lemma member_mset_neg_iff_zcount: "x ∈# mset_neg M  zcount M x < 0"
  by (metis member_mset_pos_iff_zcount mset_pos_uminus neg_le_0_iff_le not_le zcount_uminus)

lemma mset_pos_mset_neg_disjoint[simp]: "set_mset (mset_pos Δ)  set_mset (mset_neg Δ) = {}"
  by (auto simp: member_mset_pos_iff_zcount member_mset_neg_iff_zcount)

lemma zcount_sum: "zcount (MMM. f M) t = (MMM. zcount (f M) t)"
  by (induct MM rule: infinite_finite_induct) auto

lemma zcount_filter_invariant: "zcount {# t'∈#zM. t'=t #} t = zcount M t"
  by auto

lemma in_filter_zmset_in_zmset[simp]: "x ∈#z filter_zmset P M  x ∈#z M"
  by (metis count_filter_zmset zcount_ne_zero_iff)

lemma pos_filter_zmset_pos_zmset[simp]: "0 < zcount (filter_zmset P M) x  0 < zcount M x"
  by (metis (full_types) count_filter_zmset less_irrefl)

lemma neg_filter_zmset_neg_zmset[simp]: "0 > zcount (filter_zmset P M) x  0 > zcount M x"
  by (metis (full_types) count_filter_zmset less_irrefl)


lift_definition update_zmultiset :: "'t zmultiset  't  int  't zmultiset" is
  "λ(A,B) T D.(if D>0 then (A + replicate_mset (nat D) T, B)
                    else (A,B + replicate_mset (nat (-D)) T))"
  by (auto simp: equiv_zmset_def if_split)

lemma zcount_update_zmultiset: "zcount (update_zmultiset M t n) t' = zcount M t' + (if t = t' then n else 0)"
  by transfer auto

lemma (in order) order_zmset_exists_foundation:
  fixes   t :: 'a
  assumes "0 < zcount M t"
  shows   "s. s  t  0 < zcount M s  (u. 0 < zcount M u  ¬ u < s)"
  using assms
proof -
  let ?M = "{t. 0 < zcount M t}"
  from assms have "t  ?M"
    by simp
  then have "s?M. s  t  (u?M. ¬ u < s)"
    by - (drule order_finite_set_exists_foundation[rotated 1], auto)
  then show ?thesis by auto
qed

lemma (in order) order_zmset_exists_foundation':
  fixes   t :: 'a
  assumes "0 < zcount M t"
  shows   "s. s  t  0 < zcount M s  (u<s. zcount M u  0)"
  using assms order_zmset_exists_foundation
  by (meson le_less_linear)

lemma (in order) order_zmset_exists_foundation_neg:
  fixes   t :: 'a
  assumes "zcount M t < 0"
  shows   "s. s  t  zcount M s < 0  (u. zcount M u < 0  ¬ u < s)"
  using assms
proof -
  let ?M = "{t. zcount M t < 0}"
  from assms have "t  ?M"
    by simp
  then have "s?M. s  t  (u?M. ¬ u < s)"
    by - (drule order_finite_set_exists_foundation[rotated 1], auto)
  then show ?thesis by auto
qed

lemma (in order) order_zmset_exists_foundation_neg':
  fixes   t :: 'a
  assumes "zcount M t < 0"
  shows   "s. s  t  zcount M s < 0  (u<s. 0  zcount M u)"
  using assms order_zmset_exists_foundation_neg
  by (meson le_less_linear)

lemma (in order) elem_order_zmset_exists_foundation:
  fixes x :: 'a
  assumes "x ∈#z M"
  shows   "s∈#zM. s  x  (u∈#zM. ¬ u < s)"
  by (rule order_finite_set_exists_foundation[OF finite_set_zmset, OF assms(1)])

subsubsection‹Image of a Signed Multiset›

lift_definition image_zmset :: "('a  'b)  'a zmultiset  'b zmultiset" is
  "λf (M, N). (image_mset f M, image_mset f N)"
  by (auto simp: equiv_zmset_def simp flip: image_mset_union)

syntax (ASCII)
  "_comprehension_zmset" :: "'a  'b  'b zmultiset  'a zmultiset"  ("({#_/. _ :#z _#})")
syntax
  "_comprehension_zmset" :: "'a  'b  'b zmultiset  'a zmultiset"  ("({#_/. _ ∈#z _#})")
translations
  "{#e. x ∈#z M#}"  "CONST image_zmset (λx. e) M"

lemma image_zmset_empty[simp]: "image_zmset f {#}z = {#}z"
  by transfer (auto simp: equiv_zmset_def)

lemma image_zmset_single[simp]: "image_zmset f {#x#}z = {#f x#}z"
  by transfer (simp add: equiv_zmset_def)

lemma image_zmset_union[simp]: "image_zmset f (M + N) = image_zmset f M + image_zmset f N"
  by transfer (auto simp: equiv_zmset_def)

lemma image_zmset_Diff[simp]: "image_zmset f (A - B) = image_zmset f A - image_zmset f B"
proof -
  have "image_zmset f (A - B + B) = image_zmset f (A - B) + image_zmset f B"
    using image_zmset_union by blast
  then show ?thesis by simp
qed

lemma mset_neg_image_zmset: "mset_neg M = {#}  mset_neg (image_zmset f M) = {#}"
  unfolding multiset_eq_iff count_empty
  by transfer (auto simp add: image_mset_subseteq_mono mset_subset_eqI mset_subset_eq_count)

lemma nonneg_zcount_image_zmset[simp]: "(t. 0  zcount M t)  0  zcount (image_zmset f M) t"
  by (meson mset_neg_empty_iff mset_neg_image_zmset)

lemma image_zmset_add_zmset[simp]: "image_zmset f (add_zmset t M) = add_zmset (f t) (image_zmset f M)"
  by transfer (auto simp: equiv_zmset_def)

lemma pos_zcount_image_zmset[simp]: "(t. 0  zcount M t)  0 < zcount M t  0 < zcount (image_zmset f M) (f t)"
  apply transfer
  subgoal for M t f
    apply (induct M)
    subgoal for Mp Mn
      apply simp
      apply (metis count_diff count_image_mset_ge_count image_mset_Diff less_le_trans subseteq_mset_def zero_less_diff)
      done
    done
  done

lemma set_zmset_transfer[transfer_rule]:
  "(rel_fun (pcr_zmultiset (=)) (rel_set (=)))
   (λ(Mp, Mn). set_mset Mp  set_mset Mn - {x. count Mp x = count Mn x}) set_zmset"
  by (auto simp: rel_fun_def pcr_zmultiset_def cr_zmultiset_def
      rel_set_eq multiset.rel_eq set_zmset_def zcount.abs_eq count_eq_zero_iff[symmetric]
      simp del: zcount_ne_zero_iff)

lemma zcount_image_zmset:
  "zcount (image_zmset f M) x = (y  f -` {x}  set_zmset M. zcount M y)"
  apply (transfer fixing: f x)
  subgoal for M
    apply (cases M; clarify)
    subgoal for Mp Mn
      unfolding count_image_mset int_sum
    proof -
      have "(xf -` {x}  set_mset Mp. int (count Mp x)) =
        (xf -` {x}  (set_mset Mp  set_mset Mn). int (count Mp x))" (is "?S1 = _")
        by (subst sum.same_carrier[where C="f -` {x}  (set_mset Mp  set_mset Mn)"])
          (auto simp: count_eq_zero_iff)
      moreover
      have "(xf -` {x}  set_mset Mn. int (count Mn x)) =
        (xf -` {x}  (set_mset Mp  set_mset Mn). int (count Mn x))"(is "?S2 = _")
        by (subst sum.same_carrier[where C="f -` {x}  (set_mset Mp  set_mset Mn)"])
          (auto simp: count_eq_zero_iff)
      moreover
      have "(xf -` {x}  (set_mset Mp  set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
        = (xf -` {x}  (set_mset Mp  set_mset Mn). int (count Mp x) - int (count Mn x))"
        (is "?S = _")
        by (subst sum.same_carrier[where C="f -` {x}  (set_mset Mp  set_mset Mn)"]) auto
      ultimately show "?S1 - ?S2 = ?S"
        by (auto simp: sum_subtractf)
    qed
    done
  done

lemma zmset_empty_image_zmset_empty: "(t. zcount M t = 0)  zcount (image_zmset f M) t = 0"
  by (auto simp: zcount_image_zmset)

lemma in_image_zmset_in_zmset: "t ∈#z image_zmset f M  t. t ∈#z M"
  by (rule ccontr) simp

lemma zcount_image_zmset_zero: "(m. m ∈#z M  f m  x)  x ∉#z image_zmset f M"
  unfolding set_zmset_def
  by (simp add: zcount_image_zmset) (metis Int_emptyI sum.empty vimage_singleton_eq)

lemma image_zmset_pre: "t ∈#z image_zmset f M  m. m ∈#z M  f m = t"
proof (rule ccontr)
  assume t: "t ∈#z image_zmset f M"
  assume "m. m ∈#z M  f m = t"
  then have "m ∈#z M  ¬ f m = t" for m
    by blast
  then have "zcount (image_zmset f M) t = 0"
    by (meson t zcount_image_zmset_zero)
  with t show False
    by (meson zcount_ne_zero_iff)
qed

lemma pos_image_zmset_obtain_pre:
  "(t. 0  zcount M t)  0 < zcount (image_zmset f M) t  m. 0 < zcount M m  f m = t"
proof -
  assume nonneg: "0  zcount M t" for t
  assume "0 < zcount (image_zmset f M) t"
  then have "t ∈#z image_zmset f M"
    by (simp add: pos_zcount_in_zmset)
  then obtain x where x: "x ∈#z M" "f x = t"
    by (auto dest: image_zmset_pre)
  with nonneg have "0 < zcount M x"
    by (meson zmset_elem_nonneg)
  with x show ?thesis
    by auto
qed

subsection‹Streams›

definition relates :: "('a  'a  bool)  'a stream  bool" where
  "relates φ s = φ (shd s) (shd (stl s))"

lemma relatesD[dest]: "relates P s  P (shd s) (shd (stl s))"
  unfolding relates_def by simp

lemma alw_relatesD[dest]: "alw (relates P) s  P (shd s) (shd (stl s))"
  by auto

lemma relatesI[intro]: "P (shd s) (shd (stl s))  relates P s"
  by (auto simp: relates_def)

lemma alw_holds_smap_conv_comp: "alw (holds P) (smap f s) = alw (λs. (P o f) (shd s)) s"
  apply (rule iffI)
   apply (coinduction arbitrary: s)
   apply auto []
  apply (coinduction arbitrary: s)
  apply auto
  done

lemma alw_relates: "alw (relates P) s  P (shd s) (shd (stl s))  alw (relates P) (stl s)"
  apply (rule iffI)
   apply (auto simp: relates_def dest: alwD) []
  apply (coinduction arbitrary: s)
  apply (auto simp: relates_def)
  done

subsection‹Notation›

no_notation AND  (infix "aand" 60)
no_notation OR   (infix "or" 60)
no_notation IMPL (infix "imp" 60)

notation AND  (infixr "aand" 70)
notation OR   (infixr "or" 65)
notation IMPL (infixr "imp" 60)

lifting_update multiset.lifting
lifting_forget multiset.lifting

(*<*)
end
(*>*)