produce _def and _val theorems in value_type

[lsf37]

Produce a _def theorem for the value type that provides direct symbolic access to the right-hand side of the value_type definition. This avoids having to unfold those terms in subsequent proofs.

The numeric value as as term is still available as <type-name>_val.

value_type is now restricted to types nat and int on the right-hand side (int being cast to nat automatically). Other types can still be used, but have to be cast to nat manually. It turns out that so far we have only needed int and nat, so this works out without changes to any of the value_type definitions.

[lsf37]

I haven't yet used the new _def theorems to eliminate previous manual instance of that, because my first search&replace attempt turned out to be too aggressive. I might add another commit to this PR for that, but the current state at least works and is worth looking at.

[Xaphiosis]

I think this is a solid start (going via _val for now). Content looks good. For aarch64 branch, we'll have to do the update as well. Maybe after pre-VSpace_C, but before VSpace_C. Thoughts?

Commits:

• lib: produce _def and _val thes in value_type : thms?
• is it worth repeating that it's for nat/int in the commit message?
• proof: proof updates for value_type _def -> _val - you can probably skip the second proof here
• Rename _def into _val occurrences for value_type name. Does not make full use of value_type _def theorems yet. - this is hard to understand, perhaps the word "generated" could make an appearance to help? "Rename occurrences of _def to _val for value_type-generated names." ?

[Xaphiosis]

@michaelmcinerney should possibly be aware this is in the queue

[lsf37]

I think this is a solid start (going via _val for now). Content looks good. For aarch64 branch, we'll have to do the update as well. Maybe after pre-VSpace_C, but before VSpace_C. Thoughts?

Let's not block anything on this one. I'm happy to do the rebase whenever it goes in and the aarch64 branch is ready for it.

Commits:

• lib: produce _def and _val thes in value_type : thms?
• is it worth repeating that it's for nat/int in the commit message?
• proof: proof updates for value_type _def -> _val - you can probably skip the second proof here
• Rename _def into _val occurrences for value_type name. Does not make full use of value_type _def theorems yet. - this is hard to understand, perhaps the word "generated" could make an appearance to help? "Rename occurrences of _def to _val for value_type-generated names." ?

Thanks, will go through these

• lib: produce _def and _val thes in value_type : thms
• repeat that it's for nat/int in the commit message
• proof: proof updates for value_type _def -> _val - skip the second proof
• Rename _def into _val occurrences for value_type name. Does not make full use of value_type _def theorems yet. - "Rename occurrences of _def to _val for value_type-generated names." ?

[corlewis]

I haven't used value_type myself so can't comment on the practicalities of the change, but this looks good to me.

As another nitpick; in the first commit message - "The numeric value as 'a' term"