|
5252
|
1 |
(* Title: HOL/UNITY/Union.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1998 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Unions of programs
|
|
|
7 |
|
|
|
8 |
From Misra's Chapter 5: Asynchronous Compositions of Programs
|
|
|
9 |
*)
|
|
|
10 |
|
|
|
11 |
Union = SubstAx + FP +
|
|
|
12 |
|
|
|
13 |
constdefs
|
|
|
14 |
|
|
5259
|
15 |
Join :: ['a program, 'a program] => 'a program
|
|
5252
|
16 |
"Join prgF prgG == (|Init = Init prgF Int Init prgG,
|
|
|
17 |
Acts = Acts prgF Un Acts prgG|)"
|
|
|
18 |
|
|
5259
|
19 |
Null :: 'a program
|
|
|
20 |
"Null == (|Init = UNIV, Acts = {id}|)"
|
|
|
21 |
|
|
5252
|
22 |
end
|