src/HOL/MiniML/Generalize.thy
author nipkow
Mon, 03 Nov 1997 09:58:06 +0100
changeset 4072 d0d32dd77440
parent 2625 69c1b8a493de
child 5184 9b8547a9496a
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/Generalize.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
Generalizing type schemes with respect to a context
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
Generalize = Instance +
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
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
    12
(* gen: binding (generalising) the variables which are not free in the context *)
2525
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
types ctxt = type_scheme list
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    15
    
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    16
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    17
  gen :: [ctxt, typ] => type_scheme
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    18
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    19
primrec gen typ
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    20
  "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
    21
  "gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    22
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    23
(* executable version of gen: Implementation with free_tv_ML *)
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
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    26
  gen_ML_aux :: [nat list, typ] => type_scheme
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    27
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    28
primrec gen_ML_aux typ
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    29
  "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
    30
  "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    31
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    32
consts
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    33
  gen_ML :: [ctxt, typ] => type_scheme
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
defs
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    36
  gen_ML_def "gen_ML A t == gen_ML_aux (free_tv_ML A) t"
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
end