|
8334
|
1 |
(* Title: HOL/UNITY/Detects
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tanja Vos, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 2000 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Detects = WFair + Reach +
|
|
|
10 |
|
|
|
11 |
|
|
|
12 |
consts
|
|
|
13 |
op_Detects :: "['a set, 'a set] => 'a program set" (infixl "Detects" 60)
|
|
|
14 |
op_Equality :: "['a set, 'a set] => 'a set" (infixl "<==>" 60)
|
|
|
15 |
|
|
|
16 |
defs
|
|
|
17 |
Detects_def "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
|
|
|
18 |
Equality_def "A <==> B == (-A Un B) Int (A Un -B)"
|
|
|
19 |
|
|
|
20 |
end
|
|
|
21 |
|