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