*Post by JÃ¸rgen Villadsen*Is the fact "Num.numerals" useful at all?

It is used once in HOL/ex/Primrec.thy but it seems that it can be omitted.

It is literally this:

lemma numerals: "Numeral1 = (1::nat)" "2 = Suc (Suc 0)"

by (rule numeral_One) (rule numeral_2_eq_2)

I certainly don’t see the point of making a special case of 1 and 2, especially given that it is almost never used. There are a few uses in the AFP, see below. I’m sure they could all be eliminated easily. I’m not sure who would volunteer to do this.

Larry Paulson

/Applicative_Lifting/Combinators.thy: then show ?thesis by (simp add: numerals)

/Card_Number_Partitions/Card_Number_Partitions.thy: from this show ?thesis by (auto simp add: numerals(2))

/Card_Number_Partitions/Card_Number_Partitions.thy: by (simp add: numerals(2) del: Partition.simps)

/Program-Conflict-Analysis/ConstraintSystems.thy: from S_ENTRY_PAT[of "{#q#}+{#q'#}", simplified] REVSPLIT(1) REVSPLIT'(1) have S_ENTRY: "(v, mon_w fg w, {#q#} + {#q'#}) \<in> S_cs fg (2::nat)" by (simp add: numerals)

/Regular_Algebras/Dioid_Power_Sum.thy:lemmas powsum_simps = powsum_def atLeastAtMostSuc_conv numerals

/Tree_Decomposition/TreewidthTree.thy: lessI less_or_eq_imp_le numerals(2))

/Word_Lib/Word_Lemmas.thy: by (metis numerals(1) power_not_zero power_zero_numeral)