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