Quelle Multiset_Order.thy Sprache: Isabelle

(*  Title:      HOL/Library/Multiset_Order.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
    Author:     Martin Desharnais, MPI-INF Saarbruecken
*)

section \<open>More Theorems about the Multiset Order\<close>

theory Multiset_Order
imports Multiset
begin

subsection \<open>Alternative Characterizations\<close>

subsubsection \<open>The Dershowitz--Manna Ordering\<close>

definition multp\<^sub>D\<^sub>M where
  "multp\<^sub>D\<^sub>M r M N \
   (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)))"

lemma multp\<^sub>D\<^sub>M_imp_multp:
  "multp\<^sub>D\<^sub>M r M N \ multp r M N"
proof -
  assume "multp\<^sub>D\<^sub>M r M N"
  then obtain X Y where
    "X \ {#}" and "X \# N" and "M = N - X + Y" and "\k. k \# Y \ (\a. a \# X \ r k a)"
    unfolding multp\<^sub>D\<^sub>M_def by blast
  then have "multp r (N - X + Y) (N - X + X)"
    by (intro one_step_implies_multp) (auto simp: Bex_def trans_def)
  with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "multp r M N"
    by (metis subset_mset.diff_add)
qed

subsubsection \<open>The Huet--Oppen Ordering\<close>

definition multp\<^sub>H\<^sub>O where
  "multp\<^sub>H\<^sub>O r M N \ M \ N \ (\y. count N y < count M y \ (\x. r y x \ count M x < count N x))"

lemma multp_imp_multp\<^sub>H\<^sub>O:
  assumes "asymp r" and "transp r"
  shows "multp r M N \ multp\<^sub>H\<^sub>O r M N"
  unfolding multp_def mult_def
proof (induction rule: trancl_induct)
  case (base P)
  then show ?case
    using \<open>asymp r\<close>
    by (auto elim!: mult1_lessE simp: count_eq_zero_iff multp\<^sub>H\<^sub>O_def split: if_splits
        dest!: Suc_lessD)
next
  case (step N P)
  from step(3) have "M \ N" and
    **: "\y. count N y < count M y \ (\x. r y x \ count M x < count N x)"
    by (simp_all add: multp\<^sub>H\<^sub>O_def)
  from step(2) obtain M0 a K where
    *: "P = add_mset a M0" "N = M0 + K" "a \# K" "\b. b \# K \ r b a"
    using \<open>asymp r\<close> by (auto elim: mult1_lessE)
  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P"
    using *(4) \<open>asymp r\<close>
    by (metis asympD add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
        count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last)
  moreover
  have count_a: "\z. r a z \ count M z < count P z" if "count P a \ count M a"
  proof -
    from \<open>a \<notin># K\<close> and that have "count N a < count M a"
      unfolding *(1,2) by (auto simp add: not_in_iff)
    with ** obtain z where z: "r a z" "count M z < count N z"
      by blast
    with * have "count N z \ count P z"
      using \<open>asymp r\<close>
      by (metis add_diff_cancel_left' add_mset_add_single asympD diff_diff_add_mset
          diff_single_trivial in_diff_count not_le_imp_less)
    with z show ?thesis by auto
  qed
  have "\x. r y x \ count M x < count P x" if count_y: "count P y < count M y" for y
  proof (cases "y = a")
    case True
    with count_y count_a show ?thesis by auto
  next
    case False
    show ?thesis
    proof (cases "y \# K")
      case True
      with *(4) have "r y a" by simp
      then show ?thesis
        by (cases "count P a \ count M a") (auto dest: count_a intro: \transp r\[THEN transpD])
    next
      case False
      with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
        by (simp add: not_in_iff)
      with count_y ** obtain z where z: "r y z" "count M z < count N z" by auto
      show ?thesis
      proof (cases "z \# K")
        case True
        with *(4) have "r z a" by simp
        with z(1) show ?thesis
          by (cases "count P a \ count M a") (auto dest!: count_a intro: \transp r\[THEN transpD])
      next
        case False
        with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
          by (auto simp add: not_in_iff)
        with z show ?thesis by auto
      qed
    qed
  qed
  ultimately show ?case unfolding multp\<^sub>H\<^sub>O_def by blast
qed

lemma multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M: "multp\<^sub>H\<^sub>O r M N \<Longrightarrow> multp\<^sub>D\<^sub>M r M N"
unfolding multp\<^sub>D\<^sub>M_def
proof (intro iffI exI conjI)
  assume "multp\<^sub>H\<^sub>O r M N"
  then obtain z where z: "count M z < count N z"
    unfolding multp\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
  define X where "X = N - M"
  define Y where "Y = M - N"
  from z show "X \ {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
  from z show "X \# N" unfolding X_def by auto
  show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
  show "\k. k \# Y \ (\a. a \# X \ r k a)"
  proof (intro allI impI)
    fix k
    assume "k \# Y"
    then have "count N k < count M k" unfolding Y_def
      by (auto simp add: in_diff_count)
    with \<open>multp\<^sub>H\<^sub>O r M N\<close> obtain a where "r k a" and "count M a < count N a"
      unfolding multp\<^sub>H\<^sub>O_def by blast
    then show "\a. a \# X \ r k a" unfolding X_def
      by (auto simp add: in_diff_count)
  qed
qed

lemma multp_eq_multp\<^sub>D\<^sub>M: "asymp r \<Longrightarrow> transp r \<Longrightarrow> multp r = multp\<^sub>D\<^sub>M r"
  using multp\<^sub>D\<^sub>M_imp_multp multp_imp_multp\<^sub>H\<^sub>O[THEN multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M]
  by blast

