Re: [isabelle] Theorem dependencies in jEdit



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

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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