Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Thu, 13 Oct 94 12:31:42 PDT
From: dfura@elvis.ds.boeing.com (David Fura)
Message-Id: <9410131931.AA20051@elvis.ds.boeing.com>
To: info-hol@leopard.cs.byu.edu
Subject: probability theory in HOL

Greetings,

Has anybody implemented probability theory in HOL or another
prover, or know about somebody who has?

I'm interested in representing probabilistic measures such as
'reliablity' and have a simple embedding that seems adequate
for this.  It's not very elegant though and I'd be open to
suggestions for improvement.  This topic may be of interest 
to others as well?

I use the libraries 'sets' and 'reals'.
 

% the type for an 'event' %
let V = ":(*s#*e#*p)set";;

% an event (over a predicate P) is defined as the set of tuples
  satisfying P % 
let EVENT = new_definition
   (`EVENT`,
     "! (P :*s->*e->*p->bool).
      EVENT P = { (s, e, p) | P s e p }"
   );;

% a 'placeholder' defn of probability (yuk) %
let PROB = new_definition
   (`PROB`,
    "! v :^V. PROB v = @n. &0 <= n /\ n <= &1"
   );;

% the axioms of probability (again yuk) 
  UNIV is the universal set, while INTER and UNION are the
  intersection and union operators % 
let PROB_AXIOMS_THM = mk_thm
   ([],
    "(!v:^V. PROB v >= &0) /\
     (PROB (UNIV:^V) = &1) /\
     (!v1 v2 :^V.
      (v1 INTER v2 = {}) ==> (PROB (v1 UNION v2) = PROB v1 + PROB v2))"
   );;

% here's a useful thm for manipulating probs % 
let LESS_EQ_PROBS = prove_thm
   (`LESS_EQ_PROBS`,
    "! (P1 P2 :*s->*e->*p->bool) .
     (!s e p. P1 s e p ==> P2 s e p) ==>
       (PROB (EVENT P1) <= PROB (EVENT P2))",

% and another %
let EVENT_PROBS_ADD = prove_thm
   (`EVENT_PROBS_ADD`,
    "! (P P1 P2 :*s->*e->*p->bool).
     (!s e p. ~(P1 s e p = P2 s e p)) ==>
       (!s e p. P s e p = P1 s e p \/ P2 s e p) ==>
         (PROB (EVENT P) = PROB (EVENT P1) + PROB (EVENT P2))",

Thanks,

Dave