isabelle: src/Cube/Base.thy@f6af6b265d20 (annotated)

4583 6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	1	(* Title: Cube/Base.thy
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	2	ID: $Id$
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	3	Author: Tobias Nipkow
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	4	Copyright 1993 University of Cambridge
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	5
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	6	Barendregt's Lambda-Cube.
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	7	*)
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	8
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	9	Base = Pure +
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	10
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	11	types
14773 556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	12	term
4583 6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	13
14773 556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	14	types
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	15	context typing
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	16	nonterminals
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	17	context_ typing_
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	18
4583 6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	19	consts
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	20	Abs, Prod :: "[term, term => term] => term"
14773 556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	21	Trueprop :: "[context, typing] => prop"
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	22	MT_context :: "context"
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	23	Context :: "[typing, context] => context"
4583 6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	24	star :: "term" ("*")
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	25	box :: "term" ("[]")
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	26	"^" :: "[term, term] => term" (infixl 20)
14773 556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	27	Has_type :: "[term, term] => typing"
4583 6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	28
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	29	syntax
14773 556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	30	Trueprop :: "[context_, typing_] => prop" ("(_/ \|- _)")
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	31	Trueprop1 :: "typing_ => prop" ("(_)")
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	32	"" :: "id => context_" ("_")
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	33	"" :: "var => context_" ("_")
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	34	MT_context :: "context_" ("")
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	35	Context :: "[typing_, context_] => context_" ("_ _")
556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	36	Has_type :: "[term, term] => typing_" ("(_:/ _)" [0, 0] 5)
4583 6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	37	Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	38	Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	39	"->" :: "[term, term] => term" (infixr 10)
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	40
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	41	translations
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	42	(prop) "x:X" == (prop) "\|- x:X"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	43	"Lam x:A. B" == "Abs(A, %x. B)"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	44	"Pi x:A. B" => "Prod(A, %x. B)"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	45	"A -> B" => "Prod(A, _K(B))"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	46
12110 f8b4b11cd79d eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 4584 diff changeset	47	syntax (xsymbols)
14773 556d9cc73711 adapted syntax to cope with lack of non-logical types; wenzelm parents: 12110 diff changeset	48	Trueprop :: "[context_, typing_] => prop" ("(_/ \\<turnstile> _)")
4584 3588b8f9613f added symbols syntax; wenzelm parents: 4583 diff changeset	49	box :: "term" ("\\<box>")
3588b8f9613f added symbols syntax; wenzelm parents: 4583 diff changeset	50	Lam :: "[idt, term, term] => term" ("(3\\<Lambda>_:_./ _)" [0, 0, 0] 10)
3588b8f9613f added symbols syntax; wenzelm parents: 4583 diff changeset	51	Pi :: "[idt, term, term] => term" ("(3\\<Pi>_:_./ _)" [0, 0] 10)
3588b8f9613f added symbols syntax; wenzelm parents: 4583 diff changeset	52	"op ->" :: "[term, term] => term" (infixr "\\<rightarrow>" 10)
3588b8f9613f added symbols syntax; wenzelm parents: 4583 diff changeset	53
3588b8f9613f added symbols syntax; wenzelm parents: 4583 diff changeset	54
4583 6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	55	rules
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	56	s_b "*: []"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	57
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	58	strip_s "[\| A:*; a:A ==> G \|- x:X \|] ==> a:A G \|- x:X"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	59	strip_b "[\| A:[]; a:A ==> G \|- x:X \|] ==> a:A G \|- x:X"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	60
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	61	app "[\| F:Prod(A, B); C:A \|] ==> F^C: B(C)"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	62
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	63	pi_ss "[\| A:; !!x. x:A ==> B(x): \|] ==> Prod(A, B):*"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	64
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	65	lam_ss "[\| A:; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x): \|]
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	66	==> Abs(A, f) : Prod(A, B)"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	67
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	68	beta "Abs(A, f)^a == f(a)"
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	69
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	70	end
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	71
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	72
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	73	ML
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	74
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	75	val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
6d9be46ea566 reorganized into individual theories; wenzelm parents: diff changeset	76

author	kleing
	Fri, 27 May 2005 01:09:44 +0200
changeset 16095	f6af6b265d20
parent 14854	61bdf2ae4dc5
permissions	-rw-r--r--