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

lemma finite_distinct_bounded: "finite A ⟹ finite {xs. distinct xs ∧ set xs ⊆ A}"
  apply (rule finite_subset[of _ "⋃n ∈ {0 .. card A}. {xs.  length xs = n ∧ distinct xs ∧ set xs ⊆ A}"])
  subgoal by clarsimp (metis card_mono distinct_card)
  subgoal by auto
  done


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 "(∑x∈M. f x) = (∑x∈M. 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) < (∑m∈M. f m) ⟹ ∃m∈M. 0 < f m"
  by (meson not_le sum_nonpos)

lemma sum_if_distrib_add: "finite A ⟹ b ∈ A ⟹ (∑a∈A. if a=b then X b + Y a else X a) = (∑a∈A. 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   "∃s∈M. s ≤ t ∧ (∀u∈M. ¬ 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" "∀u∈M. ¬ 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 (∑x∈M. {#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 (∑m∈M. 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 (∑M∈MM. f M) t = (∑M∈MM. 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 "(∑x∈f -` {x} ∩ set_mset Mp. int (count Mp x)) =
        (∑x∈f -` {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 "(∑x∈f -` {x} ∩ set_mset Mn. int (count Mn x)) =
        (∑x∈f -` {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 "(∑x∈f -` {x} ∩ (set_mset Mp ∪ set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
        = (∑x∈f -` {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
(*>*)