src/HOL/MiniML/Type.thy
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2525 477c05586286
child 2625 69c1b8a493de
permissions -rw-r--r--
added AxClasses test;
     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 mk_scheme typ
    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 free_tv typ
    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 free_tv type_scheme
    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 free_tv list
    54   "free_tv [] = {}"
    55   "free_tv (x#l) = (free_tv x) Un (free_tv l)"
    56 
    57 (* executable version of free_tv: Implementation with lists *)
    58 consts
    59   free_tv_ML :: ['a::type_struct] => nat list
    60 
    61 primrec free_tv_ML type_scheme
    62   "free_tv_ML (FVar m) = [m]"
    63   "free_tv_ML (BVar m) = []"
    64   "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
    65 
    66 primrec free_tv_ML list
    67   "free_tv_ML [] = []"
    68   "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
    69 
    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 constdefs
    75         new_tv :: [nat,'a::type_struct] => bool
    76         "new_tv n ts == ! m. m:(free_tv ts) --> m<n"
    77 
    78   
    79 (* bound_tv s: the type variables occuring bound in the type structure s *)
    80 
    81 consts
    82   bound_tv :: ['a::type_struct] => nat set
    83 
    84 primrec bound_tv type_scheme
    85   "bound_tv (FVar m) = {}"
    86   "bound_tv (BVar m) = {m}"
    87   "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
    88 
    89 primrec bound_tv list
    90   "bound_tv [] = {}"
    91   "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
    92 
    93 
    94 (* minimal new free / bound variable *)
    95 
    96 consts
    97   min_new_bound_tv :: 'a::type_struct => nat
    98 
    99 primrec min_new_bound_tv type_scheme
   100   "min_new_bound_tv (FVar n) = 0"
   101   "min_new_bound_tv (BVar n) = Suc n"
   102   "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
   103 
   104 
   105 (* substitutions *)
   106 
   107 (* type variable substitution *) 
   108 types
   109         subst = nat => typ
   110 
   111 (* identity *)
   112 constdefs
   113         id_subst :: subst
   114         "id_subst == (%n.TVar n)"
   115 
   116 (* extension of substitution to type structures *)
   117 consts
   118   app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
   119 
   120 primrec app_subst typ 
   121   app_subst_TVar "$ S (TVar n) = S n" 
   122   app_subst_Fun  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 
   123 
   124 primrec app_subst type_scheme
   125   "$ S (FVar n) = mk_scheme (S n)"
   126   "$ S (BVar n) = (BVar n)"
   127   "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
   128 
   129 defs
   130   app_subst_list "$ S == map ($ S)"
   131 
   132 (* domain of a substitution *)
   133 constdefs
   134         dom :: subst => nat set
   135         "dom S == {n. S n ~= TVar n}" 
   136 
   137 (* codomain of a substitution: the introduced variables *)
   138 
   139 constdefs
   140         cod :: subst => nat set
   141         "cod S == (UN m:dom S. (free_tv (S m)))"
   142 
   143 defs
   144         free_tv_subst   "free_tv S == (dom S) Un (cod S)" 
   145 
   146   
   147 (* unification algorithm mgu *)
   148 consts
   149         mgu :: [typ,typ] => subst option
   150 rules
   151         mgu_eq   "mgu t1 t2 = Some U ==> $U t1 = $U t2"
   152         mgu_mg   "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==>
   153                   ? R. S = $R o U"
   154         mgu_Some   "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U"
   155         mgu_free "mgu t1 t2 = Some U ==>   \
   156 \		  (free_tv U) <= (free_tv t1) Un (free_tv t2)"
   157 
   158 end