added FIXMEs
authorblanchet
Tue Nov 07 15:16:40 2017 +0100 (19 months ago)
changeset 67020c32254ab1901
parent 67019 7a3724078363
child 67021 41f1f8c4259b
added FIXMEs
src/HOL/Library/Multiset_Order.thy
     1.1 --- a/src/HOL/Library/Multiset_Order.thy	Tue Nov 07 14:52:27 2017 +0100
     1.2 +++ b/src/HOL/Library/Multiset_Order.thy	Tue Nov 07 15:16:40 2017 +0100
     1.3 @@ -166,8 +166,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
     1.8 -  "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
     1.9 +lemma less_multiset_less_multiset\<^sub>H\<^sub>O: "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
    1.10    unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
    1.11  
    1.12  lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
    1.13 @@ -178,8 +177,8 @@
    1.14    unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
    1.15    by (simp add: less_le_not_le subseteq_mset_def)
    1.16  
    1.17 -lemma le_multiset_right_total:
    1.18 -  shows "M < add_mset x M"
    1.19 +(* FIXME: "le" should be "less" in this and other names *)
    1.20 +lemma le_multiset_right_total: "M < add_mset x M"
    1.21    unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
    1.22  
    1.23  lemma less_eq_multiset_empty_left[simp]:
    1.24 @@ -190,16 +189,18 @@
    1.25    unfolding less_multiset\<^sub>H\<^sub>O
    1.26    by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
    1.27  
    1.28 -lemma less_eq_multiset_empty_right[simp]:
    1.29 -  "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
    1.30 +lemma less_eq_multiset_empty_right[simp]: "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
    1.31    by (metis less_eq_multiset_empty_left antisym)
    1.32  
    1.33 +(* FIXME: "le" should be "less" in this and other names *)
    1.34  lemma le_multiset_empty_left[simp]: "M \<noteq> {#} \<Longrightarrow> {#} < M"
    1.35    by (simp add: less_multiset\<^sub>H\<^sub>O)
    1.36  
    1.37 +(* FIXME: "le" should be "less" in this and other names *)
    1.38  lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
    1.39    using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
    1.40  
    1.41 +(* FIXME: "le" should be "less" in this and other names *)
    1.42  lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
    1.43    by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
    1.44