src/HOL/MiniML/Generalize.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5518 654ead0ba4f7
child 14422 b8da5f258b04
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* Title:     HOL/MiniML/Generalize.thy
     2    ID:        $Id$
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
     4    Copyright  1996 TU Muenchen
     5 
     6 Generalizing type schemes with respect to a context
     7 *)
     8 
     9 Generalize = Instance +
    10 
    11 
    12 (* gen: binding (generalising) the variables which are not free in the context *)
    13 
    14 types ctxt = type_scheme list
    15     
    16 consts
    17   gen :: [ctxt, typ] => type_scheme
    18 
    19 primrec
    20   "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
    21   "gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
    22 
    23 (* executable version of gen: Implementation with free_tv_ML *)
    24 
    25 consts
    26   gen_ML_aux :: [nat list, typ] => type_scheme
    27 
    28 primrec
    29   "gen_ML_aux A (TVar n) = (if (n: set A) then (FVar n) else (BVar n))"
    30   "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
    31 
    32 consts
    33   gen_ML :: [ctxt, typ] => type_scheme
    34 
    35 defs
    36   gen_ML_def "gen_ML A t == gen_ML_aux (free_tv_ML A) t"
    37 
    38 end