From: Stepan Holub <holub@karlin.mff.cuni.cz>

Dear list,

I am aware of the "unfinished" status of unused_thms command.

Nevertheless, I want to point out its unsatisfactory behavior for

composed theorems.

In

=============

theory Unused

imports Main

begin

lemma eq: assumes "a = (1::nat)" shows "a + a = 2" and "0 + 1 + a = a + a"

using assms by simp+

unused_thms

end

===============

the output for unused_thms is

??.Unused.eq_1: ?a = 1 ⟹ ?a + ?a = 2

If either of the two claims of eq is used, the lemma is not listed at all.

If the claims are given separate names:

lemma assumes "a = (1::nat)" shows eq1: "a + a = 2" and eq2: "0 + 1 +

a = a + a"

only the eq1 is listed, and it disappears even if eq2 is used:

======================

theory Unused

imports Main

begin

lemma assumes "a = (1::nat)" shows eq1: "a + a = 2" and eq2: "0 + 1 +

a = a + a"

using assms by simp+

lemma eq3: assumes "a = (1::nat)" shows "0 + 1 + a + 1 = a + a + 1"

unfolding eq2[OF assms] by simp

unused_thms

end

======================

Stepan

Last updated: Dec 08 2021 at 09:20 UTC