src/HOL/MiniML/Type.thy

 (* Title:     HOL/MiniML/Type.thy
    ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
 
 MiniML-types and type substitutions.
 *)
 
 Type = Maybe + 
 
 (* new class for structures containing type variables *)
-classes
-        type_struct < term 
+axclass  type_struct < term 
+
 
 (* type expressions *)
 datatype
         typ = TVar nat | "->" typ typ (infixr 70)
 
-(* type variable substitution *)
+(* type schemata *)
+datatype
+        type_scheme = FVar nat | BVar nat | "=->" type_scheme type_scheme (infixr 70)
+
+
+(* embedding types into type schemata *)    
+consts
+  mk_scheme :: typ => type_scheme
+
+primrec mk_scheme typ
+  "mk_scheme (TVar n) = (FVar n)"
+  "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"
+
+
+instance  typ::type_struct
+instance  type_scheme::type_struct  
+instance  list::(type_struct)type_struct
+instance  fun::(term,type_struct)type_struct
+
+
+(* free_tv s: the type variables occuring freely in the type structure s *)
+
+consts
+  free_tv :: ['a::type_struct] => nat set
+
+primrec free_tv typ
+  free_tv_TVar    "free_tv (TVar m) = {m}"
+  free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
+
+primrec free_tv type_scheme
+  "free_tv (FVar m) = {m}"
+  "free_tv (BVar m) = {}"
+  "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
+
+primrec free_tv list
+  "free_tv [] = {}"
+  "free_tv (x#l) = (free_tv x) Un (free_tv l)"
+
+(* executable version of free_tv: Implementation with lists *)
+consts
+  free_tv_ML :: ['a::type_struct] => nat list
+
+primrec free_tv_ML type_scheme
+  "free_tv_ML (FVar m) = [m]"
+  "free_tv_ML (BVar m) = []"
+  "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
+
+primrec free_tv_ML list
+  "free_tv_ML [] = []"
+  "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
+
+  
+(* new_tv s n computes whether n is a new type variable w.r.t. a type 
+   structure s, i.e. whether n is greater than any type variable 
+   occuring in the type structure *)
+constdefs
+        new_tv :: [nat,'a::type_struct] => bool
+        "new_tv n ts == ! m. m:(free_tv ts) --> m<n"
+
+  
+(* bound_tv s: the type variables occuring bound in the type structure s *)
+
+consts
+  bound_tv :: ['a::type_struct] => nat set
+
+primrec bound_tv type_scheme
+  "bound_tv (FVar m) = {}"
+  "bound_tv (BVar m) = {m}"
+  "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
+
+primrec bound_tv list
+  "bound_tv [] = {}"
+  "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
+
+
+(* minimal new free / bound variable *)
+
+consts
+  min_new_bound_tv :: 'a::type_struct => nat
+
+primrec min_new_bound_tv type_scheme
+  "min_new_bound_tv (FVar n) = 0"
+  "min_new_bound_tv (BVar n) = Suc n"
+  "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
+
+
+(* substitutions *)
+
+(* type variable substitution *) 
 types
         subst = nat => typ
-
-arities
-        typ::type_struct
-        list::(type_struct)type_struct
-        fun::(term,type_struct)type_struct
-
-(* substitutions *)
 
 (* identity *)
 constdefs
         id_subst :: subst
         "id_subst == (%n.TVar n)"
 
 (* extension of substitution to type structures *)
 consts
-        app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
+  app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
 
-primrec app_subst typ
-  app_subst_TVar  "$ s (TVar n) = s n" 
-  app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
+primrec app_subst typ 
+  app_subst_TVar "$ S (TVar n) = S n" 
+  app_subst_Fun  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 
+
+primrec app_subst type_scheme
+  "$ S (FVar n) = mk_scheme (S n)"
+  "$ S (BVar n) = (BVar n)"
+  "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
 
 defs
-        app_subst_list  "$ s == map ($ s)"
-  
-(* free_tv s: the type variables occuring freely in the type structure s *)
-consts
-        free_tv :: ['a::type_struct] => nat set
-
-primrec free_tv typ
-  "free_tv (TVar m) = {m}"
-  "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
-
-primrec free_tv List.list
-  "free_tv [] = {}"
-  "free_tv (x#l) = (free_tv x) Un (free_tv l)"
+  app_subst_list "$ S == map ($ S)"
 
 (* domain of a substitution *)
 constdefs
         dom :: subst => nat set
-        "dom s == {n. s n ~= TVar n}" 
+        "dom S == {n. S n ~= TVar n}" 
 
-(* codomain of a substitutions: the introduced variables *)
+(* codomain of a substitution: the introduced variables *)
+
 constdefs
         cod :: subst => nat set
-        "cod s == (UN m:dom s. free_tv (s m))"
+        "cod S == (UN m:dom S. (free_tv (S m)))"
 
 defs
-        free_tv_subst   "free_tv s == (dom s) Un (cod s)"
+        free_tv_subst   "free_tv S == (dom S) Un (cod S)" 
 
-(* new_tv s n computes whether n is a new type variable w.r.t. a type 
-   structure s, i.e. whether n is greater than any type variable 
-   occuring in the type structure *)
-constdefs
-        new_tv :: [nat,'a::type_struct] => bool
-        "new_tv n ts == ! m. m:free_tv ts --> m<n"
-
+  
 (* unification algorithm mgu *)
 consts
-        mgu :: [typ,typ] => subst maybe
+        mgu :: [typ,typ] => subst option
 rules
-        mgu_eq   "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
-        mgu_mg   "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
-                  ? r. s = $r o u"
-        mgu_Ok   "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
-        mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
+        mgu_eq   "mgu t1 t2 = Some U ==> $U t1 = $U t2"
+        mgu_mg   "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==>
+                  ? R. S = $R o U"
+        mgu_Some   "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U"
+        mgu_free "mgu t1 t2 = Some U ==>   \
+\		  (free_tv U) <= (free_tv t1) Un (free_tv t2)"
 
 end
-