[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.