src/HOL/Library/Multiset.thy
changeset 59958 4538d41e8e54
parent 59949 fc4c896c8e74
child 59986 f38b94549dc8
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Apr 08 15:04:06 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Apr 08 15:21:20 2015 +0200
     1.3 @@ -1778,21 +1778,21 @@
     1.4  
     1.5  subsubsection {* Partial-order properties *}
     1.6  
     1.7 -definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
     1.8 -  "M' <# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
     1.9 -
    1.10 -definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
    1.11 -  "M' <=# M \<longleftrightarrow> M' <# M \<or> M' = M"
    1.12 -
    1.13 -notation (xsymbols) less_multiset (infix "\<subset>#" 50)
    1.14 -notation (xsymbols) le_multiset (infix "\<subseteq>#" 50)
    1.15 +definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<#" 50) where
    1.16 +  "M' #<# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
    1.17 +
    1.18 +definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<=#" 50) where
    1.19 +  "M' #<=# M \<longleftrightarrow> M' #<# M \<or> M' = M"
    1.20 +
    1.21 +notation (xsymbols) less_multiset (infix "#\<subset>#" 50)
    1.22 +notation (xsymbols) le_multiset (infix "#\<subseteq>#" 50)
    1.23  
    1.24  interpretation multiset_order: order le_multiset less_multiset
    1.25  proof -
    1.26 -  have irrefl: "\<And>M :: 'a multiset. \<not> M \<subset># M"
    1.27 +  have irrefl: "\<And>M :: 'a multiset. \<not> M #\<subset># M"
    1.28    proof
    1.29      fix M :: "'a multiset"
    1.30 -    assume "M \<subset># M"
    1.31 +    assume "M #\<subset># M"
    1.32      then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
    1.33      have "trans {(x'::'a, x). x' < x}"
    1.34        by (rule transI) simp
    1.35 @@ -1809,13 +1809,13 @@
    1.36        by (induct rule: finite_induct) (auto intro: order_less_trans)
    1.37      with aux1 show False by simp
    1.38    qed
    1.39 -  have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
    1.40 +  have trans: "\<And>K M N :: 'a multiset. K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># N"
    1.41      unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
    1.42    show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
    1.43      by default (auto simp add: le_multiset_def irrefl dest: trans)
    1.44  qed
    1.45  
    1.46 -lemma mult_less_irrefl [elim!]: "M \<subset># (M::'a::order multiset) ==> R"
    1.47 +lemma mult_less_irrefl [elim!]: "M #\<subset># (M::'a::order multiset) ==> R"
    1.48    by simp
    1.49  
    1.50  
    1.51 @@ -1829,21 +1829,21 @@
    1.52  apply (simp add: add.assoc)
    1.53  done
    1.54  
    1.55 -lemma union_less_mono2: "B \<subset># D ==> C + B \<subset># C + (D::'a::order multiset)"
    1.56 +lemma union_less_mono2: "B #\<subset># D ==> C + B #\<subset># C + (D::'a::order multiset)"
    1.57  apply (unfold less_multiset_def mult_def)
    1.58  apply (erule trancl_induct)
    1.59   apply (blast intro: mult1_union)
    1.60  apply (blast intro: mult1_union trancl_trans)
    1.61  done
    1.62  
    1.63 -lemma union_less_mono1: "B \<subset># D ==> B + C \<subset># D + (C::'a::order multiset)"
    1.64 +lemma union_less_mono1: "B #\<subset># D ==> B + C #\<subset># D + (C::'a::order multiset)"
    1.65  apply (subst add.commute [of B C])
    1.66  apply (subst add.commute [of D C])
    1.67  apply (erule union_less_mono2)
    1.68  done
    1.69  
    1.70  lemma union_less_mono:
    1.71 -  "A \<subset># C ==> B \<subset># D ==> A + B \<subset># C + (D::'a::order multiset)"
    1.72 +  "A #\<subset># C ==> B #\<subset># D ==> A + B #\<subset># C + (D::'a::order multiset)"
    1.73    by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans)
    1.74  
    1.75  interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset
    1.76 @@ -2044,19 +2044,19 @@
    1.77    multiset_inter_left_commute
    1.78  
    1.79  lemma mult_less_not_refl:
    1.80 -  "\<not> M \<subset># (M::'a::order multiset)"
    1.81 +  "\<not> M #\<subset># (M::'a::order multiset)"
    1.82    by (fact multiset_order.less_irrefl)
    1.83  
    1.84  lemma mult_less_trans:
    1.85 -  "K \<subset># M ==> M \<subset># N ==> K \<subset># (N::'a::order multiset)"
    1.86 +  "K #\<subset># M ==> M #\<subset># N ==> K #\<subset># (N::'a::order multiset)"
    1.87    by (fact multiset_order.less_trans)
    1.88  
    1.89  lemma mult_less_not_sym:
    1.90 -  "M \<subset># N ==> \<not> N \<subset># (M::'a::order multiset)"
    1.91 +  "M #\<subset># N ==> \<not> N #\<subset># (M::'a::order multiset)"
    1.92    by (fact multiset_order.less_not_sym)
    1.93  
    1.94  lemma mult_less_asym:
    1.95 -  "M \<subset># N ==> (\<not> P ==> N \<subset># (M::'a::order multiset)) ==> P"
    1.96 +  "M #\<subset># N ==> (\<not> P ==> N #\<subset># (M::'a::order multiset)) ==> P"
    1.97    by (fact multiset_order.less_asym)
    1.98  
    1.99  ML {*