author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 5184 | 9b8547a9496a |
child 13537 | f506eb568121 |
permissions | -rw-r--r-- |
1300 | 1 |
(* Title: HOL/MiniML/Type.thy |
2 |
ID: $Id$ |
|
2525 | 3 |
Author: Wolfgang Naraschewski and Tobias Nipkow |
4 |
Copyright 1996 TU Muenchen |
|
1300 | 5 |
|
6 |
MiniML-types and type substitutions. |
|
7 |
*) |
|
8 |
||
9 |
Type = Maybe + |
|
10 |
||
11 |
(* new class for structures containing type variables *) |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5184
diff
changeset
|
12 |
axclass type_struct < type |
2525 | 13 |
|
1300 | 14 |
|
15 |
(* type expressions *) |
|
16 |
datatype |
|
1476 | 17 |
typ = TVar nat | "->" typ typ (infixr 70) |
1300 | 18 |
|
2525 | 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 |
||
5184 | 28 |
primrec |
2525 | 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 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5184
diff
changeset
|
36 |
instance fun::(type,type_struct)type_struct |
2525 | 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 |
||
5184 | 44 |
primrec |
2525 | 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 |
||
5184 | 48 |
primrec |
2525 | 49 |
"free_tv (FVar m) = {m}" |
50 |
"free_tv (BVar m) = {}" |
|
51 |
"free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)" |
|
52 |
||
5184 | 53 |
primrec |
2525 | 54 |
"free_tv [] = {}" |
55 |
"free_tv (x#l) = (free_tv x) Un (free_tv l)" |
|
56 |
||
2625 | 57 |
|
2525 | 58 |
(* executable version of free_tv: Implementation with lists *) |
59 |
consts |
|
60 |
free_tv_ML :: ['a::type_struct] => nat list |
|
61 |
||
5184 | 62 |
primrec |
2525 | 63 |
"free_tv_ML (FVar m) = [m]" |
64 |
"free_tv_ML (BVar m) = []" |
|
65 |
"free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)" |
|
66 |
||
5184 | 67 |
primrec |
2525 | 68 |
"free_tv_ML [] = []" |
69 |
"free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)" |
|
70 |
||
71 |
||
72 |
(* new_tv s n computes whether n is a new type variable w.r.t. a type |
|
73 |
structure s, i.e. whether n is greater than any type variable |
|
74 |
occuring in the type structure *) |
|
75 |
constdefs |
|
76 |
new_tv :: [nat,'a::type_struct] => bool |
|
77 |
"new_tv n ts == ! m. m:(free_tv ts) --> m<n" |
|
78 |
||
79 |
||
80 |
(* bound_tv s: the type variables occuring bound in the type structure s *) |
|
81 |
||
82 |
consts |
|
83 |
bound_tv :: ['a::type_struct] => nat set |
|
84 |
||
5184 | 85 |
primrec |
2525 | 86 |
"bound_tv (FVar m) = {}" |
87 |
"bound_tv (BVar m) = {m}" |
|
88 |
"bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)" |
|
89 |
||
5184 | 90 |
primrec |
2525 | 91 |
"bound_tv [] = {}" |
92 |
"bound_tv (x#l) = (bound_tv x) Un (bound_tv l)" |
|
93 |
||
94 |
||
95 |
(* minimal new free / bound variable *) |
|
96 |
||
97 |
consts |
|
98 |
min_new_bound_tv :: 'a::type_struct => nat |
|
99 |
||
5184 | 100 |
primrec |
2525 | 101 |
"min_new_bound_tv (FVar n) = 0" |
102 |
"min_new_bound_tv (BVar n) = Suc n" |
|
103 |
"min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)" |
|
104 |
||
105 |
||
106 |
(* substitutions *) |
|
107 |
||
108 |
(* type variable substitution *) |
|
1300 | 109 |
types |
1476 | 110 |
subst = nat => typ |
1300 | 111 |
|
112 |
(* identity *) |
|
1557 | 113 |
constdefs |
1476 | 114 |
id_subst :: subst |
3842 | 115 |
"id_subst == (%n. TVar n)" |
1300 | 116 |
|
117 |
(* extension of substitution to type structures *) |
|
118 |
consts |
|
2525 | 119 |
app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$") |
1300 | 120 |
|
5184 | 121 |
primrec |
2525 | 122 |
app_subst_TVar "$ S (TVar n) = S n" |
123 |
app_subst_Fun "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" |
|
124 |
||
5184 | 125 |
primrec |
2525 | 126 |
"$ S (FVar n) = mk_scheme (S n)" |
127 |
"$ S (BVar n) = (BVar n)" |
|
128 |
"$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)" |
|
1604 | 129 |
|
1300 | 130 |
defs |
2525 | 131 |
app_subst_list "$ S == map ($ S)" |
1300 | 132 |
|
133 |
(* domain of a substitution *) |
|
1557 | 134 |
constdefs |
1476 | 135 |
dom :: subst => nat set |
2525 | 136 |
"dom S == {n. S n ~= TVar n}" |
1300 | 137 |
|
2525 | 138 |
(* codomain of a substitution: the introduced variables *) |
139 |
||
1557 | 140 |
constdefs |
1575 | 141 |
cod :: subst => nat set |
2525 | 142 |
"cod S == (UN m:dom S. (free_tv (S m)))" |
1300 | 143 |
|
144 |
defs |
|
2525 | 145 |
free_tv_subst "free_tv S == (dom S) Un (cod S)" |
1300 | 146 |
|
2525 | 147 |
|
1300 | 148 |
(* unification algorithm mgu *) |
149 |
consts |
|
2525 | 150 |
mgu :: [typ,typ] => subst option |
1300 | 151 |
rules |
2525 | 152 |
mgu_eq "mgu t1 t2 = Some U ==> $U t1 = $U t2" |
153 |
mgu_mg "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==> |
|
154 |
? R. S = $R o U" |
|
155 |
mgu_Some "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U" |
|
156 |
mgu_free "mgu t1 t2 = Some U ==> \ |
|
157 |
\ (free_tv U) <= (free_tv t1) Un (free_tv t2)" |
|
1300 | 158 |
|
159 |
end |