src/HOL/Library/Extended_Nat.thy
 changeset 62376 85f38d5f8807 parent 62374 cb27a55d868a child 62378 85ed00c1fe7c
```     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Feb 09 09:21:10 2016 +0100
1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Feb 10 18:43:19 2016 +0100
1.3 @@ -62,6 +62,9 @@
1.4  lemma not_enat_eq [iff]: "(\<forall>y. x \<noteq> enat y) = (x = \<infinity>)"
1.5    by (cases x) auto
1.6
1.7 +lemma enat_ex_split: "(\<exists>c::enat. P c) \<longleftrightarrow> P \<infinity> \<or> (\<exists>c::nat. P c)"
1.8 +  by (metis enat.exhaust)
1.9 +
1.10  primrec the_enat :: "enat \<Rightarrow> nat"
1.11    where "the_enat (enat n) = n"
1.12
1.13 @@ -359,11 +362,16 @@
1.14
1.15  end
1.16
1.17 -instance enat :: ordered_comm_semiring
1.18 +instance enat :: dioid
1.19 +proof
1.20 +  fix a b :: enat show "(a \<le> b) = (\<exists>c. b = a + c)"
1.21 +    by (cases a b rule: enat2_cases) (auto simp: le_iff_add enat_ex_split)
1.22 +qed
1.23 +
1.24 +instance enat :: "ordered_comm_semiring"
1.25  proof
1.26    fix a b c :: enat
1.27 -  assume "a \<le> b" and "0 \<le> c"
1.28 -  thus "c * a \<le> c * b"
1.29 +  assume "a \<le> b" and "0 \<le> c" thus "c * a \<le> c * b"
1.30      unfolding times_enat_def less_eq_enat_def zero_enat_def
1.31      by (simp split: enat.splits)
1.32  qed
```