src/HOL/UNITY/WFair.thy
changeset 6536 281d44905cab
parent 5931 325300576da7
child 6801 9e0037839d63
equal deleted inserted replaced
6535:880f31a62784 6536:281d44905cab
    15   (*This definition specifies weak fairness.  The rest of the theory
    15   (*This definition specifies weak fairness.  The rest of the theory
    16     is generic to all forms of fairness.*)
    16     is generic to all forms of fairness.*)
    17   transient :: "'a set => 'a program set"
    17   transient :: "'a set => 'a program set"
    18     "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
    18     "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
    19 
    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 
    20 
       
    21 consts
    23 
    22 
    24 consts leadsto :: "'a program => ('a set * 'a set) set"
    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 
    25   
    31   
    26 inductive "leadsto F"
    32 inductive "leadsto F"
    27   intrs 
    33   intrs 
    28 
    34 
    29     Basis  "F : ensures A B ==> (A,B) : leadsto F"
    35     Basis  "F : A ensures B ==> (A,B) : leadsto F"
    30 
    36 
    31     Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
    37     Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
    32 	   ==> (A,C) : leadsto F"
    38 	   ==> (A,C) : leadsto F"
    33 
    39 
    34     (*Encoding using powerset of the desired axiom
    40     (*Encoding using powerset of the desired axiom
    38 
    44 
    39   monos Pow_mono
    45   monos Pow_mono
    40 
    46 
    41 
    47 
    42   
    48   
    43 constdefs (*visible version of the relation*)
    49 defs
    44   leadsTo :: "['a set, 'a set] => 'a program set"
    50   ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
    45     "leadsTo A B == {F. (A,B) : leadsto F}"
    51 
       
    52   leadsTo_def "A leadsTo B == {F. (A,B) : leadsto F}"
       
    53 
       
    54 constdefs
    46   
    55   
    47   (*wlt F B is the largest set that leads to B*)
    56   (*wlt F B is the largest set that leads to B*)
    48   wlt :: "['a program, 'a set] => 'a set"
    57   wlt :: "['a program, 'a set] => 'a set"
    49     "wlt F B == Union {A. F: leadsTo A B}"
    58     "wlt F B == Union {A. F: A leadsTo B}"
    50 
    59 
    51 end
    60 end