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 *)


31 
consts

1476

32 
id_subst :: subst

1300

33 
defs

1476

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

1300

35 


36 
(* extension of substitution to type structures *)


37 
consts

1476

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

1300

39 


40 
rules

1476

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


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

1300

43 
defs

1476

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

1300

45 


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


47 
consts

1476

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

1300

49 


50 
rules

1476

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


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


53 
free_tv_Nil "free_tv [] = {}"


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

1300

55 


56 
(* domain of a substitution *)


57 
consts

1476

58 
dom :: subst => nat set

1300

59 
defs

1476

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

1300

61 


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


63 
consts

1376

64 
cod :: subst => nat set

1300

65 
defs

1476

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

1300

67 


68 
defs

1476

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

1300

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

1476

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

1476

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

1300

82 
rules

1476

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"


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

1300

88 


89 
end


90 
