Theory LambdaType

(*  Title:      HOL/Proofs/Lambda/LambdaType.thy
    Author:     Stefan Berghofer
    Copyright   2000 TU Muenchen
*)

section ‹Simply-typed lambda terms›

theory LambdaType imports ListApplication begin


subsection ‹Environments›

definition
  shift :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a ⇒ nat ⇒ 'a"  ("_⟨_:_⟩" [90, 0, 0] 91) where
  "e⟨i:a⟩ = (λj. if j < i then e j else if j = i then a else e (j - 1))"

lemma shift_eq [simp]: "i = j ⟹ (e⟨i:T⟩) j = T"
  by (simp add: shift_def)

lemma shift_gt [simp]: "j < i ⟹ (e⟨i:T⟩) j = e j"
  by (simp add: shift_def)

lemma shift_lt [simp]: "i < j ⟹ (e⟨i:T⟩) j = e (j - 1)"
  by (simp add: shift_def)

lemma shift_commute [simp]: "e⟨i:U⟩⟨0:T⟩ = e⟨0:T⟩⟨Suc i:U⟩"
  by (rule ext) (simp_all add: shift_def split: nat.split)


subsection ‹Types and typing rules›

datatype type =
    Atom nat
  | Fun type type    (infixr "⇒" 200)

inductive typing :: "(nat ⇒ type) ⇒ dB ⇒ type ⇒ bool"  ("_ ⊢ _ : _" [50, 50, 50] 50)
  where
    Var [intro!]: "env x = T ⟹ env ⊢ Var x : T"
  | Abs [intro!]: "env⟨0:T⟩ ⊢ t : U ⟹ env ⊢ Abs t : (T ⇒ U)"
  | App [intro!]: "env ⊢ s : T ⇒ U ⟹ env ⊢ t : T ⟹ env ⊢ (s ° t) : U"

inductive_cases typing_elims [elim!]:
  "e ⊢ Var i : T"
  "e ⊢ t ° u : T"
  "e ⊢ Abs t : T"

primrec
  typings :: "(nat ⇒ type) ⇒ dB list ⇒ type list ⇒ bool"
