src/HOL/MiniML/Generalize.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;
nipkow@2525
     1
(* Title:     HOL/MiniML/Generalize.thy
nipkow@2525
     2
   ID:        $Id$
nipkow@2525
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
nipkow@2525
     4
   Copyright  1996 TU Muenchen
nipkow@2525
     5
nipkow@2525
     6
Generalizing type schemes with respect to a context
nipkow@2525
     7
*)
nipkow@2525
     8
nipkow@2525
     9
Generalize = Instance +
nipkow@2525
    10
nipkow@2525
    11
nipkow@2525
    12
(* gen: binding (generalising) the variables which are not free in the type scheme *)
nipkow@2525
    13
nipkow@2525
    14
types ctxt = type_scheme list
nipkow@2525
    15
    
nipkow@2525
    16
consts
nipkow@2525
    17
  gen :: [ctxt, typ] => type_scheme
nipkow@2525
    18
nipkow@2525
    19
primrec gen typ
nipkow@2525
    20
  "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
nipkow@2525
    21
  "gen A (t1 -> t2) = ((gen A t1) =-> (gen A t2))"
nipkow@2525
    22
nipkow@2525
    23
(* executable version of gen: Implementation with free_tv_ML *)
nipkow@2525
    24
nipkow@2525
    25
consts
nipkow@2525
    26
  gen_ML_aux :: [nat list, typ] => type_scheme
nipkow@2525
    27
nipkow@2525
    28
primrec gen_ML_aux typ
nipkow@2525
    29
  "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
nipkow@2525
    30
  "gen_ML_aux A (t1 -> t2) = ((gen_ML_aux A t1) =-> (gen_ML_aux A t2))"
nipkow@2525
    31
nipkow@2525
    32
consts
nipkow@2525
    33
  gen_ML :: [ctxt, typ] => type_scheme
nipkow@2525
    34
nipkow@2525
    35
defs
nipkow@2525
    36
  gen_ML_def "gen_ML A t == gen_ML_aux (free_tv_ML A) t"
nipkow@2525
    37
nipkow@2525
    38
end