| author | wenzelm |
| Fri, 22 Oct 1999 20:25:19 +0200 | |
| changeset 7922 | b284079cd902 |
| parent 7188 | 2bc63a44721b |
| child 8251 | 9be357df93d4 |
| permissions | -rw-r--r-- |
| 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 |
||
|
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6842
diff
changeset
|
6 |
Abstraction over replicated components (PLam) |
|
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6842
diff
changeset
|
7 |
General products of programs (Pi operation) |
| 5899 | 8 |
*) |
9 |
||
|
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6842
diff
changeset
|
10 |
PPROD = Lift_prog + |
| 5899 | 11 |
|
12 |
constdefs |
|
13 |
||
| 6842 | 14 |
PLam :: ['a set, 'a => 'b program] => ('a => 'b) program
|
15 |
"PLam I F == JN i:I. lift_prog i (F i)" |
|
| 5899 | 16 |
|
17 |
syntax |
|
| 6842 | 18 |
"@PLam" :: [pttrn, 'a set, 'b set] => ('a => 'b) set ("(3plam _:_./ _)" 10)
|
| 5899 | 19 |
|
20 |
translations |
|
| 6842 | 21 |
"plam x:A. B" == "PLam A (%x. B)" |
| 5899 | 22 |
|
23 |
end |