author  paulson 
Thu, 01 Oct 1998 18:28:18 +0200  
changeset 5596  b29d18d8c4d2 
parent 5584  aad639e56d4e 
child 5611  6957f124ca97 
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 
5596  15 
"JOIN I prg == mk_program (INT i:I. Init (prg i), 
16 
UN i:I. Acts (prg i))" 

5252  17 

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

5252  21 

5584  22 
SKIP :: 'a program 
5596  23 
"SKIP == mk_program (UNIV, {})" 
5259  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 