isabelle: src/HOL/UNITY/PPROD.thy@f8bfc61ee1b5 (annotated)

5899 13d4753079fe new theory PPROD paulson parents: diff changeset	1	(* Title: HOL/UNITY/PPROD.thy
13d4753079fe new theory PPROD paulson parents: diff changeset	2	ID: $Id$
13d4753079fe new theory PPROD paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
13d4753079fe new theory PPROD paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
13d4753079fe new theory PPROD paulson parents: diff changeset	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 13d4753079fe new theory PPROD paulson parents: diff changeset	8	*)
13d4753079fe new theory PPROD paulson parents: diff changeset	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 13d4753079fe new theory PPROD paulson parents: diff changeset	11
13d4753079fe new theory PPROD paulson parents: diff changeset	12	constdefs
13d4753079fe new theory PPROD paulson parents: diff changeset	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 13d4753079fe new theory PPROD paulson parents: diff changeset	17
13d4753079fe new theory PPROD paulson parents: diff changeset	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 13d4753079fe new theory PPROD paulson parents: diff changeset	20
13d4753079fe new theory PPROD paulson parents: diff changeset	21	translations
6842 56e08e264961 renamed PPI to plam paulson parents: 6835 diff changeset	22	"plam x:A. B" == "PLam A (%x. B)"
5899 13d4753079fe new theory PPROD paulson parents: diff changeset	23
13d4753079fe new theory PPROD paulson parents: diff changeset	24	end

author	wenzelm
	Mon, 04 Mar 2002 19:06:52 +0100
changeset 13012	f8bfc61ee1b5
parent 8251	9be357df93d4
child 13786	ab8f39f48a6f
permissions	-rw-r--r--