isabelle: src/HOLCF/Up1.thy@0eb9ee70c8f8 (annotated)

2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	1	(* Title: HOLCF/Up1.thy
d63ffafce255 * empty log message * oheimb parents: diff changeset	2	ID: $Id$
d63ffafce255 * empty log message * oheimb parents: diff changeset	3	Author: Franz Regensburger
d63ffafce255 * empty log message * oheimb parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
d63ffafce255 * empty log message * oheimb parents: diff changeset	5
d63ffafce255 * empty log message * oheimb parents: diff changeset	6
d63ffafce255 * empty log message * oheimb parents: diff changeset	7	Lifting
d63ffafce255 * empty log message * oheimb parents: diff changeset	8
d63ffafce255 * empty log message * oheimb parents: diff changeset	9	*)
d63ffafce255 * empty log message * oheimb parents: diff changeset	10
6543 da7b170fc8a7 patched sum_case; wenzelm parents: 3842 diff changeset	11	Up1 = Cfun3 + Sum + Datatype +
2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	12
d63ffafce255 * empty log message * oheimb parents: diff changeset	13	(* new type for lifting *)
d63ffafce255 * empty log message * oheimb parents: diff changeset	14
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2278 diff changeset	15	typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	16
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	17	instance u :: (sq_ord)sq_ord
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	18
2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	19	consts
d63ffafce255 * empty log message * oheimb parents: diff changeset	20	Iup :: "'a => ('a)u"
d63ffafce255 * empty log message * oheimb parents: diff changeset	21	Ifup :: "('a->'b)=>('a)u => 'b"
d63ffafce255 * empty log message * oheimb parents: diff changeset	22
d63ffafce255 * empty log message * oheimb parents: diff changeset	23	defs
d63ffafce255 * empty log message * oheimb parents: diff changeset	24	Iup_def "Iup x == Abs_Up(Inr(x))"
d63ffafce255 * empty log message * oheimb parents: diff changeset	25	Ifup_def "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU \| Inr(z) => f`z"
3842 b55686a7b22c fixed dots; wenzelm parents: 3323 diff changeset	26	less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of
2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	27	Inl(y1) => True
d63ffafce255 * empty log message * oheimb parents: diff changeset	28	\| Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False
d63ffafce255 * empty log message * oheimb parents: diff changeset	29	\| Inr(z2) => y2<<z2))"
d63ffafce255 * empty log message * oheimb parents: diff changeset	30	end

author	wenzelm
	Wed, 08 Mar 2000 17:48:31 +0100
changeset 8364	0eb9ee70c8f8
parent 6543	da7b170fc8a7
child 10212	33fe2d701ddd
permissions	-rw-r--r--