Re: [isabelle] Numeral is acting strangely



Lawrence Paulson wrote:
0 and 1 are constants in their own right. They are not made by number_of. Their number_of equivalents are displayed as Numeral0 and Numeral1. Having 0 and 1 as constants allows them to be involved in many axiomatic type classes concerning algebraic properties. Users normally should not notice.

A related issue: for type nat, while 1 = Suc 0, this is not a syntactic identity.

Larry Paulson



But there 's something more than this going on that seems odd.


> read "Numeral1";
val it = Const ("Numeral.Numeral1", "'a::Numeral.number") : Term.term

So Numeral1 is a constant in its own right

(tc is a smarter version of thms_containing)

> tc["Numeral1"];
Exception- ERROR "thms_containing: undeclared consts \"Numeral.Numeral1\""
   raised
> tc["Numeral.Numeral1"];
Exception- ERROR "thms_containing: undeclared consts \"Numeral.Numeral1\""
   raised

> Goal "Numeral1 = 1" ;
### Obsolete goal command encountered
Level 0 (1 subgoal)
number_of (Numeral.Pls BIT bit.B1) = (1::'a)
 1. number_of (Numeral.Pls BIT bit.B1) = (1::'a)

But here the constant "Numeral.Numeral1" somehow gets translated to
number_of (Numeral.Pls BIT bit.B1)

What is happening here?

Jeremy





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