--- a/NEWS Thu Jul 07 09:24:03 2016 +0200
+++ b/NEWS Thu Jul 07 17:34:39 2016 +0200
@@ -350,6 +350,16 @@
less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
INCOMPATIBILITY.
+* Some typeclass constraints about multisets have been reduced from ordered or
+linordered to preorder. Multisets have the additional typeclasses order_bot,
+no_top, ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
+and linordered_cancel_ab_semigroup_add.
+INCOMPATIBILITY.
+
+* There are some new simplification rules about multisets and the multiset
+ordering.
+INCOMPATIBILITY.
+
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
INCOMPATIBILITY.
--- a/src/HOL/Library/Multiset.thy Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Jul 07 17:34:39 2016 +0200
@@ -2488,7 +2488,7 @@
subsubsection \<open>Partial-order properties\<close>
-lemma (in order) mult1_lessE:
+lemma (in preorder) mult1_lessE:
assumes "(N, M) \<in> mult1 {(a, b). a < b}"
obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K"
"a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
@@ -2499,7 +2499,7 @@
ultimately show thesis by (auto intro: that)
qed
-instantiation multiset :: (order) order
+instantiation multiset :: (preorder) order
begin
definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
@@ -2515,7 +2515,7 @@
assume "M < M"
then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
have "trans {(x'::'a, x). x' < x}"
- by (rule transI) simp
+ by (metis (mono_tags, lifting) case_prodD case_prodI less_trans mem_Collect_eq transI)
moreover note MM
ultimately have "\<exists>I J K. M = I + J \<and> 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})"
@@ -2537,7 +2537,7 @@
end \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
lemma mset_le_irrefl [elim!]:
- fixes M :: "'a::order multiset"
+ fixes M :: "'a::preorder multiset"
shows "M < M \<Longrightarrow> R"
by simp
@@ -2552,25 +2552,25 @@
apply (simp add: add.assoc)
done
-lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::order multiset)"
+lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
apply (unfold less_multiset_def mult_def)
apply (erule trancl_induct)
apply (blast intro: mult1_union)
apply (blast intro: mult1_union trancl_trans)
done
-lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::order multiset)"
+lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::preorder multiset)"
apply (subst add.commute [of B C])
apply (subst add.commute [of D C])
apply (erule union_le_mono2)
done
lemma union_less_mono:
- fixes A B C D :: "'a::order multiset"
+ fixes A B C D :: "'a::preorder multiset"
shows "A < C \<Longrightarrow> B < D \<Longrightarrow> A + B < C + D"
by (blast intro!: union_le_mono1 union_le_mono2 less_trans)
-instantiation multiset :: (order) ordered_ab_semigroup_add
+instantiation multiset :: (preorder) ordered_ab_semigroup_add
begin
instance
by standard (auto simp add: less_eq_multiset_def intro: union_le_mono2)
@@ -2769,16 +2769,16 @@
multiset_inter_assoc
multiset_inter_left_commute
-lemma mset_le_not_refl: "\<not> M < (M::'a::order multiset)"
+lemma mset_le_not_refl: "\<not> M < (M::'a::preorder multiset)"
by (fact less_irrefl)
-lemma mset_le_trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < (N::'a::order multiset)"
+lemma mset_le_trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < (N::'a::preorder multiset)"
by (fact less_trans)
-lemma mset_le_not_sym: "M < N \<Longrightarrow> \<not> N < (M::'a::order multiset)"
+lemma mset_le_not_sym: "M < N \<Longrightarrow> \<not> N < (M::'a::preorder multiset)"
by (fact less_not_sym)
-lemma mset_le_asym: "M < N \<Longrightarrow> (\<not> P \<Longrightarrow> N < (M::'a::order multiset)) \<Longrightarrow> P"
+lemma mset_le_asym: "M < N \<Longrightarrow> (\<not> P \<Longrightarrow> N < (M::'a::preorder multiset)) \<Longrightarrow> P"
by (fact less_asym)
declaration \<open>
--- a/src/HOL/Library/Multiset_Order.thy Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Thu Jul 07 17:34:39 2016 +0200
@@ -11,29 +11,9 @@
subsection \<open>Alternative characterizations\<close>
-context order
+context preorder
begin
-lemma reflp_le: "reflp (op \<le>)"
- unfolding reflp_def by simp
-
-lemma antisymP_le: "antisymP (op \<le>)"
- unfolding antisym_def by auto
-
-lemma transp_le: "transp (op \<le>)"
- unfolding transp_def by auto
-
-lemma irreflp_less: "irreflp (op <)"
- unfolding irreflp_def by simp
-
-lemma antisymP_less: "antisymP (op <)"
- unfolding antisym_def by auto
-
-lemma transp_less: "transp (op <)"
- unfolding transp_def by auto
-
-lemmas le_trans = transp_le[unfolded transp_def, rule_format]
-
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})"
@@ -43,7 +23,7 @@
proof
fix M :: "'a multiset"
have "trans {(x'::'a, x). x' < x}"
- by (rule transI) simp
+ by (rule transI) (blast intro: less_trans)
moreover
assume "(M, M) \<in> mult {(x, y). x < y}"
ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
@@ -91,7 +71,7 @@
from step(2) obtain M0 a K where
*: "P = M0 + {#a#}" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
by (blast elim: mult1_lessE)
- from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) split: if_splits)
+ 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 \<le> count M a"
with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
@@ -99,7 +79,7 @@
with ** obtain z where z: "z > a" "count M z < count N z"
by blast
with * have "count N z \<le> count P z"
- by (force simp add: not_in_iff)
+ by (auto elim: less_asym intro: count_inI)
with z have "\<exists>z > a. count M z < count P z" by auto
} note count_a = this
{ fix y
@@ -186,27 +166,6 @@
end
-context linorder
-begin
-
-lemma total_le: "total {(a :: 'a, b). a \<le> b}"
- unfolding total_on_def by auto
-
-lemma total_less: "total {(a :: 'a, b). a < b}"
- unfolding total_on_def by auto
-
-lemma linorder_mult: "class.linorder
- (\<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})"
-proof -
- interpret o: 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})"
- by (rule order_mult)
- show ?thesis by unfold_locales (auto 0 3 simp: mult\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
-qed
-
-end
lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
"M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
@@ -248,34 +207,28 @@
lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
-instantiation multiset :: (linorder) linorder
+instantiation multiset :: (preorder) ordered_ab_semigroup_add_imp_le
begin
lemma less_eq_multiset\<^sub>H\<^sub>O:
"M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
-instance 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 multiset"
- shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
- by simp
+instance by standard (auto simp: less_eq_multiset\<^sub>H\<^sub>O)
lemma
fixes M N :: "'a multiset"
shows
less_eq_multiset_plus_left[simp]: "N \<le> (M + N)" and
less_eq_multiset_plus_right[simp]: "M \<le> (M + N)"
- using [[metis_verbose = false]]
- by (metis subset_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
+ using add_le_cancel_left[of N 0] add_le_cancel_left[of M 0 N] by (simp_all add: add.commute)
lemma
fixes M N :: "'a multiset"
shows
- le_multiset_plus_plus_left_iff[simp]: "M + N < M' + N \<longleftrightarrow> M < M'" and
- le_multiset_plus_plus_right_iff[simp]: "M + N < M + N' \<longleftrightarrow> N < N'"
- unfolding less_multiset\<^sub>H\<^sub>O by auto
+ le_multiset_plus_plus_left_iff: "M + N < M' + N \<longleftrightarrow> M < M'" and
+ le_multiset_plus_plus_right_iff: "M + N < M + N' \<longleftrightarrow> N < N'"
+ by simp_all
lemma
fixes M N :: "'a multiset"
@@ -285,12 +238,21 @@
using [[metis_verbose = false]]
by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff add.commute)+
+end
+
lemma ex_gt_count_imp_le_multiset:
- "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
+ "(\<forall>y :: 'a :: order. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
unfolding less_multiset\<^sub>H\<^sub>O
- by (metis add_gr_0 count_union mem_Collect_eq not_gr0 not_le not_less_iff_gr_or_eq set_mset_def)
+ by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)
+
-end
+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 "\<not> M \<le> N \<Longrightarrow> N \<le> M"
+ by simp
instantiation multiset :: (wellorder) wellorder
begin
@@ -302,4 +264,26 @@
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 "\<exists>y. x < y"
+ by blast
+qed
+
+instance multiset :: (preorder) ordered_cancel_comm_monoid_add
+ by standard
+
+end
--- a/src/HOL/UNITY/Comp/AllocBase.thy Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Thu Jul 07 17:34:39 2016 +0200
@@ -36,17 +36,12 @@
lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
by (fact mset_append)
-lemma subseteq_le_multiset: "(A :: 'a::order multiset) \<le> A + B"
-unfolding less_eq_multiset_def apply (cases B; simp)
-apply (rule union_le_mono2[of "{#}" "_ + {#_#}" A, simplified])
-done
-
lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
apply (rule monoI)
apply (unfold prefix_def)
apply (erule genPrefix.induct, simp_all add: add_right_mono)
apply (erule order_trans)
-apply (simp add: subseteq_le_multiset)
+apply simp
done
(** setsum **)