isabelle: src/HOLCF/Lift3.thy@84c2178db936 (annotated)

2357 dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	1	(* Title: HOLCF/Lift3.thy
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	2	ID: $Id$
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	3	Author: Olaf Mueller, Robert Sandner
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	4	Copyright 1996 Technische Universitaet Muenchen
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	5
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	6	Class Instance lift::(term)pcpo
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	7	*)
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	8
2356 125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	9	Lift3 = Lift2 +
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	10
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2357 diff changeset	11	instance lift :: (term)pcpo (cpo_lift,least_lift)
2356 125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	12
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	13	consts
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	14	flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)"
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	15	flift2 :: "('a => 'b) => ('a lift -> 'b lift)"
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	16
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	17	translations
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	18	"UU" <= "Undef"
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	19
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	20	defs
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	21	flift1_def
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	22	"flift1 f == (LAM x. (case x of
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	23	Undef => UU
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	24	\| Def y => (f y)))"
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	25	flift2_def
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	26	"flift2 f == (LAM x. (case x of
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	27	Undef => Undef
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	28	\| Def y => Def (f y)))"
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	29
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	30	end
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	31

author	paulson
	Wed, 23 Apr 1997 11:00:48 +0200
changeset 3017	84c2178db936
parent 2640	ee4dfce170a0
child 3034	9c44acc3c6fa
permissions	-rw-r--r--