src/HOL/UNITY/WFair.thy
 changeset 5648 fe887910e32e parent 5340 d75c03cf77b5 child 5721 458a67fd5461
equal 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`