isabelle: src/CCL/Hered.thy@967e6c2578f2 (annotated)

17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	1	(* Title: CCL/Hered.thy
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1474 3f7d67927fe2 expanded tabs clasohm parents: 1149 diff changeset	3	Author: Martin Coen
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	6
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	7	header {* Hereditary Termination -- cf. Martin Lo\"f *}
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	8
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	9	theory Hered
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	10	imports Type
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	11	uses "coinduction.ML"
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	12	begin
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	13
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	14	text {*
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	15	Note that this is based on an untyped equality and so @{text "lam
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	16	x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"}
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	17	is. Not so useful for functions!
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	18	*}
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	19
a5a9c433f639 Initial revision clasohm parents: diff changeset	20	consts
a5a9c433f639 Initial revision clasohm parents: diff changeset	21	(* Predicates *)
a5a9c433f639 Initial revision clasohm parents: diff changeset	22	HTTgen :: "i set => i set"
a5a9c433f639 Initial revision clasohm parents: diff changeset	23	HTT :: "i set"
a5a9c433f639 Initial revision clasohm parents: diff changeset	24
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	25	axioms
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	26	(* Definitions of Hereditary Termination *)
a5a9c433f639 Initial revision clasohm parents: diff changeset	27
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	28	HTTgen_def:
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	29	"HTTgen(R) == {t. t=true \| t=false \| (EX a b. t=<a,b> & a : R & b : R) \|
3837 d7f033c74b38 fixed dots; wenzelm parents: 1474 diff changeset	30	(EX f. t=lam x. f(x) & (ALL x. f(x) : R))}"
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	31	HTT_def: "HTT == gfp(HTTgen)"
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	32
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	33	ML {* use_legacy_bindings (the_context ()) *}
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	34
a5a9c433f639 Initial revision clasohm parents: diff changeset	35	end

author	wenzelm
	Tue, 14 Mar 2006 22:06:42 +0100
changeset 19271	967e6c2578f2
parent 17456	bcf7544875b2
child 20140	98acc6d0fab6
permissions	-rw-r--r--