isabelle: src/HOL/MiniML/MiniML.thy@5d909faf0e04 (annotated)

1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	1	(* Title: HOL/MiniML/MiniML.thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	2	ID: $Id$
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	3	Author: Dieter Nazareth and Tobias Nipkow
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	4	Copyright 1995 TU Muenchen
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	5
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	6	Mini_ML with type inference rules.
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	7	*)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	8
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	9	MiniML = Type +
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	10
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	11	(* expressions *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	12	datatype
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	13	expr = Var nat \| Abs expr \| App expr expr
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	14
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	15	(* type inference rules *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	16	consts
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	17	has_type :: "(typ list * expr * typ)set"
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	18	syntax
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	19	"@has_type" :: [typ list, expr, typ] => bool
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	20	("((_) \|-/ (_) :: (_))" 60)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	21	translations
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	22	"a \|- e :: t" == "(a,e,t):has_type"
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	23
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	24	inductive "has_type"
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	25	intrs
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	26	VarI "[\| n < length a \|] ==> a \|- Var n :: nth n a"
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	27	AbsI "[\| t1#a \|- e :: t2 \|] ==> a \|- Abs e :: t1 -> t2"
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	28	AppI "[\| a \|- e1 :: t2 -> t1; a \|- e2 :: t2 \|]
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	29	==> a \|- App e1 e2 :: t1"
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	30
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	31	end
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	32

author	nipkow
	Fri, 08 Dec 1995 19:48:15 +0100
changeset 1400	5d909faf0e04
parent 1376	92f83b9d17e1
child 1476	608483c2122a
permissions	-rw-r--r--