renamed multiset ordering to free up nice <# etc. symbols for the standard subset
authorblanchet
Wed Apr 08 15:21:20 2015 +0200 (2015-04-08)
changeset 599584538d41e8e54
parent 59957 5031030aaebe
child 59959 1e3383a5204b
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
NEWS
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
     1.1 --- a/NEWS	Wed Apr 08 15:04:06 2015 +0200
     1.2 +++ b/NEWS	Wed Apr 08 15:21:20 2015 +0200
     1.3 @@ -330,6 +330,12 @@
     1.4    - Introduced "replicate_mset" operation.
     1.5    - Introduced alternative characterizations of the multiset ordering in
     1.6      "Library/Multiset_Order".
     1.7 +  - Renamed multiset ordering:
     1.8 +      <# ~> #<#
     1.9 +      <=# ~> #<=#
    1.10 +      \<subset># ~> #\<subset>#
    1.11 +      \<subseteq># ~> #\<subseteq>#
    1.12 +    INCOMPATIBILITY.
    1.13    - Renamed
    1.14        in_multiset_of ~> in_multiset_in_set
    1.15      INCOMPATIBILITY.
     2.1 --- a/src/HOL/Library/Multiset.thy	Wed Apr 08 15:04:06 2015 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Wed Apr 08 15:21:20 2015 +0200
     2.3 @@ -1778,21 +1778,21 @@
     2.4  
     2.5  subsubsection {* Partial-order properties *}
     2.6  
     2.7 -definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
     2.8 -  "M' <# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
     2.9 -
    2.10 -definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
    2.11 -  "M' <=# M \<longleftrightarrow> M' <# M \<or> M' = M"
    2.12 -
    2.13 -notation (xsymbols) less_multiset (infix "\<subset>#" 50)
    2.14 -notation (xsymbols) le_multiset (infix "\<subseteq>#" 50)
    2.15 +definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<#" 50) where
    2.16 +  "M' #<# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
    2.17 +
    2.18 +definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<=#" 50) where
    2.19 +  "M' #<=# M \<longleftrightarrow> M' #<# M \<or> M' = M"
    2.20 +
    2.21 +notation (xsymbols) less_multiset (infix "#\<subset>#" 50)
    2.22 +notation (xsymbols) le_multiset (infix "#\<subseteq>#" 50)
    2.23  
    2.24  interpretation multiset_order: order le_multiset less_multiset
    2.25  proof -
    2.26 -  have irrefl: "\<And>M :: 'a multiset. \<not> M \<subset># M"
    2.27 +  have irrefl: "\<And>M :: 'a multiset. \<not> M #\<subset># M"
    2.28    proof
    2.29      fix M :: "'a multiset"
    2.30 -    assume "M \<subset># M"
    2.31 +    assume "M #\<subset># M"
    2.32      then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
    2.33      have "trans {(x'::'a, x). x' < x}"
    2.34        by (rule transI) simp
    2.35 @@ -1809,13 +1809,13 @@
    2.36        by (induct rule: finite_induct) (auto intro: order_less_trans)
    2.37      with aux1 show False by simp
    2.38    qed
    2.39 -  have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
    2.40 +  have trans: "\<And>K M N :: 'a multiset. K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># N"
    2.41      unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
    2.42    show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
    2.43      by default (auto simp add: le_multiset_def irrefl dest: trans)
    2.44  qed
    2.45  
    2.46 -lemma mult_less_irrefl [elim!]: "M \<subset># (M::'a::order multiset) ==> R"
    2.47 +lemma mult_less_irrefl [elim!]: "M #\<subset># (M::'a::order multiset) ==> R"
    2.48    by simp
    2.49  
    2.50  
    2.51 @@ -1829,21 +1829,21 @@
    2.52  apply (simp add: add.assoc)
    2.53  done
    2.54  
    2.55 -lemma union_less_mono2: "B \<subset># D ==> C + B \<subset># C + (D::'a::order multiset)"
    2.56 +lemma union_less_mono2: "B #\<subset># D ==> C + B #\<subset># C + (D::'a::order multiset)"
    2.57  apply (unfold less_multiset_def mult_def)
    2.58  apply (erule trancl_induct)
    2.59   apply (blast intro: mult1_union)
    2.60  apply (blast intro: mult1_union trancl_trans)
    2.61  done
    2.62  
    2.63 -lemma union_less_mono1: "B \<subset># D ==> B + C \<subset># D + (C::'a::order multiset)"
    2.64 +lemma union_less_mono1: "B #\<subset># D ==> B + C #\<subset># D + (C::'a::order multiset)"
    2.65  apply (subst add.commute [of B C])
    2.66  apply (subst add.commute [of D C])
    2.67  apply (erule union_less_mono2)
    2.68  done
    2.69  
    2.70  lemma union_less_mono:
    2.71 -  "A \<subset># C ==> B \<subset># D ==> A + B \<subset># C + (D::'a::order multiset)"
    2.72 +  "A #\<subset># C ==> B #\<subset># D ==> A + B #\<subset># C + (D::'a::order multiset)"
    2.73    by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans)
    2.74  
    2.75  interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset
    2.76 @@ -2044,19 +2044,19 @@
    2.77    multiset_inter_left_commute
    2.78  
    2.79  lemma mult_less_not_refl:
    2.80 -  "\<not> M \<subset># (M::'a::order multiset)"
    2.81 +  "\<not> M #\<subset># (M::'a::order multiset)"
    2.82    by (fact multiset_order.less_irrefl)
    2.83  
    2.84  lemma mult_less_trans:
    2.85 -  "K \<subset># M ==> M \<subset># N ==> K \<subset># (N::'a::order multiset)"
    2.86 +  "K #\<subset># M ==> M #\<subset># N ==> K #\<subset># (N::'a::order multiset)"
    2.87    by (fact multiset_order.less_trans)
    2.88  
    2.89  lemma mult_less_not_sym:
    2.90 -  "M \<subset># N ==> \<not> N \<subset># (M::'a::order multiset)"
    2.91 +  "M #\<subset># N ==> \<not> N #\<subset># (M::'a::order multiset)"
    2.92    by (fact multiset_order.less_not_sym)
    2.93  
    2.94  lemma mult_less_asym:
    2.95 -  "M \<subset># N ==> (\<not> P ==> N \<subset># (M::'a::order multiset)) ==> P"
    2.96 +  "M #\<subset># N ==> (\<not> P ==> N #\<subset># (M::'a::order multiset)) ==> P"
    2.97    by (fact multiset_order.less_asym)
    2.98  
    2.99  ML {*
     3.1 --- a/src/HOL/Library/Multiset_Order.thy	Wed Apr 08 15:04:06 2015 +0200
     3.2 +++ b/src/HOL/Library/Multiset_Order.thy	Wed Apr 08 15:21:20 2015 +0200
     3.3 @@ -198,7 +198,7 @@
     3.4  end
     3.5  
     3.6  lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
     3.7 -  "M \<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
     3.8 +  "M #\<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
     3.9    unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
    3.10  
    3.11  lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
    3.12 @@ -206,10 +206,10 @@
    3.13  
    3.14  lemma le_multiset\<^sub>H\<^sub>O:
    3.15    fixes M N :: "('a \<Colon> linorder) multiset"
    3.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))"
    3.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))"
    3.18    by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
    3.19  
    3.20 -lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M \<subset># N}"
    3.21 +lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M #\<subset># N}"
    3.22    unfolding less_multiset_def by (auto intro: wf_mult wf)
    3.23  
    3.24  lemma order_multiset: "class.order
    3.25 @@ -234,52 +234,52 @@
    3.26  
    3.27  lemma le_multiset_total:
    3.28    fixes M N :: "('a \<Colon> linorder) multiset"
    3.29 -  shows "\<not> M \<subseteq># N \<Longrightarrow> N \<subseteq># M"
    3.30 +  shows "\<not> M #\<subseteq># N \<Longrightarrow> N #\<subseteq># M"
    3.31    by (metis multiset_linorder.le_cases)
    3.32  
    3.33  lemma less_eq_imp_le_multiset:
    3.34    fixes M N :: "('a \<Colon> linorder) multiset"
    3.35 -  shows "M \<le> N \<Longrightarrow> M \<subseteq># N"
    3.36 +  shows "M \<le> N \<Longrightarrow> M #\<subseteq># N"
    3.37    unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
    3.38    by (auto dest: leD simp add: less_eq_multiset.rep_eq)
    3.39  
    3.40  lemma less_multiset_right_total:
    3.41    fixes M :: "('a \<Colon> linorder) multiset"
    3.42 -  shows "M \<subset># M + {#undefined#}"
    3.43 +  shows "M #\<subset># M + {#undefined#}"
    3.44    unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
    3.45  
    3.46  lemma le_multiset_empty_left[simp]:
    3.47    fixes M :: "('a \<Colon> linorder) multiset"
    3.48 -  shows "{#} \<subseteq># M"
    3.49 +  shows "{#} #\<subseteq># M"
    3.50    by (simp add: less_eq_imp_le_multiset)
    3.51  
    3.52  lemma le_multiset_empty_right[simp]:
    3.53    fixes M :: "('a \<Colon> linorder) multiset"
    3.54 -  shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<subseteq># {#}"
    3.55 +  shows "M \<noteq> {#} \<Longrightarrow> \<not> M #\<subseteq># {#}"
    3.56    by (metis le_multiset_empty_left multiset_order.antisym)
    3.57  
    3.58  lemma less_multiset_empty_left[simp]:
    3.59    fixes M :: "('a \<Colon> linorder) multiset"
    3.60 -  shows "M \<noteq> {#} \<Longrightarrow> {#} \<subset># M"
    3.61 +  shows "M \<noteq> {#} \<Longrightarrow> {#} #\<subset># M"
    3.62    by (simp add: less_multiset\<^sub>H\<^sub>O)
    3.63  
    3.64  lemma less_multiset_empty_right[simp]:
    3.65    fixes M :: "('a \<Colon> linorder) multiset"
    3.66 -  shows "\<not> M \<subset># {#}"
    3.67 +  shows "\<not> M #\<subset># {#}"
    3.68    using le_empty less_multiset\<^sub>D\<^sub>M by blast
    3.69  
    3.70  lemma
    3.71    fixes M N :: "('a \<Colon> linorder) multiset"
    3.72    shows
    3.73 -    le_multiset_plus_left[simp]: "N \<subseteq># (M + N)" and
    3.74 -    le_multiset_plus_right[simp]: "M \<subseteq># (M + N)"
    3.75 +    le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and
    3.76 +    le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)"
    3.77    using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+
    3.78  
    3.79  lemma
    3.80    fixes M N :: "('a \<Colon> linorder) multiset"
    3.81    shows
    3.82 -    less_multiset_plus_plus_left_iff[simp]: "M + N \<subset># M' + N \<longleftrightarrow> M \<subset># M'" and
    3.83 -    less_multiset_plus_plus_right_iff[simp]: "M + N \<subset># M + N' \<longleftrightarrow> N \<subset># N'"
    3.84 +    less_multiset_plus_plus_left_iff[simp]: "M + N #\<subset># M' + N \<longleftrightarrow> M #\<subset># M'" and
    3.85 +    less_multiset_plus_plus_right_iff[simp]: "M + N #\<subset># M + N' \<longleftrightarrow> N #\<subset># N'"
    3.86    unfolding less_multiset\<^sub>H\<^sub>O by auto
    3.87  
    3.88  lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
    3.89 @@ -288,21 +288,21 @@
    3.90  lemma
    3.91    fixes M N :: "('a \<Colon> linorder) multiset"
    3.92    shows
    3.93 -    less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N \<subset># M + N" and
    3.94 -    less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M \<subset># M + N"
    3.95 +    less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N #\<subset># M + N" and
    3.96 +    less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M #\<subset># M + N"
    3.97    using [[metis_verbose = false]]
    3.98    by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
    3.99      add.commute)+
   3.100  
   3.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"
   3.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"
   3.103    unfolding less_multiset\<^sub>H\<^sub>O by (metis less_irrefl less_nat_zero_code not_gr0)
   3.104  
   3.105  lemma ex_gt_count_imp_less_multiset:
   3.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"
   3.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"
   3.108    unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order
   3.109      less_not_sym mset_leD mset_le_add_left)  
   3.110  
   3.111 -lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N \<subset># P \<Longrightarrow> M - P + N \<subset># M"
   3.112 +lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
   3.113    by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2)
   3.114  
   3.115  end