equal
deleted
inserted
replaced
1160 primrec |
1160 primrec |
1161 of_nat :: "nat \<Rightarrow> 'a" |
1161 of_nat :: "nat \<Rightarrow> 'a" |
1162 where |
1162 where |
1163 of_nat_0: "of_nat 0 = 0" |
1163 of_nat_0: "of_nat 0 = 0" |
1164 | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m" |
1164 | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m" |
|
1165 declare of_nat.simps [code] |
1165 |
1166 |
1166 lemma of_nat_1 [simp]: "of_nat 1 = 1" |
1167 lemma of_nat_1 [simp]: "of_nat 1 = 1" |
1167 by simp |
1168 by simp |
1168 |
1169 |
1169 lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n" |
1170 lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n" |