src/HOL/UNITY/Detects.thy
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 8334 7896bcbd8641
child 13785 e2fcd88be55d
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:

(*  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