lemma multp_eq_multp\<^sub>H\<^sub>O: "asymp r \<Longrightarrow> transp r \<Longrightarrow> multp r = multp\<^sub>H\<^sub>O r"
  using multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M[THEN multp\<^sub>D\<^sub>M_imp_multp] multp_imp_multp\<^sub>H\<^sub>O
  by blast

lemma multp\<^sub>D\<^sub>M_plus_plusI[simp]:
  assumes "multp\<^sub>D\<^sub>M R M1 M2"
  shows "multp\<^sub>D\<^sub>M R (M + M1) (M + M2)"
proof -
  from assms obtain X Y where
    "X \ {#}" and "X \# M2" and "M1 = M2 - X + Y" and "\k. k \# Y \ (\a. a \# X \ R k a)"
  unfolding multp\<^sub>D\<^sub>M_def by auto

  show "multp\<^sub>D\<^sub>M R (M + M1) (M + M2)"
    unfolding multp\<^sub>D\<^sub>M_def
  proof (intro exI conjI)
    show "X \ {#}"
      using \<open>X \<noteq> {#}\<close> by simp
  next
    show "X \# M + M2"
      using \<open>X \<subseteq># M2\<close>
      by (simp add: subset_mset.add_increasing)
  next
    show "M + M1 = M + M2 - X + Y"
      using \<open>X \<subseteq># M2\<close> \<open>M1 = M2 - X + Y\<close>
      by (metis multiset_diff_union_assoc union_assoc)
  next
    show "\k. k \# Y \ (\a. a \# X \ R k a)"
      using \<open>\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> R k a)\<close> by simp
  qed
qed

lemma multp\<^sub>H\<^sub>O_plus_plus[simp]: "multp\<^sub>H\<^sub>O R (M + M1) (M + M2) \<longleftrightarrow> multp\<^sub>H\<^sub>O R M1 M2"
  unfolding multp\<^sub>H\<^sub>O_def by simp

lemma strict_subset_implies_multp\<^sub>D\<^sub>M: "A \<subset># B \<Longrightarrow> multp\<^sub>D\<^sub>M r A B"
  unfolding multp\<^sub>D\<^sub>M_def
  by (metis add.right_neutral add_diff_cancel_right' empty_iff mset_subset_eq_add_right
      set_mset_empty subset_mset.lessE)

lemma strict_subset_implies_multp\<^sub>H\<^sub>O: "A \<subset># B \<Longrightarrow> multp\<^sub>H\<^sub>O r A B"
  unfolding multp\<^sub>H\<^sub>O_def
  by (simp add: leD mset_subset_eq_count)

lemma multp\<^sub>H\<^sub>O_implies_one_step_strong:
  assumes "multp\<^sub>H\<^sub>O R A B"
  defines "J \ B - A" and "K \ A - B"
  shows "J \ {#}" and "\k \# K. \x \# J. R k x"
proof -
  show "J \ {#}"
  using \<open>multp\<^sub>H\<^sub>O R A B\<close>
  by (metis Diff_eq_empty_iff_mset J_def add.right_neutral multp\<^sub>D\<^sub>M_def multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M
      multp\<^sub>H\<^sub>O_plus_plus subset_mset.add_diff_inverse subset_mset.le_zero_eq)

  show "\k\#K. \x\#J. R k x"
    using \<open>multp\<^sub>H\<^sub>O R A B\<close>
    by (metis J_def K_def in_diff_count multp\<^sub>H\<^sub>O_def)
qed

lemma multp\<^sub>H\<^sub>O_minus_inter_minus_inter_iff:
  fixes M1 M2 :: "_ multiset"
  shows "multp\<^sub>H\<^sub>O R (M1 - M2) (M2 - M1) \ multp\<^sub>H\<^sub>O R M1 M2"
  by (metis diff_intersect_left_idem multiset_inter_commute multp\<^sub>H\<^sub>O_plus_plus
      subset_mset.add_diff_inverse subset_mset.inf.cobounded1)

lemma multp\<^sub>H\<^sub>O_iff_set_mset_less\<^sub>H\<^sub>O_set_mset:
  "multp\<^sub>H\<^sub>O R M1 M2 \ (set_mset (M1 - M2) \ set_mset (M2 - M1) \
    (\<forall>y \<in># M1 - M2. (\<exists>x \<in># M2 - M1. R y x)))"
  unfolding multp\<^sub>H\<^sub>O_minus_inter_minus_inter_iff[of R M1 M2, symmetric]
  unfolding multp\<^sub>H\<^sub>O_def
  unfolding count_minus_inter_lt_count_minus_inter_iff
  unfolding minus_inter_eq_minus_inter_iff
  by auto

subsubsection \<open>Monotonicity\<close>

