# HG changeset patch
# User blanchet
# Date 1467876243 -7200
# Node ID 3f3223b90239a1d2d801ce973e34c947cb757aea
# Parent  74c609115df0859f8c4a7f521ce5810f12138c52
moved lemmas and locales around (with minor incompatibilities)

diff -r 74c609115df0 -r 3f3223b90239 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Jul 07 00:43:27 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Jul 07 09:24:03 2016 +0200
@@ -426,8 +426,6 @@
 qed
 
 
-
-
 subsubsection \<open>Pointwise ordering induced by count\<close>
 
 definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
@@ -779,6 +777,7 @@
 
 interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
 
+
 subsubsection \<open>Conditionally complete lattice\<close>
 
 instantiation multiset :: (type) Inf
@@ -2577,6 +2576,7 @@
   by standard (auto simp add: less_eq_multiset_def intro: union_le_mono2)
 end
 
+
 subsubsection \<open>Termination proofs with multiset orders\<close>
 
 lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"
diff -r 74c609115df0 -r 3f3223b90239 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Thu Jul 07 00:43:27 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Thu Jul 07 09:24:03 2016 +0200
@@ -9,7 +9,7 @@
 imports Multiset
 begin
 
-subsubsection \<open>Alternative characterizations\<close>
+subsection \<open>Alternative characterizations\<close>
 
 context order
 begin
@@ -215,96 +215,91 @@
 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 less_eq_multiset\<^sub>H\<^sub>O:
-  fixes M N :: "('a :: linorder) multiset"
-  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 < N}"
-  unfolding less_multiset_def by (auto intro: wf_mult wf)
-
-instantiation multiset :: (linorder) linorder
-begin
-  instance by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
-end
-
-instantiation multiset :: (wellorder) wellorder
-begin
-  instance by standard (metis less_multiset_def wf wf_def wf_mult)
-end
-
-lemma less_eq_multiset_total:
-  fixes M N :: "('a :: linorder) multiset"
-  shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
-  by simp
-
 lemma subset_eq_imp_le_multiset:
-  fixes M N :: "('a :: linorder) multiset"
   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 le_multiset_right_total:
-  fixes M :: "('a :: linorder) multiset"
   shows "M < M + {#x#}"
   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 "{#} \<le> M"
   by (simp add: subset_eq_imp_le_multiset)
 
+lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
+  by (rule cancel_comm_monoid_add_class.add_cancel_left_right)
+
+lemma ex_gt_imp_less_multiset: "(\<exists>y. 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 less_eq_multiset_empty_right[simp]:
-  fixes M :: "('a :: linorder) multiset"
-  shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
+  "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 "M \<noteq> {#} \<Longrightarrow> {#} < M"
+lemma le_multiset_empty_left[simp]: "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 "\<not> M < {#}"
+lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
   using subset_eq_empty less_multiset\<^sub>D\<^sub>M by blast
 
+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
+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
+
 lemma
-  fixes M N :: "('a :: linorder) multiset"
+  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 [[metis_verbose = false]]
+  by (metis subset_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
 
 lemma
-  fixes M N :: "('a :: linorder) multiset"
+  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
 
-lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
-  by (rule cancel_comm_monoid_add_class.add_cancel_left_right)
-
 lemma
-  fixes M N :: "('a :: linorder) multiset"
+  fixes M N :: "'a multiset"
   shows
     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 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 < N"
-  unfolding less_multiset\<^sub>H\<^sub>O
-  by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
+  by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff add.commute)+
 
 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_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
+
+instantiation multiset :: (wellorder) wellorder
+begin
+
+lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
+  unfolding less_multiset_def by (auto intro: wf_mult wf)
+
+instance by standard (metis less_multiset_def wf wf_def wf_mult)
 
 end
+
+end
diff -r 74c609115df0 -r 3f3223b90239 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 07 00:43:27 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 07 09:24:03 2016 +0200
@@ -39,7 +39,6 @@
 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
 
 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"