Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Trying to simplify with setsum

Email Gateway (Aug 17 2022 at 13:28):

From: John Matthews <matthews@galois.com>
Hi,

I am trying to simplify a subgoal that contains an occurrence of
setsum, using the theorem setsum_Un. However, Isabelle refuses to
match the LHS of setsum_Un with the appropriate subterm. Here's a
nonsensical lemma to show what I mean:

lemma
"setsum (f::nat => nat) (ran ((a::nat ~=> nat) | A) \<union> ran (a | B)) = Z"

None of the following tactics work:

apply (subst setsum_Un)
apply (auto simp only: setsum_Un)
apply (erule_tac setsum_Un[THEN ssubst])

I think I'm either missing something obvious, or else that the type
'nat' has not been made an instance of the appropriate axclasses.

Thanks,
-john

Last updated: Nov 21 2024 at 12:39 UTC