src/HOL/Library/Multiset_Order.thy
changeset 64587 8355a6e2df79
parent 64418 91eae3a1be51
child 64978 5b9ba120d222
     1.1 --- a/src/HOL/Library/Multiset_Order.thy	Sat Dec 17 15:22:00 2016 +0100
     1.2 +++ b/src/HOL/Library/Multiset_Order.thy	Sat Dec 17 15:22:13 2016 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4  
     1.5  definition less_multiset\<^sub>D\<^sub>M where
     1.6    "less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
     1.7 -   (\<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)))"
     1.8 +   (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
     1.9  
    1.10  
    1.11  text \<open>The Huet--Oppen ordering:\<close>
    1.12 @@ -123,11 +123,11 @@
    1.13  proof -
    1.14    assume "less_multiset\<^sub>D\<^sub>M M N"
    1.15    then obtain X Y where
    1.16 -    "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)"
    1.17 +    "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
    1.18      unfolding less_multiset\<^sub>D\<^sub>M_def by blast
    1.19    then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
    1.20      by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
    1.21 -  with \<open>M = N - X + Y\<close> \<open>X \<le># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
    1.22 +  with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
    1.23      by (metis subset_mset.diff_add)
    1.24  qed
    1.25  
    1.26 @@ -140,7 +140,7 @@
    1.27    define X where "X = N - M"
    1.28    define Y where "Y = M - N"
    1.29    from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
    1.30 -  from z show "X \<le># N" unfolding X_def by auto
    1.31 +  from z show "X \<subseteq># N" unfolding X_def by auto
    1.32    show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
    1.33    show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
    1.34    proof (intro allI impI)
    1.35 @@ -175,7 +175,7 @@
    1.36  lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
    1.37  
    1.38  lemma subset_eq_imp_le_multiset:
    1.39 -  shows "M \<le># N \<Longrightarrow> M \<le> N"
    1.40 +  shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
    1.41    unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
    1.42    by (simp add: less_le_not_le subseteq_mset_def)
    1.43  
    1.44 @@ -201,7 +201,7 @@
    1.45  lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
    1.46    using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
    1.47  
    1.48 -lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
    1.49 +lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
    1.50    by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
    1.51  
    1.52  instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le