added lemmas
authornipkow
Wed Feb 13 02:13:46 2019 +0100 (2 months ago)
changeset 6980074c1a0643010
parent 69799 18cb541a975f
child 69801 a99a0f5474c5
added lemmas
src/HOL/Library/Extended_Nat.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Sun Feb 10 22:24:22 2019 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Feb 13 02:13:46 2019 +0100
     1.3 @@ -392,6 +392,9 @@
     1.4  it does not have the cancellation property. Would it be worthwhile to
     1.5  a generalize linordered_semidom to a new class that includes enat? *)
     1.6  
     1.7 +lemma add_diff_assoc_enat: "z \<le> y \<Longrightarrow> x + (y - z) = x + y - (z::enat)"
     1.8 +by(cases x)(auto simp add: diff_enat_def split: enat.split)
     1.9 +
    1.10  lemma enat_ord_number [simp]:
    1.11    "(numeral m :: enat) \<le> numeral n \<longleftrightarrow> (numeral m :: nat) \<le> numeral n"
    1.12    "(numeral m :: enat) < numeral n \<longleftrightarrow> (numeral m :: nat) < numeral n"
    1.13 @@ -528,6 +531,9 @@
    1.14  lemma enat_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::enat) \<and> b < c"
    1.15    unfolding plus_enat_def by (simp split: enat.split)
    1.16  
    1.17 +lemma plus_eq_infty_iff_enat[simp]: "(m::enat) + n = \<infinity> \<longleftrightarrow> m=\<infinity> \<or> n=\<infinity>"
    1.18 +using enat_add_left_cancel by fastforce
    1.19 +
    1.20  ML \<open>
    1.21  structure Cancel_Enat_Common =
    1.22  struct