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 

1604

39 
primrec app_subst typ


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


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


42 

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 

1575

50 
primrec free_tv typ

1900

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


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

1575

53 


54 
primrec free_tv List.list

1900

55 
"free_tv [] = {}"


56 
"free_tv (x#l) = (free_tv x) Un (free_tv l)"

1300

57 


58 
(* domain of a substitution *)

1557

59 
constdefs

1476

60 
dom :: subst => nat set

1557

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

1300

62 


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

1557

64 
constdefs

1575

65 
cod :: subst => nat set


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

1557

74 
constdefs

1476

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

1557

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

1300

77 


78 
(* unification algorithm mgu *)


79 
consts

1476

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

1300

81 
rules

1476

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


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


84 
? r. s = $r o u"


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


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

1300

87 


88 
end


89 
