src/HOL/Library/Multiset_Order.thy
author fleury <Mathias.Fleury@mpi-inf.mpg.de>
Thu Feb 16 13:54:22 2017 +0100 (2017-02-16)
changeset 65031 52e2c99f3711
parent 65028 87e003397834
child 65546 7c58f69451b0
permissions -rw-r--r--
use the cancellation simprocs directly
     1 (*  Title:      HOL/Library/Multiset_Order.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, Inria, LORIA, MPII
     4 *)
     5 
     6 section \<open>More Theorems about the Multiset Order\<close>
     7 
     8 theory Multiset_Order
     9 imports Multiset
    10 begin
    11 
    12 subsection \<open>Alternative characterizations\<close>
    13 
    14 context preorder
    15 begin
    16 
    17 lemma order_mult: "class.order
    18   (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
    19   (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
    20   (is "class.order ?le ?less")
    21 proof -
    22   have irrefl: "\<And>M :: 'a multiset. \<not> ?less M M"
    23   proof
    24     fix M :: "'a multiset"
    25     have "trans {(x'::'a, x). x' < x}"
    26       by (rule transI) (blast intro: less_trans)
    27     moreover
    28     assume "(M, M) \<in> mult {(x, y). x < y}"
    29     ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
    30       \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
    31       by (rule mult_implies_one_step)
    32     then obtain I J K where "M = I + J" and "M = I + K"
    33       and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
    34     then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
    35     have "finite (set_mset K)" by simp
    36     moreover note aux2
    37     ultimately have "set_mset K = {}"
    38       by (induct rule: finite_induct)
    39        (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
    40     with aux1 show False by simp
    41   qed
    42   have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
    43     unfolding mult_def by (blast intro: trancl_trans)
    44   show "class.order ?le ?less"
    45     by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
    46 qed
    47 
    48 text \<open>The Dershowitz--Manna ordering:\<close>
    49 
    50 definition less_multiset\<^sub>D\<^sub>M where
    51   "less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
    52    (\<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)))"
    53 
    54 
    55 text \<open>The Huet--Oppen ordering:\<close>
    56 
    57 definition less_multiset\<^sub>H\<^sub>O where
    58   "less_multiset\<^sub>H\<^sub>O M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
    59 
    60 lemma mult_imp_less_multiset\<^sub>H\<^sub>O:
    61   "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
    62 proof (unfold mult_def, induct rule: trancl_induct)
    63   case (base P)
    64   then show ?case
    65     by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^sub>H\<^sub>O_def split: if_splits dest!: Suc_lessD)
    66 next
    67   case (step N P)
    68   from step(3) have "M \<noteq> N" and
    69     **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
    70     by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
    71   from step(2) obtain M0 a K where
    72     *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
    73     by (blast elim: mult1_lessE)
    74   from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
    75   moreover
    76   { assume "count P a \<le> count M a"
    77     with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
    78       by (auto simp add: not_in_iff)
    79       with ** obtain z where z: "z > a" "count M z < count N z"
    80         by blast
    81       with * have "count N z \<le> count P z" 
    82         by (auto elim: less_asym intro: count_inI)
    83       with z have "\<exists>z > a. count M z < count P z" by auto
    84   } note count_a = this
    85   { fix y
    86     assume count_y: "count P y < count M y"
    87     have "\<exists>x>y. count M x < count P x"
    88     proof (cases "y = a")
    89       case True
    90       with count_y count_a show ?thesis by auto
    91     next
    92       case False
    93       show ?thesis
    94       proof (cases "y \<in># K")
    95         case True
    96         with *(4) have "y < a" by simp
    97         then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
    98       next
    99         case False
   100         with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
   101           by (simp add: not_in_iff)
   102         with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto
   103         show ?thesis
   104         proof (cases "z \<in># K")
   105           case True
   106           with *(4) have "z < a" by simp
   107           with z(1) show ?thesis
   108             by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
   109         next
   110           case False
   111           with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
   112             by (auto simp add: not_in_iff)
   113           with z show ?thesis by auto
   114         qed
   115       qed
   116     qed
   117   }
   118   ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast
   119 qed
   120 
   121 lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
   122   "less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}"
   123 proof -
   124   assume "less_multiset\<^sub>D\<^sub>M M N"
   125   then obtain X Y where
   126     "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)"
   127     unfolding less_multiset\<^sub>D\<^sub>M_def by blast
   128   then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
   129     by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
   130   with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
   131     by (metis subset_mset.diff_add)
   132 qed
   133 
   134 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"
   135 unfolding less_multiset\<^sub>D\<^sub>M_def
   136 proof (intro iffI exI conjI)
   137   assume "less_multiset\<^sub>H\<^sub>O M N"
   138   then obtain z where z: "count M z < count N z"
   139     unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
   140   define X where "X = N - M"
   141   define Y where "Y = M - N"
   142   from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
   143   from z show "X \<subseteq># N" unfolding X_def by auto
   144   show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
   145   show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
   146   proof (intro allI impI)
   147     fix k
   148     assume "k \<in># Y"
   149     then have "count N k < count M k" unfolding Y_def
   150       by (auto simp add: in_diff_count)
   151     with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a"
   152       unfolding less_multiset\<^sub>H\<^sub>O_def by blast
   153     then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def
   154       by (auto simp add: in_diff_count)
   155   qed
   156 qed
   157 
   158 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"
   159   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)
   160 
   161 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"
   162   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)
   163 
   164 lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
   165 lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]
   166 
   167 end
   168 
   169 lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
   170   "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
   171   unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
   172 
   173 lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
   174 lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
   175 
   176 lemma subset_eq_imp_le_multiset:
   177   shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
   178   unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
   179   by (simp add: less_le_not_le subseteq_mset_def)
   180 
   181 lemma le_multiset_right_total:
   182   shows "M < add_mset x M"
   183   unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
   184 
   185 lemma less_eq_multiset_empty_left[simp]:
   186   shows "{#} \<le> M"
   187   by (simp add: subset_eq_imp_le_multiset)
   188 
   189 lemma ex_gt_imp_less_multiset: "(\<exists>y. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
   190   unfolding less_multiset\<^sub>H\<^sub>O
   191   by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
   192 
   193 lemma less_eq_multiset_empty_right[simp]:
   194   "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
   195   by (metis less_eq_multiset_empty_left antisym)
   196 
   197 lemma le_multiset_empty_left[simp]: "M \<noteq> {#} \<Longrightarrow> {#} < M"
   198   by (simp add: less_multiset\<^sub>H\<^sub>O)
   199 
   200 lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
   201   using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
   202 
   203 lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
   204   by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
   205 
   206 instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le
   207 begin
   208 
   209 lemma less_eq_multiset\<^sub>H\<^sub>O:
   210   "M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
   211   by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
   212 
   213 instance by standard (auto simp: less_eq_multiset\<^sub>H\<^sub>O)
   214 
   215 lemma
   216   fixes M N :: "'a multiset"
   217   shows
   218     less_eq_multiset_plus_left: "N \<le> (M + N)" and
   219     less_eq_multiset_plus_right: "M \<le> (M + N)"
   220   by simp_all
   221 
   222 lemma
   223   fixes M N :: "'a multiset"
   224   shows
   225     le_multiset_plus_left_nonempty: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
   226     le_multiset_plus_right_nonempty: "N \<noteq> {#} \<Longrightarrow> M < M + N"
   227     by simp_all
   228 
   229 end
   230 
   231 
   232 subsection \<open>Simprocs\<close>
   233 
   234 lemma mset_le_add_iff1:
   235   "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i-j) u + m \<le> n)"
   236 proof -
   237   assume "j \<le> i"
   238   then have "j + (i - j) = i"
   239     using le_add_diff_inverse by blast
   240   then show ?thesis
   241     by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
   242 qed
   243 
   244 lemma mset_le_add_iff2:
   245   "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j-i) u + n)"
   246 proof -
   247   assume "i \<le> j"
   248   then have "i + (j - i) = j"
   249     using le_add_diff_inverse by blast
   250   then show ?thesis
   251     by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
   252 qed
   253 
   254 simproc_setup msetless_cancel
   255   ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" |
   256    "add_mset a m < n" | "m < add_mset a n" |
   257    "replicate_mset p a < n" | "m < replicate_mset p a" |
   258    "repeat_mset p m < n" | "m < repeat_mset p n") =
   259   \<open>fn phi => Cancel_Simprocs.less_cancel\<close>
   260 
   261 simproc_setup msetle_cancel
   262   ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
   263    "add_mset a m \<le> n" | "m \<le> add_mset a n" |
   264    "replicate_mset p a \<le> n" | "m \<le> replicate_mset p a" |
   265    "repeat_mset p m \<le> n" | "m \<le> repeat_mset p n") =
   266   \<open>fn phi => Cancel_Simprocs.less_eq_cancel\<close>
   267 
   268 
   269 subsection \<open>Additional facts and instantiations\<close>
   270 
   271 lemma ex_gt_count_imp_le_multiset:
   272   "(\<forall>y :: 'a :: order. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
   273   unfolding less_multiset\<^sub>H\<^sub>O
   274   by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)
   275 
   276 lemma mset_lt_single_iff[iff]: "{#x#} < {#y#} \<longleftrightarrow> x < y"
   277   unfolding less_multiset\<^sub>H\<^sub>O by simp
   278 
   279 lemma mset_le_single_iff[iff]: "{#x#} \<le> {#y#} \<longleftrightarrow> x \<le> y" for x y :: "'a::order"
   280   unfolding less_eq_multiset\<^sub>H\<^sub>O by force
   281 
   282 
   283 instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
   284   by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
   285 
   286 lemma less_eq_multiset_total:
   287   fixes M N :: "'a :: linorder multiset"
   288   shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
   289   by simp
   290 
   291 instantiation multiset :: (wellorder) wellorder
   292 begin
   293 
   294 lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
   295   unfolding less_multiset_def by (auto intro: wf_mult wf)
   296 
   297 instance by standard (metis less_multiset_def wf wf_def wf_mult)
   298 
   299 end
   300 
   301 instantiation multiset :: (preorder) order_bot
   302 begin
   303 
   304 definition bot_multiset :: "'a multiset" where "bot_multiset = {#}"
   305 
   306 instance by standard (simp add: bot_multiset_def)
   307 
   308 end
   309 
   310 instance multiset :: (preorder) no_top
   311 proof standard
   312   fix x :: "'a multiset"
   313   obtain a :: 'a where True by simp
   314   have "x < x + (x + {#a#})"
   315     by simp
   316   then show "\<exists>y. x < y"
   317     by blast
   318 qed
   319 
   320 instance multiset :: (preorder) ordered_cancel_comm_monoid_add
   321   by standard
   322 
   323 end