isabelle: src/HOL/MiniML/MiniML.thy@c7a8f374339b (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
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	17	has_type :: "(type_expr list * expr * type_expr)set"
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	18	syntax
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	19	"@has_type" :: "[type_expr list, expr, type_expr] => bool"
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"
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	27	AbsI "[\| t1#a \|- e :: t2 \|] ==> a \|- Abs e :: Fun t1 t2"
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	28	AppI "[\| a \|- e1 :: Fun t2 t1; a \|- e2 :: t2 \|]
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
	Wed, 25 Oct 1995 09:46:46 +0100
changeset 1300	c7a8f374339b
child 1376	92f83b9d17e1
permissions	-rw-r--r--