src/HOL/UNITY/WFair.thy
 author paulson Thu, 24 Aug 2000 12:39:24 +0200 changeset 9685 6d123a7e30bd parent 8006 299127ded09d child 10293 354e885b3e0a permissions -rw-r--r--
xsymbols for leads-to and Join
```
(*  Title:      HOL/UNITY/WFair
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright   1998  University of Cambridge

Weak Fairness versions of transient, ensures, leadsTo.

From Misra, "A Logic for Concurrent Programming", 1994
*)

WFair = UNITY +

constdefs

(*This definition specifies weak fairness.  The rest of the theory
is generic to all forms of fairness.*)
transient :: "'a set => 'a program set"
"transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"

ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
"A ensures B == (A-B co A Un B) Int transient (A-B)"

consts

(*LEADS-TO constant for the inductive definition*)
leads :: "'a program => ('a set * 'a set) set"

intrs

Basis  "F : A ensures B ==> (A,B) : leads F"

Trans  "[| (A,B) : leads F;  (B,C) : leads F |] ==> (A,C) : leads F"

(*Encoding using powerset of the desired axiom
(!!A. A : S ==> (A,B) : leads F) ==> (Union S, B) : leads F
*)
Union  "{(A,B) | A. A: S} : Pow (leads F) ==> (Union S, B) : leads F"

monos Pow_mono

constdefs

(*visible version of the LEADS-TO relation*)
leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
"A leadsTo B == {F. (A,B) : leads F}"

(*wlt F B is the largest set that leads to B*)
wlt :: "['a program, 'a set] => 'a set"
"wlt F B == Union {A. F: A leadsTo B}"

syntax (xsymbols)
"op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\\<longmapsto>" 60)

end
```