[isabelle-dev] the function "real"

[Tobias Nipkow]

On 12/11/2015 15:31, Lawrence Paulson wrote:
> There are a great many examples of theorems involving various coercion functions and the relations =, <, <=. In a number of cases, the “real” versions were declared as [iff]-rules, while the “of_nat/of_int” versions were declared as [simp]-rules only. When identifying the two, I decided it would make sense to go for iff, for maximum automation, but I now think this was a mistake. I’m trying the alternative right now.

Same here. I avoid modifications of the claset as much as possible these days 
because it can lead to proof searches going astray although the goal had nothing 
to do with those modifications.

Tobias

> Larry
>
>> On 12 Nov 2015, at 13:30, Tobias Nipkow <nipkow at in.tum.de> wrote:
>>
>> I am not surprised at all that the simplifier behaves differently because the simpset is modified all the time and is full of theorems wih coercions. But blast is another matter. Concrete questions:
>>
>> - Are there any coercion-related permanent intro/dest/elim theorems (either before or now)?
>>
>> - Could they kick in during a proof concerned only with basic set theory and first order logic?
>>
>> I want to make sure that it is not something else that caused blast to break.
>>
>> Tobias
>>
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151112/19194f98/attachment.bin>