src/HOL/UNITY/WFair.thy
author paulson
Thu, 06 Aug 1998 15:47:26 +0200
changeset 5277 e4297d03e5d2
parent 5253 82a5ca6290aa
child 5340 d75c03cf77b5
permissions -rw-r--r--
A higher-level treatment of LeadsTo, minimizing use of "reachable"
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
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    24
consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    25
       leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
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"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    29
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    30
inductive "leadsto acts"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    31
  intrs 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    32
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    33
    Basis  "ensures acts A B ==> leadsTo acts A B"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    34
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    35
    Trans  "[| leadsTo acts A B;  leadsTo acts B C |]
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    36
	   ==> leadsTo acts A C"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    37
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    38
    (*Encoding using powerset of the desired axiom
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    39
       (!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    40
    *)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    41
    Union  "(UN A:S. {(A,B)}) : Pow (leadsto acts)
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    42
	   ==> leadsTo acts (Union S) B"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    43
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    44
  monos "[Pow_mono]"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    45
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    46
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    47
(*wlt acts B is the largest set that leads to B*)
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    48
constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    49
  "wlt acts B == Union {A. leadsTo acts A B}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    50
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    51
end