lemma multp\<^sub>D\<^sub>M_mono_strong:
  "multp\<^sub>D\<^sub>M R M1 M2 \ (\x y. x \# M1 \ y \# M2 \ R x y \ S x y) \ multp\<^sub>D\<^sub>M S M1 M2"
  unfolding multp\<^sub>D\<^sub>M_def
  by (metis add_diff_cancel_left' in_diffD subset_mset.diff_add)

lemma multp\<^sub>H\<^sub>O_mono_strong:
  "multp\<^sub>H\<^sub>O R M1 M2 \ (\x y. x \# M1 \ y \# M2 \ R x y \ S x y) \ multp\<^sub>H\<^sub>O S M1 M2"
  unfolding multp\<^sub>H\<^sub>O_def
  by (metis count_inI less_zeroE)

subsubsection \<open>Properties of Orders\<close>

paragraph \<open>Asymmetry\<close>

text \<open>The following lemma is a negative result stating that asymmetry of an arbitrary binary
relation cannot be simply lifted to @{const multp\<^sub>H\<^sub>O}. It suffices to have four distinct values to
build a counterexample.\<close>

lemma asymp_not_liftable_to_multp\<^sub>H\<^sub>O:
  fixes a b c d :: 'a
  assumes "distinct [a, b, c, d]"
  shows "\ (\(R :: 'a \ 'a \ bool). asymp R \ asymp (multp\<^sub>H\<^sub>O R))"
proof -
  define R :: "'a \ 'a \ bool" where
    "R = (\x y. x = a \ y = c \ x = b \ y = d \ x = c \ y = b \ x = d \ y = a)"

  from assms(1) have "{#a, b#} \ {#c, d#}"
    by (metis add_mset_add_single distinct.simps(2) list.set(1) list.simps(15) multi_member_this
        set_mset_add_mset_insert set_mset_single)

  from assms(1) have "asymp R"
    by (auto simp: R_def intro: asymp_onI)
  moreover have "\ asymp (multp\<^sub>H\<^sub>O R)"
    unfolding asymp_on_def Set.ball_simps not_all not_imp not_not
  proof (intro exI conjI)
    show "multp\<^sub>H\<^sub>O R {#a, b#} {#c, d#}"
      unfolding multp\<^sub>H\<^sub>O_def
      using \<open>{#a, b#} \<noteq> {#c, d#}\<close> R_def assms by auto
  next
    show "multp\<^sub>H\<^sub>O R {#c, d#} {#a, b#}"
      unfolding multp\<^sub>H\<^sub>O_def
      using \<open>{#a, b#} \<noteq> {#c, d#}\<close> R_def assms by auto
  qed
  ultimately show ?thesis
    unfolding not_all not_imp by auto
qed

text \<open>However, if the binary relation is both asymmetric and transitive, then @{const multp\<^sub>H\<^sub>O} is
also asymmetric.\<close>

lemma asymp_on_multp\<^sub>H\<^sub>O:
  assumes "asymp_on A R" and "transp_on A R" and
    B_sub_A: "\M. M \ B \ set_mset M \ A"
  shows "asymp_on B (multp\<^sub>H\<^sub>O R)"
proof (rule asymp_onI)
  fix M1 M2 :: "'a multiset"
  assume "M1 \ B" "M2 \ B" "multp\<^sub>H\<^sub>O R M1 M2"

  from \<open>transp_on A R\<close> B_sub_A have tran: "transp_on (set_mset (M1 - M2)) R"
    using \<open>M1 \<in> B\<close>
    by (meson in_diffD subset_eq transp_on_subset)

  from \<open>asymp_on A R\<close> B_sub_A have asym: "asymp_on (set_mset (M1 - M2)) R"
    using \<open>M1 \<in> B\<close>
    by (meson in_diffD subset_eq asymp_on_subset)

  show "\ multp\<^sub>H\<^sub>O R M2 M1"
  proof (cases "M1 - M2 = {#}")
    case True
    then show ?thesis
      using multp\<^sub>H\<^sub>O_implies_one_step_strong(1) by metis
  next
    case False
    hence "\m\#M1 - M2. \x\#M1 - M2. x \ m \ \ R m x"
      using Finite_Set.bex_max_element[of "set_mset (M1 - M2)" R, OF finite_set_mset asym tran]
      by simp
    with \<open>transp_on A R\<close> B_sub_A have "\<exists>y\<in>#M2 - M1. \<forall>x\<in>#M1 - M2. \<not> R y x"
      using \<open>multp\<^sub>H\<^sub>O R M1 M2\<close>[THEN multp\<^sub>H\<^sub>O_implies_one_step_strong(2)]
      using asym[THEN irreflp_on_if_asymp_on, THEN irreflp_onD]
      by (metis \<open>M1 \<in> B\<close> \<open>M2 \<in> B\<close> in_diffD subsetD transp_onD)
    thus ?thesis
      unfolding multp\<^sub>H\<^sub>O_iff_set_mset_less\<^sub>H\<^sub>O_set_mset by simp
  qed
qed

lemma asymp_multp\<^sub>H\<^sub>O:
  assumes "asymp R" and "transp R"
  shows "asymp (multp\<^sub>H\<^sub>O R)"
  using assms asymp_on_multp\<^sub>H\<^sub>O[of UNIV, simplified] by metis

paragraph \<open>Irreflexivity\<close>

lemma irreflp_on_multp\<^sub>H\<^sub>O[simp]: "irreflp_on B (multp\<^sub>H\<^sub>O R)"
    by (simp add: irreflp_onI multp\<^sub>H\<^sub>O_def)

paragraph \<open>Transitivity\<close>

lemma transp_on_multp\<^sub>H\<^sub>O:
  assumes "asymp_on A R" and "transp_on A R" and B_sub_A: "\M. M \ B \ set_mset M \ A"
  shows "transp_on B (multp\<^sub>H\<^sub>O R)"
proof (rule transp_onI)
  from assms have "asymp_on B (multp\<^sub>H\<^sub>O R)"
    using asymp_on_multp\<^sub>H\<^sub>O by metis

  fix M1 M2 M3
  assume hyps: "M1 \ B" "M2 \ B" "M3 \ B" "multp\<^sub>H\<^sub>O R M1 M2" "multp\<^sub>H\<^sub>O R M2 M3"

  from assms have
    [intro]: "asymp_on (set_mset M1 \ set_mset M2) R" "transp_on (set_mset M1 \ set_mset M2) R"
    using \<open>M1 \<in> B\<close> \<open>M2 \<in> B\<close>
    by (simp_all add: asymp_on_subset transp_on_subset)

  from assms have "transp_on (set_mset M1) R"
    by (meson transp_on_subset hyps(1))

  from \<open>multp\<^sub>H\<^sub>O R M1 M2\<close> have
    "M1 \ M2" and
    "\y. count M2 y < count M1 y \ (\x. R y x \ count M1 x < count M2 x)"
    unfolding multp\<^sub>H\<^sub>O_def by simp_all

  from \<open>multp\<^sub>H\<^sub>O R M2 M3\<close> have
    "M2 \ M3" and
    "\y. count M3 y < count M2 y \ (\x. R y x \ count M2 x < count M3 x)"
    unfolding multp\<^sub>H\<^sub>O_def by simp_all

  show "multp\<^sub>H\<^sub>O R M1 M3"
  proof (rule ccontr)
    let ?P = "\x. count M3 x < count M1 x \ (\y. R x y \ count M1 y \ count M3 y)"

    assume "\ multp\<^sub>H\<^sub>O R M1 M3"
    hence "M1 = M3 \ (\x. ?P x)"
      unfolding multp\<^sub>H\<^sub>O_def by force
    thus False
    proof (elim disjE)
      assume "M1 = M3"
      thus False
        using \<open>asymp_on B (multp\<^sub>H\<^sub>O R)\<close>[THEN asymp_onD]
        using \<open>M2 \<in> B\<close> \<open>M3 \<in> B\<close> \<open>multp\<^sub>H\<^sub>O R M1 M2\<close> \<open>multp\<^sub>H\<^sub>O R M2 M3\<close>
        by metis
    next
      assume "\x. ?P x"
      hence "\x \# M1 + M2. ?P x"
        by (auto simp: count_inI)
      have "\y \# M1 + M2. ?P y \ (\z \# M1 + M2. R y z \ \ ?P z)"
      proof (rule Finite_Set.bex_max_element_with_property)
        show "\x \# M1 + M2. ?P x"
          using \<open>\<exists>x. ?P x\<close>
          by (auto simp: count_inI)
      qed auto
      then obtain x where
        "x \# M1 + M2" and
        "count M3 x < count M1 x" and
        "\y. R x y \ count M1 y \ count M3 y" and
        "\y \# M1 + M2. R x y \ count M3 y < count M1 y \ (\z. R y z \ count M1 z < count M3 z)"
        by force

      let ?Q = "\x'. R\<^sup>=\<^sup>= x x' \ count M3 x' < count M2 x'"
      show False
      proof (cases "\x'. ?Q x'")
        case True
        have "\y \# M1 + M2. ?Q y \ (\z \# M1 + M2. R y z \ \ ?Q z)"
        proof (rule Finite_Set.bex_max_element_with_property)
          show "\x \# M1 + M2. ?Q x"
            using \<open>\<exists>x. ?Q x\<close>
            by (auto simp: count_inI)
        qed auto
        then obtain x' where
          "x' \# M1 + M2" and
          "R\<^sup>=\<^sup>= x x'" and
          "count M3 x' < count M2 x'" and
          maximality_x': "\z \# M1 + M2. R x' z \ \ (R\<^sup>=\<^sup>= x z) \ count M3 z \ count M2 z"
          by (auto simp: linorder_not_less)
        with \<open>multp\<^sub>H\<^sub>O R M2 M3\<close> obtain y' where
          "R x' y'" and "count M2 y' < count M3 y'"
          unfolding multp\<^sub>H\<^sub>O_def by auto
        hence "count M2 y' < count M1 y'"
          by (smt (verit) \<open>R\<^sup>=\<^sup>= x x'\<close> \<open>\<forall>y. R x y \<longrightarrow> count M3 y \<le> count M1 y\<close>
              \<open>count M3 x < count M1 x\<close> \<open>count M3 x' < count M2 x'\<close> assms(2) count_inI
              dual_order.strict_trans1 hyps(1) hyps(2) hyps(3) less_nat_zero_code B_sub_A subsetD
              sup2E transp_onD)
        with \<open>multp\<^sub>H\<^sub>O R M1 M2\<close> obtain y'' where
          "R y' y''" and "count M1 y'' < count M2 y''"
          unfolding multp\<^sub>H\<^sub>O_def by auto
        hence "count M3 y'' < count M2 y''"
          by (smt (verit, del_insts) \<open>R x' y'\<close> \<open>R\<^sup>=\<^sup>= x x'\<close> \<open>\<forall>y. R x y \<longrightarrow> count M3 y \<le> count M1 y\<close>
              \<open>count M2 y' < count M3 y'\<close> \<open>count M3 x < count M1 x\<close> \<open>count M3 x' < count M2 x'\<close>
              assms(2) count_greater_zero_iff dual_order.strict_trans1 hyps(1) hyps(2) hyps(3)
              less_nat_zero_code linorder_not_less B_sub_A subset_iff sup2E transp_onD)

        moreover have "count M2 y'' \ count M3 y''"
        proof -
          have "y'' \# M1 + M2"
            by (metis \<open>count M1 y'' < count M2 y''\<close> count_inI not_less_iff_gr_or_eq union_iff)

          moreover have "R x' y''"
            by (metis \<open>R x' y'\<close> \<open>R y' y''\<close> \<open>count M2 y' < count M1 y'\<close>
                \<open>transp_on (set_mset M1 \<union> set_mset M2) R\<close> \<open>x' \<in># M1 + M2\<close> calculation count_inI
                nat_neq_iff set_mset_union transp_onD union_iff)

          moreover have "R\<^sup>=\<^sup>= x y''"
            using \<open>R\<^sup>=\<^sup>= x x'\<close>
            by (metis (mono_tags, opaque_lifting) \<open>transp_on (set_mset M1 \<union> set_mset M2) R\<close>
                \<open>x \<in># M1 + M2\<close> \<open>x' \<in># M1 + M2\<close> calculation(1) calculation(2) set_mset_union sup2I1
                transp_onD transp_on_reflclp)

          ultimately show ?thesis
            using maximality_x'[rule_format, of y''] by metis
        qed

        ultimately show ?thesis
          by linarith
      next
        case False
        hence "\x'. R\<^sup>=\<^sup>= x x' \ count M2 x' \ count M3 x'"
          by auto
        hence "count M2 x \ count M3 x"
          by simp
        hence "count M2 x < count M1 x"
          using \<open>count M3 x < count M1 x\<close> by linarith
        with \<open>multp\<^sub>H\<^sub>O R M1 M2\<close> obtain y where
          "R x y" and "count M1 y < count M2 y"
          unfolding multp\<^sub>H\<^sub>O_def by auto
        hence "count M3 y < count M2 y"
          using \<open>\<forall>y. R x y \<longrightarrow> count M3 y \<le> count M1 y\<close> dual_order.strict_trans2 by metis
        then show ?thesis
          using False \<open>R x y\<close> by auto
      qed
    qed
  qed
qed

lemma transp_multp\<^sub>H\<^sub>O:
  assumes "asymp R" and "transp R"
  shows "transp (multp\<^sub>H\<^sub>O R)"
  using assms transp_on_multp\<^sub>H\<^sub>O[of UNIV, simplified] by metis

paragraph \<open>Totality\<close>

lemma totalp_on_multp\<^sub>D\<^sub>M:
  "totalp_on A R \ (\M. M \ B \ set_mset M \ A) \ totalp_on B (multp\<^sub>D\<^sub>M R)"
  by (smt (verit, ccfv_SIG) count_inI in_mono multp\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M not_less_iff_gr_or_eq
      totalp_onD totalp_onI)

lemma totalp_multp\<^sub>D\<^sub>M: "totalp R \<Longrightarrow> totalp (multp\<^sub>D\<^sub>M R)"
  by (rule totalp_on_multp\<^sub>D\<^sub>M[of UNIV R UNIV, simplified])

lemma totalp_on_multp\<^sub>H\<^sub>O:
  "totalp_on A R \ (\M. M \ B \ set_mset M \ A) \ totalp_on B (multp\<^sub>H\<^sub>O R)"
  by (smt (verit, ccfv_SIG) count_inI in_mono multp\<^sub>H\<^sub>O_def not_less_iff_gr_or_eq totalp_onD
      totalp_onI)

lemma totalp_multp\<^sub>H\<^sub>O: "totalp R \<Longrightarrow> totalp (multp\<^sub>H\<^sub>O R)"
  by (rule totalp_on_multp\<^sub>H\<^sub>O[of UNIV R UNIV, simplified])

paragraph \<open>Type Classes\<close>

context preorder
begin

lemma order_mult: "class.order
  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
  (is "class.order ?le ?less")
proof -
  have irrefl: "\M :: 'a multiset. \ ?less M M"
  proof
    fix M :: "'a multiset"
    have "trans {(x'::'a, x). x' < x}"
      by (rule transI) (blast intro: less_trans)
    moreover
    assume "(M, M) \ mult {(x, y). x < y}"
    ultimately have "\I J K. M = I + J \ M = I + K
      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
      by (rule mult_implies_one_step)
    then obtain I J K where "M = I + J" and "M = I + K"
      and "J \ {#}" and "(\k\set_mset K. \j\set_mset J. (k, j) \ {(x, y). x < y})" by blast
    then have aux1: "K \ {#}" and aux2: "\k\set_mset K. \j\set_mset K. k < j" by auto
    have "finite (set_mset K)" by simp
    moreover note aux2
    ultimately have "set_mset K = {}"
      by (induct rule: finite_induct)
       (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
    with aux1 show False by simp
  qed
  have trans: "\K M N :: 'a multiset. ?less K M \ ?less M N \ ?less K N"
    unfolding mult_def by (blast intro: trancl_trans)
  show "class.order ?le ?less"
    by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
qed

text \<open>The Dershowitz--Manna ordering:\<close>

definition less_multiset\<^sub>D\<^sub>M where
  "less_multiset\<^sub>D\<^sub>M M N \
   (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"

text \<open>The Huet--Oppen ordering:\<close>

definition less_multiset\<^sub>H\<^sub>O where
  "less_multiset\<^sub>H\<^sub>O M N \ M \ N \ (\y. count N y < count M y \ (\x. y < x \ count M x < count N x))"

lemma mult_imp_less_multiset\<^sub>H\<^sub>O:
  "(M, N) \ mult {(x, y). x < y} \ less_multiset\<^sub>H\<^sub>O M N"
  unfolding multp_def[of "(<)", symmetric]
  using multp_imp_multp\<^sub>H\<^sub>O[of "(<)"]
  by (simp add: less_multiset\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_def)

lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
  "less_multiset\<^sub>D\<^sub>M M N \ (M, N) \ mult {(x, y). x < y}"
  unfolding multp_def[of "(<)", symmetric]
  by (rule multp\<^sub>D\<^sub>M_imp_multp[of "(<)" M N]) (simp add: less_multiset\<^sub>D\<^sub>M_def multp\<^sub>D\<^sub>M_def)

lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N"
  unfolding less_multiset\<^sub>D\<^sub>M_def less_multiset\<^sub>H\<^sub>O_def
  unfolding multp\<^sub>D\<^sub>M_def[symmetric] multp\<^sub>H\<^sub>O_def[symmetric]
  by (rule multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M)

lemma mult_less_multiset\<^sub>D\<^sub>M: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>D\<^sub>M M N"
  unfolding multp_def[of "(<)", symmetric]
  using multp_eq_multp\<^sub>D\<^sub>M[of "(<)", simplified]
  by (simp add: multp\<^sub>D\<^sub>M_def less_multiset\<^sub>D\<^sub>M_def)

lemma mult_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
  unfolding multp_def[of "(<)", symmetric]
  using multp_eq_multp\<^sub>H\<^sub>O[of "(<)", simplified]
  by (simp add: multp\<^sub>H\<^sub>O_def less_multiset\<^sub>H\<^sub>O_def)

lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]

end

lemma less_multiset_less_multiset\<^sub>H\<^sub>O: "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
  unfolding less_multiset_def multp_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..

lemma less_multiset\<^sub>D\<^sub>M:
  "M < N \ (\X Y. X \ {#} \ X \# N \ M = N - X + Y \ (\k. k \# Y \ (\a. a \# X \ k < a)))"
  by (rule mult\<^sub>D\<^sub>M[folded multp_def less_multiset_def])

lemma less_multiset\<^sub>H\<^sub>O:
  "M < N \ M \ N \ (\y. count N y < count M y \ (\x>y. count M x < count N x))"
  by (rule mult\<^sub>H\<^sub>O[folded multp_def less_multiset_def])

lemma subset_eq_imp_le_multiset:
  shows "M \# N \ M \ N"
  unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
  by (simp add: less_le_not_le subseteq_mset_def)

(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_right_total: "M < add_mset x M"
  unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp

lemma less_eq_multiset_empty_left[simp]: "{#} \ M"
  by (simp add: subset_eq_imp_le_multiset)

lemma ex_gt_imp_less_multiset: "(\y. y \# N \ (\x. x \# M \ x < y)) \ M < N"
  unfolding less_multiset\<^sub>H\<^sub>O
  by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)

lemma less_eq_multiset_empty_right[simp]: "M \ {#} \ \ M \ {#}"
  by (metis less_eq_multiset_empty_left antisym)

(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_empty_left[simp]: "M \ {#} \ {#} < M"
  by (simp add: less_multiset\<^sub>H\<^sub>O)

(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_empty_right[simp]: "\ M < {#}"
  using subset_mset.le_zero_eq less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M by blast

(* FIXME: "le" should be "less" in this and other names *)
lemma union_le_diff_plus: "P \# M \ N < P \ M - P + N < M"
  by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)

instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le
begin

lemma less_eq_multiset\<^sub>H\<^sub>O:
  "M \ N \ (\y. count N y < count M y \ (\x. y < x \ count M x < count N x))"
  by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)

instance by standard (auto simp: less_eq_multiset\<^sub>H\<^sub>O)

lemma
  fixes M N :: "'a multiset"
  shows less_eq_multiset_plus_left: "N \ (M + N)"
    and less_eq_multiset_plus_right: "M \ (M + N)"
  by simp_all

lemma
  fixes M N :: "'a multiset"
  shows le_multiset_plus_left_nonempty: "M \ {#} \ N < M + N"
    and le_multiset_plus_right_nonempty: "N \ {#} \ M < M + N"
    by simp_all

end

lemma all_lt_Max_imp_lt_mset: "N \ {#} \ (\a \# M. a < Max (set_mset N)) \ M < N"
  by (meson Max_in[OF finite_set_mset] ex_gt_imp_less_multiset set_mset_eq_empty_iff)

lemma lt_imp_ex_count_lt: "M < N \ \y. count M y < count N y"
  by (meson less_eq_multiset\<^sub>H\<^sub>O less_le_not_le)

lemma subset_imp_less_mset: "A \# B \ A < B"
  by (simp add: order.not_eq_order_implies_strict subset_eq_imp_le_multiset)

lemma image_mset_strict_mono:
  assumes mono_f: "\x \ set_mset M. \y \ set_mset N. x < y \ f x < f y"
    and less: "M < N"
  shows "image_mset f M < image_mset f N"
proof -
  obtain Y X where
    y_nemp: "Y \ {#}" and y_sub_N: "Y \# N" and M_eq: "M = N - Y + X" and
    ex_y: "\x. x \# X \ (\y. y \# Y \ x < y)"
    using less[unfolded less_multiset\<^sub>D\<^sub>M] by blast

  have x_sub_M: "X \# M"
    using M_eq by simp

  let ?fY = "image_mset f Y"
  let ?fX = "image_mset f X"

  show ?thesis
    unfolding less_multiset\<^sub>D\<^sub>M
  proof (intro exI conjI)
    show "image_mset f M = image_mset f N - ?fY + ?fX"
      using M_eq[THEN arg_cong, of "image_mset f"] y_sub_N
      by (metis image_mset_Diff image_mset_union)
  next
    obtain y where y: "\x. x \# X \ y x \# Y \ x < y x"
      using ex_y by metis

    show "\fx. fx \# ?fX \ (\fy. fy \# ?fY \ fx < fy)"
    proof (intro allI impI)
      fix fx
      assume "fx \# ?fX"
      then obtain x where fx: "fx = f x" and x_in: "x \# X"
        by auto
      hence y_in: "y x \# Y" and y_gt: "x < y x"
        using y[rule_format, OF x_in] by blast+
      hence "f (y x) \# ?fY \ f x < f (y x)"
        using mono_f y_sub_N x_sub_M x_in
        by (metis image_eqI in_image_mset mset_subset_eqD)
      thus "\fy. fy \# ?fY \ fx < fy"
        unfolding fx by auto
    qed
  qed (auto simp: y_nemp y_sub_N image_mset_subseteq_mono)
qed

lemma image_mset_mono:
  assumes mono_f: "\x \ set_mset M. \y \ set_mset N. x < y \ f x < f y"
    and less: "M \ N"
  shows "image_mset f M \ image_mset f N"
  by (metis eq_iff image_mset_strict_mono less less_imp_le mono_f order.not_eq_order_implies_strict)

lemma mset_lt_single_right_iff[simp]: "M < {#y#} \ (\x \# M. x < y)" for y :: "'a::linorder"
proof (rule iffI)
  assume M_lt_y: "M < {#y#}"
  show "\x \# M. x < y"
  proof
    fix x
    assume x_in: "x \# M"
    hence M: "M - {#x#} + {#x#} = M"
      by (meson insert_DiffM2)
    hence "\ {#x#} < {#y#} \ x < y"
      using x_in M_lt_y
      by (metis diff_single_eq_union le_multiset_empty_left less_add_same_cancel2 mset_le_trans)
    also have "\ {#y#} < M"
      using M_lt_y mset_le_not_sym by blast
    ultimately show "x < y"
      by (metis (no_types) Max_ge all_lt_Max_imp_lt_mset empty_iff finite_set_mset insertE
        less_le_trans linorder_less_linear mset_le_not_sym set_mset_add_mset_insert
        set_mset_eq_empty_iff x_in)
  qed
next
  assume y_max: "\x \# M. x < y"
  show "M < {#y#}"
    by (rule all_lt_Max_imp_lt_mset) (auto intro!: y_max)
qed

lemma mset_le_single_right_iff[simp]:
  "M \ {#y#} \ M = {#y#} \ (\x \# M. x < y)" for y :: "'a::linorder"
  by (meson less_eq_multiset_def mset_lt_single_right_iff)

subsubsection \<open>Simplifications\<close>

lemma multp\<^sub>H\<^sub>O_repeat_mset_repeat_mset[simp]:
  assumes "n \ 0"
  shows "multp\<^sub>H\<^sub>O R (repeat_mset n A) (repeat_mset n B) \ multp\<^sub>H\<^sub>O R A B"
proof (rule iffI)
  assume hyp: "multp\<^sub>H\<^sub>O R (repeat_mset n A) (repeat_mset n B)"
  hence
    1: "repeat_mset n A \ repeat_mset n B" and
    2: "\y. n * count B y < n * count A y \ (\x. R y x \ n * count A x < n * count B x)"
    by (simp_all add: multp\<^sub>H\<^sub>O_def)

  from 1 \<open>n \<noteq> 0\<close> have "A \<noteq> B"
    by auto

  moreover from 2 \<open>n \<noteq> 0\<close> have "\<forall>y. count B y < count A y \<longrightarrow> (\<exists>x. R y x \<and> count A x < count B x)"
    by auto

  ultimately show "multp\<^sub>H\<^sub>O R A B"
    by (simp add: multp\<^sub>H\<^sub>O_def)
next
  assume "multp\<^sub>H\<^sub>O R A B"
  hence 1: "A \ B" and 2: "\y. count B y < count A y \ (\x. R y x \ count A x < count B x)"
    by (simp_all add: multp\<^sub>H\<^sub>O_def)

  from 1 have "repeat_mset n A \ repeat_mset n B"
    by (simp add: assms repeat_mset_cancel1)

  moreover from 2 have "\y. n * count B y < n * count A y \
    (\<exists>x. R y x \<and> n * count A x < n * count B x)"
    by auto

  ultimately show "multp\<^sub>H\<^sub>O R (repeat_mset n A) (repeat_mset n B)"
    by (simp add: multp\<^sub>H\<^sub>O_def)
qed

lemma multp\<^sub>H\<^sub>O_double_double[simp]: "multp\<^sub>H\<^sub>O R (A + A) (B + B) \<longleftrightarrow> multp\<^sub>H\<^sub>O R A B"
  using multp\<^sub>H\<^sub>O_repeat_mset_repeat_mset[of 2]
  by (simp add: numeral_Bit0)

subsection \<open>Simprocs\<close>

lemma mset_le_add_iff1:
  "j \ (i::nat) \ (repeat_mset i u + m \ repeat_mset j u + n) = (repeat_mset (i-j) u + m \ n)"
proof -
  assume "j \ i"
  then have "j + (i - j) = i"
    using le_add_diff_inverse by blast
  then show ?thesis
    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
qed

lemma mset_le_add_iff2:
  "i \ (j::nat) \ (repeat_mset i u + m \ repeat_mset j u + n) = (m \ repeat_mset (j-i) u + n)"
proof -
  assume "i \ j"
  then have "i + (j - i) = j"
    using le_add_diff_inverse by blast
  then show ?thesis
    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
qed

simproc_setup msetless_cancel
  ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" |
   "add_mset a m < n" | "m < add_mset a n" |
   "replicate_mset p a < n" | "m < replicate_mset p a" |
   "repeat_mset p m < n" | "m < repeat_mset p n") =
  \<open>K Cancel_Simprocs.less_cancel\<close>

simproc_setup msetle_cancel
  ("(l::'a::preorder multiset) + m \ n" | "(l::'a multiset) \ m + n" |
   "add_mset a m \ n" | "m \ add_mset a n" |
   "replicate_mset p a \ n" | "m \ replicate_mset p a" |
   "repeat_mset p m \ n" | "m \ repeat_mset p n") =
  \<open>K Cancel_Simprocs.less_eq_cancel\<close>

subsection \<open>Additional facts and instantiations\<close>

lemma ex_gt_count_imp_le_multiset:
  "(\y :: 'a :: order. y \# M + N \ y \ x) \ count M x < count N x \ M < N"
  unfolding less_multiset\<^sub>H\<^sub>O
  by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)

lemma mset_lt_single_iff[iff]: "{#x#} < {#y#} \ x < y"
  unfolding less_multiset\<^sub>H\<^sub>O by simp

lemma mset_le_single_iff[iff]: "{#x#} \ {#y#} \ x \ y" for x y :: "'a::order"
  unfolding less_eq_multiset\<^sub>H\<^sub>O by force

instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
  by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)

