author  paulson 
Thu, 13 Aug 1998 18:06:40 +0200  
changeset 5313  1861a564d7e2 
parent 5259  86d80749453f 
child 5584  aad639e56d4e 
permissions  rwrr 
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 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

14 
JOIN :: ['a set, 'a => 'b program] => 'b program 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

15 
"JOIN I prg == (Init = INT i:I. Init (prg i), 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

16 
Acts = UN i:I. Acts (prg i))" 
5252  17 

5259  18 
Join :: ['a program, 'a program] => 'a program 
5252  19 
"Join prgF prgG == (Init = Init prgF Int Init prgG, 
20 
Acts = Acts prgF Un Acts prgG)" 

21 

5259  22 
Null :: 'a program 
23 
"Null == (Init = UNIV, Acts = {id})" 

24 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

25 
syntax 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

26 
"@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10) 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

27 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

28 
translations 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

29 
"JN x:A. B" == "JOIN A (%x. B)" 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

30 

5252  31 
end 