--- a/NEWS Tue Jul 05 10:26:23 2016 +0200
+++ b/NEWS Tue Jul 05 13:05:04 2016 +0200
@@ -311,6 +311,43 @@
Some functions have been renamed:
ms_lesseq_impl -> subset_eq_mset_impl
+* Multisets are now ordered with the multiset ordering
+ #\<subseteq># ~> \<le>
+ #\<subset># ~> <
+ le_multiset ~> less_eq_multiset
+ less_multiset ~> le_multiset
+INCOMPATIBILITY
+
+* The prefix multiset_order has been discontinued: the theorems can be directly
+accessed.
+INCOMPATILBITY
+
+* Some theorems about the multiset ordering have been renamed:
+ le_multiset_def ~> less_eq_multiset_def
+ less_multiset_def ~> le_multiset_def
+ less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset
+ mult_less_not_refl ~> mset_le_not_refl
+ mult_less_trans ~> mset_le_trans
+ mult_less_not_sym ~> mset_le_not_sym
+ mult_less_asym ~> mset_le_asym
+ mult_less_irrefl ~> mset_le_irrefl
+ union_less_mono2{,1,2} ~> union_le_mono2{,1,2}
+
+ le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O
+ le_multiset_total ~> less_eq_multiset_total
+ less_multiset_right_total ~> subset_eq_imp_le_multiset
+ le_multiset_empty_left ~> less_eq_multiset_empty_left
+ le_multiset_empty_right ~> less_eq_multiset_empty_right
+ less_multiset_empty_right ~> le_multiset_empty_left
+ less_multiset_empty_left ~> le_multiset_empty_right
+ union_less_diff_plus ~> union_le_diff_plus
+ ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset
+ less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty
+ le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
+ less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff
+ less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
+INCOMPATIBILITY
+
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
INCOMPATIBILITY.
--- a/src/HOL/Library/Multiset.thy Tue Jul 05 10:26:23 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Jul 05 13:05:04 2016 +0200
@@ -2500,21 +2500,20 @@
ultimately show thesis by (auto intro: that)
qed
-definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#\<subset>#" 50)
- where "M' #\<subset># M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#\<subseteq>#" 50)
- where "M' #\<subseteq># M \<longleftrightarrow> M' #\<subset># M \<or> M' = M"
-
-notation (ASCII)
- less_multiset (infix "#<#" 50) and
- le_multiset (infix "#<=#" 50)
-
-interpretation multiset_order: order le_multiset less_multiset
+instantiation multiset :: (order) order
+begin
+
+definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+ where "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+ where "less_eq_multiset M' M \<longleftrightarrow> M' < M \<or> M' = M"
+
+instance
proof -
- have irrefl: "\<not> M #\<subset># M" for M :: "'a multiset"
+ have irrefl: "\<not> M < M" for M :: "'a multiset"
proof
- assume "M #\<subset># M"
+ 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
@@ -2531,15 +2530,16 @@
by (induct rule: finite_induct) (auto intro: order_less_trans)
with * show False by simp
qed
- have trans: "K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># N" for K M N :: "'a multiset"
+ have trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < N" for K M N :: "'a multiset"
unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
- show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
- by standard (auto simp add: le_multiset_def irrefl dest: trans)
-qed \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
-
-lemma mult_less_irrefl [elim!]:
+ show "OFCLASS('a multiset, order_class)"
+ by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
+qed
+end \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
+
+lemma mset_le_irrefl [elim!]:
fixes M :: "'a::order multiset"
- shows "M #\<subset># M \<Longrightarrow> R"
+ shows "M < M \<Longrightarrow> R"
by simp
@@ -2553,27 +2553,29 @@
apply (simp add: add.assoc)
done
-lemma union_less_mono2: "B #\<subset># D \<Longrightarrow> C + B #\<subset># C + (D::'a::order multiset)"
+lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::order 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_less_mono1: "B #\<subset># D \<Longrightarrow> B + C #\<subset># D + (C::'a::order multiset)"
+lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::order multiset)"
apply (subst add.commute [of B C])
apply (subst add.commute [of D C])
-apply (erule union_less_mono2)
+apply (erule union_le_mono2)
done
lemma union_less_mono:
fixes A B C D :: "'a::order multiset"
- shows "A #\<subset># C \<Longrightarrow> B #\<subset># D \<Longrightarrow> A + B #\<subset># C + D"
- by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans)
-
-interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset
- by standard (auto simp add: le_multiset_def intro: union_less_mono2)
-
+ 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
+begin
+instance
+ by standard (auto simp add: less_eq_multiset_def intro: union_le_mono2)
+end
subsubsection \<open>Termination proofs with multiset orders\<close>
@@ -2767,17 +2769,17 @@
multiset_inter_assoc
multiset_inter_left_commute
-lemma mult_less_not_refl: "\<not> M #\<subset># (M::'a::order multiset)"
- by (fact multiset_order.less_irrefl)
-
-lemma mult_less_trans: "K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># (N::'a::order multiset)"
- by (fact multiset_order.less_trans)
-
-lemma mult_less_not_sym: "M #\<subset># N \<Longrightarrow> \<not> N #\<subset># (M::'a::order multiset)"
- by (fact multiset_order.less_not_sym)
-
-lemma mult_less_asym: "M #\<subset># N \<Longrightarrow> (\<not> P \<Longrightarrow> N #\<subset># (M::'a::order multiset)) \<Longrightarrow> P"
- by (fact multiset_order.less_asym)
+lemma mset_le_not_refl: "\<not> M < (M::'a::order multiset)"
+ by (fact less_irrefl)
+
+lemma mset_le_trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < (N::'a::order multiset)"
+ by (fact less_trans)
+
+lemma mset_le_not_sym: "M < N \<Longrightarrow> \<not> N < (M::'a::order multiset)"
+ by (fact less_not_sym)
+
+lemma mset_le_asym: "M < N \<Longrightarrow> (\<not> P \<Longrightarrow> N < (M::'a::order multiset)) \<Longrightarrow> P"
+ by (fact less_asym)
declaration \<open>
let
@@ -2951,8 +2953,8 @@
qed
text \<open>
- Exercise for the casual reader: add implementations for @{const le_multiset}
- and @{const less_multiset} (multiset order).
+ Exercise for the casual reader: add implementations for @{term "op \<le>"}
+ and @{term "op <"} (multiset order).
\<close>
text \<open>Quickcheck generators\<close>
--- a/src/HOL/Library/Multiset_Order.thy Tue Jul 05 10:26:23 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Tue Jul 05 13:05:04 2016 +0200
@@ -62,7 +62,7 @@
have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
unfolding mult_def by (blast intro: trancl_trans)
show "class.order ?le ?less"
- by standard (auto simp add: le_multiset_def irrefl dest: trans)
+ by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
qed
text \<open>The Dershowitz--Manna ordering:\<close>
@@ -209,88 +209,88 @@
end
lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
- "M #\<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
+ "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
-lemma le_multiset\<^sub>H\<^sub>O:
+lemma less_eq_multiset\<^sub>H\<^sub>O:
fixes M N :: "('a :: linorder) multiset"
- 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))"
- by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
+ shows "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)
-lemma wf_less_multiset: "wf {(M :: ('a :: wellorder) multiset, N). M #\<subset># N}"
+lemma wf_less_multiset: "wf {(M :: ('a :: wellorder) multiset, N). M < N}"
unfolding less_multiset_def by (auto intro: wf_mult wf)
lemma order_multiset: "class.order
- (le_multiset :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)
- (less_multiset :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)"
+ (op \<le> :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)
+ (op < :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)"
by unfold_locales
lemma linorder_multiset: "class.linorder
- (le_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)
- (less_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)"
- by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O le_multiset_def not_less_iff_gr_or_eq)
+ (op \<le> :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)
+ (op < :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)"
+ by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O less_eq_multiset_def not_less_iff_gr_or_eq)
interpretation multiset_linorder: linorder
- "le_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
- "less_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
+ "op \<le> :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
+ "op < :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
by (rule linorder_multiset)
interpretation multiset_wellorder: wellorder
- "le_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
- "less_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
+ "op \<le> :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
+ "op < :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
by unfold_locales (blast intro: wf_less_multiset [unfolded wf_def, simplified, rule_format])
-lemma le_multiset_total:
+lemma less_eq_multiset_total:
fixes M N :: "('a :: linorder) multiset"
- shows "\<not> M #\<subseteq># N \<Longrightarrow> N #\<subseteq># M"
+ shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
by (metis multiset_linorder.le_cases)
-lemma less_eq_imp_le_multiset:
+lemma subset_eq_imp_le_multiset:
fixes M N :: "('a :: linorder) multiset"
- shows "M \<le># N \<Longrightarrow> M #\<subseteq># N"
- unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
+ shows "M \<le># N \<Longrightarrow> M \<le> N"
+ unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
by (simp add: less_le_not_le subseteq_mset_def)
-lemma less_multiset_right_total:
+lemma le_multiset_right_total:
+ fixes M :: "('a :: linorder) multiset"
+ shows "M < M + {#undefined#}"
+ unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
+
+lemma less_eq_multiset_empty_left[simp]:
fixes M :: "('a :: linorder) multiset"
- shows "M #\<subset># M + {#undefined#}"
- unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
+ shows "{#} \<le> M"
+ by (simp add: subset_eq_imp_le_multiset)
+
+lemma less_eq_multiset_empty_right[simp]:
+ fixes M :: "('a :: linorder) multiset"
+ shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
+ by (metis less_eq_multiset_empty_left antisym)
lemma le_multiset_empty_left[simp]:
fixes M :: "('a :: linorder) multiset"
- shows "{#} #\<subseteq># M"
- by (simp add: less_eq_imp_le_multiset)
+ shows "M \<noteq> {#} \<Longrightarrow> {#} < M"
+ by (simp add: less_multiset\<^sub>H\<^sub>O)
lemma le_multiset_empty_right[simp]:
fixes M :: "('a :: linorder) multiset"
- shows "M \<noteq> {#} \<Longrightarrow> \<not> M #\<subseteq># {#}"
- by (metis le_multiset_empty_left multiset_order.antisym)
-
-lemma less_multiset_empty_left[simp]:
- fixes M :: "('a :: linorder) multiset"
- shows "M \<noteq> {#} \<Longrightarrow> {#} #\<subset># M"
- by (simp add: less_multiset\<^sub>H\<^sub>O)
-
-lemma less_multiset_empty_right[simp]:
- fixes M :: "('a :: linorder) multiset"
- shows "\<not> M #\<subset># {#}"
+ shows "\<not> M < {#}"
using subset_eq_empty less_multiset\<^sub>D\<^sub>M by blast
lemma
fixes M N :: "('a :: linorder) multiset"
shows
- le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and
- le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)"
- using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
+ 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)+
lemma
fixes M N :: "('a :: linorder) multiset"
shows
- less_multiset_plus_plus_left_iff[simp]: "M + N #\<subset># M' + N \<longleftrightarrow> M #\<subset># M'" and
- less_multiset_plus_plus_right_iff[simp]: "M + N #\<subset># M + N' \<longleftrightarrow> N #\<subset># N'"
+ 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
lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
@@ -299,22 +299,22 @@
lemma
fixes M N :: "('a :: linorder) multiset"
shows
- less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N #\<subset># M + N" and
- less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M #\<subset># M + N"
+ le_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
+ le_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M < M + N"
using [[metis_verbose = false]]
- by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
+ by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff
add.commute)+
-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"
+lemma ex_gt_imp_less_multiset: "(\<exists>y :: 'a :: linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
unfolding less_multiset\<^sub>H\<^sub>O
by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
-
-lemma ex_gt_count_imp_less_multiset:
- "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N"
+
+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"
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)
-lemma union_less_diff_plus: "P \<le># M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
- by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2)
+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)
end
--- a/src/HOL/UNITY/Comp/AllocBase.thy Tue Jul 05 10:26:23 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Tue Jul 05 13:05:04 2016 +0200
@@ -36,9 +36,9 @@
lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
by (fact mset_append)
-lemma subseteq_le_multiset: "A #\<subseteq># A + B"
-unfolding le_multiset_def apply (cases B; simp)
-apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
+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])
apply (simp add: less_multiset\<^sub>H\<^sub>O)
done
@@ -47,7 +47,7 @@
apply (unfold prefix_def)
apply (erule genPrefix.induct, simp_all add: add_right_mono)
apply (erule order_trans)
-apply (simp add: less_eq_multiset_def subseteq_le_multiset)
+apply (simp add: subseteq_le_multiset)
done
(** setsum **)
--- a/src/HOL/UNITY/Follows.thy Tue Jul 05 10:26:23 2016 +0200
+++ b/src/HOL/UNITY/Follows.thy Tue Jul 05 13:05:04 2016 +0200
@@ -175,19 +175,7 @@
subsection\<open>Multiset union properties (with the multiset ordering)\<close>
-(*TODO: remove when multiset is of sort ord again*)
-instantiation multiset :: (order) ordered_ab_semigroup_add
-begin
-definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
- "M' < M \<longleftrightarrow> M' #\<subset># M"
-
-definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
- "(M'::'a multiset) \<le> M \<longleftrightarrow> M' #\<subseteq># M"
-
-instance
- by standard (auto simp add: less_eq_multiset_def less_multiset_def multiset_order.less_le_not_le add.commute multiset_order.add_right_mono)
-end
lemma increasing_union:
"[| F \<in> increasing f; F \<in> increasing g |]