src/HOL/UNITY/WFair.thy
author paulson
Thu, 11 Nov 1999 10:25:29 +0100
changeset 8006 299127ded09d
parent 7346 dace49c16aca
child 9685 6d123a7e30bd
permissions -rw-r--r--
tidied
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/WFair
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
Weak Fairness versions of transient, ensures, leadsTo.
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
From Misra, "A Logic for Concurrent Programming", 1994
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     9
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    10
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents: 5253
diff changeset
    11
WFair = UNITY +
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    13
constdefs
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    14
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    15
  (*This definition specifies weak fairness.  The rest of the theory
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    16
    is generic to all forms of fairness.*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    17
  transient :: "'a set => 'a program set"
5931
325300576da7 Finally removing "Compl" from HOL
paulson
parents: 5721
diff changeset
    18
    "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    19
8006
paulson
parents: 7346
diff changeset
    20
  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
paulson
parents: 7346
diff changeset
    21
    "A ensures B == (A-B co A Un B) Int transient (A-B)"
paulson
parents: 7346
diff changeset
    22
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    23
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    24
consts
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    25
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    26
  (*LEADS-TO constant for the inductive definition*)
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    27
  leads :: "'a program => ('a set * 'a set) set"
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    28
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    29
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    30
inductive "leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    31
  intrs 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    32
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    33
    Basis  "F : A ensures B ==> (A,B) : leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    34
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    35
    Trans  "[| (A,B) : leads F;  (B,C) : leads F |] ==> (A,C) : leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    36
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    37
    (*Encoding using powerset of the desired axiom
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    38
       (!!A. A : S ==> (A,B) : leads F) ==> (Union S, B) : leads F
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    39
    *)
7346
dace49c16aca arguably clearer definition of the inductive case of
paulson
parents: 6801
diff changeset
    40
    Union  "{(A,B) | A. A: S} : Pow (leads F) ==> (Union S, B) : leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    41
5721
458a67fd5461 Changed interface of inductive.
berghofe
parents: 5648
diff changeset
    42
  monos Pow_mono
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    43
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    44
8006
paulson
parents: 7346
diff changeset
    45
constdefs
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    46
8006
paulson
parents: 7346
diff changeset
    47
  (*visible version of the LEADS-TO relation*)
paulson
parents: 7346
diff changeset
    48
  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
paulson
parents: 7346
diff changeset
    49
    "A leadsTo B == {F. (A,B) : leads F}"
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    50
  
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    51
  (*wlt F B is the largest set that leads to B*)
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    52
  wlt :: "['a program, 'a set] => 'a set"
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    53
    "wlt F B == Union {A. F: A leadsTo B}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    54
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    55
end