Something weird in Nat.thy

[Jasmin Blanchette]

Hi Larry,

According to "hg annotate", I'm the guilty party here. I think the idea was that these lemmas were indeed already derived ad hoc and I wanted to avoid duplicates -- and probably I was too lazy or not courageous enough to get rid of the ad hoc versions and enforce the new versions throughout. By all means, if you or anybody else wants to refactor this, go ahead.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html


> On 18. Dec 2024, at 22:53, Lawrence Paulson via isabelle-dev <isabelle-dev at mailman.proof.cit.tum.de> wrote:
> 
> This theory sets up type “nat” as a standard datatype. But then it hides everything. I am okay with the hide_const for pred, but some of the facts being hidden are useful and are even derived again later in an ad-hoc manner. Any ideas why?
> 
> hide_const (open) Nat.pred ― ‹hide everything related to the selector›
> hide_fact
>  nat.case_eq_if
>  nat.collapse
>  nat.expand
>  nat.sel
>  nat.exhaust_sel
>  nat.split_sel
>  nat.split_sel_asm
> 
> Larry
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20241219/edcd1cdc/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4674 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20241219/edcd1cdc/attachment.bin>