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"
```