## Stream: Mirror: Isabelle Users Mailing List

### Topic: [isabelle] unused_thms in composed theorems

#### Email Gateway (Feb 19 2021 at 14:04):

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