src/HOL/Library/Extended_Nat.thy
changeset 45934 9321cd2572fe
parent 45775 6c340de26a0d
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Mon Dec 19 14:41:08 2011 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Dec 20 11:40:56 2011 +0100
     1.3 @@ -49,6 +49,9 @@
     1.4  
     1.5  declare [[coercion "enat::nat\<Rightarrow>enat"]]
     1.6  
     1.7 +lemmas enat2_cases = enat.exhaust[case_product enat.exhaust]
     1.8 +lemmas enat3_cases = enat.exhaust[case_product enat.exhaust enat.exhaust]
     1.9 +
    1.10  lemma not_infinity_eq [iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
    1.11    by (cases x) auto
    1.12  
    1.13 @@ -165,9 +168,9 @@
    1.14  instance proof
    1.15    fix n m q :: enat
    1.16    show "n + m + q = n + (m + q)"
    1.17 -    by (cases n, auto, cases m, auto, cases q, auto)
    1.18 +    by (cases n m q rule: enat3_cases) auto
    1.19    show "n + m = m + n"
    1.20 -    by (cases n, auto, cases m, auto)
    1.21 +    by (cases n m rule: enat2_cases) auto
    1.22    show "0 + n = n"
    1.23      by (cases n) (simp_all add: zero_enat_def)
    1.24  qed
    1.25 @@ -341,6 +344,14 @@
    1.26    "(\<infinity>::enat) < q \<longleftrightarrow> False"
    1.27    by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
    1.28  
    1.29 +lemma number_of_le_enat_iff[simp]:
    1.30 +  shows "number_of m \<le> enat n \<longleftrightarrow> number_of m \<le> n"
    1.31 +by (auto simp: number_of_enat_def)
    1.32 +
    1.33 +lemma number_of_less_enat_iff[simp]:
    1.34 +  shows "number_of m < enat n \<longleftrightarrow> number_of m < n"
    1.35 +by (auto simp: number_of_enat_def)
    1.36 +
    1.37  lemma enat_ord_code [code]:
    1.38    "enat m \<le> enat n \<longleftrightarrow> m \<le> n"
    1.39    "enat m < enat n \<longleftrightarrow> m < n"