Up to index of Isabelle/HOL/Lambda
theory StrongNorm(* Title: HOL/Lambda/StrongNorm.thy ID: $Id: StrongNorm.thy,v 1.2 2005/06/17 14:13:08 haftmann Exp $ Author: Stefan Berghofer Copyright 2000 TU Muenchen *) header {* Strong normalization for simply-typed lambda calculus *} theory StrongNorm imports Type InductTermi begin text {* Formalization by Stefan Berghofer. Partly based on a paper proof by Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. *} subsection {* Properties of @{text IT} *} lemma lift_IT [intro!]: "t ∈ IT ==> (!!i. lift t i ∈ IT)" apply (induct set: IT) apply (simp (no_asm)) apply (rule conjI) apply (rule impI, rule IT.Var, erule lists.induct, simp (no_asm), rule lists.Nil, simp (no_asm), erule IntE, rule lists.Cons, blast, assumption)+ apply auto done lemma lifts_IT: "ts ∈ lists IT ==> map (λt. lift t 0) ts ∈ lists IT" by (induct ts) auto lemma subst_Var_IT: "r ∈ IT ==> (!!i j. r[Var i/j] ∈ IT)" apply (induct set: IT) txt {* Case @{term Var}: *} apply (simp (no_asm) add: subst_Var) apply ((rule conjI impI)+, rule IT.Var, erule lists.induct, simp (no_asm), rule lists.Nil, simp (no_asm), erule IntE, erule CollectE, rule lists.Cons, fast, assumption)+ txt {* Case @{term Lambda}: *} apply atomize apply simp apply (rule IT.Lambda) apply fast txt {* Case @{term Beta}: *} apply atomize apply (simp (no_asm_use) add: subst_subst [symmetric]) apply (rule IT.Beta) apply auto done lemma Var_IT: "Var n ∈ IT" apply (subgoal_tac "Var n °° [] ∈ IT") apply simp apply (rule IT.Var) apply (rule lists.Nil) done lemma app_Var_IT: "t ∈ IT ==> t ° Var i ∈ IT" apply (induct set: IT) apply (subst app_last) apply (rule IT.Var) apply simp apply (rule lists.Cons) apply (rule Var_IT) apply (rule lists.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 {* Well-typed substitution preserves termination *} lemma subst_type_IT: "!!t e T u i. t ∈ IT ==> e〈i:U〉 \<turnstile> t : T ==> u ∈ IT ==> e \<turnstile> u : U ==> t[u/i] ∈ IT" (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 "t ∈ IT" thus "!!e T' u i. PROP ?Q t e T' u i T" proof induct fix e T' u i assume uIT: "u ∈ IT" assume uT: "e \<turnstile> u : T" { case (Var n rs e_ T'_ u_ i_) assume nT: "e〈i:T〉 \<turnstile> Var n °° rs : T'" let ?ty = "{t. ∃T'. e〈i:T〉 \<turnstile> t : T'}" let ?R = "λt. ∀e T' u i. e〈i:T〉 \<turnstile> t : T' --> u ∈ IT --> e \<turnstile> u : T --> t[u/i] ∈ IT" show "(Var n °° rs)[u/i] ∈ IT" 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〉 \<turnstile> Var n ° a °° as : T'" by simp then obtain Ts where headT: "e〈i:T〉 \<turnstile> Var n ° a : Ts \<Rrightarrow> T'" and argsT: "e〈i:T〉 \<tturnstile> as : Ts" by (rule list_app_typeE) from headT obtain T'' where varT: "e〈i:T〉 \<turnstile> Var n : T'' => Ts \<Rrightarrow> T'" and argT: "e〈i:T〉 \<turnstile> a : T''" by cases simp_all from varT True have T: "T = T'' => Ts \<Rrightarrow> T'" by cases auto with uT have uT': "e \<turnstile> u : T'' => Ts \<Rrightarrow> T'" by simp from T have "(Var 0 °° map (λt. lift t 0) (map (λt. t[u/i]) as))[(u ° a[u/i])/0] ∈ IT" proof (rule MI2) from T have "(lift u 0 ° Var 0)[a[u/i]/0] ∈ IT" proof (rule MI1) have "lift u 0 ∈ IT" by (rule lift_IT) thus "lift u 0 ° Var 0 ∈ IT" by (rule app_Var_IT) show "e〈0:T''〉 \<turnstile> lift u 0 ° Var 0 : Ts \<Rrightarrow> T'" proof (rule typing.App) show "e〈0:T''〉 \<turnstile> lift u 0 : T'' => Ts \<Rrightarrow> T'" by (rule lift_type) (rule uT') show "e〈0:T''〉 \<turnstile> 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 "a[u/i] ∈ IT" by simp from argT uT show "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) simp qed thus "u ° a[u/i] ∈ IT" by simp from Var have "as ∈ lists {t. ?R t}" by cases (simp_all add: Cons) moreover from argsT have "as ∈ lists ?ty" by (rule lists_typings) ultimately have "as ∈ lists ({t. ?R t} ∩ ?ty)" by (rule lists_IntI) hence "map (λt. lift t 0) (map (λt. t[u/i]) as) ∈ lists IT" (is "(?ls as) ∈ _") proof induct case Nil show ?case by fastsimp next case (Cons b bs) hence I: "?R b" by simp from Cons obtain U where "e〈i:T〉 \<turnstile> b : U" by fast with uT uIT I have "b[u/i] ∈ IT" by simp hence "lift (b[u/i]) 0 ∈ IT" by (rule lift_IT) hence "lift (b[u/i]) 0 # ?ls bs ∈ lists IT" by (rule lists.Cons) (rule Cons) thus ?case by simp qed thus "Var 0 °° ?ls as ∈ IT" by (rule IT.Var) have "e〈0:Ts \<Rrightarrow> T'〉 \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp moreover from uT argsT have "e \<tturnstile> map (λt. t[u/i]) as : Ts" by (rule substs_lemma) hence "e〈0:Ts \<Rrightarrow> T'〉 \<tturnstile> ?ls as : Ts" by (rule lift_types) ultimately show "e〈0:Ts \<Rrightarrow> T'〉 \<turnstile> Var 0 °° ?ls as : T'" by (rule list_app_typeI) from argT uT have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) (rule refl) with uT' show "e \<turnstile> u ° a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App) qed with Cons True show ?thesis by (simp add: map_compose [symmetric] o_def) qed next case False from Var have "rs ∈ lists {t. ?R t}" by simp moreover from nT obtain Ts where "e〈i:T〉 \<tturnstile> rs : Ts" by (rule list_app_typeE) hence "rs ∈ lists ?ty" by (rule lists_typings) ultimately have "rs ∈ lists ({t. ?R t} ∩ ?ty)" by (rule lists_IntI) hence "map (λx. x[u/i]) rs ∈ lists IT" proof induct case Nil show ?case by fastsimp next case (Cons a as) hence I: "?R a" by simp from Cons obtain U where "e〈i:T〉 \<turnstile> a : U" by fast with uT uIT I have "a[u/i] ∈ IT" by simp hence "(a[u/i] # map (λt. t[u/i]) as) ∈ lists IT" by (rule lists.Cons) (rule Cons) thus ?case by simp qed with False show ?thesis by (auto simp add: subst_Var) qed next case (Lambda r e_ T'_ u_ i_) assume "e〈i:T〉 \<turnstile> Abs r : T'" and "!!e T' u i. PROP ?Q r e T' u i T" with uIT uT show "Abs r[u/i] ∈ IT" by fastsimp next case (Beta r a as e_ T'_ u_ i_) assume T: "e〈i:T〉 \<turnstile> 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 "Abs (r[lift u 0/Suc i]) ° a[u/i] °° map (λt. t[u/i]) as ∈ IT" proof (rule IT.Beta) have "Abs r ° a °° as ->β r[a/0] °° as" by (rule apps_preserves_beta) (rule beta.beta) with T have "e〈i:T〉 \<turnstile> r[a/0] °° as : T'" by (rule subject_reduction) hence "(r[a/0] °° as)[u/i] ∈ IT" by (rule SI1) thus "r[lift u 0/Suc i][a[u/i]/0] °° map (λt. t[u/i]) as ∈ IT" by (simp del: subst_map add: subst_subst subst_map [symmetric]) from T obtain U where "e〈i:T〉 \<turnstile> Abs r ° a : U" by (rule list_app_typeE) fast then obtain T'' where "e〈i:T〉 \<turnstile> a : T''" by cases simp_all thus "a[u/i] ∈ IT" by (rule SI2) qed thus "(Abs r ° a °° as)[u/i] ∈ IT" by simp } qed qed subsection {* Well-typed terms are strongly normalizing *} lemma type_implies_IT: "e \<turnstile> t : T ==> t ∈ IT" proof - assume "e \<turnstile> t : T" thus ?thesis proof induct case Var show ?case by (rule Var_IT) next case Abs show ?case by (rule IT.Lambda) next case (App T U e s t) have "(Var 0 ° lift t 0)[s/0] ∈ IT" proof (rule subst_type_IT) have "lift t 0 ∈ IT" by (rule lift_IT) hence "[lift t 0] ∈ lists IT" by (rule lists.Cons) (rule lists.Nil) hence "Var 0 °° [lift t 0] ∈ IT" 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〉 \<turnstile> Var 0 : T => U" by (rule typing.Var) simp moreover have "e〈0:T => U〉 \<turnstile> lift t 0 : T" by (rule lift_type) ultimately show "e〈0:T => U〉 \<turnstile> Var 0 ° lift t 0 : U" by (rule typing.App) qed thus ?case by simp qed qed theorem type_implies_termi: "e \<turnstile> t : T ==> t ∈ termi beta" proof - assume "e \<turnstile> t : T" hence "t ∈ IT" by (rule type_implies_IT) thus ?thesis by (rule IT_implies_termi) qed end
lemma lift_IT:
t ∈ IT ==> lift t i ∈ IT
lemma lifts_IT:
ts ∈ lists IT ==> map (%t. lift t 0) ts ∈ lists IT
lemma subst_Var_IT:
r ∈ IT ==> r[Var i/j] ∈ IT
lemma Var_IT:
Var n ∈ IT
lemma app_Var_IT:
t ∈ IT ==> t ° Var i ∈ IT
lemma subst_type_IT:
[| t ∈ IT; e〈i:U〉 |- t : T; u ∈ IT; e |- u : U |] ==> t[u/i] ∈ IT
lemma type_implies_IT:
e |- t : T ==> t ∈ IT
theorem type_implies_termi:
e |- t : T ==> t ∈ termi beta