isabelle: src/HOLCF/Up1.thy@60c83075e41f (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
10212 33fe2d701ddd * empty log message * nipkow parents: 6543 diff changeset	11	Up1 = Cfun3 + Sum_Type + 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))"
10834 a7897aebbffc * empty log message * nipkow parents: 10212 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
	Mon, 05 Feb 2001 14:54:04 +0100
changeset 11067	60c83075e41f
parent 10834	a7897aebbffc
child 12030	46d57d0290a2
permissions	-rw-r--r--