src/HOL/MiniML/Instance.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5184 9b8547a9496a
child 14422 b8da5f258b04
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
nipkow@2525
     1
(* Title:     HOL/MiniML/Instance.thy
nipkow@2525
     2
   ID:        $Id$
nipkow@2525
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
nipkow@2525
     4
   Copyright  1996 TU Muenchen
nipkow@2525
     5
nipkow@2525
     6
Instances of type schemes
nipkow@2525
     7
*)
nipkow@2525
     8
nipkow@2525
     9
Instance = Type + 
nipkow@2525
    10
nipkow@2525
    11
  
nipkow@2525
    12
(* generic instances of a type scheme *)
nipkow@2525
    13
nipkow@2525
    14
consts
nipkow@2525
    15
  bound_typ_inst :: [subst, type_scheme] => typ
nipkow@2525
    16
berghofe@5184
    17
primrec
nipkow@2525
    18
  "bound_typ_inst S (FVar n) = (TVar n)"
nipkow@2525
    19
  "bound_typ_inst S (BVar n) = (S n)"
nipkow@2525
    20
  "bound_typ_inst S (sch1 =-> sch2) = ((bound_typ_inst S sch1) -> (bound_typ_inst S sch2))"
nipkow@2525
    21
nipkow@2525
    22
consts
nipkow@2525
    23
  bound_scheme_inst :: [nat => type_scheme, type_scheme] => type_scheme
nipkow@2525
    24
berghofe@5184
    25
primrec
nipkow@2525
    26
  "bound_scheme_inst S (FVar n) = (FVar n)"
nipkow@2525
    27
  "bound_scheme_inst S (BVar n) = (S n)"
nipkow@2525
    28
  "bound_scheme_inst S (sch1 =-> sch2) = ((bound_scheme_inst S sch1) =-> (bound_scheme_inst S sch2))"
nipkow@2525
    29
  
nipkow@2525
    30
consts
nipkow@2525
    31
  "<|" :: [typ, type_scheme] => bool (infixr 70)
nipkow@2525
    32
defs
nipkow@2525
    33
  is_bound_typ_instance "t <| sch == ? S. t = (bound_typ_inst S sch)" 
nipkow@2525
    34
nipkow@2525
    35
instance type_scheme :: ord
nipkow@2525
    36
defs le_type_scheme_def "sch' <= (sch::type_scheme) == !t. t <| sch' --> t <| sch"
nipkow@2525
    37
nipkow@2525
    38
consts
nipkow@2525
    39
  subst_to_scheme :: [nat => type_scheme, typ] => type_scheme
nipkow@2525
    40
berghofe@5184
    41
primrec
nipkow@2525
    42
  "subst_to_scheme B (TVar n) = (B n)"
nipkow@2525
    43
  "subst_to_scheme B (t1 -> t2) = ((subst_to_scheme B t1) =-> (subst_to_scheme B t2))"
nipkow@2525
    44
  
nipkow@2525
    45
instance list :: (ord)ord
nipkow@2525
    46
defs le_env_def
nipkow@4502
    47
  "A <= B == length B = length A & (!i. i < length A --> A!i <= B!i)"
nipkow@2525
    48
nipkow@2525
    49
end