src/HOL/UNITY/WFair.thy
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5155 21177b8a4d7f
permissions -rw-r--r--
New UNITY theory
paulson@4776
     1
(*  Title:      HOL/UNITY/WFair
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Weak Fairness versions of transient, ensures, leadsTo.
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming", 1994
paulson@4776
     9
*)
paulson@4776
    10
paulson@4776
    11
WFair = Traces + Vimage +
paulson@4776
    12
paulson@4776
    13
constdefs
paulson@4776
    14
paulson@4776
    15
  transient :: "[('a * 'a)set set, 'a set] => bool"
paulson@4776
    16
    "transient Acts A == EX act:Acts. A <= Domain act & act^^A <= Compl A"
paulson@4776
    17
paulson@4776
    18
  ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
paulson@4776
    19
    "ensures Acts A B == constrains Acts (A-B) (A Un B) & transient Acts (A-B)"
paulson@4776
    20
paulson@4776
    21
consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
paulson@4776
    22
       leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
paulson@4776
    23
  
paulson@4776
    24
translations
paulson@4776
    25
  "leadsTo Acts A B" == "(A,B) : leadsto Acts"
paulson@4776
    26
paulson@4776
    27
inductive "leadsto Acts"
paulson@4776
    28
  intrs 
paulson@4776
    29
paulson@4776
    30
    Basis  "ensures Acts A B ==> leadsTo Acts A B"
paulson@4776
    31
paulson@4776
    32
    Trans  "[| leadsTo Acts A B;  leadsTo Acts B C |]
paulson@4776
    33
	   ==> leadsTo Acts A C"
paulson@4776
    34
paulson@4776
    35
    Union  "(UN A:S. {(A,B)}) : Pow (leadsto Acts)
paulson@4776
    36
	   ==> leadsTo Acts (Union S) B"
paulson@4776
    37
paulson@4776
    38
  monos "[Pow_mono]"
paulson@4776
    39
paulson@4776
    40
constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
paulson@4776
    41
  "wlt Acts B == Union {A. leadsTo Acts A B}"
paulson@4776
    42
paulson@4776
    43
end