Theory LambdaType
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"
proof (induct ts arbitrary: Ts)
case Nil
then show ?case
by simp
next
case c: (Cons a ts)
show ?case
proof (cases Ts)
case Nil
with c show ?thesis
by simp
next
case (Cons T list)
with c show ?thesis by force
qed
qed
lemma types_snoc: "e ⊩ ts : Ts ⟹ e ⊢ t : T ⟹ e ⊩ ts @ [t] : Ts @ [T]"
by (induct ts arbitrary: Ts) (auto split: list.split_asm)
lemma types_snoc_eq: "e ⊩ ts @ [t] : Ts @ [T] =
(e ⊩ ts : Ts ∧ e ⊢ t : T)"
proof (induct ts arbitrary: Ts)
case Nil
then show ?case
by (auto split: list.split)
next
case (Cons a ts)
have "¬ e ⊩ ts @ [t] : []"
by (cases "ts @ [t]"; simp)
with Cons show ?case
by (auto split: list.split)
qed
text ‹Cannot use ‹rev_exhaust› from the ‹List› theory, since it is not constructive›
lemma rev_exhaust2 [extraction_expand]:
obtains (Nil) "xs = []" | (snoc) ys y where "xs = ys @ [y]"
proof -
have §: "xs = rev ys ⟹ thesis" for ys
by (cases ys) (simp_all add: local.Nil snoc)
show thesis
using § [of "rev xs"] by simp
qed
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"
proof (induct ts arbitrary: t T)
case Nil
then show ?case by auto
next
case (Cons a b t T)
then show ?case
by (auto simp: split: list.split)
qed
lemma list_app_typeE:
"e ⊢ t °° ts : T ⟹ (⋀Ts. e ⊢ t : Ts ⇛ T ⟹ e ⊩ ts : Ts ⟹ C) ⟹ C"
using list_app_typeD by iprover
lemma list_app_typeI:
"e ⊢ t : Ts ⇛ T ⟹ e ⊩ ts : Ts ⟹ e ⊢ t °° ts : T"
by (induct ts arbitrary: t Ts) (auto simp add: split: list.split_asm)
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"
by (induct ts arbitrary: T U rule: rev_induct) auto
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"
proof (induct us arbitrary: ts Ts U)
case Nil
then show ?case
by (simp add: var_app_type_eq)
next
case (Cons a b ts Ts U)
then show ?case
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 Ts' T')
apply (drule_tac T="Atom nat" and U="T' ⇒ Ts' ⇛ T" in var_app_type_eq)
apply assumption
apply simp
apply (rename_tac 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)
using var_app_type_eq apply fastforce
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)
using var_app_type_eq apply fastforce
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)
using var_app_type_eq by fastforce
qed
lemma var_app_typesE: "e ⊢ Var i °° ts : T ⟹
(⋀Ts. e ⊢ Var i : Ts ⇛ T ⟹ e ⊩ ts : Ts ⟹ P) ⟹ P"
by (iprover intro: typing.Var dest: var_app_types [of _ _ "[]", simplified])
lemma abs_typeE:
assumes "e ⊢ Abs t : T" "⋀U V. e⟨0:U⟩ ⊢ t : V ⟹ P"
shows "P"
proof (cases T)
case (Atom x1)
with assms(1) show ?thesis
apply-
apply (rule FalseE)
apply (erule typing.cases)
apply simp_all
done
next
case (Fun type1 type2)
with assms show ?thesis
apply atomize
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
qed
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"
by (induct ts arbitrary: Ts) (auto split: list.split)
subsection ‹Substitution lemmas›
lemma subst_lemma:
"e ⊢ t : T ⟹ e' ⊢ u : U ⟹ e = e'⟨i:U⟩ ⟹ e' ⊢ t[u/i] : T"
proof (induct arbitrary: e' i U u set: typing)
case (Var env x T)
then show ?case
by (force simp add: shift_def)
next
case (Abs env T t U)
then show ?case by force
qed auto
lemma substs_lemma:
"e ⊢ u : T ⟹ e⟨i:T⟩ ⊩ ts : Ts ⟹
e ⊩ (map (λt. t[u/i]) ts) : Ts"
proof (induct ts arbitrary: Ts)
case Nil
then show ?case
by auto
next
case (Cons a ts)
with subst_lemma show ?case
by (auto split: list.split)
qed
subsection ‹Subject reduction›
lemma subject_reduction: "e ⊢ t : T ⟹ t →⇩β t' ⟹ e ⊢ t' : T"
proof (induct arbitrary: t' set: typing)
case (App env s T U t)
with subst_lemma show ?case
by auto
qed auto
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