(* Title: HOL/Proofs/Lambda/StrongNorm.thy Author: Stefan Berghofer Copyright 2000 TU Muenchen *) section ‹Strong normalization for simply-typed lambda calculus› theory StrongNorm imports LambdaType 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 ‹IT›› 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 ‹Case @{term Var}:› 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 ‹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: "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 ‹Well-typed substitution preserves termination› lemma subst_type_IT: "⋀t e T u i. IT t ⟹ e⟨i:U⟩ ⊢ t : T ⟹ IT u ⟹ e ⊢ u : U ⟹ 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⟨i:T⟩ ⊢ t : T' ⟶ IT u ⟶ e ⊢ u : T ⟶ 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 (λt. t[u/i]) as))[(u ° 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 →⇩_{β}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 ‹Well-typed terms are strongly normalizing› 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 ‹IT t› 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