src/HOL/UNITY/WFair.thy
author paulson
Thu Apr 29 10:51:58 1999 +0200 (1999-04-29)
changeset 6536 281d44905cab
parent 5931 325300576da7
child 6801 9e0037839d63
permissions -rw-r--r--
made many specification operators infix
     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 
    21 consts
    22 
    23   ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
    24 
    25   (*LEADS-TO constant for the inductive definition*)
    26   leadsto :: "'a program => ('a set * 'a set) set"
    27 
    28   (*visible version of the LEADS-TO relation*)
    29   leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
    30 
    31   
    32 inductive "leadsto F"
    33   intrs 
    34 
    35     Basis  "F : A ensures B ==> (A,B) : leadsto F"
    36 
    37     Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
    38 	   ==> (A,C) : leadsto F"
    39 
    40     (*Encoding using powerset of the desired axiom
    41        (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F
    42     *)
    43     Union  "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F"
    44 
    45   monos Pow_mono
    46 
    47 
    48   
    49 defs
    50   ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
    51 
    52   leadsTo_def "A leadsTo B == {F. (A,B) : leadsto F}"
    53 
    54 constdefs
    55   
    56   (*wlt F B is the largest set that leads to B*)
    57   wlt :: "['a program, 'a set] => 'a set"
    58     "wlt F B == Union {A. F: A leadsTo B}"
    59 
    60 end