<commit_before>(* Title:     HOL/MiniML/Type.thy
   ID:        $Id$
   Author:    <NAME> and <NAME>
   Copyright  1995 TU Muenchen

MiniML-types and type substitutions.
*)

Type = Maybe + 

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

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

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

arities
        typ::type_struct
        list::(type_struct)type_struct
        fun::(term,type_struct)type_struct

(* substitutions *)

(* 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 ("$")

rules
        app_subst_TVar  "$ s (TVar n) = s n" 
        app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
defs
        app_subst_list  "$ s == map ($ s)"
  
(* free_tv s: the type variables occuring freely in the type structure s *)
consts
        free_tv :: ['a::type_struct] => nat set

rules
        free_tv_TVar    "free_tv (TVar m) = {m}"
        free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
        free_tv_Nil     "free_tv [] = {}"
        free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"

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

(* codomain of a substitutions: 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)"

(* 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"

(* unification algorithm mgu *)
consts
        mgu :: [typ,typ] => subst maybe
rules
        mgu_eq   "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
        mgu_mg   "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
                  ? r. s = $r o u"<commit_msg>replaced rules by primrec section<commit_after>(* Title:     HOL/MiniML/Type.thy
   ID:        $Id$
   Author:    <NAME> and <NAME>
   Copyright  1995 TU Muenchen

MiniML-types and type substitutions.
*)

Type = Maybe + 

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

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

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

arities
        typ::type_struct
        list::(type_struct)type_struct
        fun::(term,type_struct)type_struct

(* substitutions *)

(* 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 ("$")

rules
        app_subst_TVar  "$ s (TVar n) = s n" 
        app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
defs
        app_subst_list  "$ s == map ($ s)"
  
(* free_tv s: the type variables occuring freely in the type structure s *)
consts
        free_tv :: ['a::type_struct] => nat set

primrec free_tv typ
  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 List.list
  free_tv_Nil     "free_tv [] = {}"
  free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"

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

(* codomain of a substitutions: 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)"

(* 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"

(* unification algorithm mgu *)
consts
        mgu :: [typ,typ] => subst maybe
rules
        mgu_eq   "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
        mgu_mg   "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
                  ? r. s = $r o u"
{'fraction_non_alphanumeric': 0.13274336283185842, 'fraction_numerical': 0.009984116178806445, 'mean_word_length': 2.354642313546423, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 35, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1744516', 'n_tokens_mistral': 1619, 'n_tokens_neox': 1595, 'n_words': 510}