# Theory LambdaType

theory LambdaType
imports ListApplication
```(*  Title:      HOL/Proofs/Lambda/LambdaType.thy
Author:     Stefan Berghofer
*)

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"

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

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

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: "e ⊩ ts @ [t] : Ts ⟹
(⋀Us U. Ts = Us @ [U] ⟹ e ⊩ ts : Us ⟹ e ⊢ t : U ⟹ P) ⟹ P"
apply (cases Ts rule: rev_exhaust2)
apply simp
apply (case_tac "ts @ [t]")
done

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
```