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.