more instantiations for multiset
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Thu Jul 07 17:34:39 2016 +0200 (2016-07-07)
changeset 634109789ccc2a477
parent 63409 3f3223b90239
child 63412 def97df48390
more instantiations for multiset
NEWS
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
src/HOL/UNITY/Comp/AllocBase.thy
     1.1 --- a/NEWS	Thu Jul 07 09:24:03 2016 +0200
     1.2 +++ b/NEWS	Thu Jul 07 17:34:39 2016 +0200
     1.3 @@ -350,6 +350,16 @@
     1.4      less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Some typeclass constraints about multisets have been reduced from ordered or
     1.8 +linordered to preorder. Multisets have the additional typeclasses order_bot,
     1.9 +no_top, ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
    1.10 +and linordered_cancel_ab_semigroup_add.
    1.11 +INCOMPATIBILITY.
    1.12 +
    1.13 +* There are some new simplification rules about multisets and the multiset
    1.14 +ordering.
    1.15 +INCOMPATIBILITY.
    1.16 +
    1.17  * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
    1.18  INCOMPATIBILITY.
    1.19  
     2.1 --- a/src/HOL/Library/Multiset.thy	Thu Jul 07 09:24:03 2016 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Thu Jul 07 17:34:39 2016 +0200
     2.3 @@ -2488,7 +2488,7 @@
     2.4  
     2.5  subsubsection \<open>Partial-order properties\<close>
     2.6  
     2.7 -lemma (in order) mult1_lessE:
     2.8 +lemma (in preorder) mult1_lessE:
     2.9    assumes "(N, M) \<in> mult1 {(a, b). a < b}"
    2.10    obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K"
    2.11      "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
    2.12 @@ -2499,7 +2499,7 @@
    2.13    ultimately show thesis by (auto intro: that)
    2.14  qed
    2.15  
    2.16 -instantiation multiset :: (order) order
    2.17 +instantiation multiset :: (preorder) order
    2.18  begin
    2.19  
    2.20  definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
    2.21 @@ -2515,7 +2515,7 @@
    2.22      assume "M < M"
    2.23      then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
    2.24      have "trans {(x'::'a, x). x' < x}"
    2.25 -      by (rule transI) simp
    2.26 +      by (metis (mono_tags, lifting) case_prodD case_prodI less_trans mem_Collect_eq transI)
    2.27      moreover note MM
    2.28      ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
    2.29        \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
    2.30 @@ -2537,7 +2537,7 @@
    2.31  end \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
    2.32  
    2.33  lemma mset_le_irrefl [elim!]:
    2.34 -  fixes M :: "'a::order multiset"
    2.35 +  fixes M :: "'a::preorder multiset"
    2.36    shows "M < M \<Longrightarrow> R"
    2.37    by simp
    2.38  
    2.39 @@ -2552,25 +2552,25 @@
    2.40  apply (simp add: add.assoc)
    2.41  done
    2.42  
    2.43 -lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::order multiset)"
    2.44 +lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
    2.45  apply (unfold less_multiset_def mult_def)
    2.46  apply (erule trancl_induct)
    2.47   apply (blast intro: mult1_union)
    2.48  apply (blast intro: mult1_union trancl_trans)
    2.49  done
    2.50  
    2.51 -lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::order multiset)"
    2.52 +lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::preorder multiset)"
    2.53  apply (subst add.commute [of B C])
    2.54  apply (subst add.commute [of D C])
    2.55  apply (erule union_le_mono2)
    2.56  done
    2.57  
    2.58  lemma union_less_mono:
    2.59 -  fixes A B C D :: "'a::order multiset"
    2.60 +  fixes A B C D :: "'a::preorder multiset"
    2.61    shows "A < C \<Longrightarrow> B < D \<Longrightarrow> A + B < C + D"
    2.62    by (blast intro!: union_le_mono1 union_le_mono2 less_trans)
    2.63  
    2.64 -instantiation multiset :: (order) ordered_ab_semigroup_add
    2.65 +instantiation multiset :: (preorder) ordered_ab_semigroup_add
    2.66  begin
    2.67  instance
    2.68    by standard (auto simp add: less_eq_multiset_def intro: union_le_mono2)
    2.69 @@ -2769,16 +2769,16 @@
    2.70    multiset_inter_assoc
    2.71    multiset_inter_left_commute
    2.72  
    2.73 -lemma mset_le_not_refl: "\<not> M < (M::'a::order multiset)"
    2.74 +lemma mset_le_not_refl: "\<not> M < (M::'a::preorder multiset)"
    2.75    by (fact less_irrefl)
    2.76  
    2.77 -lemma mset_le_trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < (N::'a::order multiset)"
    2.78 +lemma mset_le_trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < (N::'a::preorder multiset)"
    2.79    by (fact less_trans)
    2.80  
    2.81 -lemma mset_le_not_sym: "M < N \<Longrightarrow> \<not> N < (M::'a::order multiset)"
    2.82 +lemma mset_le_not_sym: "M < N \<Longrightarrow> \<not> N < (M::'a::preorder multiset)"
    2.83    by (fact less_not_sym)
    2.84  
    2.85 -lemma mset_le_asym: "M < N \<Longrightarrow> (\<not> P \<Longrightarrow> N < (M::'a::order multiset)) \<Longrightarrow> P"
    2.86 +lemma mset_le_asym: "M < N \<Longrightarrow> (\<not> P \<Longrightarrow> N < (M::'a::preorder multiset)) \<Longrightarrow> P"
    2.87    by (fact less_asym)
    2.88  
    2.89  declaration \<open>
     3.1 --- a/src/HOL/Library/Multiset_Order.thy	Thu Jul 07 09:24:03 2016 +0200
     3.2 +++ b/src/HOL/Library/Multiset_Order.thy	Thu Jul 07 17:34:39 2016 +0200
     3.3 @@ -11,29 +11,9 @@
     3.4  
     3.5  subsection \<open>Alternative characterizations\<close>
     3.6  
     3.7 -context order
     3.8 +context preorder
     3.9  begin
    3.10  
    3.11 -lemma reflp_le: "reflp (op \<le>)"
    3.12 -  unfolding reflp_def by simp
    3.13 -
    3.14 -lemma antisymP_le: "antisymP (op \<le>)"
    3.15 -  unfolding antisym_def by auto
    3.16 -
    3.17 -lemma transp_le: "transp (op \<le>)"
    3.18 -  unfolding transp_def by auto
    3.19 -
    3.20 -lemma irreflp_less: "irreflp (op <)"
    3.21 -  unfolding irreflp_def by simp
    3.22 -
    3.23 -lemma antisymP_less: "antisymP (op <)"
    3.24 -  unfolding antisym_def by auto
    3.25 -
    3.26 -lemma transp_less: "transp (op <)"
    3.27 -  unfolding transp_def by auto
    3.28 -
    3.29 -lemmas le_trans = transp_le[unfolded transp_def, rule_format]
    3.30 -
    3.31  lemma order_mult: "class.order
    3.32    (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
    3.33    (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
    3.34 @@ -43,7 +23,7 @@
    3.35    proof
    3.36      fix M :: "'a multiset"
    3.37      have "trans {(x'::'a, x). x' < x}"
    3.38 -      by (rule transI) simp
    3.39 +      by (rule transI) (blast intro: less_trans)
    3.40      moreover
    3.41      assume "(M, M) \<in> mult {(x, y). x < y}"
    3.42      ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
    3.43 @@ -91,7 +71,7 @@
    3.44    from step(2) obtain M0 a K where
    3.45      *: "P = M0 + {#a#}" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
    3.46      by (blast elim: mult1_lessE)
    3.47 -  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) split: if_splits)
    3.48 +  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
    3.49    moreover
    3.50    { assume "count P a \<le> count M a"
    3.51      with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
    3.52 @@ -99,7 +79,7 @@
    3.53        with ** obtain z where z: "z > a" "count M z < count N z"
    3.54          by blast
    3.55        with * have "count N z \<le> count P z" 
    3.56 -        by (force simp add: not_in_iff)
    3.57 +        by (auto elim: less_asym intro: count_inI)
    3.58        with z have "\<exists>z > a. count M z < count P z" by auto
    3.59    } note count_a = this
    3.60    { fix y
    3.61 @@ -186,27 +166,6 @@
    3.62  
    3.63  end
    3.64  
    3.65 -context linorder
    3.66 -begin
    3.67 -
    3.68 -lemma total_le: "total {(a :: 'a, b). a \<le> b}"
    3.69 -  unfolding total_on_def by auto
    3.70 -
    3.71 -lemma total_less: "total {(a :: 'a, b). a < b}"
    3.72 -  unfolding total_on_def by auto
    3.73 -
    3.74 -lemma linorder_mult: "class.linorder
    3.75 -  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
    3.76 -  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
    3.77 -proof -
    3.78 -  interpret o: order
    3.79 -    "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)"
    3.80 -    "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
    3.81 -    by (rule order_mult)
    3.82 -  show ?thesis by unfold_locales (auto 0 3 simp: mult\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
    3.83 -qed
    3.84 -
    3.85 -end
    3.86  
    3.87  lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
    3.88    "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
    3.89 @@ -248,34 +207,28 @@
    3.90  lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
    3.91    by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
    3.92  
    3.93 -instantiation multiset :: (linorder) linorder
    3.94 +instantiation multiset :: (preorder) ordered_ab_semigroup_add_imp_le
    3.95  begin
    3.96  
    3.97  lemma less_eq_multiset\<^sub>H\<^sub>O:
    3.98    "M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
    3.99    by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
   3.100  
   3.101 -instance by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
   3.102 -
   3.103 -lemma less_eq_multiset_total:
   3.104 -  fixes M N :: "'a multiset"
   3.105 -  shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
   3.106 -  by simp
   3.107 +instance by standard (auto simp: less_eq_multiset\<^sub>H\<^sub>O)
   3.108  
   3.109  lemma
   3.110    fixes M N :: "'a multiset"
   3.111    shows
   3.112      less_eq_multiset_plus_left[simp]: "N \<le> (M + N)" and
   3.113      less_eq_multiset_plus_right[simp]: "M \<le> (M + N)"
   3.114 -  using [[metis_verbose = false]]
   3.115 -  by (metis subset_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
   3.116 +  using add_le_cancel_left[of N 0] add_le_cancel_left[of M 0 N] by (simp_all add: add.commute)
   3.117  
   3.118  lemma
   3.119    fixes M N :: "'a multiset"
   3.120    shows
   3.121 -    le_multiset_plus_plus_left_iff[simp]: "M + N < M' + N \<longleftrightarrow> M < M'" and
   3.122 -    le_multiset_plus_plus_right_iff[simp]: "M + N < M + N' \<longleftrightarrow> N < N'"
   3.123 -  unfolding less_multiset\<^sub>H\<^sub>O by auto
   3.124 +    le_multiset_plus_plus_left_iff: "M + N < M' + N \<longleftrightarrow> M < M'" and
   3.125 +    le_multiset_plus_plus_right_iff: "M + N < M + N' \<longleftrightarrow> N < N'"
   3.126 +  by simp_all
   3.127  
   3.128  lemma
   3.129    fixes M N :: "'a multiset"
   3.130 @@ -285,12 +238,21 @@
   3.131    using [[metis_verbose = false]]
   3.132    by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff add.commute)+
   3.133  
   3.134 +end
   3.135 +
   3.136  lemma ex_gt_count_imp_le_multiset:
   3.137 -  "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
   3.138 +  "(\<forall>y :: 'a :: order. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
   3.139    unfolding less_multiset\<^sub>H\<^sub>O
   3.140 -  by (metis add_gr_0 count_union mem_Collect_eq not_gr0 not_le not_less_iff_gr_or_eq set_mset_def)
   3.141 +  by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)
   3.142 +
   3.143  
   3.144 -end
   3.145 +instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
   3.146 +  by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
   3.147 +
   3.148 +lemma less_eq_multiset_total:
   3.149 +  fixes M N :: "'a :: linorder multiset"
   3.150 +  shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
   3.151 +  by simp
   3.152  
   3.153  instantiation multiset :: (wellorder) wellorder
   3.154  begin
   3.155 @@ -302,4 +264,26 @@
   3.156  
   3.157  end
   3.158  
   3.159 +instantiation multiset :: (preorder) order_bot
   3.160 +begin
   3.161 +
   3.162 +definition bot_multiset :: "'a multiset" where "bot_multiset = {#}"
   3.163 +
   3.164 +instance by standard (simp add: bot_multiset_def)
   3.165 +
   3.166  end
   3.167 +
   3.168 +instance multiset :: (preorder) no_top
   3.169 +proof standard
   3.170 +  fix x :: "'a multiset"
   3.171 +  obtain a :: 'a where True by simp
   3.172 +  have "x < x + (x + {#a#})"
   3.173 +    by simp
   3.174 +  then show "\<exists>y. x < y"
   3.175 +    by blast
   3.176 +qed
   3.177 +
   3.178 +instance multiset :: (preorder) ordered_cancel_comm_monoid_add
   3.179 +  by standard
   3.180 +
   3.181 +end
     4.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 07 09:24:03 2016 +0200
     4.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 07 17:34:39 2016 +0200
     4.3 @@ -36,17 +36,12 @@
     4.4  lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
     4.5    by (fact mset_append)
     4.6  
     4.7 -lemma subseteq_le_multiset: "(A :: 'a::order multiset) \<le> A + B"
     4.8 -unfolding less_eq_multiset_def apply (cases B; simp)
     4.9 -apply (rule union_le_mono2[of "{#}" "_ + {#_#}" A, simplified])
    4.10 -done
    4.11 -
    4.12  lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
    4.13  apply (rule monoI)
    4.14  apply (unfold prefix_def)
    4.15  apply (erule genPrefix.induct, simp_all add: add_right_mono)
    4.16  apply (erule order_trans)
    4.17 -apply (simp add: subseteq_le_multiset)
    4.18 +apply simp
    4.19  done
    4.20  
    4.21  (** setsum **)