equal
deleted
inserted
replaced
132 lemma zero_ne_eSuc [simp]: "0 \<noteq> eSuc n" |
132 lemma zero_ne_eSuc [simp]: "0 \<noteq> eSuc n" |
133 by (rule eSuc_ne_0 [symmetric]) |
133 by (rule eSuc_ne_0 [symmetric]) |
134 |
134 |
135 lemma eSuc_inject [simp]: "eSuc m = eSuc n \<longleftrightarrow> m = n" |
135 lemma eSuc_inject [simp]: "eSuc m = eSuc n \<longleftrightarrow> m = n" |
136 by (simp add: eSuc_def split: enat.splits) |
136 by (simp add: eSuc_def split: enat.splits) |
|
137 |
|
138 lemma eSuc_enat_iff: "eSuc x = enat y \<longleftrightarrow> (\<exists>n. y = Suc n \<and> x = enat n)" |
|
139 by (cases y) (auto simp: enat_0 eSuc_enat[symmetric]) |
|
140 |
|
141 lemma enat_eSuc_iff: "enat y = eSuc x \<longleftrightarrow> (\<exists>n. y = Suc n \<and> enat n = x)" |
|
142 by (cases y) (auto simp: enat_0 eSuc_enat[symmetric]) |
137 |
143 |
138 subsection {* Addition *} |
144 subsection {* Addition *} |
139 |
145 |
140 instantiation enat :: comm_monoid_add |
146 instantiation enat :: comm_monoid_add |
141 begin |
147 begin |