src/HOL/UNITY/WFair.thy
 changeset 6536 281d44905cab parent 5931 325300576da7 child 6801 9e0037839d63
equal 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 `
`    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`