src/HOL/Library/Multiset_Order.thy
author wenzelm
Mon Apr 25 16:09:26 2016 +0200 (2016-04-25)
changeset 63040 eb4ddd18d635
parent 62430 9527ff088c15
child 63310 caaacf37943f
permissions -rw-r--r--
eliminated old 'def';
tuned comments;
     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 subsubsection \<open>Alternative characterizations\<close>
    13 
    14 context order
    15 begin
    16 
    17 lemma reflp_le: "reflp (op \<le>)"
    18   unfolding reflp_def by simp
    19 
    20 lemma antisymP_le: "antisymP (op \<le>)"
    21   unfolding antisym_def by auto
    22 
    23 lemma transp_le: "transp (op \<le>)"
    24   unfolding transp_def by auto
    25 
    26 lemma irreflp_less: "irreflp (op <)"
    27   unfolding irreflp_def by simp
    28 
    29 lemma antisymP_less: "antisymP (op <)"
    30   unfolding antisym_def by auto
    31 
    32 lemma transp_less: "transp (op <)"
    33   unfolding transp_def by auto
    34 
    35 lemmas le_trans = transp_le[unfolded transp_def, rule_format]
    36 
    37 lemma order_mult: "class.order
    38   (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
    39   (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
    40   (is "class.order ?le ?less")
    41 proof -
    42   have irrefl: "\<And>M :: 'a multiset. \<not> ?less M M"
    43   proof
    44     fix M :: "'a multiset"
    45     have "trans {(x'::'a, x). x' < x}"
    46       by (rule transI) simp
    47     moreover
    48     assume "(M, M) \<in> mult {(x, y). x < y}"
    49     ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
    50       \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
    51       by (rule mult_implies_one_step)
    52     then obtain I J K where "M = I + J" and "M = I + K"
    53       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
    54     then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
    55     have "finite (set_mset K)" by simp
    56     moreover note aux2
    57     ultimately have "set_mset K = {}"
    58       by (induct rule: finite_induct)
    59        (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
    60     with aux1 show False by simp
    61   qed
    62   have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
    63     unfolding mult_def by (blast intro: trancl_trans)
    64   show "class.order ?le ?less"
    65     by standard (auto simp add: le_multiset_def irrefl dest: trans)
    66 qed
    67 
    68 text \<open>The Dershowitz--Manna ordering:\<close>
    69 
    70 definition less_multiset\<^sub>D\<^sub>M where
    71   "less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
    72    (\<exists>X Y. X \<noteq> {#} \<and> X \<le># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
    73 
    74 
    75 text \<open>The Huet--Oppen ordering:\<close>
    76 
    77 definition less_multiset\<^sub>H\<^sub>O where
    78   "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))"
    79 
    80 lemma mult_imp_less_multiset\<^sub>H\<^sub>O:
    81   "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
    82 proof (unfold mult_def, induct rule: trancl_induct)
    83   case (base P)
    84   then show ?case
    85     by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^sub>H\<^sub>O_def split: if_splits dest!: Suc_lessD)
    86 next
    87   case (step N P)
    88   from step(3) have "M \<noteq> N" and
    89     **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
    90     by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
    91   from step(2) obtain M0 a K where
    92     *: "P = M0 + {#a#}" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
    93     by (blast elim: mult1_lessE)
    94   from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) split: if_splits)
    95   moreover
    96   { assume "count P a \<le> count M a"
    97     with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
    98       by (auto simp add: not_in_iff)
    99       with ** obtain z where z: "z > a" "count M z < count N z"
   100         by blast
   101       with * have "count N z \<le> count P z" 
   102         by (force simp add: not_in_iff)
   103       with z have "\<exists>z > a. count M z < count P z" by auto
   104   } note count_a = this
   105   { fix y
   106     assume count_y: "count P y < count M y"
   107     have "\<exists>x>y. count M x < count P x"
   108     proof (cases "y = a")
   109       case True
   110       with count_y count_a show ?thesis by auto
   111     next
   112       case False
   113       show ?thesis
   114       proof (cases "y \<in># K")
   115         case True
   116         with *(4) have "y < a" by simp
   117         then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
   118       next
   119         case False
   120         with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
   121           by (simp add: not_in_iff)
   122         with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto
   123         show ?thesis
   124         proof (cases "z \<in># K")
   125           case True
   126           with *(4) have "z < a" by simp
   127           with z(1) show ?thesis
   128             by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
   129         next
   130           case False
   131           with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
   132             by (auto simp add: not_in_iff)
   133           with z show ?thesis by auto
   134         qed
   135       qed
   136     qed
   137   }
   138   ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast
   139 qed
   140 
   141 lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
   142   "less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}"
   143 proof -
   144   assume "less_multiset\<^sub>D\<^sub>M M N"
   145   then obtain X Y where
   146     "X \<noteq> {#}" and "X \<le># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
   147     unfolding less_multiset\<^sub>D\<^sub>M_def by blast
   148   then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
   149     by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
   150   with \<open>M = N - X + Y\<close> \<open>X \<le># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
   151     by (metis subset_mset.diff_add)
   152 qed
   153 
   154 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"
   155 unfolding less_multiset\<^sub>D\<^sub>M_def
   156 proof (intro iffI exI conjI)
   157   assume "less_multiset\<^sub>H\<^sub>O M N"
   158   then obtain z where z: "count M z < count N z"
   159     unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
   160   define X where "X = N - M"
   161   define Y where "Y = M - N"
   162   from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
   163   from z show "X \<le># N" unfolding X_def by auto
   164   show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
   165   show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
   166   proof (intro allI impI)
   167     fix k
   168     assume "k \<in># Y"
   169     then have "count N k < count M k" unfolding Y_def
   170       by (auto simp add: in_diff_count)
   171     with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a"
   172       unfolding less_multiset\<^sub>H\<^sub>O_def by blast
   173     then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def
   174       by (auto simp add: in_diff_count)
   175   qed
   176 qed
   177 
   178 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"
   179   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)
   180 
   181 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"
   182   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)
   183 
   184 lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
   185 lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]
   186 
   187 end
   188 
   189 context linorder
   190 begin
   191 
   192 lemma total_le: "total {(a :: 'a, b). a \<le> b}"
   193   unfolding total_on_def by auto
   194 
   195 lemma total_less: "total {(a :: 'a, b). a < b}"
   196   unfolding total_on_def by auto
   197 
   198 lemma linorder_mult: "class.linorder
   199   (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
   200   (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
   201 proof -
   202   interpret o: order
   203     "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)"
   204     "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
   205     by (rule order_mult)
   206   show ?thesis by unfold_locales (auto 0 3 simp: mult\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
   207 qed
   208 
   209 end
   210 
   211 lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
   212   "M #\<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
   213   unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
   214 
   215 lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
   216 lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
   217 
   218 lemma le_multiset\<^sub>H\<^sub>O:
   219   fixes M N :: "('a :: linorder) multiset"
   220   shows "M #\<subseteq># N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
   221   by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
   222 
   223 lemma wf_less_multiset: "wf {(M :: ('a :: wellorder) multiset, N). M #\<subset># N}"
   224   unfolding less_multiset_def by (auto intro: wf_mult wf)
   225 
   226 lemma order_multiset: "class.order
   227   (le_multiset :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)
   228   (less_multiset :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)"
   229   by unfold_locales
   230 
   231 lemma linorder_multiset: "class.linorder
   232   (le_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)
   233   (less_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)"
   234   by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O le_multiset_def not_less_iff_gr_or_eq)
   235 
   236 interpretation multiset_linorder: linorder
   237   "le_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
   238   "less_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
   239   by (rule linorder_multiset)
   240 
   241 interpretation multiset_wellorder: wellorder
   242   "le_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
   243   "less_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
   244   by unfold_locales (blast intro: wf_less_multiset [unfolded wf_def, simplified, rule_format])
   245 
   246 lemma le_multiset_total:
   247   fixes M N :: "('a :: linorder) multiset"
   248   shows "\<not> M #\<subseteq># N \<Longrightarrow> N #\<subseteq># M"
   249   by (metis multiset_linorder.le_cases)
   250 
   251 lemma less_eq_imp_le_multiset:
   252   fixes M N :: "('a :: linorder) multiset"
   253   shows "M \<le># N \<Longrightarrow> M #\<subseteq># N"
   254   unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
   255   by (simp add: less_le_not_le subseteq_mset_def)
   256 
   257 lemma less_multiset_right_total:
   258   fixes M :: "('a :: linorder) multiset"
   259   shows "M #\<subset># M + {#undefined#}"
   260   unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
   261 
   262 lemma le_multiset_empty_left[simp]:
   263   fixes M :: "('a :: linorder) multiset"
   264   shows "{#} #\<subseteq># M"
   265   by (simp add: less_eq_imp_le_multiset)
   266 
   267 lemma le_multiset_empty_right[simp]:
   268   fixes M :: "('a :: linorder) multiset"
   269   shows "M \<noteq> {#} \<Longrightarrow> \<not> M #\<subseteq># {#}"
   270   by (metis le_multiset_empty_left multiset_order.antisym)
   271 
   272 lemma less_multiset_empty_left[simp]:
   273   fixes M :: "('a :: linorder) multiset"
   274   shows "M \<noteq> {#} \<Longrightarrow> {#} #\<subset># M"
   275   by (simp add: less_multiset\<^sub>H\<^sub>O)
   276 
   277 lemma less_multiset_empty_right[simp]:
   278   fixes M :: "('a :: linorder) multiset"
   279   shows "\<not> M #\<subset># {#}"
   280   using le_empty less_multiset\<^sub>D\<^sub>M by blast
   281 
   282 lemma
   283   fixes M N :: "('a :: linorder) multiset"
   284   shows
   285     le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and
   286     le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)"
   287   using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+
   288 
   289 lemma
   290   fixes M N :: "('a :: linorder) multiset"
   291   shows
   292     less_multiset_plus_plus_left_iff[simp]: "M + N #\<subset># M' + N \<longleftrightarrow> M #\<subset># M'" and
   293     less_multiset_plus_plus_right_iff[simp]: "M + N #\<subset># M + N' \<longleftrightarrow> N #\<subset># N'"
   294   unfolding less_multiset\<^sub>H\<^sub>O by auto
   295 
   296 lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
   297   by (metis add.commute add_diff_cancel_right' monoid_add_class.add.left_neutral)
   298 
   299 lemma
   300   fixes M N :: "('a :: linorder) multiset"
   301   shows
   302     less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N #\<subset># M + N" and
   303     less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M #\<subset># M + N"
   304   using [[metis_verbose = false]]
   305   by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
   306     add.commute)+
   307 
   308 lemma ex_gt_imp_less_multiset: "(\<exists>y :: 'a :: linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M #\<subset># N"
   309   unfolding less_multiset\<^sub>H\<^sub>O
   310   by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
   311   
   312 lemma ex_gt_count_imp_less_multiset:
   313   "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N"
   314   unfolding less_multiset\<^sub>H\<^sub>O
   315   by (metis add_gr_0 count_union mem_Collect_eq not_gr0 not_le not_less_iff_gr_or_eq set_mset_def)
   316 
   317 lemma union_less_diff_plus: "P \<le># M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
   318   by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2)
   319 
   320 end