src/HOL/UNITY/Detects.thy
author paulson
Fri, 03 Mar 2000 18:26:19 +0100
changeset 8334 7896bcbd8641
child 13785 e2fcd88be55d
permissions -rw-r--r--
Added Tanja's Detects and Reachability theories. Also changed object-quantifiers to meta-quantifiers in ball_constrains_UN/INT...
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8334
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Detects
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     2
    ID:         $Id$
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     3
    Author:     Tanja Vos, Cambridge University Computer Laboratory
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     4
    Copyright   2000  University of Cambridge
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     5
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     6
Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     7
*)
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     8
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     9
Detects = WFair + Reach + 
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    10
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    11
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    12
consts
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    13
   op_Detects  :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    14
   op_Equality :: "['a set, 'a set] => 'a set"          (infixl "<==>" 60)
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    15
   
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    16
defs
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    17
  Detects_def "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    18
  Equality_def "A <==> B == (-A Un B) Int (A Un -B)"
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    19
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    20
end
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    21