src/HOL/MiniML/Type.thy
author nipkow
Fri, 08 Dec 1995 19:48:15 +0100
changeset 1400 5d909faf0e04
parent 1384 007ad29ce6ca
child 1476 608483c2122a
permissions -rw-r--r--
Introduced Monad syntax Pat := Val; Cont
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     1
(* Title:     HOL/MiniML/Type.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
MiniML-types and type substitutions.
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
Type = Maybe + 
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
(* new class for structures containing type variables *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    12
classes
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    13
	type_struct < term 
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 expressions *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    16
datatype
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1384
diff changeset
    17
	typ = TVar nat | "->" typ typ (infixr 70)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    18
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    19
(* type variable substitution *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    20
types
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1384
diff changeset
    21
	subst = nat => typ
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    22
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    23
arities
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1384
diff changeset
    24
	typ::type_struct
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    25
	list::(type_struct)type_struct
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    26
	fun::(term,type_struct)type_struct
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    27
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    28
(* substitutions *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    29
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    30
(* identity *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    31
consts
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1300
diff changeset
    32
	id_subst :: subst
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    33
defs
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    34
	id_subst_def "id_subst == (%n.TVar n)"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    35
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    36
(* extension of substitution to type structures *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    37
consts
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1300
diff changeset
    38
	app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    39
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    40
rules
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    41
	app_subst_TVar  "$ s (TVar n) = s n" 
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1384
diff changeset
    42
	app_subst_Fun	"$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    43
defs
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    44
        app_subst_list	"$ s == map ($ s)"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    45
  
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    46
(* free_tv s: the type variables occuring freely in the type structure s *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    47
consts
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1300
diff changeset
    48
	free_tv :: ['a::type_struct] => nat set
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    49
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    50
rules
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    51
	free_tv_TVar	"free_tv (TVar m) = {m}"
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1384
diff changeset
    52
	free_tv_Fun	"free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    53
	free_tv_Nil	"free_tv [] = {}"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    54
	free_tv_Cons	"free_tv (x#l) = (free_tv x) Un (free_tv l)"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    55
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    56
(* domain of a substitution *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    57
consts
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1300
diff changeset
    58
	dom :: subst => nat set
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    59
defs
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    60
	dom_def 	"dom s == {n. s n ~= TVar n}" 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    61
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    62
(* codomain of a substitutions: the introduced variables *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    63
consts
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1300
diff changeset
    64
     cod :: subst => nat set
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    65
defs
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    66
	cod_def		"cod s == (UN m:dom s. free_tv (s m))"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    67
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    68
defs
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    69
	free_tv_subst	"free_tv s == (dom s) Un (cod s)"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    70
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    71
(* new_tv s n computes whether n is a new type variable w.r.t. a type 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    72
   structure s, i.e. whether n is greater than any type variable 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    73
   occuring in the type structure *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    74
consts
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1300
diff changeset
    75
	new_tv :: [nat,'a::type_struct] => bool
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    76
defs
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    77
        new_tv_def      "new_tv n ts == ! m. m:free_tv ts --> m<n"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    78
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    79
(* unification algorithm mgu *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    80
consts
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1384
diff changeset
    81
	mgu :: [typ,typ] => subst maybe
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    82
rules
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1384
diff changeset
    83
	mgu_eq 	 "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1384
diff changeset
    84
	mgu_mg 	 "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1384
diff changeset
    85
		  ? r. s = $r o u"
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1384
diff changeset
    86
	mgu_Ok	 "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    87
	mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    88
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    89
end
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    90