src/HOL/UNITY/Detects.thy

Added Tanja's Detects and Reachability theories. Also
changed object-quantifiers to meta-quantifiers in ball_constrains_UN/INT...

(*  Title:      HOL/UNITY/Detects
    ID:         $Id$
    Author:     Tanja Vos, Cambridge University Computer Laboratory
    Copyright   2000  University of Cambridge

Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
*)

Detects = WFair + Reach + 


consts
   op_Detects  :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
   op_Equality :: "['a set, 'a set] => 'a set"          (infixl "<==>" 60)
   
defs
  Detects_def "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
  Equality_def "A <==> B == (-A Un B) Int (A Un -B)"

end