isabelle: src/HOLCF/ex/Fix2.thy@78bdb2d04771 (annotated)

1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	1	(* Title: HOLCF/ex/Fix2.thy
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	2	ID: $Id$
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	3	Author: Franz Regensburger
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	4	Copyright 1995 Technische Universitaet Muenchen
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	5
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	6	Show that fix is the unique least fixed-point operator.
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	7	From axioms gix1_def,gix2_def it follows that fix = gix
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	8
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	9	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	10
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	11	Fix2 = Fix +
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	12
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	13	consts
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	14
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15	gix :: "('a->'a)->'a"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	16
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	17	rules
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	18
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	19	gix1_def "F`(gix`F) = gix`F"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	20	gix2_def "F`y=y ==> gix`F << y"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	21
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	22	end
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	23
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	24
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	25
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	26
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	27
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	28
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	29
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	30
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	31
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	32
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	33
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	34
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	35
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	36
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	37
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	38

author	clasohm
	Fri, 24 Nov 1995 11:46:23 +0100
changeset 1367	78bdb2d04771
parent 1274	ea0668a1c0ba
child 1479	21eb5e156d91
permissions	-rw-r--r--