src/HOL/Library/Multiset_Order.thy
 author wenzelm Wed Jun 17 17:54:09 2015 +0200 (2015-06-17) changeset 60502 aa58872267ee parent 60495 d7ff0a1df90a parent 60500 903bb1495239 child 60679 ade12ef2773c permissions -rw-r--r--
manual merge;
```     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 default (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: "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
```
```    81 proof (unfold mult_def less_multiset\<^sub>H\<^sub>O_def, induct rule: trancl_induct)
```
```    82   case (base P)
```
```    83   then show ?case unfolding mult1_def by force
```
```    84 next
```
```    85   case (step N P)
```
```    86   from step(2) obtain M0 a K where
```
```    87     *: "P = M0 + {#a#}" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
```
```    88     unfolding mult1_def by blast
```
```    89   then have count_K_a: "count K a = 0" by auto
```
```    90   with step(3) *(1,2) have "M \<noteq> P" by (force dest: *(3) split: if_splits)
```
```    91   moreover
```
```    92   { assume "count P a \<le> count M a"
```
```    93     with count_K_a have "count N a < count M a" unfolding *(1,2) by auto
```
```    94       with step(3) obtain z where z: "z > a" "count M z < count N z" by blast
```
```    95       with * have "count N z \<le> count P z" by force
```
```    96       with z have "\<exists>z > a. count M z < count P z" by auto
```
```    97   } note count_a = this
```
```    98   { fix y
```
```    99     assume count_y: "count P y < count M y"
```
```   100     have "\<exists>x>y. count M x < count P x"
```
```   101     proof (cases "y = a")
```
```   102       case True
```
```   103       with count_y count_a show ?thesis by auto
```
```   104     next
```
```   105       case False
```
```   106       show ?thesis
```
```   107       proof (cases "y \<in># K")
```
```   108         case True
```
```   109         with *(3) have "y < a" by simp
```
```   110         then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
```
```   111       next
```
```   112         case False
```
```   113         with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2) by simp
```
```   114         with count_y step(3) obtain z where z: "z > y" "count M z < count N z" by auto
```
```   115         show ?thesis
```
```   116         proof (cases "z \<in># K")
```
```   117           case True
```
```   118           with *(3) have "z < a" by simp
```
```   119           with z(1) show ?thesis
```
```   120             by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
```
```   121         next
```
```   122           case False
```
```   123           with count_K_a have "count N z \<le> count P z" unfolding * by auto
```
```   124           with z show ?thesis by auto
```
```   125         qed
```
```   126       qed
```
```   127     qed
```
```   128   }
```
```   129   ultimately show ?case by blast
```
```   130 qed
```
```   131
```
```   132 lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
```
```   133   "less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}"
```
```   134 proof -
```
```   135   assume "less_multiset\<^sub>D\<^sub>M M N"
```
```   136   then obtain X Y where
```
```   137     "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)"
```
```   138     unfolding less_multiset\<^sub>D\<^sub>M_def by blast
```
```   139   then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
```
```   140     by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
```
```   141   with \<open>M = N - X + Y\<close> \<open>X \<le># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
```
```   142     by (metis subset_mset.diff_add)
```
```   143 qed
```
```   144
```
```   145 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"
```
```   146 unfolding less_multiset\<^sub>D\<^sub>M_def
```
```   147 proof (intro iffI exI conjI)
```
```   148   assume "less_multiset\<^sub>H\<^sub>O M N"
```
```   149   then obtain z where z: "count M z < count N z"
```
```   150     unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
```
```   151   def X \<equiv> "N - M"
```
```   152   def Y \<equiv> "M - N"
```
```   153   from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
```
```   154   from z show "X \<le># N" unfolding X_def by auto
```
```   155   show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
```
```   156   show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
```
```   157   proof (intro allI impI)
```
```   158     fix k
```
```   159     assume "k \<in># Y"
```
```   160     then have "count N k < count M k" unfolding Y_def by auto
```
```   161     with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a"
```
```   162       unfolding less_multiset\<^sub>H\<^sub>O_def by blast
```
```   163     then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def by auto
```
```   164   qed
```
```   165 qed
```
```   166
```
```   167 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"
```
```   168   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)
```
```   169
```
```   170 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"
```
```   171   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)
```
```   172
```
```   173 lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
```
```   174 lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]
```
```   175
```
```   176 end
```
```   177
```
```   178 context linorder
```
```   179 begin
```
```   180
```
```   181 lemma total_le: "total {(a \<Colon> 'a, b). a \<le> b}"
```
```   182   unfolding total_on_def by auto
```
```   183
```
```   184 lemma total_less: "total {(a \<Colon> 'a, b). a < b}"
```
```   185   unfolding total_on_def by auto
```
```   186
```
```   187 lemma linorder_mult: "class.linorder
```
```   188   (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
```
```   189   (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
```
```   190 proof -
```
```   191   interpret o: order
```
```   192     "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)"
```
```   193     "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
```
```   194     by (rule order_mult)
```
```   195   show ?thesis by unfold_locales (auto 0 3 simp: mult\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
```
```   196 qed
```
```   197
```
```   198 end
```
```   199
```
```   200 lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
```
```   201   "M #\<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
```
```   202   unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
```
```   203
```
```   204 lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
```
```   205 lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
```
```   206
```
```   207 lemma le_multiset\<^sub>H\<^sub>O:
```
```   208   fixes M N :: "('a \<Colon> linorder) multiset"
```
```   209   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))"
```
```   210   by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
```
```   211
```
```   212 lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M #\<subset># N}"
```
```   213   unfolding less_multiset_def by (auto intro: wf_mult wf)
```
```   214
```
```   215 lemma order_multiset: "class.order
```
```   216   (le_multiset :: ('a \<Colon> order) multiset \<Rightarrow> ('a \<Colon> order) multiset \<Rightarrow> bool)
```
```   217   (less_multiset :: ('a \<Colon> order) multiset \<Rightarrow> ('a \<Colon> order) multiset \<Rightarrow> bool)"
```
```   218   by unfold_locales
```
```   219
```
```   220 lemma linorder_multiset: "class.linorder
```
```   221   (le_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool)
```
```   222   (less_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool)"
```
```   223   by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O le_multiset_def not_less_iff_gr_or_eq)
```
```   224
```
```   225 interpretation multiset_linorder: linorder
```
```   226   "le_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool"
```
```   227   "less_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool"
```
```   228   by (rule linorder_multiset)
```
```   229
```
```   230 interpretation multiset_wellorder: wellorder
```
```   231   "le_multiset :: ('a \<Colon> wellorder) multiset \<Rightarrow> ('a \<Colon> wellorder) multiset \<Rightarrow> bool"
```
```   232   "less_multiset :: ('a \<Colon> wellorder) multiset \<Rightarrow> ('a \<Colon> wellorder) multiset \<Rightarrow> bool"
```
```   233   by unfold_locales (blast intro: wf_less_multiset[unfolded wf_def, rule_format])
```
```   234
```
```   235 lemma le_multiset_total:
```
```   236   fixes M N :: "('a \<Colon> linorder) multiset"
```
```   237   shows "\<not> M #\<subseteq># N \<Longrightarrow> N #\<subseteq># M"
```
```   238   by (metis multiset_linorder.le_cases)
```
```   239
```
```   240 lemma less_eq_imp_le_multiset:
```
```   241   fixes M N :: "('a \<Colon> linorder) multiset"
```
```   242   shows "M \<le># N \<Longrightarrow> M #\<subseteq># N"
```
```   243   unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
```
```   244   by (simp add: less_le_not_le subseteq_mset_def)
```
```   245
```
```   246 lemma less_multiset_right_total:
```
```   247   fixes M :: "('a \<Colon> linorder) multiset"
```
```   248   shows "M #\<subset># M + {#undefined#}"
```
```   249   unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
```
```   250
```
```   251 lemma le_multiset_empty_left[simp]:
```
```   252   fixes M :: "('a \<Colon> linorder) multiset"
```
```   253   shows "{#} #\<subseteq># M"
```
```   254   by (simp add: less_eq_imp_le_multiset)
```
```   255
```
```   256 lemma le_multiset_empty_right[simp]:
```
```   257   fixes M :: "('a \<Colon> linorder) multiset"
```
```   258   shows "M \<noteq> {#} \<Longrightarrow> \<not> M #\<subseteq># {#}"
```
```   259   by (metis le_multiset_empty_left multiset_order.antisym)
```
```   260
```
```   261 lemma less_multiset_empty_left[simp]:
```
```   262   fixes M :: "('a \<Colon> linorder) multiset"
```
```   263   shows "M \<noteq> {#} \<Longrightarrow> {#} #\<subset># M"
```
```   264   by (simp add: less_multiset\<^sub>H\<^sub>O)
```
```   265
```
```   266 lemma less_multiset_empty_right[simp]:
```
```   267   fixes M :: "('a \<Colon> linorder) multiset"
```
```   268   shows "\<not> M #\<subset># {#}"
```
```   269   using le_empty less_multiset\<^sub>D\<^sub>M by blast
```
```   270
```
```   271 lemma
```
```   272   fixes M N :: "('a \<Colon> linorder) multiset"
```
```   273   shows
```
```   274     le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and
```
```   275     le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)"
```
```   276   using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+
```
```   277
```
```   278 lemma
```
```   279   fixes M N :: "('a \<Colon> linorder) multiset"
```
```   280   shows
```
```   281     less_multiset_plus_plus_left_iff[simp]: "M + N #\<subset># M' + N \<longleftrightarrow> M #\<subset># M'" and
```
```   282     less_multiset_plus_plus_right_iff[simp]: "M + N #\<subset># M + N' \<longleftrightarrow> N #\<subset># N'"
```
```   283   unfolding less_multiset\<^sub>H\<^sub>O by auto
```
```   284
```
```   285 lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
```
```   286   by (metis add.commute add_diff_cancel_right' monoid_add_class.add.left_neutral)
```
```   287
```
```   288 lemma
```
```   289   fixes M N :: "('a \<Colon> linorder) multiset"
```
```   290   shows
```
```   291     less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N #\<subset># M + N" and
```
```   292     less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M #\<subset># M + N"
```
```   293   using [[metis_verbose = false]]
```
```   294   by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
```
```   295     add.commute)+
```
```   296
```
```   297 lemma ex_gt_imp_less_multiset: "(\<exists>y \<Colon> 'a \<Colon> linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M #\<subset># N"
```
```   298   unfolding less_multiset\<^sub>H\<^sub>O by (metis less_irrefl less_nat_zero_code not_gr0)
```
```   299
```
```   300 lemma ex_gt_count_imp_less_multiset:
```
```   301   "(\<forall>y \<Colon> 'a \<Colon> linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N"
```
```   302   unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order
```
```   303     less_not_sym mset_leD mset_le_add_left)
```
```   304
```
```   305 lemma union_less_diff_plus: "P \<le># M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
```
```   306   by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2)
```
```   307
```
```   308 end
```