src/HOL/UNITY/WFair.thy
author paulson
Wed Nov 18 15:10:46 1998 +0100 (1998-11-18)
changeset 5931 325300576da7
parent 5721 458a67fd5461
child 6536 281d44905cab
permissions -rw-r--r--
Finally removing "Compl" from HOL
     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 = UNITY +
    12 
    13 constdefs
    14 
    15   (*This definition specifies weak fairness.  The rest of the theory
    16     is generic to all forms of fairness.*)
    17   transient :: "'a set => 'a program set"
    18     "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
    19 
    20   ensures :: "['a set, 'a set] => 'a program set"
    21     "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
    22 
    23 
    24 consts leadsto :: "'a program => ('a set * 'a set) set"
    25   
    26 inductive "leadsto F"
    27   intrs 
    28 
    29     Basis  "F : ensures A B ==> (A,B) : leadsto F"
    30 
    31     Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
    32 	   ==> (A,C) : leadsto F"
    33 
    34     (*Encoding using powerset of the desired axiom
    35        (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F
    36     *)
    37     Union  "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F"
    38 
    39   monos Pow_mono
    40 
    41 
    42   
    43 constdefs (*visible version of the relation*)
    44   leadsTo :: "['a set, 'a set] => 'a program set"
    45     "leadsTo A B == {F. (A,B) : leadsto F}"
    46   
    47   (*wlt F B is the largest set that leads to B*)
    48   wlt :: "['a program, 'a set] => 'a set"
    49     "wlt F B == Union {A. F: leadsTo A B}"
    50 
    51 end