(* Title: HOL/Proofs/Lambda/StrongNorm.thy
Author: Stefan Berghofer
Copyright 2000 TU Muenchen
*)
section \<open>Strong normalization for simply-typed lambda calculus\<close>
theory StrongNorm imports LambdaType InductTermi begin
text \<open>
Formalization by Stefan Berghofer. Partly based on a paper proof by
Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
\<close>
subsection \<open>Properties of \<open>IT\<close>\<close>
lemma lift_IT [intro!]: "IT t \ IT (lift t i)"
apply (induct arbitrary: i set: IT)
apply (simp (no_asm))
apply (rule conjI)
apply
(rule impI,
rule IT.Var,
erule listsp.induct,
simp (no_asm),
simp (no_asm),
rule listsp.Cons,
blast,
assumption)+
apply auto
done
lemma lifts_IT: "listsp IT ts \ listsp IT (map (\t. lift t 0) ts)"
by (induct ts) auto
lemma subst_Var_IT: "IT r \ IT (r[Var i/j])"
apply (induct arbitrary: i j set: IT)
txt \<open>Case \<^term>\<open>Var\<close>:\<close>
apply (simp (no_asm) add: subst_Var)
apply
((rule conjI impI)+,
rule IT.Var,
erule listsp.induct,
simp (no_asm),
simp (no_asm),
rule listsp.Cons,
fast,
assumption)+
txt \<open>Case \<^term>\<open>Lambda\<close>:\<close>
apply atomize
apply simp
apply (rule IT.Lambda)
apply fast
txt \<open>Case \<^term>\<open>Beta\<close>:\<close>
apply atomize
apply (simp (no_asm_use) add: subst_subst [symmetric])
apply (rule IT.Beta)
apply auto
done
lemma Var_IT: "IT (Var n)"
apply (subgoal_tac "IT (Var n \\ [])")
apply simp
apply (rule IT.Var)
apply (rule listsp.Nil)
done
lemma app_Var_IT: "IT t \ IT (t \ Var i)"
apply (induct set: IT)
apply (subst app_last)
apply (rule IT.Var)
apply simp
apply (rule listsp.Cons)
apply (rule Var_IT)
apply (rule listsp.Nil)
apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]])
apply (erule subst_Var_IT)
apply (rule Var_IT)
apply (subst app_last)
apply (rule IT.Beta)
apply (subst app_last [symmetric])
apply assumption
apply assumption
done
subsection \<open>Well-typed substitution preserves termination\<close>
lemma subst_type_IT:
"\t e T u i. IT t \ e\i:U\ \ t : T \
IT u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> IT (t[u/i])"
(is "PROP ?P U" is "\t e T u i. _ \ PROP ?Q t e T u i U")
proof (induct U)
fix T t
assume MI1: "\T1 T2. T = T1 \ T2 \ PROP ?P T1"
assume MI2: "\T1 T2. T = T1 \ T2 \ PROP ?P T2"
assume "IT t"
thus "\e T' u i. PROP ?Q t e T' u i T"
proof induct
fix e T' u i
assume uIT: "IT u"
assume uT: "e \ u : T"
{
case (Var rs n e1 T'1 u1 i1)
assume nT: "e\i:T\ \ Var n \\ rs : T'"
let ?ty = "\t. \T'. e\i:T\ \ t : T'"
let ?R = "\t. \e T' u i.
e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> IT u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> IT (t[u/i])"
show "IT ((Var n \\ rs)[u/i])"
proof (cases "n = i")
case True
show ?thesis
proof (cases rs)
case Nil
with uIT True show ?thesis by simp
next
case (Cons a as)
with nT have "e\i:T\ \ Var n \ a \\ as : T'" by simp
then obtain Ts
where headT: "e\i:T\ \ Var n \ a : Ts \ T'"
and argsT: "e\i:T\ \ as : Ts"
by (rule list_app_typeE)
from headT obtain T''
where varT: "e\i:T\ \ Var n : T'' \ Ts \ T'"
and argT: "e\i:T\ \ a : T''"
by cases simp_all
from varT True have T: "T = T'' \ Ts \ T'"
by cases auto
with uT have uT': "e \ u : T'' \ Ts \ T'" by simp
from T have "IT ((Var 0 \\ map (\t. lift t 0)
(map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0])"
proof (rule MI2)
from T have "IT ((lift u 0 \ Var 0)[a[u/i]/0])"
proof (rule MI1)
have "IT (lift u 0)" by (rule lift_IT [OF uIT])
thus "IT (lift u 0 \ Var 0)" by (rule app_Var_IT)
show "e\0:T''\ \ lift u 0 \ Var 0 : Ts \ T'"
proof (rule typing.App)
show "e\0:T''\ \ lift u 0 : T'' \ Ts \ T'"
by (rule lift_type) (rule uT')
show "e\0:T''\ \ Var 0 : T''"
by (rule typing.Var) simp
qed
from Var have "?R a" by cases (simp_all add: Cons)
with argT uIT uT show "IT (a[u/i])" by simp
from argT uT show "e \ a[u/i] : T''"
by (rule subst_lemma) simp
qed
thus "IT (u \ a[u/i])" by simp
from Var have "listsp ?R as"
by cases (simp_all add: Cons)
moreover from argsT have "listsp ?ty as"
by (rule lists_typings)
ultimately have "listsp (\t. ?R t \ ?ty t) as"
by simp
hence "listsp IT (map (\t. lift t 0) (map (\t. t[u/i]) as))"
(is "listsp IT (?ls as)")
proof induct
case Nil
show ?case by fastforce
next
case (Cons b bs)
hence I: "?R b" by simp
from Cons obtain U where "e\i:T\ \ b : U" by fast
with uT uIT I have "IT (b[u/i])" by simp
hence "IT (lift (b[u/i]) 0)" by (rule lift_IT)
hence "listsp IT (lift (b[u/i]) 0 # ?ls bs)"
by (rule listsp.Cons) (rule Cons)
thus ?case by simp
qed
thus "IT (Var 0 \\ ?ls as)" by (rule IT.Var)
have "e\0:Ts \ T'\ \ Var 0 : Ts \ T'"
by (rule typing.Var) simp
moreover from uT argsT have "e \ map (\t. t[u/i]) as : Ts"
by (rule substs_lemma)
hence "e\0:Ts \ T'\ \ ?ls as : Ts"
by (rule lift_types)
ultimately show "e\0:Ts \ T'\ \ Var 0 \\ ?ls as : T'"
by (rule list_app_typeI)
from argT uT have "e \ a[u/i] : T''"
by (rule subst_lemma) (rule refl)
with uT' show "e \ u \ a[u/i] : Ts \ T'"
by (rule typing.App)
qed
with Cons True show ?thesis
by (simp add: comp_def)
qed
next
case False
from Var have "listsp ?R rs" by simp
moreover from nT obtain Ts where "e\i:T\ \ rs : Ts"
by (rule list_app_typeE)
hence "listsp ?ty rs" by (rule lists_typings)
ultimately have "listsp (\t. ?R t \ ?ty t) rs"
by simp
hence "listsp IT (map (\x. x[u/i]) rs)"
proof induct
case Nil
show ?case by fastforce
next
case (Cons a as)
hence I: "?R a" by simp
from Cons obtain U where "e\i:T\ \ a : U" by fast
with uT uIT I have "IT (a[u/i])" by simp
hence "listsp IT (a[u/i] # map (\t. t[u/i]) as)"
by (rule listsp.Cons) (rule Cons)
thus ?case by simp
qed
with False show ?thesis by (auto simp add: subst_Var)
qed
next
case (Lambda r e1 T'1 u1 i1)
assume "e\i:T\ \ Abs r : T'"
and "\e T' u i. PROP ?Q r e T' u i T"
with uIT uT show "IT (Abs r[u/i])"
by fastforce
next
case (Beta r a as e1 T'1 u1 i1)
assume T: "e\i:T\ \ Abs r \ a \\ as : T'"
assume SI1: "\e T' u i. PROP ?Q (r[a/0] \\ as) e T' u i T"
assume SI2: "\e T' u i. PROP ?Q a e T' u i T"
have "IT (Abs (r[lift u 0/Suc i]) \ a[u/i] \\ map (\t. t[u/i]) as)"
proof (rule IT.Beta)
have "Abs r \ a \\ as \\<^sub>\ r[a/0] \\ as"
by (rule apps_preserves_beta) (rule beta.beta)
with T have "e\i:T\ \ r[a/0] \\ as : T'"
by (rule subject_reduction)
hence "IT ((r[a/0] \\ as)[u/i])"
using uIT uT by (rule SI1)
thus "IT (r[lift u 0/Suc i][a[u/i]/0] \\ map (\t. t[u/i]) as)"
by (simp del: subst_map add: subst_subst subst_map [symmetric])
from T obtain U where "e\i:T\ \ Abs r \ a : U"
by (rule list_app_typeE) fast
then obtain T'' where "e\i:T\ \ a : T''" by cases simp_all
thus "IT (a[u/i])" using uIT uT by (rule SI2)
qed
thus "IT ((Abs r \ a \\ as)[u/i])" by simp
}
qed
qed
subsection \<open>Well-typed terms are strongly normalizing\<close>
lemma type_implies_IT:
assumes "e \ t : T"
shows "IT t"
using assms
proof induct
case Var
show ?case by (rule Var_IT)
next
case Abs
show ?case by (rule IT.Lambda) (rule Abs)
next
case (App e s T U t)
have "IT ((Var 0 \ lift t 0)[s/0])"
proof (rule subst_type_IT)
have "IT (lift t 0)" using \<open>IT t\<close> by (rule lift_IT)
hence "listsp IT [lift t 0]" by (rule listsp.Cons) (rule listsp.Nil)
hence "IT (Var 0 \\ [lift t 0])" by (rule IT.Var)
also have "Var 0 \\ [lift t 0] = Var 0 \ lift t 0" by simp
finally show "IT \" .
have "e\0:T \ U\ \ Var 0 : T \ U"
by (rule typing.Var) simp
moreover have "e\0:T \ U\ \ lift t 0 : T"
by (rule lift_type) (rule App.hyps)
ultimately show "e\0:T \ U\ \ Var 0 \ lift t 0 : U"
by (rule typing.App)
show "IT s" by fact
show "e \ s : T \ U" by fact
qed
thus ?case by simp
qed
theorem type_implies_termi: "e \ t : T \ termip beta t"
proof -
assume "e \ t : T"
hence "IT t" by (rule type_implies_IT)
thus ?thesis by (rule IT_implies_termi)
qed
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