lemma less_eq_multiset_total: "\ M \ N \ N \ M" for M N :: "'a :: linorder multiset"
  by simp

instantiation multiset :: (wellorder) wellorder
begin

lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
  unfolding less_multiset_def multp_def by (auto intro: wf_mult wf)

instance
proof intro_classes
  fix P :: "'a multiset \ bool" and a :: "'a multiset"
  have "wfp ((<) :: 'a \ 'a \ bool)"
    using wfp_on_less .
  hence "wfp ((<) :: 'a multiset \ 'a multiset \ bool)"
    unfolding less_multiset_def by (rule wfp_multp)
  thus "(\x. (\y. y < x \ P y) \ P x) \ P a"
    unfolding wfp_on_def[of UNIV, simplified] by metis
qed

end

instantiation multiset :: (preorder) order_bot
begin

definition bot_multiset :: "'a multiset" where "bot_multiset = {#}"

instance by standard (simp add: bot_multiset_def)

end

instance multiset :: (preorder) no_top
proof standard
  fix x :: "'a multiset"
  obtain a :: 'a where True by simp
  have "x < x + (x + {#a#})"
    by simp
  then show "\y. x < y"
    by blast
qed

instance multiset :: (preorder) ordered_cancel_comm_monoid_add
  by standard

instantiation multiset :: (linorder) distrib_lattice
begin

