Email Gateway (Feb 06 2026 at 09:12): 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
Email Gateway (Mar 02 2026 at 11:15):From: Makarius <makarius@sketis.net>
On 06/02/2026 10:11, Andrea Vezzosi wrote:
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?what I would wish for:
thm_deps (with_instantiations right_id) test (* dependencies: 3 protectD protectI right_id (x=1) *)
That would require more details in the internal recording inferences (or
rather proof terms), and is presently not feasible.
Makarius
Email Gateway (Mar 02 2026 at 11:46):From: Andrea Vezzosi <vezzosi.ndr@gmail.com>
On Mar 2 2026, at 12:14 pm, Makarius <makarius@sketis.net> wrote:
That would require more details in the internal recording inferences
(or
rather proof terms), and is presently not feasible.
Fair enough, thanks for confirming this. I ended up creating
pre-specialized theorems to work around it.
Best regards,
Andrea
Last updated: Mar 14 2026 at 08:38 UTC