(* Title: HOL/Lambda/Eta.thy ID: $Id: Eta.thy,v 1.21 2005/09/22 21:56:35 nipkow Exp $ Author: Tobias Nipkow and Stefan Berghofer Copyright 1995, 2005 TU Muenchen *) header {* Eta-reduction *} theory Eta imports ParRed begin subsection {* Definition of eta-reduction and relatives *} consts free :: "dB => nat => bool" primrec "free (Var j) i = (j = i)" "free (s ° t) i = (free s i ∨ free t i)" "free (Abs s) i = free s (i + 1)" consts eta :: "(dB × dB) set" syntax "_eta" :: "[dB, dB] => bool" (infixl "-e>" 50) "_eta_rtrancl" :: "[dB, dB] => bool" (infixl "-e>>" 50) "_eta_reflcl" :: "[dB, dB] => bool" (infixl "-e>=" 50) translations "s -e> t" == "(s, t) ∈ eta" "s -e>> t" == "(s, t) ∈ eta^*" "s -e>= t" == "(s, t) ∈ eta^=" inductive eta intros eta [simp, intro]: "¬ free s 0 ==> Abs (s ° Var 0) -e> s[dummy/0]" appL [simp, intro]: "s -e> t ==> s ° u -e> t ° u" appR [simp, intro]: "s -e> t ==> u ° s -e> u ° t" abs [simp, intro]: "s -e> t ==> Abs s -e> Abs t" inductive_cases eta_cases [elim!]: "Abs s -e> z" "s ° t -e> u" "Var i -e> t" subsection "Properties of eta, subst and free" lemma subst_not_free [rule_format, simp]: "∀i t u. ¬ free s i --> s[t/i] = s[u/i]" apply (induct_tac s) apply (simp_all add: subst_Var) done lemma free_lift [simp]: "∀i k. free (lift t k) i = (i < k ∧ free t i ∨ k < i ∧ free t (i - 1))" apply (induct_tac t) apply (auto cong: conj_cong) apply arith done lemma free_subst [simp]: "∀i k t. free (s[t/k]) i = (free s k ∧ free t i ∨ free s (if i < k then i else i + 1))" apply (induct_tac s) prefer 2 apply simp apply blast prefer 2 apply simp apply (simp add: diff_Suc subst_Var split: nat.split) done lemma free_eta [rule_format]: "s -e> t ==> ∀i. free t i = free s i" apply (erule eta.induct) apply (simp_all cong: conj_cong) done lemma not_free_eta: "[| s -e> t; ¬ free s i |] ==> ¬ free t i" apply (simp add: free_eta) done lemma eta_subst [rule_format, simp]: "s -e> t ==> ∀u i. s[u/i] -e> t[u/i]" apply (erule eta.induct) apply (simp_all add: subst_subst [symmetric]) done theorem lift_subst_dummy: "!!i dummy. ¬ free s i ==> lift (s[dummy/i]) i = s" by (induct s) simp_all subsection "Confluence of eta" lemma square_eta: "square eta eta (eta^=) (eta^=)" apply (unfold square_def id_def) apply (rule impI [THEN allI [THEN allI]]) apply simp apply (erule eta.induct) apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1]) apply safe prefer 5 apply (blast intro!: eta_subst intro: free_eta [THEN iffD1]) apply blast+ done theorem eta_confluent: "confluent eta" apply (rule square_eta [THEN square_reflcl_confluent]) done subsection "Congruence rules for eta*" lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'" apply (erule rtrancl_induct) apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ done lemma rtrancl_eta_AppL: "s -e>> s' ==> s ° t -e>> s' ° t" apply (erule rtrancl_induct) apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ done lemma rtrancl_eta_AppR: "t -e>> t' ==> s ° t -e>> s ° t'" apply (erule rtrancl_induct) apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ done lemma rtrancl_eta_App: "[| s -e>> s'; t -e>> t' |] ==> s ° t -e>> s' ° t'" apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans) done subsection "Commutation of beta and eta" lemma free_beta [rule_format]: "s -> t ==> ∀i. free t i --> free s i" apply (erule beta.induct) apply simp_all done lemma beta_subst [rule_format, intro]: "s -> t ==> ∀u i. s[u/i] -> t[u/i]" apply (erule beta.induct) apply (simp_all add: subst_subst [symmetric]) done lemma subst_Var_Suc [simp]: "∀i. t[Var i/i] = t[Var(i)/i + 1]" apply (induct_tac t) apply (auto elim!: linorder_neqE simp: subst_Var) done lemma eta_lift [rule_format, simp]: "s -e> t ==> ∀i. lift s i -e> lift t i" apply (erule eta.induct) apply simp_all done lemma rtrancl_eta_subst [rule_format]: "∀s t i. s -e> t --> u[s/i] -e>> u[t/i]" apply (induct_tac u) apply (simp_all add: subst_Var) apply (blast) apply (blast intro: rtrancl_eta_App) apply (blast intro!: rtrancl_eta_Abs eta_lift) done lemma square_beta_eta: "square beta eta (eta^*) (beta^=)" apply (unfold square_def) apply (rule impI [THEN allI [THEN allI]]) apply (erule beta.induct) apply (slowsimp intro: rtrancl_eta_subst eta_subst) apply (blast intro: rtrancl_eta_AppL) apply (blast intro: rtrancl_eta_AppR) apply simp; apply (slowsimp intro: rtrancl_eta_Abs free_beta iff del: dB.distinct simp: dB.distinct) (*23 seconds?*) done lemma confluent_beta_eta: "confluent (beta ∪ eta)" apply (assumption | rule square_rtrancl_reflcl_commute confluent_Un beta_confluent eta_confluent square_beta_eta)+ done subsection "Implicit definition of eta" text {* @{term "Abs (lift s 0 ° Var 0) -e> s"} *} lemma not_free_iff_lifted [rule_format]: "∀i. (¬ free s i) = (∃t. s = lift t i)" apply (induct_tac s) apply simp apply clarify apply (rule iffI) apply (erule linorder_neqE) apply (rule_tac x = "Var nat" in exI) apply simp apply (rule_tac x = "Var (nat - 1)" in exI) apply simp apply clarify apply (rule notE) prefer 2 apply assumption apply (erule thin_rl) apply (case_tac t) apply simp apply simp apply simp apply simp apply (erule thin_rl) apply (erule thin_rl) apply (rule allI) apply (rule iffI) apply (elim conjE exE) apply (rename_tac u1 u2) apply (rule_tac x = "u1 ° u2" in exI) apply simp apply (erule exE) apply (erule rev_mp) apply (case_tac t) apply simp apply simp apply blast apply simp apply simp apply (erule thin_rl) apply (rule allI) apply (rule iffI) apply (erule exE) apply (rule_tac x = "Abs t" in exI) apply simp apply (erule exE) apply (erule rev_mp) apply (case_tac t) apply simp apply simp apply simp apply blast done theorem explicit_is_implicit: "(∀s u. (¬ free s 0) --> R (Abs (s ° Var 0)) (s[u/0])) = (∀s. R (Abs (lift s 0 ° Var 0)) s)" apply (auto simp add: not_free_iff_lifted) done subsection {* Parallel eta-reduction *} consts par_eta :: "(dB × dB) set" syntax "_par_eta" :: "[dB, dB] => bool" (infixl "=e>" 50) translations "s =e> t" == "(s, t) ∈ par_eta" syntax (xsymbols) "_par_eta" :: "[dB, dB] => bool" (infixl "=>η" 50) inductive par_eta intros var [simp, intro]: "Var x =>η Var x" eta [simp, intro]: "¬ free s 0 ==> s =>η s'==> Abs (s ° Var 0) =>η s'[dummy/0]" app [simp, intro]: "s =>η s' ==> t =>η t' ==> s ° t =>η s' ° t'" abs [simp, intro]: "s =>η t ==> Abs s =>η Abs t" lemma free_par_eta [simp]: assumes eta: "s =>η t" shows "!!i. free t i = free s i" using eta by induct (simp_all cong: conj_cong) lemma par_eta_refl [simp]: "t =>η t" by (induct t) simp_all lemma par_eta_lift [simp]: assumes eta: "s =>η t" shows "!!i. lift s i =>η lift t i" using eta by induct simp_all lemma par_eta_subst [simp]: assumes eta: "s =>η t" shows "!!u u' i. u =>η u' ==> s[u/i] =>η t[u'/i]" using eta by induct (simp_all add: subst_subst [symmetric] subst_Var) theorem eta_subset_par_eta: "eta ⊆ par_eta" apply (rule subsetI) apply clarify apply (erule eta.induct) apply (blast intro!: par_eta_refl)+ done theorem par_eta_subset_eta: "par_eta ⊆ eta*" apply (rule subsetI) apply clarify apply (erule par_eta.induct) apply blast apply (rule rtrancl_into_rtrancl) apply (rule rtrancl_eta_Abs) apply (rule rtrancl_eta_AppL) apply assumption apply (rule eta.eta) apply simp apply (rule rtrancl_eta_App) apply assumption+ apply (rule rtrancl_eta_Abs) apply assumption done subsection {* n-ary eta-expansion *} consts eta_expand :: "nat => dB => dB" primrec eta_expand_0: "eta_expand 0 t = t" eta_expand_Suc: "eta_expand (Suc n) t = Abs (lift (eta_expand n t) 0 ° Var 0)" lemma eta_expand_Suc': "!!t. eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 ° Var 0))" by (induct n) simp_all theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)" by (induct k) (simp_all add: lift_lift) theorem eta_expand_beta: assumes u: "u => u'" shows "!!t t'. t => t' ==> eta_expand k (Abs t) ° u => t'[u'/0]" proof (induct k) case 0 with u show ?case by simp next case (Suc k) hence "Abs (lift t (Suc 0)) ° Var 0 => lift t' (Suc 0)[Var 0/0]" by (blast intro: par_beta_lift) with Suc show ?case by (simp del: eta_expand_Suc add: eta_expand_Suc') qed theorem eta_expand_red: assumes t: "t => t'" shows "eta_expand k t => eta_expand k t'" by (induct k) (simp_all add: t) theorem eta_expand_eta: "!!t t'. t =>η t' ==> eta_expand k t =>η t'" proof (induct k) case 0 show ?case by simp next case (Suc k) have "Abs (lift (eta_expand k t) 0 ° Var 0) =>η lift t' 0[arbitrary/0]" by (fastsimp intro: par_eta_lift Suc) thus ?case by simp qed subsection {* Elimination rules for parallel eta reduction *} theorem par_eta_elim_app: assumes eta: "t =>η u" shows "!!u1' u2'. u = u1' ° u2' ==> ∃u1 u2 k. t = eta_expand k (u1 ° u2) ∧ u1 =>η u1' ∧ u2 =>η u2'" using eta proof induct case (app s s' t t') have "s ° t = eta_expand 0 (s ° t)" by simp with app show ?case by blast next case (eta dummy s s') then obtain u1'' u2'' where s': "s' = u1'' ° u2''" by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm) then have "∃u1 u2 k. s = eta_expand k (u1 ° u2) ∧ u1 =>η u1'' ∧ u2 =>η u2''" by (rule eta) then obtain u1 u2 k where s: "s = eta_expand k (u1 ° u2)" and u1: "u1 =>η u1''" and u2: "u2 =>η u2''" by iprover from u1 u2 eta s' have "¬ free u1 0" and "¬ free u2 0" by (simp_all del: free_par_eta add: free_par_eta [symmetric]) with s have "Abs (s ° Var 0) = eta_expand (Suc k) (u1[dummy/0] ° u2[dummy/0])" by (simp del: lift_subst add: lift_subst_dummy lift_eta_expand) moreover from u1 par_eta_refl have "u1[dummy/0] =>η u1''[dummy/0]" by (rule par_eta_subst) moreover from u2 par_eta_refl have "u2[dummy/0] =>η u2''[dummy/0]" by (rule par_eta_subst) ultimately show ?case using eta s' by (simp only: subst.simps dB.simps) blast next case var thus ?case by simp next case abs thus ?case by simp qed theorem par_eta_elim_abs: assumes eta: "t =>η t'" shows "!!u'. t' = Abs u' ==> ∃u k. t = eta_expand k (Abs u) ∧ u =>η u'" using eta proof induct case (abs s t) have "Abs s = eta_expand 0 (Abs s)" by simp with abs show ?case by blast next case (eta dummy s s') then obtain u'' where s': "s' = Abs u''" by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm) then have "∃u k. s = eta_expand k (Abs u) ∧ u =>η u''" by (rule eta) then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u =>η u''" by iprover from eta u s' have "¬ free u (Suc 0)" by (simp del: free_par_eta add: free_par_eta [symmetric]) with s have "Abs (s ° Var 0) = eta_expand (Suc k) (Abs (u[lift dummy 0/Suc 0]))" by (simp del: lift_subst add: lift_eta_expand lift_subst_dummy) moreover from u par_eta_refl have "u[lift dummy 0/Suc 0] =>η u''[lift dummy 0/Suc 0]" by (rule par_eta_subst) ultimately show ?case using eta s' by fastsimp next case var thus ?case by simp next case app thus ?case by simp qed subsection {* Eta-postponement theorem *} text {* Based on a proof by Masako Takahashi \cite{Takahashi-IandC}. *} theorem par_eta_beta: "!!s u. s =>η t ==> t => u ==> ∃t'. s => t' ∧ t' =>η u" proof (induct t rule: measure_induct [of size, rule_format]) case (1 t) from 1(3) show ?case proof cases case (var n) with 1 show ?thesis by (auto intro: par_beta_refl) next case (abs r' r'') with 1 have "s =>η Abs r'" by simp then obtain r k where s: "s = eta_expand k (Abs r)" and rr: "r =>η r'" by (blast dest: par_eta_elim_abs) from abs have "size r' < size t" by simp with abs(2) rr obtain t' where rt: "r => t'" and t': "t' =>η r''" by (blast dest: 1) with s abs show ?thesis by (auto intro: eta_expand_red eta_expand_eta) next case (app q' q'' r' r'') with 1 have "s =>η q' ° r'" by simp then obtain q r k where s: "s = eta_expand k (q ° r)" and qq: "q =>η q'" and rr: "r =>η r'" by (blast dest: par_eta_elim_app [OF _ refl]) from app have "size q' < size t" and "size r' < size t" by simp_all with app(2,3) qq rr obtain t' t'' where "q => t'" and "t' =>η q''" and "r => t''" and "t'' =>η r''" by (blast dest: 1) with s app show ?thesis by (fastsimp intro: eta_expand_red eta_expand_eta) next case (beta q' q'' r' r'') with 1 have "s =>η Abs q' ° r'" by simp then obtain q r k k' where s: "s = eta_expand k (eta_expand k' (Abs q) ° r)" and qq: "q =>η q'" and rr: "r =>η r'" by (blast dest: par_eta_elim_app par_eta_elim_abs) from beta have "size q' < size t" and "size r' < size t" by simp_all with beta(2,3) qq rr obtain t' t'' where "q => t'" and "t' =>η q''" and "r => t''" and "t'' =>η r''" by (blast dest: 1) with s beta show ?thesis by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst) qed qed theorem eta_postponement': assumes eta: "s -e>> t" shows "!!u. t => u ==> ∃t'. s => t' ∧ t' -e>> u" using eta [simplified rtrancl_subset [OF eta_subset_par_eta par_eta_subset_eta, symmetric]] proof induct case 1 thus ?case by blast next case (2 s' s'' s''') from 2 obtain t' where s': "s' => t'" and t': "t' =>η s'''" by (auto dest: par_eta_beta) from s' obtain t'' where s: "s => t''" and t'': "t'' -e>> t'" by (blast dest: 2) from par_eta_subset_eta t' have "t' -e>> s'''" .. with t'' have "t'' -e>> s'''" by (rule rtrancl_trans) with s show ?case by iprover qed theorem eta_postponement: assumes st: "(s, t) ∈ (beta ∪ eta)*" shows "(s, t) ∈ eta* O beta*" using st proof induct case 1 show ?case by blast next case (2 s' s'') from 2(3) obtain t' where s: "s ->β* t'" and t': "t' -e>> s'" by blast from 2(2) show ?case proof assume "s' -> s''" with beta_subset_par_beta have "s' => s''" .. with t' obtain t'' where st: "t' => t''" and tu: "t'' -e>> s''" by (auto dest: eta_postponement') from par_beta_subset_beta st have "t' ->β* t''" .. with s have "s ->β* t''" by (rule rtrancl_trans) thus ?thesis using tu .. next assume "s' -e> s''" with t' have "t' -e>> s''" .. with s show ?thesis .. qed qed end
lemmas eta_cases:
[| Abs s -e> z; !!dummy s. [| ¬ free s 0; s = s ° Var 0; z = s[dummy/0] |] ==> P; !!t. [| s -e> t; z = Abs t |] ==> P |] ==> P
[| s ° t -e> u; !!t. [| s -e> t; u = t ° t |] ==> P; !!t. [| t -e> t; u = s ° t |] ==> P |] ==> P
Var i -e> t ==> P
lemma subst_not_free:
¬ free s i ==> s[t/i] = s[u/i]
lemma free_lift:
∀i k. free (lift t k) i = (i < k ∧ free t i ∨ k < i ∧ free t (i - 1))
lemma free_subst:
∀i k t. free (s[t/k]) i = (free s k ∧ free t i ∨ free s (if i < k then i else i + 1))
lemma free_eta:
s -e> t ==> free t i = free s i
lemma not_free_eta:
[| s -e> t; ¬ free s i |] ==> ¬ free t i
lemma eta_subst:
s -e> t ==> s[u/i] -e> t[u/i]
theorem lift_subst_dummy:
¬ free s i ==> lift (s[dummy/i]) i = s
lemma square_eta:
square eta eta (eta=) (eta=)
theorem eta_confluent:
confluent eta
lemma rtrancl_eta_Abs:
s -e>> s' ==> Abs s -e>> Abs s'
lemma rtrancl_eta_AppL:
s -e>> s' ==> s ° t -e>> s' ° t
lemma rtrancl_eta_AppR:
t -e>> t' ==> s ° t -e>> s ° t'
lemma rtrancl_eta_App:
[| s -e>> s'; t -e>> t' |] ==> s ° t -e>> s' ° t'
lemma free_beta:
[| s -> t; free t i |] ==> free s i
lemma beta_subst:
s -> t ==> s[u/i] -> t[u/i]
lemma subst_Var_Suc:
∀i. t[Var i/i] = t[Var i/i + 1]
lemma eta_lift:
s -e> t ==> lift s i -e> lift t i
lemma rtrancl_eta_subst:
s -e> t ==> u[s/i] -e>> u[t/i]
lemma square_beta_eta:
square beta eta (eta*) (beta=)
lemma confluent_beta_eta:
confluent (beta ∪ eta)
lemma not_free_iff_lifted:
(¬ free s i) = (∃t. s = lift t i)
theorem explicit_is_implicit:
(∀s u. ¬ free s 0 --> R (Abs (s ° Var 0)) (s[u/0])) = (∀s. R (Abs (lift s 0 ° Var 0)) s)
lemma free_par_eta:
s =e> t ==> free t i = free s i
lemma par_eta_refl:
t =e> t
lemma par_eta_lift:
s =e> t ==> lift s i =e> lift t i
lemma par_eta_subst:
[| s =e> t; u =e> u' |] ==> s[u/i] =e> t[u'/i]
theorem eta_subset_par_eta:
eta ⊆ par_eta
theorem par_eta_subset_eta:
par_eta ⊆ eta*
lemma eta_expand_Suc':
eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 ° Var 0))
theorem lift_eta_expand:
lift (eta_expand k t) i = eta_expand k (lift t i)
theorem eta_expand_beta:
[| u => u'; t => t' |] ==> eta_expand k (Abs t) ° u => t'[u'/0]
theorem eta_expand_red:
t => t' ==> eta_expand k t => eta_expand k t'
theorem eta_expand_eta:
t =e> t' ==> eta_expand k t =e> t'
theorem par_eta_elim_app:
[| t =e> u; u = u1' ° u2' |] ==> ∃u1 u2 k. t = eta_expand k (u1 ° u2) ∧ u1 =e> u1' ∧ u2 =e> u2'
theorem par_eta_elim_abs:
[| t =e> t'; t' = Abs u' |] ==> ∃u k. t = eta_expand k (Abs u) ∧ u =e> u'
theorem par_eta_beta:
[| s =e> t; t => u |] ==> ∃t'. s => t' ∧ t' =e> u
theorem eta_postponement':
[| s -e>> t; t => u |] ==> ∃t'. s => t' ∧ t' -e>> u
theorem eta_postponement:
(s, t) ∈ (beta ∪ eta)* ==> (s, t) ∈ eta* O beta*