Re: [isabelle] Theorem dependencies in jEdit



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
----------------------------------------------------------------------------




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