Re: [isabelle] Question about numerals

> On 13 Aug 2016, at 16:33, JÃrgen Villadsen <jovi at> wrote:
> 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)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.