src/HOL/MiniML/Type.thy

gave Greatest_le its proper name

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

MiniML-types and type substitutions.
*)

Type = Maybe + 

(* new class for structures containing type variables *)
axclass  type_struct < term 


(* type expressions *)
datatype
        typ = TVar nat | "->" typ typ (infixr 70)

(* type schemata *)
datatype
        type_scheme = FVar nat | BVar nat | "=->" type_scheme type_scheme (infixr 70)


(* embedding types into type schemata *)    
consts
  mk_scheme :: typ => type_scheme

primrec
  "mk_scheme (TVar n) = (FVar n)"
  "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"


instance  typ::type_struct
instance  type_scheme::type_struct  
instance  list::(type_struct)type_struct
instance  fun::(term,type_struct)type_struct


(* free_tv s: the type variables occuring freely in the type structure s *)

consts
  free_tv :: ['a::type_struct] => nat set

primrec
  free_tv_TVar    "free_tv (TVar m) = {m}"
  free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"

primrec
  "free_tv (FVar m) = {m}"
  "free_tv (BVar m) = {}"
  "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"

primrec
  "free_tv [] = {}"
  "free_tv (x#l) = (free_tv x) Un (free_tv l)"

  
(* executable version of free_tv: Implementation with lists *)
consts
  free_tv_ML :: ['a::type_struct] => nat list

primrec
  "free_tv_ML (FVar m) = [m]"
  "free_tv_ML (BVar m) = []"
  "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"

primrec
  "free_tv_ML [] = []"
  "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"

  
(* new_tv s n computes whether n is a new type variable w.r.t. a type 
   structure s, i.e. whether n is greater than any type variable 
   occuring in the type structure *)
constdefs
        new_tv :: [nat,'a::type_struct] => bool
        "new_tv n ts == ! m. m:(free_tv ts) --> m<n"

  
(* bound_tv s: the type variables occuring bound in the type structure s *)

consts
  bound_tv :: ['a::type_struct] => nat set

primrec
  "bound_tv (FVar m) = {}"
  "bound_tv (BVar m) = {m}"
  "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"

primrec
  "bound_tv [] = {}"
  "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"


(* minimal new free / bound variable *)

consts
  min_new_bound_tv :: 'a::type_struct => nat

primrec
  "min_new_bound_tv (FVar n) = 0"
  "min_new_bound_tv (BVar n) = Suc n"
  "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"


(* substitutions *)

(* type variable substitution *) 
types
        subst = nat => typ

(* identity *)
constdefs
        id_subst :: subst
        "id_subst == (%n. TVar n)"

(* extension of substitution to type structures *)
consts
  app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")

primrec
  app_subst_TVar "$ S (TVar n) = S n" 
  app_subst_Fun  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 

primrec
  "$ S (FVar n) = mk_scheme (S n)"
  "$ S (BVar n) = (BVar n)"
  "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"

defs
  app_subst_list "$ S == map ($ S)"

(* domain of a substitution *)
constdefs
        dom :: subst => nat set
        "dom S == {n. S n ~= TVar n}" 

(* codomain of a substitution: the introduced variables *)

constdefs
        cod :: subst => nat set
        "cod S == (UN m:dom S. (free_tv (S m)))"

defs
        free_tv_subst   "free_tv S == (dom S) Un (cod S)" 

  
(* unification algorithm mgu *)
consts
        mgu :: [typ,typ] => subst option
rules
        mgu_eq   "mgu t1 t2 = Some U ==> $U t1 = $U t2"
        mgu_mg   "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==>
                  ? R. S = $R o U"
        mgu_Some   "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U"
        mgu_free "mgu t1 t2 = Some U ==>   \
\		  (free_tv U) <= (free_tv t1) Un (free_tv t2)"

end