isabelle: src/ZF/Resid/Terms.thy@f23494fa8dc1 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: Terms.thy
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Ole Rasmussen
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	5	Logic Image: ZF
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	6	*)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	7
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	8	Terms = Cube+
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	9
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	10	consts
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	11	lambda :: i
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	12	unmark :: i=>i
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	13	Apl :: [i,i]=>i
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	14
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	15	translations
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	16	"Apl(n,m)" == "App(0,n,m)"
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	17
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	18	inductive
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	19	domains "lambda" <= "redexes"
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	20	intrs
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	21	Lambda_Var " n:nat ==> Var(n):lambda"
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	22	Lambda_Fun " u:lambda ==> Fun(u):lambda"
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	23	Lambda_App "[\|u:lambda; v:lambda\|]==> Apl(u,v):lambda"
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	24	type_intrs "redexes.intrs@bool_typechecks"
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	25
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	26	defs
3840 e0baea4d485a fixed dots; wenzelm parents: 1478 diff changeset	27	unmark_def "unmark(u) == redex_rec(u,%i. Var(i),
e0baea4d485a fixed dots; wenzelm parents: 1478 diff changeset	28	%x m. Fun(m),
e0baea4d485a fixed dots; wenzelm parents: 1478 diff changeset	29	%b x y m p. Apl(m,p))"
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	30	end
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	31
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	32

author	paulson
	Fri, 17 Jul 1998 11:13:43 +0200
changeset 5156	f23494fa8dc1
parent 3840	e0baea4d485a
child 6046	2c8a8be36c94
permissions	-rw-r--r--