equal
deleted
inserted
replaced
3 Copyright 2000 University of Cambridge |
3 Copyright 2000 University of Cambridge |
4 |
4 |
5 Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo |
5 Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo |
6 *) |
6 *) |
7 |
7 |
8 section{*The Detects Relation*} |
8 section\<open>The Detects Relation\<close> |
9 |
9 |
10 theory Detects imports FP SubstAx begin |
10 theory Detects imports FP SubstAx begin |
11 |
11 |
12 definition Detects :: "['a set, 'a set] => 'a program set" (infixl "Detects" 60) |
12 definition Detects :: "['a set, 'a set] => 'a program set" (infixl "Detects" 60) |
13 where "A Detects B = (Always (-A \<union> B)) \<inter> (B LeadsTo A)" |
13 where "A Detects B = (Always (-A \<union> B)) \<inter> (B LeadsTo A)" |