Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Immediate theorem dependencies (like thm_deps)...

Email Gateway (Feb 06 2026 at 09:12):

From: Andrea Vezzosi <vezzosi.ndr@gmail.com>

Dear Mailing list,

the thm_deps command shows the lemmas used to prove a theorem, how hard
would it be to implement a version that also prints out the
instantiation of free variables, at least for a specified subset of theorems?

An example below to clarify:

lemma right_id : "x + 0 = x"
  sorry

lemma test : "1 + 0 = 1"
  by (rule right_id)
  done

Here's what I get from thm_deps test:

dependencies: 3
    protectD
    protectI
    right_id

what I would wish for:

thm_deps (with_instantiations right_id) test
(*
dependencies: 3
    protectD
    protectI
    right_id (x=1)
*)

or actually just an equivalent Isabelle/ML function of a type like
thm list -> thm -> (thm * term list) list.

Best regards,
Andrea

Last updated: Feb 22 2026 at 05:16 UTC