(* Title: HOL/Proofs/Lambda/Standardization.thy Author: Stefan Berghofer Copyright 2005 TU Muenchen *) section ‹Standardization› theory Standardization imports NormalForm begin text ‹ Based on lecture notes by Ralph Matthes @{cite "Matthes-ESSLLI2000"}, original proof idea due to Ralph Loader @{cite Loader1998}. › subsection ‹Standard reduction relation› declare listrel_mono [mono_set] inductive sred :: "dB ⇒ dB ⇒ bool" (infixl "→⇩_{s}" 50) and sredlist :: "dB list ⇒ dB list ⇒ bool" (infixl "[→⇩_{s}]" 50) where "s [→⇩_{s}] t ≡ listrelp op →⇩_{s}s t" | Var: "rs [→⇩_{s}] rs' ⟹ Var x °° rs →⇩_{s}Var x °° rs'" | Abs: "r →⇩_{s}r' ⟹ ss [→⇩_{s}] ss' ⟹ Abs r °° ss →⇩_{s}Abs r' °° ss'" | Beta: "r[s/0] °° ss →⇩_{s}t ⟹ Abs r ° s °° ss →⇩_{s}t" lemma refl_listrelp: "∀x∈set xs. R x x ⟹ listrelp R xs xs" by (induct xs) (auto intro: listrelp.intros) lemma refl_sred: "t →⇩_{s}t" by (induct t rule: Apps_dB_induct) (auto intro: refl_listrelp sred.intros) lemma refl_sreds: "ts [→⇩_{s}] ts" by (simp add: refl_sred refl_listrelp) lemma listrelp_conj1: "listrelp (λx y. R x y ∧ S x y) x y ⟹ listrelp R x y" by (erule listrelp.induct) (auto intro: listrelp.intros) lemma listrelp_conj2: "listrelp (λx y. R x y ∧ S x y) x y ⟹ listrelp S x y" by (erule listrelp.induct) (auto intro: listrelp.intros) lemma listrelp_app: assumes xsys: "listrelp R xs ys" shows "listrelp R xs' ys' ⟹ listrelp R (xs @ xs') (ys @ ys')" using xsys by (induct arbitrary: xs' ys') (auto intro: listrelp.intros) lemma lemma1: assumes r: "r →⇩_{s}r'" and s: "s →⇩_{s}s'" shows "r ° s →⇩_{s}r' ° s'" using r proof induct case (Var rs rs' x) then have "rs [→⇩_{s}] rs'" by (rule listrelp_conj1) moreover have "[s] [→⇩_{s}] [s']" by (iprover intro: s listrelp.intros) ultimately have "rs @ [s] [→⇩_{s}] rs' @ [s']" by (rule listrelp_app) hence "Var x °° (rs @ [s]) →⇩_{s}Var x °° (rs' @ [s'])" by (rule sred.Var) thus ?case by (simp only: app_last) next case (Abs r r' ss ss') from Abs(3) have "ss [→⇩_{s}] ss'" by (rule listrelp_conj1) moreover have "[s] [→⇩_{s}] [s']" by (iprover intro: s listrelp.intros) ultimately have "ss @ [s] [→⇩_{s}] ss' @ [s']" by (rule listrelp_app) with ‹r →⇩_{s}r'› have "Abs r °° (ss @ [s]) →⇩_{s}Abs r' °° (ss' @ [s'])" by (rule sred.Abs) thus ?case by (simp only: app_last) next case (Beta r u ss t) hence "r[u/0] °° (ss @ [s]) →⇩_{s}t ° s'" by (simp only: app_last) hence "Abs r ° u °° (ss @ [s]) →⇩_{s}t ° s'" by (rule sred.Beta) thus ?case by (simp only: app_last) qed lemma lemma1': assumes ts: "ts [→⇩_{s}] ts'" shows "r →⇩_{s}r' ⟹ r °° ts →⇩_{s}r' °° ts'" using ts by (induct arbitrary: r r') (auto intro: lemma1) lemma lemma2_1: assumes beta: "t →⇩_{β}u" shows "t →⇩_{s}u" using beta proof induct case (beta s t) have "Abs s ° t °° [] →⇩_{s}s[t/0] °° []" by (iprover intro: sred.Beta refl_sred) thus ?case by simp next case (appL s t u) thus ?case by (iprover intro: lemma1 refl_sred) next case (appR s t u) thus ?case by (iprover intro: lemma1 refl_sred) next case (abs s t) hence "Abs s °° [] →⇩_{s}Abs t °° []" by (iprover intro: sred.Abs listrelp.Nil) thus ?case by simp qed lemma listrelp_betas: assumes ts: "listrelp op →⇩_{β}⇧^{*}ts ts'" shows "⋀t t'. t →⇩_{β}⇧^{*}t' ⟹ t °° ts →⇩_{β}⇧^{*}t' °° ts'" using ts by induct auto lemma lemma2_2: assumes t: "t →⇩_{s}u" shows "t →⇩_{β}⇧^{*}u" using t by induct (auto dest: listrelp_conj2 intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp) lemma sred_lift: assumes s: "s →⇩_{s}t" shows "lift s i →⇩_{s}lift t i" using s proof (induct arbitrary: i) case (Var rs rs' x) hence "map (λt. lift t i) rs [→⇩_{s}] map (λt. lift t i) rs'" by induct (auto intro: listrelp.intros) thus ?case by (cases "x < i") (auto intro: sred.Var) next case (Abs r r' ss ss') from Abs(3) have "map (λt. lift t i) ss [→⇩_{s}] map (λt. lift t i) ss'" by induct (auto intro: listrelp.intros) thus ?case by (auto intro: sred.Abs Abs) next case (Beta r s ss t) thus ?case by (auto intro: sred.Beta) qed lemma lemma3: assumes r: "r →⇩_{s}r'" shows "s →⇩_{s}s' ⟹ r[s/x] →⇩_{s}r'[s'/x]" using r proof (induct arbitrary: s s' x) case (Var rs rs' y) hence "map (λt. t[s/x]) rs [→⇩_{s}] map (λt. t[s'/x]) rs'" by induct (auto intro: listrelp.intros Var) moreover have "Var y[s/x] →⇩_{s}Var y[s'/x]" proof (cases "y < x") case True thus ?thesis by simp (rule refl_sred) next case False thus ?thesis by (cases "y = x") (auto simp add: Var intro: refl_sred) qed ultimately show ?case by simp (rule lemma1') next case (Abs r r' ss ss') from Abs(4) have "lift s 0 →⇩_{s}lift s' 0" by (rule sred_lift) hence "r[lift s 0/Suc x] →⇩_{s}r'[lift s' 0/Suc x]" by (fast intro: Abs.hyps) moreover from Abs(3) have "map (λt. t[s/x]) ss [→⇩_{s}] map (λt. t[s'/x]) ss'" by induct (auto intro: listrelp.intros Abs) ultimately show ?case by simp (rule sred.Abs) next case (Beta r u ss t) thus ?case by (auto simp add: subst_subst intro: sred.Beta) qed lemma lemma4_aux: assumes rs: "listrelp (λt u. t →⇩_{s}u ∧ (∀r. u →⇩_{β}r ⟶ t →⇩_{s}r)) rs rs'" shows "rs' => ss ⟹ rs [→⇩_{s}] ss" using rs proof (induct arbitrary: ss) case Nil thus ?case by cases (auto intro: listrelp.Nil) next case (Cons x y xs ys) note Cons' = Cons show ?case proof (cases ss) case Nil with Cons show ?thesis by simp next case (Cons y' ys') hence ss: "ss = y' # ys'" by simp from Cons Cons' have "y →⇩_{β}y' ∧ ys' = ys ∨ y' = y ∧ ys => ys'" by simp hence "x # xs [→⇩_{s}] y' # ys'" proof assume H: "y →⇩_{β}y' ∧ ys' = ys" with Cons' have "x →⇩_{s}y'" by blast moreover from Cons' have "xs [→⇩_{s}] ys" by (iprover dest: listrelp_conj1) ultimately have "x # xs [→⇩_{s}] y' # ys" by (rule listrelp.Cons) with H show ?thesis by simp next assume H: "y' = y ∧ ys => ys'" with Cons' have "x →⇩_{s}y'" by blast moreover from H have "xs [→⇩_{s}] ys'" by (blast intro: Cons') ultimately show ?thesis by (rule listrelp.Cons) qed with ss show ?thesis by simp qed qed lemma lemma4: assumes r: "r →⇩_{s}r'" shows "r' →⇩_{β}r'' ⟹ r →⇩_{s}r''" using r proof (induct arbitrary: r'') case (Var rs rs' x) then obtain ss where rs: "rs' => ss" and r'': "r'' = Var x °° ss" by (blast dest: head_Var_reduction) from Var(1) rs have "rs [→⇩_{s}] ss" by (rule lemma4_aux) hence "Var x °° rs →⇩_{s}Var x °° ss" by (rule sred.Var) with r'' show ?case by simp next case (Abs r r' ss ss') from ‹Abs r' °° ss' →⇩_{β}r''› show ?case proof fix s assume r'': "r'' = s °° ss'" assume "Abs r' →⇩_{β}s" then obtain r''' where s: "s = Abs r'''" and r''': "r' →⇩_{β}r'''" by cases auto from r''' have "r →⇩_{s}r'''" by (blast intro: Abs) moreover from Abs have "ss [→⇩_{s}] ss'" by (iprover dest: listrelp_conj1) ultimately have "Abs r °° ss →⇩_{s}Abs r''' °° ss'" by (rule sred.Abs) with r'' s show "Abs r °° ss →⇩_{s}r''" by simp next fix rs' assume "ss' => rs'" with Abs(3) have "ss [→⇩_{s}] rs'" by (rule lemma4_aux) with ‹r →⇩_{s}r'› have "Abs r °° ss →⇩_{s}Abs r' °° rs'" by (rule sred.Abs) moreover assume "r'' = Abs r' °° rs'" ultimately show "Abs r °° ss →⇩_{s}r''" by simp next fix t u' us' assume "ss' = u' # us'" with Abs(3) obtain u us where ss: "ss = u # us" and u: "u →⇩_{s}u'" and us: "us [→⇩_{s}] us'" by cases (auto dest!: listrelp_conj1) have "r[u/0] →⇩_{s}r'[u'/0]" using Abs(1) and u by (rule lemma3) with us have "r[u/0] °° us →⇩_{s}r'[u'/0] °° us'" by (rule lemma1') hence "Abs r ° u °° us →⇩_{s}r'[u'/0] °° us'" by (rule sred.Beta) moreover assume "Abs r' = Abs t" and "r'' = t[u'/0] °° us'" ultimately show "Abs r °° ss →⇩_{s}r''" using ss by simp qed next case (Beta r s ss t) show ?case by (rule sred.Beta) (rule Beta)+ qed lemma rtrancl_beta_sred: assumes r: "r →⇩_{β}⇧^{*}r'" shows "r →⇩_{s}r'" using r by induct (iprover intro: refl_sred lemma4)+ subsection ‹Leftmost reduction and weakly normalizing terms› inductive lred :: "dB ⇒ dB ⇒ bool" (infixl "→⇩_{l}" 50) and lredlist :: "dB list ⇒ dB list ⇒ bool" (infixl "[→⇩_{l}]" 50) where "s [→⇩_{l}] t ≡ listrelp op →⇩_{l}s t" | Var: "rs [→⇩_{l}] rs' ⟹ Var x °° rs →⇩_{l}Var x °° rs'" | Abs: "r →⇩_{l}r' ⟹ Abs r →⇩_{l}Abs r'" | Beta: "r[s/0] °° ss →⇩_{l}t ⟹ Abs r ° s °° ss →⇩_{l}t" lemma lred_imp_sred: assumes lred: "s →⇩_{l}t" shows "s →⇩_{s}t" using lred proof induct case (Var rs rs' x) then have "rs [→⇩_{s}] rs'" by induct (iprover intro: listrelp.intros)+ then show ?case by (rule sred.Var) next case (Abs r r') from ‹r →⇩_{s}r'› have "Abs r °° [] →⇩_{s}Abs r' °° []" using listrelp.Nil by (rule sred.Abs) then show ?case by simp next case (Beta r s ss t) from ‹r[s/0] °° ss →⇩_{s}t› show ?case by (rule sred.Beta) qed inductive WN :: "dB => bool" where Var: "listsp WN rs ⟹ WN (Var n °° rs)" | Lambda: "WN r ⟹ WN (Abs r)" | Beta: "WN ((r[s/0]) °° ss) ⟹ WN ((Abs r ° s) °° ss)" lemma listrelp_imp_listsp1: assumes H: "listrelp (λx y. P x) xs ys" shows "listsp P xs" using H by induct auto lemma listrelp_imp_listsp2: assumes H: "listrelp (λx y. P y) xs ys" shows "listsp P ys" using H by induct auto lemma lemma5: assumes lred: "r →⇩_{l}r'" shows "WN r" and "NF r'" using lred by induct (iprover dest: listrelp_conj1 listrelp_conj2 listrelp_imp_listsp1 listrelp_imp_listsp2 intro: WN.intros NF.intros [simplified listall_listsp_eq])+ lemma lemma6: assumes wn: "WN r" shows "∃r'. r →⇩_{l}r'" using wn proof induct case (Var rs n) then have "∃rs'. rs [→⇩_{l}] rs'" by induct (iprover intro: listrelp.intros)+ then show ?case by (iprover intro: lred.Var) qed (iprover intro: lred.intros)+ lemma lemma7: assumes r: "r →⇩_{s}r'" shows "NF r' ⟹ r →⇩_{l}r'" using r proof induct case (Var rs rs' x) from ‹NF (Var x °° rs')› have "listall NF rs'" by cases simp_all with Var(1) have "rs [→⇩_{l}] rs'" proof induct case Nil show ?case by (rule listrelp.Nil) next case (Cons x y xs ys) hence "x →⇩_{l}y" and "xs [→⇩_{l}] ys" by simp_all thus ?case by (rule listrelp.Cons) qed thus ?case by (rule lred.Var) next case (Abs r r' ss ss') from ‹NF (Abs r' °° ss')› have ss': "ss' = []" by (rule Abs_NF) from Abs(3) have ss: "ss = []" using ss' by cases simp_all from ss' Abs have "NF (Abs r')" by simp hence "NF r'" by cases simp_all with Abs have "r →⇩_{l}r'" by simp hence "Abs r →⇩_{l}Abs r'" by (rule lred.Abs) with ss ss' show ?case by simp next case (Beta r s ss t) hence "r[s/0] °° ss →⇩_{l}t" by simp thus ?case by (rule lred.Beta) qed lemma WN_eq: "WN t = (∃t'. t →⇩_{β}⇧^{*}t' ∧ NF t')" proof assume "WN t" then have "∃t'. t →⇩_{l}t'" by (rule lemma6) then obtain t' where t': "t →⇩_{l}t'" .. then have NF: "NF t'" by (rule lemma5) from t' have "t →⇩_{s}t'" by (rule lred_imp_sred) then have "t →⇩_{β}⇧^{*}t'" by (rule lemma2_2) with NF show "∃t'. t →⇩_{β}⇧^{*}t' ∧ NF t'" by iprover next assume "∃t'. t →⇩_{β}⇧^{*}t' ∧ NF t'" then obtain t' where t': "t →⇩_{β}⇧^{*}t'" and NF: "NF t'" by iprover from t' have "t →⇩_{s}t'" by (rule rtrancl_beta_sred) then have "t →⇩_{l}t'" using NF by (rule lemma7) then show "WN t" by (rule lemma5) qed end