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