src/HOL/UNITY/Union.thy
author wenzelm
Fri Nov 09 00:09:47 2001 +0100 (2001-11-09)
changeset 12114 a8e860c86252
parent 10064 1a77667b21ef
child 13792 d1811693899c
permissions -rw-r--r--
eliminated old "symbols" syntax, use "xsymbols" instead;
paulson@5252
     1
(*  Title:      HOL/UNITY/Union.thy
paulson@5252
     2
    ID:         $Id$
paulson@5252
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5252
     4
    Copyright   1998  University of Cambridge
paulson@5252
     5
paulson@5252
     6
Unions of programs
paulson@5252
     7
paulson@5804
     8
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
paulson@5252
     9
*)
paulson@5252
    10
paulson@5252
    11
Union = SubstAx + FP +
paulson@5252
    12
paulson@5252
    13
constdefs
paulson@10064
    14
paulson@10064
    15
  (*FIXME: conjoin Init F Int Init G ~= {} *) 
paulson@10064
    16
  ok :: ['a program, 'a program] => bool      (infixl 65)
paulson@10064
    17
    "F ok G == Acts F <= AllowedActs G &
paulson@10064
    18
               Acts G <= AllowedActs F"
paulson@10064
    19
paulson@10064
    20
  (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) 
paulson@10064
    21
  OK  :: ['a set, 'a => 'b program] => bool
paulson@10064
    22
    "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
paulson@10064
    23
paulson@5648
    24
  JOIN  :: ['a set, 'a => 'b program] => 'b program
paulson@10064
    25
    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
paulson@10064
    26
			     INT i:I. AllowedActs (F i))"
paulson@5252
    27
paulson@5648
    28
  Join :: ['a program, 'a program] => 'a program      (infixl 65)
paulson@10064
    29
    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
paulson@10064
    30
			     AllowedActs F Int AllowedActs G)"
paulson@5252
    31
paulson@6295
    32
  SKIP :: 'a program
paulson@10064
    33
    "SKIP == mk_program (UNIV, {}, UNIV)"
paulson@10064
    34
paulson@10064
    35
  (*Characterizes safety properties.  Used with specifying AllowedActs*)
paulson@10064
    36
  safety_prop :: "'a program set => bool"
paulson@10064
    37
    "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
paulson@5259
    38
paulson@5313
    39
syntax
paulson@7359
    40
  "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)
paulson@5313
    41
  "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
paulson@5313
    42
paulson@5313
    43
translations
paulson@5313
    44
  "JN x:A. B"   == "JOIN A (%x. B)"
paulson@7359
    45
  "JN x y. B"   == "JN x. JN y. B"
paulson@7359
    46
  "JN x. B"     == "JOIN UNIV (%x. B)"
paulson@5313
    47
wenzelm@12114
    48
syntax (xsymbols)
paulson@9685
    49
  SKIP      :: 'a program                              ("\\<bottom>")
paulson@9685
    50
  "op Join" :: ['a program, 'a program] => 'a program  (infixl "\\<squnion>" 65)
paulson@9685
    51
  "@JOIN1"  :: [pttrns, 'b set] => 'b set              ("(3\\<Squnion> _./ _)" 10)
paulson@9685
    52
  "@JOIN"   :: [pttrn, 'a set, 'b set] => 'b set       ("(3\\<Squnion> _:_./ _)" 10)
paulson@9685
    53
paulson@5252
    54
end