src/HOL/MiniML/Instance.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5184 9b8547a9496a
child 14422 b8da5f258b04
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     1
(* Title:     HOL/MiniML/Instance.thy
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     2
   ID:        $Id$
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     4
   Copyright  1996 TU Muenchen
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     5
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     6
Instances of type schemes
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     7
*)
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     8
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     9
Instance = Type + 
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    10
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    11
  
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    12
(* generic instances of a type scheme *)
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    13
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    14
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    15
  bound_typ_inst :: [subst, type_scheme] => typ
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    16
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 4502
diff changeset
    17
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    18
  "bound_typ_inst S (FVar n) = (TVar n)"
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    19
  "bound_typ_inst S (BVar n) = (S n)"
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    20
  "bound_typ_inst S (sch1 =-> sch2) = ((bound_typ_inst S sch1) -> (bound_typ_inst S sch2))"
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    21
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    22
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    23
  bound_scheme_inst :: [nat => type_scheme, type_scheme] => type_scheme
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    24
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 4502
diff changeset
    25
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    26
  "bound_scheme_inst S (FVar n) = (FVar n)"
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    27
  "bound_scheme_inst S (BVar n) = (S n)"
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    28
  "bound_scheme_inst S (sch1 =-> sch2) = ((bound_scheme_inst S sch1) =-> (bound_scheme_inst S sch2))"
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    29
  
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    30
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    31
  "<|" :: [typ, type_scheme] => bool (infixr 70)
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    32
defs
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    33
  is_bound_typ_instance "t <| sch == ? S. t = (bound_typ_inst S sch)" 
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    34
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    35
instance type_scheme :: ord
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    36
defs le_type_scheme_def "sch' <= (sch::type_scheme) == !t. t <| sch' --> t <| sch"
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    37
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    38
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    39
  subst_to_scheme :: [nat => type_scheme, typ] => type_scheme
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    40
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 4502
diff changeset
    41
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    42
  "subst_to_scheme B (TVar n) = (B n)"
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    43
  "subst_to_scheme B (t1 -> t2) = ((subst_to_scheme B t1) =-> (subst_to_scheme B t2))"
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    44
  
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    45
instance list :: (ord)ord
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    46
defs le_env_def
4502
337c073de95e nth -> !
nipkow
parents: 2525
diff changeset
    47
  "A <= B == length B = length A & (!i. i < length A --> A!i <= B!i)"
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    48
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    49
end