1300

1 
(* Title: HOL/MiniML/Type.thy


2 
ID: $Id$


3 
Author: Dieter Nazareth and Tobias Nipkow


4 
Copyright 1995 TU Muenchen


5 


6 
MiniMLtypes and type substitutions.


7 
*)


8 


9 
Type = Maybe +


10 


11 
(* new class for structures containing type variables *)


12 
classes

1476

13 
type_struct < term

1300

14 


15 
(* type expressions *)


16 
datatype

1476

17 
typ = TVar nat  ">" typ typ (infixr 70)

1300

18 


19 
(* type variable substitution *)


20 
types

1476

21 
subst = nat => typ

1300

22 


23 
arities

1476

24 
typ::type_struct


25 
list::(type_struct)type_struct


26 
fun::(term,type_struct)type_struct

1300

27 


28 
(* substitutions *)


29 


30 
(* identity *)

1557

31 
constdefs

1476

32 
id_subst :: subst

1557

33 
"id_subst == (%n.TVar n)"

1300

34 


35 
(* extension of substitution to type structures *)


36 
consts

1476

37 
app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")

1300

38 


39 
rules

1476

40 
app_subst_TVar "$ s (TVar n) = s n"


41 
app_subst_Fun "$ s (t1 > t2) = ($ s t1) > ($ s t2)"

1300

42 
defs

1476

43 
app_subst_list "$ s == map ($ s)"

1300

44 


45 
(* free_tv s: the type variables occuring freely in the type structure s *)


46 
consts

1476

47 
free_tv :: ['a::type_struct] => nat set

1300

48 

1575

49 
primrec free_tv typ


50 
free_tv_TVar "free_tv (TVar m) = {m}"


51 
free_tv_Fun "free_tv (t1 > t2) = (free_tv t1) Un (free_tv t2)"


52 


53 
primrec free_tv List.list


54 
free_tv_Nil "free_tv [] = {}"


55 
free_tv_Cons "free_tv (x#l) = (free_tv x) Un (free_tv l)"

1300

56 


57 
(* domain of a substitution *)

1557

58 
constdefs

1476

59 
dom :: subst => nat set

1557

60 
"dom s == {n. s n ~= TVar n}"

1300

61 


62 
(* codomain of a substitutions: the introduced variables *)

1557

63 
constdefs

1575

64 
cod :: subst => nat set


65 
"cod s == (UN m:dom s. free_tv (s m))"

1300

66 


67 
defs

1476

68 
free_tv_subst "free_tv s == (dom s) Un (cod s)"

1300

69 


70 
(* new_tv s n computes whether n is a new type variable w.r.t. a type


71 
structure s, i.e. whether n is greater than any type variable


72 
occuring in the type structure *)

1557

73 
constdefs

1476

74 
new_tv :: [nat,'a::type_struct] => bool

1557

75 
"new_tv n ts == ! m. m:free_tv ts > m<n"

1300

76 


77 
(* unification algorithm mgu *)


78 
consts

1476

79 
mgu :: [typ,typ] => subst maybe

1300

80 
rules

1476

81 
mgu_eq "mgu t1 t2 = Ok u ==> $u t1 = $u t2"


82 
mgu_mg "[ (mgu t1 t2) = Ok u; $s t1 = $s t2 ] ==>


83 
? r. s = $r o u"


84 
mgu_Ok "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"


85 
mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"

1300

86 


87 
end


88 
