src/HOL/UNITY/WFair.thy
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5155 21177b8a4d7f
permissions -rw-r--r--
New UNITY theory
     1 (*  Title:      HOL/UNITY/WFair
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Weak Fairness versions of transient, ensures, leadsTo.
     7 
     8 From Misra, "A Logic for Concurrent Programming", 1994
     9 *)
    10 
    11 WFair = Traces + Vimage +
    12 
    13 constdefs
    14 
    15   transient :: "[('a * 'a)set set, 'a set] => bool"
    16     "transient Acts A == EX act:Acts. A <= Domain act & act^^A <= Compl A"
    17 
    18   ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
    19     "ensures Acts A B == constrains Acts (A-B) (A Un B) & transient Acts (A-B)"
    20 
    21 consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
    22        leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
    23   
    24 translations
    25   "leadsTo Acts A B" == "(A,B) : leadsto Acts"
    26 
    27 inductive "leadsto Acts"
    28   intrs 
    29 
    30     Basis  "ensures Acts A B ==> leadsTo Acts A B"
    31 
    32     Trans  "[| leadsTo Acts A B;  leadsTo Acts B C |]
    33 	   ==> leadsTo Acts A C"
    34 
    35     Union  "(UN A:S. {(A,B)}) : Pow (leadsto Acts)
    36 	   ==> leadsTo Acts (Union S) B"
    37 
    38   monos "[Pow_mono]"
    39 
    40 constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
    41   "wlt Acts B == Union {A. leadsTo Acts A B}"
    42 
    43 end