27 |
27 |
28 (* substitutions *) |
28 (* substitutions *) |
29 |
29 |
30 (* identity *) |
30 (* identity *) |
31 consts |
31 consts |
32 id_subst :: "subst" |
32 id_subst :: subst |
33 defs |
33 defs |
34 id_subst_def "id_subst == (%n.TVar n)" |
34 id_subst_def "id_subst == (%n.TVar n)" |
35 |
35 |
36 (* extension of substitution to type structures *) |
36 (* extension of substitution to type structures *) |
37 consts |
37 consts |
38 app_subst :: "[subst, 'a::type_struct] => 'a::type_struct" ("$") |
38 app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$") |
39 |
39 |
40 rules |
40 rules |
41 app_subst_TVar "$ s (TVar n) = s n" |
41 app_subst_TVar "$ s (TVar n) = s n" |
42 app_subst_Fun "$ s (Fun t1 t2) = Fun ($ s t1) ($ s t2)" |
42 app_subst_Fun "$ s (Fun t1 t2) = Fun ($ s t1) ($ s t2)" |
43 defs |
43 defs |
44 app_subst_list "$ s == map ($ s)" |
44 app_subst_list "$ s == map ($ s)" |
45 |
45 |
46 (* free_tv s: the type variables occuring freely in the type structure s *) |
46 (* free_tv s: the type variables occuring freely in the type structure s *) |
47 consts |
47 consts |
48 free_tv :: "['a::type_struct] => nat set" |
48 free_tv :: ['a::type_struct] => nat set |
49 |
49 |
50 rules |
50 rules |
51 free_tv_TVar "free_tv (TVar m) = {m}" |
51 free_tv_TVar "free_tv (TVar m) = {m}" |
52 free_tv_Fun "free_tv (Fun t1 t2) = (free_tv t1) Un (free_tv t2)" |
52 free_tv_Fun "free_tv (Fun t1 t2) = (free_tv t1) Un (free_tv t2)" |
53 free_tv_Nil "free_tv [] = {}" |
53 free_tv_Nil "free_tv [] = {}" |
54 free_tv_Cons "free_tv (x#l) = (free_tv x) Un (free_tv l)" |
54 free_tv_Cons "free_tv (x#l) = (free_tv x) Un (free_tv l)" |
55 |
55 |
56 (* domain of a substitution *) |
56 (* domain of a substitution *) |
57 consts |
57 consts |
58 dom :: "subst => nat set" |
58 dom :: subst => nat set |
59 defs |
59 defs |
60 dom_def "dom s == {n. s n ~= TVar n}" |
60 dom_def "dom s == {n. s n ~= TVar n}" |
61 |
61 |
62 (* codomain of a substitutions: the introduced variables *) |
62 (* codomain of a substitutions: the introduced variables *) |
63 consts |
63 consts |
64 cod :: "subst => nat set" |
64 cod :: subst => nat set |
65 defs |
65 defs |
66 cod_def "cod s == (UN m:dom s. free_tv (s m))" |
66 cod_def "cod s == (UN m:dom s. free_tv (s m))" |
67 |
67 |
68 defs |
68 defs |
69 free_tv_subst "free_tv s == (dom s) Un (cod s)" |
69 free_tv_subst "free_tv s == (dom s) Un (cod s)" |
70 |
70 |
71 (* new_tv s n computes whether n is a new type variable w.r.t. a type |
71 (* new_tv s n computes whether n is a new type variable w.r.t. a type |
72 structure s, i.e. whether n is greater than any type variable |
72 structure s, i.e. whether n is greater than any type variable |
73 occuring in the type structure *) |
73 occuring in the type structure *) |
74 consts |
74 consts |
75 new_tv :: "[nat,'a::type_struct] => bool" |
75 new_tv :: [nat,'a::type_struct] => bool |
76 defs |
76 defs |
77 new_tv_def "new_tv n ts == ! m. m:free_tv ts --> m<n" |
77 new_tv_def "new_tv n ts == ! m. m:free_tv ts --> m<n" |
78 |
78 |
79 (* unification algorithm mgu *) |
79 (* unification algorithm mgu *) |
80 consts |
80 consts |
81 mgu :: "[type_expr,type_expr] => subst maybe" |
81 mgu :: [type_expr,type_expr] => subst maybe |
82 rules |
82 rules |
83 mgu_eq "mgu t1 t2 = Ok u ==> $ u t1 = $ u t2" |
83 mgu_eq "mgu t1 t2 = Ok u ==> $ u t1 = $ u t2" |
84 mgu_mg "[| (mgu t1 t2) = Ok u; $ s t1 = $ s t2 |] ==> |
84 mgu_mg "[| (mgu t1 t2) = Ok u; $ s t1 = $ s t2 |] ==> |
85 ? r. s = ($ r) o u" |
85 ? r. s = ($ r) o u" |
86 mgu_Ok "$ s t1 = $ s t2 ==> ? u. mgu t1 t2 = Ok u" |
86 mgu_Ok "$ s t1 = $ s t2 ==> ? u. mgu t1 t2 = Ok u" |