src/HOL/UNITY/WFair.thy
author paulson
Thu Oct 15 11:35:07 1998 +0200 (1998-10-15)
changeset 5648 fe887910e32e
parent 5340 d75c03cf77b5
child 5721 458a67fd5461
permissions -rw-r--r--
specifications as sets of programs
paulson@4776
     1
(*  Title:      HOL/UNITY/WFair
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Weak Fairness versions of transient, ensures, leadsTo.
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming", 1994
paulson@4776
     9
*)
paulson@4776
    10
paulson@5277
    11
WFair = UNITY +
paulson@4776
    12
paulson@4776
    13
constdefs
paulson@4776
    14
paulson@5155
    15
  (*This definition specifies weak fairness.  The rest of the theory
paulson@5155
    16
    is generic to all forms of fairness.*)
paulson@5648
    17
  transient :: "'a set => 'a program set"
paulson@5648
    18
    "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}"
paulson@4776
    19
paulson@5648
    20
  ensures :: "['a set, 'a set] => 'a program set"
paulson@5648
    21
    "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
paulson@5648
    22
paulson@5648
    23
paulson@5648
    24
consts leadsto :: "'a program => ('a set * 'a set) set"
paulson@4776
    25
  
paulson@5648
    26
inductive "leadsto F"
paulson@4776
    27
  intrs 
paulson@4776
    28
paulson@5648
    29
    Basis  "F : ensures A B ==> (A,B) : leadsto F"
paulson@4776
    30
paulson@5648
    31
    Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
paulson@5648
    32
	   ==> (A,C) : leadsto F"
paulson@4776
    33
paulson@5155
    34
    (*Encoding using powerset of the desired axiom
paulson@5648
    35
       (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F
paulson@5155
    36
    *)
paulson@5648
    37
    Union  "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F"
paulson@4776
    38
paulson@4776
    39
  monos "[Pow_mono]"
paulson@4776
    40
paulson@5155
    41
paulson@5648
    42
  
paulson@5648
    43
constdefs (*visible version of the relation*)
paulson@5648
    44
  leadsTo :: "['a set, 'a set] => 'a program set"
paulson@5648
    45
    "leadsTo A B == {F. (A,B) : leadsto F}"
paulson@5648
    46
  
paulson@5648
    47
  (*wlt F B is the largest set that leads to B*)
paulson@5648
    48
  wlt :: "['a program, 'a set] => 'a set"
paulson@5648
    49
    "wlt F B == Union {A. F: leadsTo A B}"
paulson@4776
    50
paulson@4776
    51
end