Theory Type

(* Title:     MiniML/Type.thy
   Author:    Wolfgang Naraschewski and Tobias Nipkow
   Copyright  1996 TU Muenchen
*)

section "MiniML-types and type substitutions"

theory Type
imports Maybe
begin

― ‹type expressions›
datatype "typ" = TVar nat | Fun "typ" "typ" (infixr ‹->› 70)

― ‹type schemata›
datatype type_scheme = FVar nat | BVar nat | SFun type_scheme type_scheme (infixr ‹=->› 70)

― ‹embedding types into type schemata›
fun mk_scheme :: "typ => type_scheme" where
  "mk_scheme (TVar n) = (FVar n)"
| "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"

― ‹type variable substitution›
type_synonym subst = "nat => typ"

class type_struct =
  fixes free_tv :: "'a => nat set"
    ― ‹@{text "free_tv s"}: the type variables occurring freely in the type structure s›
  fixes free_tv_ML :: "'a => nat list"
    ― ‹executable version of @{text free_tv}: Implementation with lists›
  fixes bound_tv :: "'a => nat set"
    ― ‹@{text "bound_tv s"}: the type variables occurring bound in the type structure s›
  fixes min_new_bound_tv :: "'a => nat"
    ― ‹minimal new free / bound variable›
  fixes app_subst :: "subst => 'a => 'a" (‹$›)
    ― ‹extension of substitution to type structures›

instantiation "typ" :: type_struct
begin

fun free_tv_typ where
  free_tv_TVar:    "free_tv (TVar m) = {m}"
| free_tv_Fun:     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"

fun app_subst_typ where
  app_subst_TVar: "$ S (TVar n) = S n" 
| app_subst_Fun:  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 

instance ..

end

instantiation type_scheme :: type_struct
begin

fun free_tv_type_scheme where
  "free_tv (FVar m) = {m}"
| "free_tv (BVar m) = {}"
| "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"

fun free_tv_ML_type_scheme where
  "free_tv_ML (FVar m) = [m]"
| "free_tv_ML (BVar m) = []"
| "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"

fun bound_tv_type_scheme where
  "bound_tv (FVar m) = {}"
| "bound_tv (BVar m) = {m}"
| "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"

fun min_new_bound_tv_type_scheme where
  "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)"

fun app_subst_type_scheme where
  "$ S (FVar n) = mk_scheme (S n)"
| "$ S (BVar n) = (BVar n)"
| "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"

instance ..

end

instantiation list :: (type_struct) type_struct
begin

fun free_tv_list where
  "free_tv [] = {}"
| "free_tv (x#l) = (free_tv x) Un (free_tv l)"

fun free_tv_ML_list where
  "free_tv_ML [] = []"
| "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"

fun bound_tv_list where
  "bound_tv [] = {}"
| "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"

definition app_subst_list where
  app_subst_list: "$ S = map ($ S)"

instance ..

end

text  
‹‹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 
   occurring in the type structure›
definition
  new_tv :: "[nat,'a::type_struct] => bool" where
  "new_tv n ts = (∀m. m:(free_tv ts) ⟶ m<n)"

― ‹identity›
definition
  id_subst :: subst where
  "id_subst = (λn. TVar n)"

― ‹domain of a substitution›
definition
  dom :: "subst => nat set" where
  "dom S = {n. S n ≠ TVar n}" 

― ‹codomain of a substitution: the introduced variables›
definition
  cod :: "subst => nat set" where
  "cod S = (UN m:dom S. (free_tv (S m)))"

class of_nat =
  fixes of_nat :: "nat ⇒ 'a"

instantiation nat :: of_nat
begin

definition
  "of_nat n = n"

instance ..

end

class typ_of =
  fixes typ_of :: "'a ⇒ typ"

instantiation "typ" :: typ_of
begin

definition
  "typ_of T = T"

instance ..

end

instantiation "fun" :: (of_nat, typ_of) type_struct
begin

definition free_tv_fun where
  "free_tv f = (let S = λn. typ_of (f (of_nat n)) in (dom S) Un (cod S))"

instance ..

end

lemma free_tv_subst:
  "free_tv S = (dom S) Un (cod S)"
by (simp add: free_tv_fun_def of_nat_nat_def typ_of_typ_def )

