Email Gateway (Aug 19 2022 at 16:51): Email Gateway (Aug 19 2022 at 16:51):From: Joachim Breitner <breitner@kit.edu>
Dear List,
in order to get a better handle on my formalizations I’d like to build
some tools, similar to unused_thms, that can aid guide my reorganization
of lemmas and theories. The data I need for that are the theory graph
and the lemma dependencies.
I found this code to extract the list of theorems used by a particular
theorem:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2006-March/msg00091.html
which I adjusted to today’s definition of PThm.
In that thread it is noted that "-p 1" has to be used. Is that
information still valid in 2014? I could not find a mention of this
option in the systems manual nor "isabelle jedit --help". Note that I do
not care about the dependencies on lemmas in the underlying heap (if
that makes a difference).
It seems that adding
ML "Proofterm.proofs := 2"
to the top of my developments makes the code above actually do something
useful, but not ":= 1", which I presume corresponds to what "-p 1" used
to be. Is this mode "1" still supported?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 16:51):From: Lars Noschinski <noschinl@in.tum.de>
On 18.12.2014 11:24, Joachim Breitner wrote:
in order to get a better handle on my formalizations I’d like to build
some tools, similar to unused_thms, that can aid guide my reorganization
of lemmas and theories. The data I need for that are the theory graph
and the lemma dependencies.I found this code to extract the list of theorems used by a particular
theorem:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2006-March/msg00091.html
which I adjusted to today’s definition of PThm.
There should be some newer code for that, written by Lukas Bulwahn and
Rafal Kolanski about two years ago. IIRC it went into the Isabelle Cookbook.
Have a look at the stuff around page 66 (in chapter 3.7 Theorems)
There ought to be some newer code in the Isabelle Cookbook (generated
from changeset 8d30446d89f0).
In that thread it is noted that "-p 1" has to be used. Is that
information still valid in 2014? I could not find a mention of this
option in the systems manual nor "isabelle jedit --help". Note that I do
not care about the dependencies on lemmas in the underlying heap (if
that makes a difference).
As far as I understand, the default level of 0 already stores the
references to named theorems, so there should be no need to enable more
detailed proof terms.
-- Lars
signature.asc
Email Gateway (Aug 19 2022 at 16:51):From: Joachim Breitner <breitner@kit.edu>
Hi Lars,
Am Donnerstag, den 18.12.2014, 11:47 +0100 schrieb Lars Noschinski:
On 18.12.2014 11:24, Joachim Breitner wrote:
There should be some newer code for that, written by Lukas Bulwahn and
Rafal Kolanski about two years ago. IIRC it went into the Isabelle Cookbook.Have a look at the stuff around page 66 (in chapter 3.7 Theorems)
There ought to be some newer code in the Isabelle Cookbook (generated
from changeset 8d30446d89f0).
thanks for the pointer. I often forget about the Cookboook. Is there a
good reason it is not included with the other documentation that comes
with Isabelle?
Based on the information there I came up with this code that traverses
the tree of used theorems, stopping at those that have a name:
fun thms_used_by_thm thm =
let
fun used_by_proof_body (PBody {thms, ...}) = thms |> map #2 |> map go |> List.concat
and go ("", _, pbodyf) = pbodyf |> Future.join |> used_by_proof_body
| go (s, _, _) = [s]
in thm |> Thm.proof_body_of |> Proofterm.strip_thm |> used_by_proof_body
end;
As far as I understand, the default level of 0 already stores the
references to named theorems, so there should be no need to enable more
detailed proof terms.
Indeed, thanks!
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 16:51):From: Makarius <makarius@sketis.net>
On Thu, 18 Dec 2014, Joachim Breitner wrote:
I often forget about the Cookboook. Is there a good reason it is not
included with the other documentation that comes with Isabelle?
The Cookbook is generally lagging behind in accuracy and quality. Many
things in it have a point and many things are very odd or outright wrong.
I have pointed out small and big mistakes quite often in the past, but it
did not improve much. Moreover, Isabelle has changed quite substantially
since the start of the Cookbook, but it did not catch up.
Based on the information there I came up with this code that traverses
the tree of used theorems, stopping at those that have a name:fun thms_used_by_thm thm =
let
fun used_by_proof_body (PBody {thms, ...}) = thms |> map #2 |> map go |> List.concat
and go ("", _, pbodyf) = pbodyf |> Future.join |> used_by_proof_body
| go (s, _, _) = [s]
in thm |> Thm.proof_body_of |> Proofterm.strip_thm |> used_by_proof_body
end;As far as I understand, the default level of 0 already stores the
references to named theorems, so there should be no need to enable more
detailed proof terms.
PThm names are always stored since about 2008. None of this really works,
though. Even 'unused_thms' remained unfinished over many years until
today, and has a bunch of conceptual problems.
There is no point to make 2-3 half-working variants of something that
needs to be done right once and for all. Anything else is just a waste of
time -- it actually prevents to get things right eventually.
Makarius
http://stop-ttip.org 1,169,875 people so far
Last updated: Apr 26 2024 at 16:20 UTC