src/HOL/UNITY/WFair.thy
author paulson
Thu Aug 24 12:39:24 2000 +0200 (2000-08-24)
changeset 9685 6d123a7e30bd
parent 8006 299127ded09d
child 10293 354e885b3e0a
permissions -rw-r--r--
xsymbols for leads-to and Join
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@5931
    18
    "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
paulson@4776
    19
paulson@8006
    20
  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
paulson@8006
    21
    "A ensures B == (A-B co A Un B) Int transient (A-B)"
paulson@8006
    22
paulson@6536
    23
paulson@6536
    24
consts
paulson@6536
    25
paulson@6536
    26
  (*LEADS-TO constant for the inductive definition*)
paulson@6801
    27
  leads :: "'a program => ('a set * 'a set) set"
paulson@5648
    28
paulson@6801
    29
paulson@6801
    30
inductive "leads F"
paulson@4776
    31
  intrs 
paulson@4776
    32
paulson@6801
    33
    Basis  "F : A ensures B ==> (A,B) : leads F"
paulson@4776
    34
paulson@6801
    35
    Trans  "[| (A,B) : leads F;  (B,C) : leads F |] ==> (A,C) : leads F"
paulson@4776
    36
paulson@5155
    37
    (*Encoding using powerset of the desired axiom
paulson@6801
    38
       (!!A. A : S ==> (A,B) : leads F) ==> (Union S, B) : leads F
paulson@5155
    39
    *)
paulson@7346
    40
    Union  "{(A,B) | A. A: S} : Pow (leads F) ==> (Union S, B) : leads F"
paulson@4776
    41
berghofe@5721
    42
  monos Pow_mono
paulson@4776
    43
paulson@5155
    44
paulson@8006
    45
constdefs
paulson@6536
    46
paulson@8006
    47
  (*visible version of the LEADS-TO relation*)
paulson@8006
    48
  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
paulson@8006
    49
    "A leadsTo B == {F. (A,B) : leads F}"
paulson@5648
    50
  
paulson@5648
    51
  (*wlt F B is the largest set that leads to B*)
paulson@5648
    52
  wlt :: "['a program, 'a set] => 'a set"
paulson@6536
    53
    "wlt F B == Union {A. F: A leadsTo B}"
paulson@4776
    54
paulson@9685
    55
syntax (xsymbols)
paulson@9685
    56
  "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\\<longmapsto>" 60)
paulson@9685
    57
paulson@4776
    58
end