src/HOL/UNITY/WFair.thy
author paulson
Wed, 19 Aug 1998 10:34:31 +0200
changeset 5340 d75c03cf77b5
parent 5277 e4297d03e5d2
child 5648 fe887910e32e
permissions -rw-r--r--
Misc changes
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.*)
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    17
  transient :: "[('a * 'a)set set, 'a set] => bool"
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    18
    "transient acts A == EX act:acts. A <= Domain act & act^^A <= Compl A"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    19
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    20
  ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    21
    "ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)"
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    22
			(*(unless acts A B) would be equivalent*)
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    23
5340
d75c03cf77b5 Misc changes
paulson
parents: 5277
diff changeset
    24
syntax leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
d75c03cf77b5 Misc changes
paulson
parents: 5277
diff changeset
    25
consts leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    26
  
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    27
translations
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    28
  "leadsTo acts A B" == "(A,B) : leadsto acts"
5340
d75c03cf77b5 Misc changes
paulson
parents: 5277
diff changeset
    29
  "~ leadsTo acts A B" <= "(A,B) ~: leadsto acts"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    30
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    31
inductive "leadsto acts"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    32
  intrs 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    33
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    34
    Basis  "ensures acts A B ==> leadsTo acts A B"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    35
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    36
    Trans  "[| leadsTo acts A B;  leadsTo acts B C |]
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    37
	   ==> leadsTo acts A C"
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
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    40
       (!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    41
    *)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    42
    Union  "(UN A:S. {(A,B)}) : Pow (leadsto acts)
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    43
	   ==> leadsTo acts (Union S) B"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    44
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    45
  monos "[Pow_mono]"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    46
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    47
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    48
(*wlt acts B is the largest set that leads to B*)
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    49
constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    50
  "wlt acts B == Union {A. leadsTo acts A B}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    51
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    52
end