Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Multiset_Order.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Multiset_Order.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
*)

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

theory Multiset_Order
imports Multiset
begin

subsection \<open>Alternative Characterizations\<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"
proof (unfold mult_def, induct rule: trancl_induct)
  case (base P)
  then show ?case
    by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^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>y. count M x < count N x)"
    by (simp_all add: less_multiset\<^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 \ b < a"
    by (blast elim: mult1_lessE)
  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
  moreover
  { assume "count P a \ count M a"
    with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
      by (auto simp add: not_in_iff)
      with ** obtain z where z: "z > a" "count M z < count N z"
        by blast
      with * have "count N z \ count P z"
        by (auto elim: less_asym intro: count_inI)
      with z have "\z > a. count M z < count P z" by auto
  } note count_a = this
  { fix y
    assume count_y: "count P y < count M y"
    have "\x>y. count M x < count P x"
    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 "y < a" by simp
        then show ?thesis by (cases "count P a \ count M a") (auto dest: count_a intro: less_trans)
      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: "z > y" "count M z < count N z" by auto
        show ?thesis
        proof (cases "z \# K")
          case True
          with *(4) have "z < a" by simp
          with z(1) show ?thesis
            by (cases "count P a \ count M a") (auto dest!: count_a intro: less_trans)
        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 less_multiset\<^sub>H\<^sub>O_def by blast
qed

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

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
proof (intro iffI exI conjI)
  assume "less_multiset\<^sub>H\<^sub>O M N"
  then obtain z where z: "count M z < count N z"
    unfolding less_multiset\<^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 \ 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>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a"
      unfolding less_multiset\<^sub>H\<^sub>O_def by blast
    then show "\a. a \# X \ k < a" unfolding X_def
      by (auto simp add: in_diff_count)
  qed
qed

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"
  by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)

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"
  by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)

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 mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..

lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded 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]:
  shows "{#} \ 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\<^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 moura

    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)

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>fn phi => 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>fn phi => 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:
  fixes M N :: "'a :: linorder multiset"
  shows "\ M \ N \ N \ M"
  by simp

instantiation multiset :: (wellorder) wellorder
begin

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

instance by standard (metis less_multiset_def wf wf_def wf_mult)

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

end

¤ Dauer der Verarbeitung: 0.6 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.