Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MiniML/Generalize.thy
author paulson
Wed, 02 Sep 1998 10:37:13 +0200
changeset 5424 771a68a468cc
parent 5184 9b8547a9496a
child 5518 654ead0ba4f7
permissions -rw-r--r--
modified proofs for new constrains_tac and ensures_tac

(* Title:     HOL/MiniML/Generalize.thy
   ID:        $Id$
   Author:    Wolfgang Naraschewski and Tobias Nipkow
   Copyright  1996 TU Muenchen

Generalizing type schemes with respect to a context
*)

Generalize = Instance +


(* gen: binding (generalising) the variables which are not free in the context *)

types ctxt = type_scheme list
    
consts
  gen :: [ctxt, typ] => type_scheme

primrec
  "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
  "gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"

(* executable version of gen: Implementation with free_tv_ML *)

consts
  gen_ML_aux :: [nat list, typ] => type_scheme

primrec
  "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
  "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"

consts
  gen_ML :: [ctxt, typ] => type_scheme

defs
  gen_ML_def "gen_ML A t == gen_ML_aux (free_tv_ML A) t"

end
isabelle