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


13 
type_struct < term


14 


15 
(* type expressions *)


16 
datatype

1400

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

1300

18 


19 
(* type variable substitution *)


20 
types

1400

21 
subst = nat => typ

1300

22 


23 
arities

1400

24 
typ::type_struct

1300

25 
list::(type_struct)type_struct


26 
fun::(term,type_struct)type_struct


27 


28 
(* substitutions *)


29 


30 
(* identity *)


31 
consts

1376

32 
id_subst :: subst

1300

33 
defs


34 
id_subst_def "id_subst == (%n.TVar n)"


35 


36 
(* extension of substitution to type structures *)


37 
consts

1376

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

1300

39 


40 
rules


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

1400

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

1300

43 
defs


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


45 


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


47 
consts

1376

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

1300

49 


50 
rules


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

1400

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

1300

53 
free_tv_Nil "free_tv [] = {}"


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


55 


56 
(* domain of a substitution *)


57 
consts

1376

58 
dom :: subst => nat set

1300

59 
defs


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


61 


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


63 
consts

1376

64 
cod :: subst => nat set

1300

65 
defs


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


67 


68 
defs


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


70 


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


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


73 
occuring in the type structure *)


74 
consts

1376

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

1300

76 
defs


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


78 


79 
(* unification algorithm mgu *)


80 
consts

1400

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

1300

82 
rules

1400

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


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


85 
? r. s = $r o u"


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

1300

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


88 


89 
end


90 
