src/HOL/MiniML/Type.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5184 9b8547a9496a
child 12338 de0f4a63baa5
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     1
(* Title:     HOL/MiniML/Type.thy
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     2
   ID:        $Id$
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
     4
   Copyright  1996 TU Muenchen
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     5
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     6
MiniML-types and type substitutions.
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     7
*)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     8
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     9
Type = Maybe + 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    10
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    11
(* new class for structures containing type variables *)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    12
axclass  type_struct < term 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    13
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    14
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    15
(* type expressions *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    16
datatype
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    17
        typ = TVar nat | "->" typ typ (infixr 70)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    18
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    19
(* type schemata *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    20
datatype
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    21
        type_scheme = FVar nat | BVar nat | "=->" type_scheme type_scheme (infixr 70)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    22
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    23
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    24
(* embedding types into type schemata *)    
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    25
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    26
  mk_scheme :: typ => type_scheme
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    27
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
    28
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    29
  "mk_scheme (TVar n) = (FVar n)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    30
  "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    31
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    32
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    33
instance  typ::type_struct
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    34
instance  type_scheme::type_struct  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    35
instance  list::(type_struct)type_struct
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    36
instance  fun::(term,type_struct)type_struct
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    37
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    38
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    39
(* free_tv s: the type variables occuring freely in the type structure s *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    40
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    41
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    42
  free_tv :: ['a::type_struct] => nat set
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    43
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
    44
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    45
  free_tv_TVar    "free_tv (TVar m) = {m}"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    46
  free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    47
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
    48
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    49
  "free_tv (FVar m) = {m}"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    50
  "free_tv (BVar m) = {}"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    51
  "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    52
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
    53
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    54
  "free_tv [] = {}"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    55
  "free_tv (x#l) = (free_tv x) Un (free_tv l)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    56
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
    57
  
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    58
(* executable version of free_tv: Implementation with lists *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    59
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    60
  free_tv_ML :: ['a::type_struct] => nat list
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    61
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
    62
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    63
  "free_tv_ML (FVar m) = [m]"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    64
  "free_tv_ML (BVar m) = []"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    65
  "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    66
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
    67
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    68
  "free_tv_ML [] = []"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    69
  "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    70
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    71
  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    72
(* new_tv s n computes whether n is a new type variable w.r.t. a type 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    73
   structure s, i.e. whether n is greater than any type variable 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    74
   occuring in the type structure *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    75
constdefs
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    76
        new_tv :: [nat,'a::type_struct] => bool
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    77
        "new_tv n ts == ! m. m:(free_tv ts) --> m<n"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    78
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    79
  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    80
(* bound_tv s: the type variables occuring bound in the type structure s *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    81
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    82
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    83
  bound_tv :: ['a::type_struct] => nat set
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    84
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
    85
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    86
  "bound_tv (FVar m) = {}"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    87
  "bound_tv (BVar m) = {m}"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    88
  "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    89
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
    90
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    91
  "bound_tv [] = {}"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    92
  "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    93
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    94
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    95
(* minimal new free / bound variable *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    96
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    97
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    98
  min_new_bound_tv :: 'a::type_struct => nat
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    99
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
   100
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   101
  "min_new_bound_tv (FVar n) = 0"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   102
  "min_new_bound_tv (BVar n) = Suc n"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   103
  "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   104
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   105
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   106
(* substitutions *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   107
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   108
(* type variable substitution *) 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   109
types
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
   110
        subst = nat => typ
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   111
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   112
(* identity *)
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1476
diff changeset
   113
constdefs
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
   114
        id_subst :: subst
3842
b55686a7b22c fixed dots;
wenzelm
parents: 2625
diff changeset
   115
        "id_subst == (%n. TVar n)"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   116
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   117
(* extension of substitution to type structures *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   118
consts
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   119
  app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   120
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
   121
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   122
  app_subst_TVar "$ S (TVar n) = S n" 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   123
  app_subst_Fun  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   124
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
   125
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   126
  "$ S (FVar n) = mk_scheme (S n)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   127
  "$ S (BVar n) = (BVar n)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   128
  "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
1604
cff41d1094ad replaced "rules" by "primrec"
nipkow
parents: 1575
diff changeset
   129
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   130
defs
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   131
  app_subst_list "$ S == map ($ S)"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   132
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   133
(* domain of a substitution *)
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1476
diff changeset
   134
constdefs
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
   135
        dom :: subst => nat set
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   136
        "dom S == {n. S n ~= TVar n}" 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   137
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   138
(* codomain of a substitution: the introduced variables *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   139
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1476
diff changeset
   140
constdefs
1575
4118fb066ba9 replaced rules by primrec section
clasohm
parents: 1557
diff changeset
   141
        cod :: subst => nat set
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   142
        "cod S == (UN m:dom S. (free_tv (S m)))"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   143
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   144
defs
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   145
        free_tv_subst   "free_tv S == (dom S) Un (cod S)" 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   146
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   147
  
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   148
(* unification algorithm mgu *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   149
consts
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   150
        mgu :: [typ,typ] => subst option
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   151
rules
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   152
        mgu_eq   "mgu t1 t2 = Some U ==> $U t1 = $U t2"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   153
        mgu_mg   "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==>
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   154
                  ? R. S = $R o U"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   155
        mgu_Some   "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   156
        mgu_free "mgu t1 t2 = Some U ==>   \
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
   157
\		  (free_tv U) <= (free_tv t1) Un (free_tv t2)"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   158
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   159
end