5899
|
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
|