author | wenzelm |
Tue, 03 Oct 2000 01:14:52 +0200 | |
changeset 10131 | 546686f0a6fb |
parent 8251 | 9be357df93d4 |
child 13786 | ab8f39f48a6f |
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 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
7188
diff
changeset
|
14 |
PLam :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
7188
diff
changeset
|
15 |
=> ((nat=>'b) * 'c) program" |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
7188
diff
changeset
|
16 |
"PLam I F == JN i:I. lift i (F i)" |
5899 | 17 |
|
18 |
syntax |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
7188
diff
changeset
|
19 |
"@PLam" :: [pttrn, nat set, 'b set] => (nat => 'b) set ("(3plam _:_./ _)" 10) |
5899 | 20 |
|
21 |
translations |
|
6842 | 22 |
"plam x:A. B" == "PLam A (%x. B)" |
5899 | 23 |
|
24 |
end |