|
2525
|
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 |
|
|
2625
|
12 |
(* gen: binding (generalising) the variables which are not free in the context *)
|
|
2525
|
13 |
|
|
|
14 |
types ctxt = type_scheme list
|
|
|
15 |
|
|
|
16 |
consts
|
|
|
17 |
gen :: [ctxt, typ] => type_scheme
|
|
|
18 |
|
|
5184
|
19 |
primrec
|
|
2525
|
20 |
"gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
|
|
2625
|
21 |
"gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
|
|
2525
|
22 |
|
|
|
23 |
(* executable version of gen: Implementation with free_tv_ML *)
|
|
|
24 |
|
|
|
25 |
consts
|
|
|
26 |
gen_ML_aux :: [nat list, typ] => type_scheme
|
|
|
27 |
|
|
5184
|
28 |
primrec
|
|
2525
|
29 |
"gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
|
|
2625
|
30 |
"gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
|
|
2525
|
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
|