src/HOL/MiniML/Type.thy
author nipkow
Mon, 25 Mar 1996 08:46:02 +0100
changeset 1604 cff41d1094ad
parent 1575 4118fb066ba9
child 1900 c7a869229091
permissions -rw-r--r--
replaced "rules" by "primrec"
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$
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     3
   Author:    Dieter Nazareth and Tobias Nipkow
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     4
   Copyright  1995 TU Muenchen
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 *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    12
classes
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    13
        type_struct < term 
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
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    19
(* type variable substitution *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    20
types
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    21
        subst = nat => typ
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    22
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    23
arities
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    24
        typ::type_struct
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    25
        list::(type_struct)type_struct
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    26
        fun::(term,type_struct)type_struct
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    27
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    28
(* substitutions *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    29
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    30
(* identity *)
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1476
diff changeset
    31
constdefs
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    32
        id_subst :: subst
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1476
diff changeset
    33
        "id_subst == (%n.TVar n)"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    34
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    35
(* extension of substitution to type structures *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    36
consts
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    37
        app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    38
1604
cff41d1094ad replaced "rules" by "primrec"
nipkow
parents: 1575
diff changeset
    39
primrec app_subst typ
cff41d1094ad replaced "rules" by "primrec"
nipkow
parents: 1575
diff changeset
    40
  app_subst_TVar  "$ s (TVar n) = s n" 
cff41d1094ad replaced "rules" by "primrec"
nipkow
parents: 1575
diff changeset
    41
  app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
cff41d1094ad replaced "rules" by "primrec"
nipkow
parents: 1575
diff changeset
    42
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    43
defs
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    44
        app_subst_list  "$ s == map ($ s)"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    45
  
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    46
(* free_tv s: the type variables occuring freely in the type structure s *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    47
consts
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    48
        free_tv :: ['a::type_struct] => nat set
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    49
1575
4118fb066ba9 replaced rules by primrec section
clasohm
parents: 1557
diff changeset
    50
primrec free_tv typ
4118fb066ba9 replaced rules by primrec section
clasohm
parents: 1557
diff changeset
    51
  free_tv_TVar    "free_tv (TVar m) = {m}"
4118fb066ba9 replaced rules by primrec section
clasohm
parents: 1557
diff changeset
    52
  free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
4118fb066ba9 replaced rules by primrec section
clasohm
parents: 1557
diff changeset
    53
4118fb066ba9 replaced rules by primrec section
clasohm
parents: 1557
diff changeset
    54
primrec free_tv List.list
4118fb066ba9 replaced rules by primrec section
clasohm
parents: 1557
diff changeset
    55
  free_tv_Nil     "free_tv [] = {}"
4118fb066ba9 replaced rules by primrec section
clasohm
parents: 1557
diff changeset
    56
  free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    57
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    58
(* domain of a substitution *)
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1476
diff changeset
    59
constdefs
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    60
        dom :: subst => nat set
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1476
diff changeset
    61
        "dom s == {n. s n ~= TVar n}" 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    62
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    63
(* codomain of a substitutions: the introduced variables *)
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1476
diff changeset
    64
constdefs
1575
4118fb066ba9 replaced rules by primrec section
clasohm
parents: 1557
diff changeset
    65
        cod :: subst => nat set
4118fb066ba9 replaced rules by primrec section
clasohm
parents: 1557
diff changeset
    66
        "cod s == (UN m:dom s. free_tv (s m))"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    67
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    68
defs
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    69
        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
    70
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    71
(* new_tv s n computes whether n is a new type variable w.r.t. a type 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    72
   structure s, i.e. whether n is greater than any type variable 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    73
   occuring in the type structure *)
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1476
diff changeset
    74
constdefs
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    75
        new_tv :: [nat,'a::type_struct] => bool
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1476
diff changeset
    76
        "new_tv n ts == ! m. m:free_tv ts --> m<n"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    77
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    78
(* unification algorithm mgu *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    79
consts
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    80
        mgu :: [typ,typ] => subst maybe
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    81
rules
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    82
        mgu_eq   "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    83
        mgu_mg   "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    84
                  ? r. s = $r o u"
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    85
        mgu_Ok   "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    86
        mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    87
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    88
end
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    89