definition inf_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where
  "inf_multiset A B = (if A < B then A else B)"

definition sup_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where
  "sup_multiset A B = (if B > A then B else A)"

instance
  by intro_classes (auto simp: inf_multiset_def sup_multiset_def)

end

lemma add_mset_lt_left_lt: "a < b \ add_mset a A < add_mset b A"
  by fastforce

lemma add_mset_le_left_le: "a \ b \ add_mset a A \ add_mset b A" for a :: "'a :: linorder"
  by fastforce

lemma add_mset_lt_right_lt: "A < B \ add_mset a A < add_mset a B"
  by fastforce

lemma add_mset_le_right_le: "A \ B \ add_mset a A \ add_mset a B"
  by fastforce

lemma add_mset_lt_lt_lt:
  assumes a_lt_b: "a < b" and A_le_B: "A < B"
  shows "add_mset a A < add_mset b B"
  by (rule less_trans[OF add_mset_lt_left_lt[OF a_lt_b] add_mset_lt_right_lt[OF A_le_B]])

lemma add_mset_lt_lt_le: "a < b \ A \ B \ add_mset a A < add_mset b B"
  using add_mset_lt_lt_lt le_neq_trans by fastforce

lemma add_mset_lt_le_lt: "a \ b \ A < B \ add_mset a A < add_mset b B" for a :: "'a :: linorder"
  using add_mset_lt_lt_lt by (metis add_mset_lt_right_lt le_less)