― ‹unification algorithm mgu›
axiomatization mgu :: "typ ⇒ typ ⇒ subst option" where
  mgu_eq:   "mgu t1 t2 = Some U ⟹ $U t1 = $U t2"
  and mgu_mg:   "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==> ∃R. S = $R ∘ U"
  and mgu_Some: "$S t1 = $S t2 ⟹ ∃U. mgu t1 t2 = Some U"
  and mgu_free: "mgu t1 t2 = Some U ⟹ free_tv U ⊆ free_tv t1 ∪ free_tv t2"


lemma mk_scheme_Fun:
  "mk_scheme t = sch1 =-> sch2 ⟹ (∃t1 t2. sch1 = mk_scheme t1 ∧ sch2 = mk_scheme t2)"
proof (induction t)
  case TVar thus ?case by auto
next
  case Fun thus ?case by auto
qed

lemma mk_scheme_injective: "(mk_scheme t = mk_scheme t') ⟹ t = t'"
proof (induction t arbitrary: t')
  case TVar thus ?case by(cases t') auto
next
  case Fun thus ?case by(cases t') auto
qed

lemma free_tv_mk_scheme[simp]: "free_tv (mk_scheme t) = free_tv t"
by (induction t) auto

lemma subst_mk_scheme[simp]: "$ S (mk_scheme t) = mk_scheme ($ S t)"
by (induction t) auto


― ‹constructor laws for @{text app_subst}›

lemma app_subst_Nil[simp]: 
  "$ S [] = []"
by (simp add: app_subst_list)

lemma app_subst_Cons[simp]: 
  "$ S (x#l) = ($ S x)#($ S l)"
by (simp add: app_subst_list)


― ‹constructor laws for @{text new_tv}›

lemma new_tv_TVar[simp]: 
  "new_tv n (TVar m) = (m<n)"
by (simp add: new_tv_def)

lemma new_tv_FVar[simp]: 
  "new_tv n (FVar m) = (m<n)"
by (simp add: new_tv_def)

lemma new_tv_BVar[simp]: 
  "new_tv n (BVar m) = True"
by (simp add: new_tv_def)

lemma new_tv_Fun[simp]: 
  "new_tv n (t1 -> t2) = (new_tv n t1 ∧ new_tv n t2)"
by (auto simp: new_tv_def)

lemma new_tv_Fun2[simp]: 
  "new_tv n (t1 =-> t2) = (new_tv n t1 ∧ new_tv n t2)"
by (auto simp: new_tv_def)

lemma new_tv_Nil[simp]: 
  "new_tv n []"
by (simp add: new_tv_def)

lemma new_tv_Cons[simp]: 
  "new_tv n (x#l) = (new_tv n x ∧ new_tv n l)"
by (auto simp: new_tv_def)

lemma new_tv_TVar_subst[simp]: "new_tv n TVar"
by (simp add: new_tv_def free_tv_subst dom_def cod_def)

lemma new_tv_id_subst [simp]: "new_tv n id_subst"
by (simp add: id_subst_def new_tv_def free_tv_subst dom_def cod_def)

lemma new_if_subst_type_scheme: "new_tv n (sch::type_scheme) ⟹
    $(λk. if k<n then S k else S' k) sch = $S sch"
by (induction sch) simp_all

lemma new_if_subst_type_scheme_list: "new_tv n (A::type_scheme list) ⟹
    $(λk. if k<n then S k else S' k) A = $S A"
by (induction A) (simp_all add: new_if_subst_type_scheme)


― ‹constructor laws for @{text dom} and @{text cod}›

lemma dom_id_subst [simp]: "dom id_subst = {}"
  unfolding dom_def id_subst_def empty_def by simp

lemma cod_id_subst [simp]: "cod id_subst = {}"
  unfolding cod_def by simp


lemma free_tv_id_subst [simp]: "free_tv id_subst = {}"
  unfolding free_tv_subst by simp

lemma free_tv_nth_A_impl_free_tv_A:
  "⟦ n < length A;  x : free_tv (A!n) ⟧ ⟹ x : free_tv A"
proof (induction A arbitrary: n)
  case Nil thus ?case by simp
next
  case (Cons a A)
  then show ?case by (fastforce simp add:nth_Cons' split: if_splits)
qed

text
‹if two substitutions yield the same result if applied to a type
   structure the substitutions coincide on the free type variables
   occurring in the type structure›

lemma typ_substitutions_only_on_free_variables: 
  "(∀x∈free_tv t. (S x) = (S' x)) ⟹ $ S (t::typ) = $ S' t"
  by (induct t) simp_all

lemma eq_free_eq_subst_te: "(∀n. n∈(free_tv t) ⟶ S1 n = S2 n) ⟹ $ S1 (t::typ) = $ S2 t"
apply (rule typ_substitutions_only_on_free_variables)
apply simp
done

lemma scheme_substitutions_only_on_free_variables:
  "(∀x∈free_tv sch. (S x) = (S' x)) ⟹ $ S (sch::type_scheme) = $ S' sch"
  by (induct sch) simp_all

lemma eq_free_eq_subst_type_scheme: 
  "(∀n. n∈(free_tv sch) ⟶ S1 n = S2 n) ⟹ $ S1 (sch::type_scheme) = $ S2 sch"
apply (rule scheme_substitutions_only_on_free_variables)
apply simp
done

lemma eq_free_eq_subst_scheme_list:
  "(∀n. n∈(free_tv A) ⟶ S1 n = S2 n) ⟹ $S1 (A::type_scheme list) = $S2 A"
proof (induct A)
  case Nil then show ?case by fastforce
next
  case Cons then show ?case by (fastforce intro: eq_free_eq_subst_type_scheme)
qed

lemma weaken_asm_Un: "((∀x∈A. (P x)) ⟶ Q) ⟹ ((∀x∈A ∪ B. (P x)) ⟶ Q)"
  by fast

lemma scheme_list_substitutions_only_on_free_variables:
  "(∀x∈free_tv A. (S x) = (S' x)) ⟹ $ S (A::type_scheme list) = $ S' A"
by (induction A) (auto simp add: eq_free_eq_subst_type_scheme)

lemma eq_subst_te_eq_free:
  "$ S1 (t::typ) = $ S2 t ⟹ n:(free_tv t) ⟹ S1 n = S2 n"
  by (induct t) auto

lemma eq_subst_type_scheme_eq_free: 
  "⟦ $ S1 (sch::type_scheme) = $ S2 sch; n:(free_tv sch) ⟧ ⟹ S1 n = S2 n"
by (induction "sch") (auto dest: mk_scheme_injective)

lemma eq_subst_scheme_list_eq_free:
  "⟦ $S1 (A::type_scheme list) = $S2 A;  n:(free_tv A) ⟧ ⟹ S1 n = S2 n"
proof (induct A)
  case Nil
  then show ?case by fastforce
next
  case Cons
  then show ?case by (fastforce intro: eq_subst_type_scheme_eq_free)
qed

lemma codD: "v : cod S ⟹ v : free_tv S"
  unfolding free_tv_subst by blast

lemma not_free_impl_id: "x ∉ free_tv S ⟹ S x = TVar x"
  unfolding free_tv_subst dom_def by blast

lemma free_tv_le_new_tv: "[| new_tv n t; m:free_tv t |] ==> m<n"
  unfolding new_tv_def by blast

lemma cod_app_subst:
  "[| v : free_tv(S n); v≠n |] ==> v : cod S"
by (force simp add: dom_def cod_def UNION_eq Bex_def)


lemma free_tv_subst_var: "free_tv (S (v::nat)) ⊆ insert v (cod S)"
apply (cases "v:dom S")
apply (fastforce simp add: cod_def)
apply (fastforce simp add: dom_def)
done

lemma free_tv_app_subst_te: "free_tv ($ S (t::typ)) ⊆ cod S ∪ free_tv t"
proof (induct t)
  case (TVar n) then show ?case by (simp add: free_tv_subst_var)
next
  case (Fun t1 t2) then show ?case by fastforce
qed

lemma free_tv_app_subst_type_scheme:
    "free_tv ($ S (sch::type_scheme)) ⊆ cod S ∪ free_tv sch"
proof (induct sch)
  case (FVar n)
  then show ?case by (simp add: free_tv_subst_var)
next
  case (BVar n)
  then show ?case by simp
next
  case (SFun t1 t2)
  then show ?case by fastforce
qed

lemma free_tv_app_subst_scheme_list: "free_tv ($ S (A::type_scheme list)) ⊆ cod S ∪ free_tv A"
proof (induct A)
  case Nil then show ?case by simp
next
  case (Cons a al)
  with free_tv_app_subst_type_scheme
  show ?case by fastforce
qed

lemma free_tv_comp_subst: 
  "free_tv (λu::nat. $ s1 (s2 u) :: typ) ⊆    
    free_tv s1 Un free_tv s2"
unfolding free_tv_subst dom_def
by (force simp add: cod_def dom_def dest!:free_tv_app_subst_te [THEN subsetD])

lemma free_tv_o_subst: 
  "free_tv ($ S1 ∘ S2) ⊆ free_tv S1 ∪ free_tv (S2 :: nat => typ)"
unfolding o_def by (rule free_tv_comp_subst)

lemma free_tv_of_substitutions_extend_to_types:
  "n : free_tv t ⟹ free_tv (S n) ⊆ free_tv ($ S t::typ)"
by (induct t) auto

lemma free_tv_of_substitutions_extend_to_schemes:
  "n : free_tv sch ⟹ free_tv (S n) ⊆ free_tv ($ S sch::type_scheme)"
by (induct sch) auto

lemma free_tv_of_substitutions_extend_to_scheme_lists [simp]:
  "n : free_tv A ⟹ free_tv (S n) ⊆ free_tv ($ S A::type_scheme list)"
by (induct A) (auto dest: free_tv_of_substitutions_extend_to_schemes)

lemma free_tv_ML_scheme:
  fixes sch :: type_scheme
  shows "(n : free_tv sch) = (n: set (free_tv_ML sch))"
by (induct sch) simp_all

lemma free_tv_ML_scheme_list:
  fixes A :: "type_scheme list"
  shows "(n : free_tv A) = (n: set (free_tv_ML A))"
by (induct_tac A) (simp_all add: free_tv_ML_scheme)


― ‹lemmata for @{text bound_tv}›

lemma bound_tv_mk_scheme [simp]: "bound_tv (mk_scheme t) = {}"
by (induct t) simp_all

lemma bound_tv_subst_scheme [simp]:
  fixes sch :: type_scheme
  shows "bound_tv ($ S sch) = bound_tv sch"
by (induct sch) simp_all

lemma bound_tv_subst_scheme_list [simp]: 
  fixes A :: "type_scheme list"
  shows "bound_tv ($ S A) = bound_tv A"
by (induct A) simp_all


― ‹Lemmata for @{text new_tv}›

lemma new_tv_subst: 
  "new_tv n S = ((∀m. n ≤ m ⟶ (S m = TVar m)) ∧  
                 (∀l. l < n ⟶ new_tv n (S l) ))"
unfolding new_tv_def  free_tv_subst cod_def dom_def
apply rule
 apply force
by simp (meson not_le)

lemma new_tv_list: "new_tv n x = (∀y∈set x. new_tv n y)"
by (induction x) simp_all

― ‹substitution affects only variables occurring freely›
lemma subst_te_new_tv:
  "new_tv n (t::typ) ⟹ $(λx. if x=n then t' else S x) t = $S t"
by (induct t) simp_all

lemma subst_te_new_type_scheme:
  "new_tv n (sch::type_scheme) ⟹ $(λx. if x=n then sch' else S x) sch = $S sch"
by (induct sch) simp_all

lemma subst_tel_new_scheme_list [simp]:
  "new_tv n (A::type_scheme list) ⟹ $(λx. if x=n then t else S x) A = $S A"
by (induct A) (simp_all add: subst_te_new_type_scheme)


― ‹all greater variables are also new›
lemma new_tv_le: 
  "n≤m ⟹ new_tv n t ⟹ new_tv m t"
by (meson less_le_trans new_tv_def)

lemma new_tv_Suc[simp]: "new_tv n t ⟹ new_tv (Suc n) t"
by (rule lessI [THEN less_imp_le [THEN new_tv_le]])

― ‹@{text new_tv} property remains if a substitution is applied›
lemma new_tv_subst_var: 
  "[| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)"
by (simp add: new_tv_subst)

lemma new_tv_subst_te [simp]:
  "new_tv n S ⟹ new_tv n (t::typ) ⟹ new_tv n ($ S t)"
by (induction t) (auto simp add: new_tv_subst)

lemma new_tv_subst_scheme_list:
  "new_tv n S ⟹ new_tv n (A::type_scheme list) ⟹ new_tv n ($ S A)"
by (meson UnE codD free_tv_app_subst_scheme_list in_mono new_tv_def)

lemma new_tv_only_depends_on_free_tv_type_scheme:
  fixes sch :: type_scheme
  shows "free_tv sch = free_tv sch' ⟹ new_tv n sch ⟹ new_tv n sch'"
  unfolding new_tv_def by simp

lemma new_tv_only_depends_on_free_tv_scheme_list:
  fixes A :: "type_scheme list"
  shows "free_tv A = free_tv A' ⟹ new_tv n A ⟹ new_tv n A'"
  unfolding new_tv_def by simp

lemma new_tv_nth_nat_A: 
  "m < length A ⟹ new_tv n A ⟹ new_tv n (A!m)"
unfolding new_tv_def using free_tv_nth_A_impl_free_tv_A by blast


― ‹composition of substitutions preserves @{text new_tv} proposition›
lemma new_tv_subst_comp_1: 
  "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (($ R) ∘ S)"
by (simp add: new_tv_subst)

lemma new_tv_subst_comp_2 :
  "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (λv.$ R (S v))"
by (simp add: new_tv_subst)

― ‹new type variables do not occur freely in a type structure›
lemma new_tv_not_free_tv:
  "new_tv n A ⟹ n ∉ free_tv A"
by (auto simp add: new_tv_def)

lemma fresh_variable_types: "∃n. new_tv n (t::typ)"
apply (unfold new_tv_def)
apply (induction t)
 apply auto[1]
by (metis less_trans linorder_cases new_tv_Fun new_tv_def)


lemma fresh_variable_type_schemes:
  "∃n. new_tv n (sch::type_scheme)"
apply (unfold new_tv_def)
apply (induct_tac sch)
  apply (auto)[1]
 apply simp
by (metis less_trans linorder_cases new_tv_Fun2 new_tv_def)

lemma fresh_variable_type_scheme_lists: 
  "∃n. new_tv n (A::type_scheme list)"
apply (induction A)
 apply (simp)
by (metis fresh_variable_type_schemes le_cases new_tv_Cons new_tv_le)

lemma make_one_new_out_of_two: 
  "[| ∃n1. (new_tv n1 x); ∃n2. (new_tv n2 y)|] ==> ∃n. (new_tv n x) ∧ (new_tv n y)"
by (meson new_tv_le nle_le)

lemma ex_fresh_variable: 
  "⋀(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ).  
          ∃n. (new_tv n A) ∧ (new_tv n A') ∧ (new_tv n t) ∧ (new_tv n t')"
by (meson fresh_variable_type_scheme_lists fresh_variable_types max.cobounded1 max.cobounded2 new_tv_le)

― ‹mgu does not introduce new type variables›
lemma mgu_new: 
  "[|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> new_tv n u"
by (meson UnE mgu_free new_tv_def subsetD)


(* lemmata for substitutions *)

lemma length_app_subst_list [simp]:
  "⋀A:: ('a::type_struct) list. length ($ S A) = length A"
unfolding app_subst_list by simp

lemma subst_TVar_scheme [simp]:
  fixes sch :: type_scheme
  shows "$ TVar sch = sch"
by (induct sch) simp_all

lemma subst_TVar_scheme_list [simp]:
  fixes A :: "type_scheme list"
  shows "$ TVar A = A"
by (induct A) (simp_all add: app_subst_list)

― ‹application of @{text id_subst} does not change type expression›
lemma app_subst_id_te [simp]: "$ id_subst = (λt::typ. t)"
by (metis id_subst_def mk_scheme_injective subst_TVar_scheme subst_mk_scheme)

lemma app_subst_id_type_scheme [simp]:
  "$ id_subst = (λsch::type_scheme. sch)"
using id_subst_def subst_TVar_scheme by auto


― ‹application of @{text id_subst} does not change list of type expressions›
lemma app_subst_id_tel [simp]: 
  "$ id_subst = (λA::type_scheme list. A)"
using id_subst_def subst_TVar_scheme_list by auto

― ‹composition of substitutions›
lemma o_id_subst [simp]: "$S ∘ id_subst = S"
unfolding id_subst_def o_def by simp

lemma subst_comp_te: "$ R ($ S t::typ) = $ (λx. $ R (S x) ) t"
by (induct t) simp_all

lemma subst_comp_type_scheme: 
  "$ R ($ S sch::type_scheme) = $ (λx. $ R (S x) ) sch"
by (induct sch) simp_all

lemma subst_comp_scheme_list: 
  "$ R ($ S A::type_scheme list) = $ (λx. $ R (S x)) A"
unfolding app_subst_list
proof (induct A)
  case Nil thus ?case by simp
next
  case Cons thus ?case by (simp add: subst_comp_type_scheme)
qed

lemma nth_subst: 
  "n < length A ⟹ ($ S A)!n = $S (A!n)"
by (simp add: app_subst_list)

end