Jørgen Villadsen

2016-08-13 15:38:30 UTC

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

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