# [isabelle] unused_thms in composed theorems

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

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