Re: [isabelle] unused_thms in proofs



On Tue, 3 May 2016, Thomas Sewell wrote:

Well, they could be optionally given dummy names. That would break the usual rule that names in the PThms (other than Pure.blah) look up facts, but would allow you to check whether they were really used.

The names in PThm nodes are not even right for global facts. It is an old confusion that is still there until today.


The other option would be to check whether they were syntactically used, of course.

That is the dual approach to inspecting the internal inferences: looking at the source with its PIDE markup. Recently I have already added some rendering for the use of formal entities, visually connecting definitions and references of items. This includes facts, but there are more ways to refer to facts than for most other items:

  (1) via literal fact references (backquotes or cartouche notation)

  (2) via declarations that put them into the context for tools to pick
    them up later, e.g. the "simp" attribute and "simp" proof method

(1) might soon be included in the PIDE markup model: it is syntactically relatively clear. (2) is more difficult, because the absence or presence of a "simp del" declaration can affect the proof. It might be better just to test-run the proof document, and see if it still works with or without certain elements.


	Makarius




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