src/HOL/UNITY/WFair.thy
author paulson
Mon, 23 Oct 2000 15:20:32 +0200
changeset 10293 354e885b3e0a
parent 9685 6d123a7e30bd
child 10797 028d22926a41
permissions -rw-r--r--
quantifiers now allowed in inductive defs
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
10293
354e885b3e0a quantifiers now allowed in inductive defs
paulson
parents: 9685
diff changeset
    37
    Union  "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    38
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    39
8006
paulson
parents: 7346
diff changeset
    40
constdefs
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    41
8006
paulson
parents: 7346
diff changeset
    42
  (*visible version of the LEADS-TO relation*)
paulson
parents: 7346
diff changeset
    43
  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
paulson
parents: 7346
diff changeset
    44
    "A leadsTo B == {F. (A,B) : leads F}"
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    45
  
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    46
  (*wlt F B is the largest set that leads to B*)
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    47
  wlt :: "['a program, 'a set] => 'a set"
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    48
    "wlt F B == Union {A. F: A leadsTo B}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    49
9685
6d123a7e30bd xsymbols for leads-to and Join
paulson
parents: 8006
diff changeset
    50
syntax (xsymbols)
6d123a7e30bd xsymbols for leads-to and Join
paulson
parents: 8006
diff changeset
    51
  "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\\<longmapsto>" 60)
6d123a7e30bd xsymbols for leads-to and Join
paulson
parents: 8006
diff changeset
    52
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    53
end