Email Gateway (Feb 19 2021 at 14:04): 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: Jul 15 2022 at 23:21 UTC