lemma add_mset_le_le_le:
  fixes a :: "'a :: linorder"
  assumes a_le_b: "a \ b" and A_le_B: "A \ B"
  shows "add_mset a A \ add_mset b B"
  by (rule order.trans[OF add_mset_le_left_le[OF a_le_b] add_mset_le_right_le[OF A_le_B]])

lemma Max_lt_imp_lt_mset:
  assumes n_nemp: "N \ {#}" and max: "Max_mset M < Max_mset N" (is "?max_M < ?max_N")
  shows "M < N"
proof (cases "M = {#}")
  case m_nemp: False

  have max_n_in_n: "?max_N \# N"
    using n_nemp by simp
  have max_n_nin_m: "?max_N \# M"
    using max Max_ge leD by auto

  have "M \ N"
    using max by auto
  moreover
  have "\x > y. count M x < count N x" if "count N y < count M y" for y
  proof -
    from that have "y \# M"
      by (simp add: count_inI)
    then have "?max_M \ y"
      by simp
    then have "?max_N > y"
      using max by auto
    then show ?thesis
      using max_n_nin_m max_n_in_n count_inI by force
  qed
  ultimately show ?thesis
    unfolding less_multiset\<^sub>H\<^sub>O by blast
qed (auto simp: n_nemp)

end

quality99%

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.