|
2525
|
1 |
(* Title: HOL/MiniML/Instance.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Wolfgang Naraschewski and Tobias Nipkow
|
|
|
4 |
Copyright 1996 TU Muenchen
|
|
|
5 |
|
|
|
6 |
Instances of type schemes
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Instance = Type +
|
|
|
10 |
|
|
|
11 |
|
|
|
12 |
(* generic instances of a type scheme *)
|
|
|
13 |
|
|
|
14 |
consts
|
|
|
15 |
bound_typ_inst :: [subst, type_scheme] => typ
|
|
|
16 |
|
|
|
17 |
primrec bound_typ_inst type_scheme
|
|
|
18 |
"bound_typ_inst S (FVar n) = (TVar n)"
|
|
|
19 |
"bound_typ_inst S (BVar n) = (S n)"
|
|
|
20 |
"bound_typ_inst S (sch1 =-> sch2) = ((bound_typ_inst S sch1) -> (bound_typ_inst S sch2))"
|
|
|
21 |
|
|
|
22 |
consts
|
|
|
23 |
bound_scheme_inst :: [nat => type_scheme, type_scheme] => type_scheme
|
|
|
24 |
|
|
|
25 |
primrec bound_scheme_inst type_scheme
|
|
|
26 |
"bound_scheme_inst S (FVar n) = (FVar n)"
|
|
|
27 |
"bound_scheme_inst S (BVar n) = (S n)"
|
|
|
28 |
"bound_scheme_inst S (sch1 =-> sch2) = ((bound_scheme_inst S sch1) =-> (bound_scheme_inst S sch2))"
|
|
|
29 |
|
|
|
30 |
consts
|
|
|
31 |
"<|" :: [typ, type_scheme] => bool (infixr 70)
|
|
|
32 |
defs
|
|
|
33 |
is_bound_typ_instance "t <| sch == ? S. t = (bound_typ_inst S sch)"
|
|
|
34 |
|
|
|
35 |
instance type_scheme :: ord
|
|
|
36 |
defs le_type_scheme_def "sch' <= (sch::type_scheme) == !t. t <| sch' --> t <| sch"
|
|
|
37 |
|
|
|
38 |
consts
|
|
|
39 |
subst_to_scheme :: [nat => type_scheme, typ] => type_scheme
|
|
|
40 |
|
|
|
41 |
primrec subst_to_scheme typ
|
|
|
42 |
"subst_to_scheme B (TVar n) = (B n)"
|
|
|
43 |
"subst_to_scheme B (t1 -> t2) = ((subst_to_scheme B t1) =-> (subst_to_scheme B t2))"
|
|
|
44 |
|
|
|
45 |
instance list :: (ord)ord
|
|
|
46 |
defs le_env_def
|
|
|
47 |
"A <= B == length B = length A & (!i. i < length A --> nth i A <= nth i B)"
|
|
|
48 |
|
|
|
49 |
end
|