src/HOL/Lambda/InductTermi.thy

+(*  Title:      HOL/Lambda/InductTermi.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+
+Inductive characterization of terminating lambda terms.
+Goes back to
+Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.
+Also rediscovered by Matthes and Joachimski.
+*)
+
+InductTermi = Acc + ListBeta +
+
+consts IT :: dB set
+inductive IT
+intrs
+VarI "rs : lists IT ==> (Var n)$$rs : IT"
+LambdaI "r : IT ==> Abs r : IT"
+BetaI "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT"
+monos "[lists_mono]"
+
+end