*To*: <makarius at sketis.net>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Canonical Proof Props*From*: <Ed.Pierzchalski at data61.csiro.au>*Date*: Thu, 15 Nov 2018 01:10:32 +0000*Accept-language*: en-US, en-AU*In-reply-to*: <539a20f2-f581-e7d7-0510-72b52469c014@sketis.net>*References*: <1542179888916.28743@data61.csiro.au>, <539a20f2-f581-e7d7-0510-72b52469c014@sketis.net>*Thread-index*: AQHUe+oXF8VS+HIB8k2STHf2v6HBxqVOlAyAgAFrw9M=*Thread-topic*: [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

**References**:**[isabelle] Canonical Proof Props***From:*Ed.Pierzchalski

**Re: [isabelle] Canonical Proof Props***From:*Makarius

- Previous by Date: Re: [isabelle] Canonical Proof Props
- Next by Date: [isabelle] Finishing all proofs in use_thy
- Previous by Thread: Re: [isabelle] Canonical Proof Props
- Next by Thread: [isabelle] Finishing all proofs in use_thy
- Cl-isabelle-users November 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list