Re: [isabelle] Canonical Proof Props



> Which leaves the canonical question: What application do you have in mind?

We're looking for stray unused lemmas in the seL4 verification proofs. These are (in some parts) old and (in all parts) large collections of proofs that have undergone more than a few refactorings. The technique of using proof node names to loosely infer "real" lemma names and their usage relationships, as well as proof node props to disambiguate/confirm those inferences, seems to be working so far, so I suppose I have no real issue yet.
________________________________________
From: Makarius <makarius at sketis.net>
Sent: Thursday, November 15, 2018 12:58 AM
To: Pierzchalski, Ed (Data61, Kensington NSW); cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] Canonical Proof Props

On 14/11/2018 08:18, Ed.Pierzchalski at data61.csiro.au wrote:
>
> I ran into the above while attempting to disambiguate the names that occur in proof bodies. That is, if a proof body refers to a prop `p` with name `"foo_1"`, I need to distinguish between `p` being proven by the first theorem in a thm list (`foo(1)`) or by a thm with the actual name `foo_1`. Since `Thm.full_prop_of` and proof bodies sometimes disagree, the easiest solution at the time was to use the proof body terms as a 'normal form', which seems unsatisfying. So, for my own education:
>
> - What is the canonical way to get the dependencies of a thm?
> - What is the canonical way to disambiguate between the first theorem of `foo` vs. a theorem named `foo_1`?

I occasionally ask myself the same questions. After so many years the
situation of proof terms is still not quite clear.

In particular, the concept did not catch up with the "authentic fact
name" reform from some years ago: In distant past, a fact name in the
theory was just a comment, and the slightly odd "disambiguation" wrt.
the proposition was used to make sense of in as proof terms. Now the
fact environment of the context is authentic, but proof terms still have
a rather weak notion of derivation name internally.

There are other fine points that don't quite work, e.g. see the
implementation of the commands 'thm_deps' and 'unused_thms'.


As usual, one needs to look very closely at the status-quo, and figure
out if a particular application has the chance to go through.

Which leaves the canonical question: What application do you have in mind?


        Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.