# Re: [isabelle] looking for some measure.union_inter theorem

Hi Henri,
while not a direct answer to your proof attempt, I believe that the lemma you are trying to prove is a simple consequence of existing lemmas:
prob(A \<union> B)
= prob((A - (A \<inter> B)) \<union> B) [by simple set theory]
= prob(A - (A \<inter> B)) + prob(B) [by lemma finite_measure_Union]
= (prob(A) - prob(A \<inter< B)) + prob(B) [by lemma finite_measure_Diff]
Hope this helps,
Stephan
On Nov 6, 2012, at 12:46 AM, Henri DEBRAT <henri.debrat at loria.fr> wrote:
> 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.*