# [isabelle] looking for some measure.union_inter theorem

Hi all,
I am trying to demonstrate the following probability lemma (prob being defined as a measure in a prob_space according to the Probability library) :
"⋀ A B. finite A ⟹ finite B ⟹ prob (A ∪ B) + prob (A ∩ B) = prob A + prob B"
The closer theorem I could discover in the Isabelle/HOL library is Finite_Set.folding_image_simple.union_inter.
Si I am trying this:
have "⋀ A B. finite A ⟹ finite B ⟹ prob (A ∪ B) + prob (A ∩ B) = prob A + prob B"
proof -
fix A B::"(nat×'proc ⇒ bool) set"
assume A:"finite A" and B:"finite B"
show "prob (A ∪ B) + prob (A ∩ B) = prob A + prob B"
proof (intro folding_image_simple.union_inter [OF _ A B, of "op +" "0::real" "λω. prob {ω}" prob], default)
There, it output I should now demonstrate that:
⋀A. finite A ⟹ prob A = fold_image op + (λω. prob {ω}) 0 A
I feel a little lost from this point, as I do not understand why f(A) + 0 = f(A) for any peculiar function f ! As far a I know, this is part of the addition definition.
Any clue ?
Thanks in advance.
H.

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