|
1 (* Title: HOL/UNITY/PPROD.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 General products of programs (Pi operation). |
|
7 Also merging of state sets. |
|
8 *) |
|
9 |
|
10 PPROD = Union + |
|
11 |
|
12 constdefs |
|
13 (*Cartesian product of two relations*) |
|
14 RTimes :: "[('a*'a) set, ('b*'b) set] => (('a*'b) * ('a*'b)) set" |
|
15 ("_ RTimes _" [81, 80] 80) |
|
16 |
|
17 "R RTimes S == {((x,y),(x',y')). (x,x'):R & (y,y'):S}" |
|
18 |
|
19 (*FIXME: syntax (symbols) to use <times> ?? |
|
20 RTimes :: "[('a*'a) set, ('b*'b) set] => (('a*'b) * ('a*'b)) set" |
|
21 ("_ \\<times> _" [81, 80] 80) |
|
22 *) |
|
23 |
|
24 constdefs |
|
25 Lcopy :: "'a program => ('a*'b) program" |
|
26 "Lcopy F == mk_program (Init F Times UNIV, |
|
27 (%act. act RTimes Id) `` Acts F)" |
|
28 |
|
29 lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set" |
|
30 "lift_act i act == {(f,f'). EX s'. f' = f(i:=s') & (f i, s') : act}" |
|
31 |
|
32 lift_prog :: "['a, 'b program] => ('a => 'b) program" |
|
33 "lift_prog i F == mk_program ({f. f i : Init F}, lift_act i `` Acts F)" |
|
34 |
|
35 (*products of programs*) |
|
36 PPROD :: ['a set, 'b program] => ('a => 'b) program |
|
37 "PPROD I F == JN i:I. lift_prog i F" |
|
38 |
|
39 syntax |
|
40 "@PPROD" :: [pttrn, 'a set, 'b set] => ('a => 'b) set ("(3PPI _:_./ _)" 10) |
|
41 |
|
42 translations |
|
43 "PPI x:A. B" == "PPROD A (%x. B)" |
|
44 |
|
45 end |