[isabelle] Question about numerals



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




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