src/HOL/Library/Multiset_Order.thy
changeset 59958 4538d41e8e54
parent 59817 75433c3ee203
child 60397 f8a513fedb31
     1.1 --- a/src/HOL/Library/Multiset_Order.thy	Wed Apr 08 15:04:06 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset_Order.thy	Wed Apr 08 15:21:20 2015 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4  end
     1.5  
     1.6  lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
     1.7 -  "M \<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
     1.8 +  "M #\<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
     1.9    unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
    1.10  
    1.11  lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
    1.12 @@ -206,10 +206,10 @@
    1.13  
    1.14  lemma le_multiset\<^sub>H\<^sub>O:
    1.15    fixes M N :: "('a \<Colon> linorder) multiset"
    1.16 -  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))"
    1.17 +  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))"
    1.18    by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
    1.19  
    1.20 -lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M \<subset># N}"
    1.21 +lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M #\<subset># N}"
    1.22    unfolding less_multiset_def by (auto intro: wf_mult wf)
    1.23  
    1.24  lemma order_multiset: "class.order
    1.25 @@ -234,52 +234,52 @@
    1.26  
    1.27  lemma le_multiset_total:
    1.28    fixes M N :: "('a \<Colon> linorder) multiset"
    1.29 -  shows "\<not> M \<subseteq># N \<Longrightarrow> N \<subseteq># M"
    1.30 +  shows "\<not> M #\<subseteq># N \<Longrightarrow> N #\<subseteq># M"
    1.31    by (metis multiset_linorder.le_cases)
    1.32  
    1.33  lemma less_eq_imp_le_multiset:
    1.34    fixes M N :: "('a \<Colon> linorder) multiset"
    1.35 -  shows "M \<le> N \<Longrightarrow> M \<subseteq># N"
    1.36 +  shows "M \<le> N \<Longrightarrow> M #\<subseteq># N"
    1.37    unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
    1.38    by (auto dest: leD simp add: less_eq_multiset.rep_eq)
    1.39  
    1.40  lemma less_multiset_right_total:
    1.41    fixes M :: "('a \<Colon> linorder) multiset"
    1.42 -  shows "M \<subset># M + {#undefined#}"
    1.43 +  shows "M #\<subset># M + {#undefined#}"
    1.44    unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
    1.45  
    1.46  lemma le_multiset_empty_left[simp]:
    1.47    fixes M :: "('a \<Colon> linorder) multiset"
    1.48 -  shows "{#} \<subseteq># M"
    1.49 +  shows "{#} #\<subseteq># M"
    1.50    by (simp add: less_eq_imp_le_multiset)
    1.51  
    1.52  lemma le_multiset_empty_right[simp]:
    1.53    fixes M :: "('a \<Colon> linorder) multiset"
    1.54 -  shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<subseteq># {#}"
    1.55 +  shows "M \<noteq> {#} \<Longrightarrow> \<not> M #\<subseteq># {#}"
    1.56    by (metis le_multiset_empty_left multiset_order.antisym)
    1.57  
    1.58  lemma less_multiset_empty_left[simp]:
    1.59    fixes M :: "('a \<Colon> linorder) multiset"
    1.60 -  shows "M \<noteq> {#} \<Longrightarrow> {#} \<subset># M"
    1.61 +  shows "M \<noteq> {#} \<Longrightarrow> {#} #\<subset># M"
    1.62    by (simp add: less_multiset\<^sub>H\<^sub>O)
    1.63  
    1.64  lemma less_multiset_empty_right[simp]:
    1.65    fixes M :: "('a \<Colon> linorder) multiset"
    1.66 -  shows "\<not> M \<subset># {#}"
    1.67 +  shows "\<not> M #\<subset># {#}"
    1.68    using le_empty less_multiset\<^sub>D\<^sub>M by blast
    1.69  
    1.70  lemma
    1.71    fixes M N :: "('a \<Colon> linorder) multiset"
    1.72    shows
    1.73 -    le_multiset_plus_left[simp]: "N \<subseteq># (M + N)" and
    1.74 -    le_multiset_plus_right[simp]: "M \<subseteq># (M + N)"
    1.75 +    le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and
    1.76 +    le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)"
    1.77    using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+
    1.78  
    1.79  lemma
    1.80    fixes M N :: "('a \<Colon> linorder) multiset"
    1.81    shows
    1.82 -    less_multiset_plus_plus_left_iff[simp]: "M + N \<subset># M' + N \<longleftrightarrow> M \<subset># M'" and
    1.83 -    less_multiset_plus_plus_right_iff[simp]: "M + N \<subset># M + N' \<longleftrightarrow> N \<subset># N'"
    1.84 +    less_multiset_plus_plus_left_iff[simp]: "M + N #\<subset># M' + N \<longleftrightarrow> M #\<subset># M'" and
    1.85 +    less_multiset_plus_plus_right_iff[simp]: "M + N #\<subset># M + N' \<longleftrightarrow> N #\<subset># N'"
    1.86    unfolding less_multiset\<^sub>H\<^sub>O by auto
    1.87  
    1.88  lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
    1.89 @@ -288,21 +288,21 @@
    1.90  lemma
    1.91    fixes M N :: "('a \<Colon> linorder) multiset"
    1.92    shows
    1.93 -    less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N \<subset># M + N" and
    1.94 -    less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M \<subset># M + N"
    1.95 +    less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N #\<subset># M + N" and
    1.96 +    less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M #\<subset># M + N"
    1.97    using [[metis_verbose = false]]
    1.98    by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
    1.99      add.commute)+
   1.100  
   1.101 -lemma ex_gt_imp_less_multiset: "(\<exists>y \<Colon> 'a \<Colon> linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M \<subset># N"
   1.102 +lemma ex_gt_imp_less_multiset: "(\<exists>y \<Colon> 'a \<Colon> linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M #\<subset># N"
   1.103    unfolding less_multiset\<^sub>H\<^sub>O by (metis less_irrefl less_nat_zero_code not_gr0)
   1.104  
   1.105  lemma ex_gt_count_imp_less_multiset:
   1.106 -  "(\<forall>y \<Colon> 'a \<Colon> linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M \<subset># N"
   1.107 +  "(\<forall>y \<Colon> 'a \<Colon> linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N"
   1.108    unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order
   1.109      less_not_sym mset_leD mset_le_add_left)  
   1.110  
   1.111 -lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N \<subset># P \<Longrightarrow> M - P + N \<subset># M"
   1.112 +lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
   1.113    by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2)
   1.114  
   1.115  end