isabelle: src/HOL/Lambda/InductTermi.thy@bd2d9dd34dfd (annotated)

5261 ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	1	(* Title: HOL/Lambda/InductTermi.thy
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	2	ID: $Id$
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	3	Author: Tobias Nipkow
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	4	Copyright 1998 TU Muenchen
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	5
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	6	Inductive characterization of terminating lambda terms.
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	7	Goes back to
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	8	Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	9	Also rediscovered by Matthes and Joachimski.
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	10	*)
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	11
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	12	InductTermi = Acc + ListBeta +
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	13
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	14	consts IT :: dB set
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	15	inductive IT
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	16	intrs
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	17	VarI "rs : lists IT ==> (Var n)$$rs : IT"
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	18	LambdaI "r : IT ==> Abs r : IT"
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	19	BetaI "[\| (r[s/0])$$ss : IT; s : IT \|] ==> (Abs r $ s)$$ss : IT"
5717 0d28dbe484b6 Changed syntax of inductive. berghofe parents: 5261 diff changeset	20	monos lists_mono
5261 ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	21
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: diff changeset	22	end

author	wenzelm
	Fri, 06 Nov 1998 14:04:54 +0100
changeset 5807	bd2d9dd34dfd
parent 5717	0d28dbe484b6
child 9102	c7ba07e3bbe8
permissions	-rw-r--r--