where
    "typings e [] Ts = (Ts = [])"
  | "typings e (t # ts) Ts =
      (case Ts of
        [] ⇒ False
      | T # Ts ⇒ e ⊢ t : T ∧ typings e ts Ts)"

abbreviation
  typings_rel :: "(nat ⇒ type) ⇒ dB list ⇒ type list ⇒ bool"
    ("_ ⊩ _ : _" [50, 50, 50] 50) where
  "env ⊩ ts : Ts == typings env ts Ts"

abbreviation
  funs :: "type list ⇒ type ⇒ type"  (infixr "⇛" 200) where
  "Ts ⇛ T == foldr Fun Ts T"


subsection ‹Some examples›

schematic_goal "e ⊢ Abs (Abs (Abs (Var 1 ° (Var 2 ° Var 1 ° Var 0)))) : ?T"
  by force

schematic_goal "e ⊢ Abs (Abs (Abs (Var 2 ° Var 0 ° (Var 1 ° Var 0)))) : ?T"
  by force


subsection ‹Lists of types›

lemma lists_typings:
    "e ⊩ ts : Ts ⟹ listsp (λt. ∃T. e ⊢ t : T) ts"
  apply (induct ts arbitrary: Ts)
   apply (case_tac Ts)
     apply simp
     apply (rule listsp.Nil)
    apply simp
  apply (case_tac Ts)
   apply simp
  apply simp
  apply (rule listsp.Cons)
   apply blast
  apply blast
  done

lemma types_snoc: "e ⊩ ts : Ts ⟹ e ⊢ t : T ⟹ e ⊩ ts @ [t] : Ts @ [T]"
  apply (induct ts arbitrary: Ts)
  apply simp
  apply (case_tac Ts)
  apply simp+
  done

lemma types_snoc_eq: "e ⊩ ts @ [t] : Ts @ [T] =
  (e ⊩ ts : Ts ∧ e ⊢ t : T)"
  apply (induct ts arbitrary: Ts)
  apply (case_tac Ts)
  apply simp+
  apply (case_tac Ts)
  apply (case_tac "ts @ [t]")
  apply simp+
  done

lemma rev_exhaust2 [extraction_expand]:
  obtains (Nil) "xs = []"  |  (snoc) ys y where "xs = ys @ [y]"
  ― ‹Cannot use ‹rev_exhaust› from the ‹List›
    theory, since it is not constructive›
  apply (subgoal_tac "∀ys. xs = rev ys ⟶ thesis")
  apply (erule_tac x="rev xs" in allE)
  apply simp
  apply (rule allI)
  apply (rule impI)
  apply (case_tac ys)
  apply simp
  apply simp
  done

lemma types_snocE:
  assumes ‹e ⊩ ts @ [t] : Ts›
  obtains Us and U where ‹Ts = Us @ [U]› ‹e ⊩ ts : Us› ‹e ⊢ t : U›
proof (cases Ts rule: rev_exhaust2)
  case Nil
  with assms show ?thesis
    by (cases "ts @ [t]") simp_all
next
  case (snoc Us U)
  with assms have "e ⊩ ts @ [t] : Us @ [U]" by simp
  then have "e ⊩ ts : Us" "e ⊢ t : U" by (simp_all add: types_snoc_eq)
  with snoc show ?thesis by (rule that)
qed


subsection ‹n-ary function types›

lemma list_app_typeD:
    "e ⊢ t °° ts : T ⟹ ∃Ts. e ⊢ t : Ts ⇛ T ∧ e ⊩ ts : Ts"
  apply (induct ts arbitrary: t T)
   apply simp
  apply (rename_tac a b t T)
  apply atomize
  apply simp
  apply (erule_tac x = "t ° a" in allE)
  apply (erule_tac x = T in allE)
  apply (erule impE)
   apply assumption
  apply (elim exE conjE)
  apply (ind_cases "e ⊢ t ° u : T" for t u T)
  apply (rule_tac x = "Ta # Ts" in exI)
  apply simp
  done

lemma list_app_typeE:
  "e ⊢ t °° ts : T ⟹ (⋀Ts. e ⊢ t : Ts ⇛ T ⟹ e ⊩ ts : Ts ⟹ C) ⟹ C"
  by (insert list_app_typeD) fast

lemma list_app_typeI:
    "e ⊢ t : Ts ⇛ T ⟹ e ⊩ ts : Ts ⟹ e ⊢ t °° ts : T"
  apply (induct ts arbitrary: t T Ts)
   apply simp
  apply (rename_tac a b t T Ts)
  apply atomize
  apply (case_tac Ts)
   apply simp
  apply simp
  apply (erule_tac x = "t ° a" in allE)
  apply (erule_tac x = T in allE)
  apply (rename_tac list)
  apply (erule_tac x = list in allE)
  apply (erule impE)
   apply (erule conjE)
   apply (erule typing.App)
   apply assumption
  apply blast
  done

text ‹
For the specific case where the head of the term is a variable,
the following theorems allow to infer the types of the arguments
without analyzing the typing derivation. This is crucial
for program extraction.
›

theorem var_app_type_eq:
  "e ⊢ Var i °° ts : T ⟹ e ⊢ Var i °° ts : U ⟹ T = U"
  apply (induct ts arbitrary: T U rule: rev_induct)
  apply simp
  apply (ind_cases "e ⊢ Var i : T" for T)
  apply (ind_cases "e ⊢ Var i : T" for T)
  apply simp
  apply simp
  apply (ind_cases "e ⊢ t ° u : T" for t u T)
  apply (ind_cases "e ⊢ t ° u : T" for t u T)
  apply atomize
  apply (erule_tac x="Ta ⇒ T" in allE)
  apply (erule_tac x="Tb ⇒ U" in allE)
  apply (erule impE)
  apply assumption
  apply (erule impE)
  apply assumption
  apply simp
  done

lemma var_app_types: "e ⊢ Var i °° ts °° us : T ⟹ e ⊩ ts : Ts ⟹
  e ⊢ Var i °° ts : U ⟹ ∃Us. U = Us ⇛ T ∧ e ⊩ us : Us"
  apply (induct us arbitrary: ts Ts U)
  apply simp
  apply (erule var_app_type_eq)
  apply assumption
  apply simp
  apply (rename_tac a b ts Ts U)
  apply atomize
  apply (case_tac U)
  apply (rule FalseE)
  apply simp
  apply (erule list_app_typeE)
  apply (ind_cases "e ⊢ t ° u : T" for t u T)
  apply (rename_tac nat Tsa Ta)
  apply (drule_tac T="Atom nat" and U="Ta ⇒ Tsa ⇛ T" in var_app_type_eq)
  apply assumption
  apply simp
  apply (rename_tac nat type1 type2)
  apply (erule_tac x="ts @ [a]" in allE)
  apply (erule_tac x="Ts @ [type1]" in allE)
  apply (erule_tac x="type2" in allE)
  apply simp
  apply (erule impE)
  apply (rule types_snoc)
  apply assumption
  apply (erule list_app_typeE)
  apply (ind_cases "e ⊢ t ° u : T" for t u T)
  apply (drule_tac T="type1 ⇒ type2" and U="Ta ⇒ Tsa ⇛ T" in var_app_type_eq)
  apply assumption
  apply simp
  apply (erule impE)
  apply (rule typing.App)
  apply assumption
  apply (erule list_app_typeE)
  apply (ind_cases "e ⊢ t ° u : T" for t u T)
  apply (frule_tac T="type1 ⇒ type2" and U="Ta ⇒ Tsa ⇛ T" in var_app_type_eq)
  apply assumption
  apply simp
  apply (erule exE)
  apply (rule_tac x="type1 # Us" in exI)
  apply simp
  apply (erule list_app_typeE)
  apply (ind_cases "e ⊢ t ° u : T" for t u T)
  apply (frule_tac T="type1 ⇒ Us ⇛ T" and U="Ta ⇒ Tsa ⇛ T" in var_app_type_eq)
  apply assumption
  apply simp
  done

lemma var_app_typesE: "e ⊢ Var i °° ts : T ⟹
  (⋀Ts. e ⊢ Var i : Ts ⇛ T ⟹ e ⊩ ts : Ts ⟹ P) ⟹ P"
  apply (drule var_app_types [of _ _ "[]", simplified])
  apply (iprover intro: typing.Var)+
  done

lemma abs_typeE: "e ⊢ Abs t : T ⟹ (⋀U V. e⟨0:U⟩ ⊢ t : V ⟹ P) ⟹ P"
  apply (cases T)
  apply (rule FalseE)
  apply (erule typing.cases)
  apply simp_all
  apply atomize
  apply (rename_tac type1 type2)
  apply (erule_tac x="type1" in allE)
  apply (erule_tac x="type2" in allE)
  apply (erule mp)
  apply (erule typing.cases)
  apply simp_all
  done


subsection ‹Lifting preserves well-typedness›

lemma lift_type [intro!]: "e ⊢ t : T ⟹ e⟨i:U⟩ ⊢ lift t i : T"
  by (induct arbitrary: i U set: typing) auto

lemma lift_types:
  "e ⊩ ts : Ts ⟹ e⟨i:U⟩ ⊩ (map (λt. lift t i) ts) : Ts"
  apply (induct ts arbitrary: Ts)
   apply simp
  apply (case_tac Ts)
   apply auto
  done


subsection ‹Substitution lemmas›

lemma subst_lemma:
    "e ⊢ t : T ⟹ e' ⊢ u : U ⟹ e = e'⟨i:U⟩ ⟹ e' ⊢ t[u/i] : T"
  apply (induct arbitrary: e' i U u set: typing)
    apply (rule_tac x = x and y = i in linorder_cases)
      apply auto
  apply blast
  done

lemma substs_lemma:
  "e ⊢ u : T ⟹ e⟨i:T⟩ ⊩ ts : Ts ⟹
     e ⊩ (map (λt. t[u/i]) ts) : Ts"
  apply (induct ts arbitrary: Ts)
   apply (case_tac Ts)
    apply simp
   apply simp
  apply atomize
  apply (case_tac Ts)
   apply simp
  apply simp
  apply (erule conjE)
  apply (erule (1) subst_lemma)
  apply (rule refl)
  done


subsection ‹Subject reduction›

lemma subject_reduction: "e ⊢ t : T ⟹ t →⇩β t' ⟹ e ⊢ t' : T"
  apply (induct arbitrary: t' set: typing)
    apply blast
   apply blast
  apply atomize
  apply (ind_cases "s ° t →⇩β t'" for s t t')
    apply hypsubst
    apply (ind_cases "env ⊢ Abs t : T ⇒ U" for env t T U)
    apply (rule subst_lemma)
      apply assumption
     apply assumption
    apply (rule ext)
    apply (case_tac x)
     apply auto
  done

theorem subject_reduction': "t →⇩β⇧* t' ⟹ e ⊢ t : T ⟹ e ⊢ t' : T"
  by (induct set: rtranclp) (iprover intro: subject_reduction)+


subsection ‹Alternative induction rule for types›

lemma type_induct [induct type]:
  assumes
  "(⋀T. (⋀T1 T2. T = T1 ⇒ T2 ⟹ P T1) ⟹
    (⋀T1 T2. T = T1 ⇒ T2 ⟹ P T2) ⟹ P T)"
  shows "P T"
proof (induct T)
  case Atom
  show ?case by (rule assms) simp_all
next
  case Fun
  show ?case by (rule assms) (insert Fun, simp_all)
qed

end