src/HOL/UNITY/WFair.thy
author paulson
Tue, 08 Jun 1999 10:59:02 +0200
changeset 6801 9e0037839d63
parent 6536 281d44905cab
child 7346 dace49c16aca
permissions -rw-r--r--
renamed the underlying relation of leadsTo from "leadsto" to "leads" to reduce the risk of confusion
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
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    20
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    21
consts
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    22
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    23
  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    24
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    25
  (*LEADS-TO constant for the inductive definition*)
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    26
  leads :: "'a program => ('a set * 'a set) set"
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    27
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    28
  (*visible version of the LEADS-TO relation*)
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    29
  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    30
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    31
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    32
inductive "leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    33
  intrs 
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
    Basis  "F : A ensures B ==> (A,B) : leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    36
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    37
    Trans  "[| (A,B) : leads F;  (B,C) : leads F |] ==> (A,C) : leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    38
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    39
    (*Encoding using powerset of the desired axiom
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    40
       (!!A. A : S ==> (A,B) : leads F) ==> (Union S, B) : leads F
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    41
    *)
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    42
    Union  "(UN A:S. {(A,B)}) : Pow (leads F) ==> (Union S, B) : leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    43
5721
458a67fd5461 Changed interface of inductive.
berghofe
parents: 5648
diff changeset
    44
  monos Pow_mono
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    45
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    46
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    47
  
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    48
defs
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    49
  ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    50
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    51
  leadsTo_def "A leadsTo B == {F. (A,B) : leads F}"
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    52
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    53
constdefs
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    54
  
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    55
  (*wlt F B is the largest set that leads to B*)
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    56
  wlt :: "['a program, 'a set] => 'a set"
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    57
    "wlt F B == Union {A. F: A leadsTo B}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    58
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    59
end