src/HOL/UNITY/WFair.thy
changeset 5648 fe887910e32e
parent 5340 d75c03cf77b5
child 5721 458a67fd5461
equal deleted inserted replaced
5647:4e8837255b87 5648:fe887910e32e
    12 
    12 
    13 constdefs
    13 constdefs
    14 
    14 
    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 * 'a)set set, 'a set] => bool"
    17   transient :: "'a set => 'a program set"
    18     "transient acts A == EX act:acts. A <= Domain act & act^^A <= Compl A"
    18     "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}"
    19 
    19 
    20   ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
    20   ensures :: "['a set, 'a set] => 'a program set"
    21     "ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)"
    21     "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
    22 			(*(unless acts A B) would be equivalent*)
       
    23 
    22 
    24 syntax leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
    23 
    25 consts leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
    24 consts leadsto :: "'a program => ('a set * 'a set) set"
    26   
    25   
    27 translations
    26 inductive "leadsto F"
    28   "leadsTo acts A B" == "(A,B) : leadsto acts"
       
    29   "~ leadsTo acts A B" <= "(A,B) ~: leadsto acts"
       
    30 
       
    31 inductive "leadsto acts"
       
    32   intrs 
    27   intrs 
    33 
    28 
    34     Basis  "ensures acts A B ==> leadsTo acts A B"
    29     Basis  "F : ensures A B ==> (A,B) : leadsto F"
    35 
    30 
    36     Trans  "[| leadsTo acts A B;  leadsTo acts B C |]
    31     Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
    37 	   ==> leadsTo acts A C"
    32 	   ==> (A,C) : leadsto F"
    38 
    33 
    39     (*Encoding using powerset of the desired axiom
    34     (*Encoding using powerset of the desired axiom
    40        (!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B
    35        (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F
    41     *)
    36     *)
    42     Union  "(UN A:S. {(A,B)}) : Pow (leadsto acts)
    37     Union  "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F"
    43 	   ==> leadsTo acts (Union S) B"
       
    44 
    38 
    45   monos "[Pow_mono]"
    39   monos "[Pow_mono]"
    46 
    40 
    47 
    41 
    48 (*wlt acts B is the largest set that leads to B*)
    42   
    49 constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
    43 constdefs (*visible version of the relation*)
    50   "wlt acts B == Union {A. leadsTo acts A B}"
    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}"
    51 
    50 
    52 end
    51 end