[isabelle] Question about numerals

[Jørgen Villadsen]

Hi,

In the example:

lemmas numeral_nat = eval_nat_numeral BitM.simps One_nat_def

lemma "dummy (0::nat) (1::nat) (2::nat) (3::nat)"
unfolding numeral_nat

I get the state:

1. dummy 0 (Suc 0) (Suc (Suc 0)) (Suc (Suc (Suc 0)))

which is what I want - but is there a better way?

The following works for 2 only:

lemma "dummy (0::nat) (1::nat) (2::nat) (3::nat)"
unfolding numerals

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.

Thanks,

Jørgen

[Lawrence Paulson]

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)

[Lars Hupel]

Post by Jørgen Villadsen
It is used once in HOL/ex/Primrec.thy but it seems that it can be omitted.

That one yes, but there's also a non-trivial occurence in HOL, namely in
a tactic in "Semiring_Normalization". While a naive cleanup is possible
(inline the lemma in the tactic), I don't think this is a good idea.

Cheers
Lars