src/HOL/MiniML/Instance.thy
author nipkow
Mon, 03 Nov 1997 09:58:06 +0100
changeset 4072 d0d32dd77440
parent 2525 477c05586286
child 4502 337c073de95e
permissions -rw-r--r--
expand_option_bind -> split_option_bind
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
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    17
primrec bound_typ_inst type_scheme
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
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    25
primrec bound_scheme_inst type_scheme
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
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    41
primrec subst_to_scheme typ
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
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    47
  "A <= B == length B = length A & (!i. i < length A --> nth i A <= nth i B)"
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