src/HOL/MiniML/Type.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5184 9b8547a9496a
child 12338 de0f4a63baa5
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* Title:     HOL/MiniML/Type.thy
     2    ID:        $Id$
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
     4    Copyright  1996 TU Muenchen
     5 
     6 MiniML-types and type substitutions.
     7 *)
     8 
     9 Type = Maybe + 
    10 
    11 (* new class for structures containing type variables *)
    12 axclass  type_struct < term 
    13 
    14 
    15 (* type expressions *)
    16 datatype
    17         typ = TVar nat | "->" typ typ (infixr 70)
    18 
    19 (* type schemata *)
    20 datatype
    21         type_scheme = FVar nat | BVar nat | "=->" type_scheme type_scheme (infixr 70)
    22 
    23 
    24 (* embedding types into type schemata *)    
    25 consts
    26   mk_scheme :: typ => type_scheme
    27 
    28 primrec
    29   "mk_scheme (TVar n) = (FVar n)"
    30   "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"
    31 
    32 
    33 instance  typ::type_struct
    34 instance  type_scheme::type_struct  
    35 instance  list::(type_struct)type_struct
    36 instance  fun::(term,type_struct)type_struct
    37 
    38 
    39 (* free_tv s: the type variables occuring freely in the type structure s *)
    40 
    41 consts
    42   free_tv :: ['a::type_struct] => nat set
    43 
    44 primrec
    45   free_tv_TVar    "free_tv (TVar m) = {m}"
    46   free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
    47 
    48 primrec
    49   "free_tv (FVar m) = {m}"
    50   "free_tv (BVar m) = {}"
    51   "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
    52 
    53 primrec
    54   "free_tv [] = {}"
    55   "free_tv (x#l) = (free_tv x) Un (free_tv l)"
    56 
    57   
    58 (* executable version of free_tv: Implementation with lists *)
    59 consts
    60   free_tv_ML :: ['a::type_struct] => nat list
    61 
    62 primrec
    63   "free_tv_ML (FVar m) = [m]"
    64   "free_tv_ML (BVar m) = []"
    65   "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
    66 
    67 primrec
    68   "free_tv_ML [] = []"
    69   "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
    70 
    71   
    72 (* new_tv s n computes whether n is a new type variable w.r.t. a type 
    73    structure s, i.e. whether n is greater than any type variable 
    74    occuring in the type structure *)
    75 constdefs
    76         new_tv :: [nat,'a::type_struct] => bool
    77         "new_tv n ts == ! m. m:(free_tv ts) --> m<n"
    78 
    79   
    80 (* bound_tv s: the type variables occuring bound in the type structure s *)
    81 
    82 consts
    83   bound_tv :: ['a::type_struct] => nat set
    84 
    85 primrec
    86   "bound_tv (FVar m) = {}"
    87   "bound_tv (BVar m) = {m}"
    88   "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
    89 
    90 primrec
    91   "bound_tv [] = {}"
    92   "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
    93 
    94 
    95 (* minimal new free / bound variable *)
    96 
    97 consts
    98   min_new_bound_tv :: 'a::type_struct => nat
    99 
   100 primrec
   101   "min_new_bound_tv (FVar n) = 0"
   102   "min_new_bound_tv (BVar n) = Suc n"
   103   "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
   104 
   105 
   106 (* substitutions *)
   107 
   108 (* type variable substitution *) 
   109 types
   110         subst = nat => typ
   111 
   112 (* identity *)
   113 constdefs
   114         id_subst :: subst
   115         "id_subst == (%n. TVar n)"
   116 
   117 (* extension of substitution to type structures *)
   118 consts
   119   app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
   120 
   121 primrec
   122   app_subst_TVar "$ S (TVar n) = S n" 
   123   app_subst_Fun  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 
   124 
   125 primrec
   126   "$ S (FVar n) = mk_scheme (S n)"
   127   "$ S (BVar n) = (BVar n)"
   128   "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
   129 
   130 defs
   131   app_subst_list "$ S == map ($ S)"
   132 
   133 (* domain of a substitution *)
   134 constdefs
   135         dom :: subst => nat set
   136         "dom S == {n. S n ~= TVar n}" 
   137 
   138 (* codomain of a substitution: the introduced variables *)
   139 
   140 constdefs
   141         cod :: subst => nat set
   142         "cod S == (UN m:dom S. (free_tv (S m)))"
   143 
   144 defs
   145         free_tv_subst   "free_tv S == (dom S) Un (cod S)" 
   146 
   147   
   148 (* unification algorithm mgu *)
   149 consts
   150         mgu :: [typ,typ] => subst option
   151 rules
   152         mgu_eq   "mgu t1 t2 = Some U ==> $U t1 = $U t2"
   153         mgu_mg   "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==>
   154                   ? R. S = $R o U"
   155         mgu_Some   "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U"
   156         mgu_free "mgu t1 t2 = Some U ==>   \
   157 \		  (free_tv U) <= (free_tv t1) Un (free_tv t2)"
   158 
   159 end