Stream: Mirror: Isabelle Development Mailing List

Topic: Something weird in Nat.thy

Email Gateway (Dec 18 2024 at 22:03):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
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

Email Gateway (Dec 19 2024 at 09:16):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
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@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

smime.p7s

Email Gateway (Dec 19 2024 at 15:49):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
I don't understand why any refactoring would be necessary. If it is a case of for example replacing nat_induct by nat.induct, sure, although explicit references are rare (38 to be precise)

Larry

On 19 Dec 2024, at 09:15, Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de> wrote:

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.

Last updated: Feb 01 2025 at 20:19 UTC