Theory HOL-Proofs-Lambda.Eta
section ‹Eta-reduction›
theory Eta imports ParRed begin
subsection ‹Definition of eta-reduction and relatives›
primrec
free :: "dB => nat => bool"
where
"free (Var j) i = (j = i)"
| "free (s ° t) i = (free s i ∨ free t i)"
| "free (Abs s) i = free s (i + 1)"
inductive
eta :: "[dB, dB] => bool" (infixl ‹→⇩η› 50)
where
eta [simp, intro]: "¬ free s 0 ==> Abs (s ° Var 0) →⇩η s[dummy/0]"
| appL [simp, intro]: "s →⇩η t ==> s ° u →⇩η t ° u"
| appR [simp, intro]: "s →⇩η t ==> u ° s →⇩η u ° t"
| abs [simp, intro]: "s →⇩η t ==> Abs s →⇩η Abs t"
abbreviation
eta_reds :: "[dB, dB] => bool" (infixl ‹→⇩η⇧*› 50) where
"s →⇩η⇧* t == eta⇧*⇧* s t"
abbreviation
eta_red0 :: "[dB, dB] => bool" (infixl ‹→⇩η⇧=› 50) where
"s →⇩η⇧= t == eta⇧=⇧= s t"
inductive_cases eta_cases [elim!]:
"Abs s →⇩η z"
"s ° t →⇩η u"
"Var i →⇩η t"
subsection ‹Properties of ‹eta›, ‹subst› and ‹free››
lemma subst_not_free [simp]: "¬ free s i ⟹ s[t/i] = s[u/i]"
by (induct s arbitrary: i t u) (simp_all add: subst_Var)
lemma free_lift [simp]:
"free (lift t k) i = (i < k ∧ free t i ∨ k < i ∧ free t (i - 1))"
apply (induct t arbitrary: i k)
apply (auto cong: conj_cong)
done
lemma free_subst [simp]:
"free (s[t/k]) i =
(free s k ∧ free t i ∨ free s (if i < k then i else i + 1))"
apply (induct s arbitrary: i k t)
prefer 2
apply simp
apply blast
prefer 2
apply simp
apply (simp add: diff_Suc subst_Var split: nat.split)
done
lemma free_eta: "s →⇩η t ==> free t i = free s i"
by (induct arbitrary: i set: eta) (simp_all cong: conj_cong)
lemma not_free_eta:
"[| s →⇩η t; ¬ free s i |] ==> ¬ free t i"
by (simp add: free_eta)
lemma eta_subst [simp]:
"s →⇩η t ==> s[u/i] →⇩η t[u/i]"
by (induct arbitrary: u i set: eta) (simp_all add: subst_subst [symmetric])
theorem lift_subst_dummy: "¬ free s i ⟹ lift (s[dummy/i]) i = s"
by (induct s arbitrary: i dummy) 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 (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 →⇩η⇧* s' ==> Abs s →⇩η⇧* Abs s'"
by (induct set: rtranclp)
(blast intro: rtranclp.rtrancl_into_rtrancl)+
lemma rtrancl_eta_AppL: "s →⇩η⇧* s' ==> s ° t →⇩η⇧* s' ° t"
by (induct set: rtranclp)
(blast intro: rtranclp.rtrancl_into_rtrancl)+
lemma rtrancl_eta_AppR: "t →⇩η⇧* t' ==> s ° t →⇩η⇧* s ° t'"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
lemma rtrancl_eta_App:
"[| s →⇩η⇧* s'; t →⇩η⇧* t' |] ==> s ° t →⇩η⇧* s' ° t'"
by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtranclp_trans)
subsection ‹Commutation of ‹beta› and ‹eta››
lemma free_beta:
"s →⇩β t ==> free t i ⟹ free s i"
by (induct arbitrary: i set: beta) auto
lemma beta_subst [intro]: "s →⇩β t ==> s[u/i] →⇩β t[u/i]"
by (induct arbitrary: u i set: beta) (simp_all add: subst_subst [symmetric])
lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
by (induct t arbitrary: i) (auto elim!: linorder_neqE simp: subst_Var)
lemma eta_lift [simp]: "s →⇩η t ==> lift s i →⇩η lift t i"
by (induct arbitrary: i set: eta) simp_all
lemma rtrancl_eta_subst: "s →⇩η t ⟹ u[s/i] →⇩η⇧* u[t/i]"
apply (induct u arbitrary: s t i)
apply (simp_all add: subst_Var)
apply blast
apply (blast intro: rtrancl_eta_App)
apply (blast intro!: rtrancl_eta_Abs eta_lift)
done
lemma rtrancl_eta_subst':
fixes s t :: dB
assumes eta: "s →⇩η⇧* t"
shows "s[u/i] →⇩η⇧* t[u/i]" using eta
by induct (iprover intro: eta_subst)+
lemma rtrancl_eta_subst'':
fixes s t :: dB
assumes eta: "s →⇩η⇧* t"
shows "u[s/i] →⇩η⇧* u[t/i]" using eta
by induct (iprover intro: rtrancl_eta_subst rtranclp_trans)+
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)
done
lemma confluent_beta_eta: "confluent (sup 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) →⇩η s››
lemma not_free_iff_lifted:
"(¬ free s i) = (∃t. s = lift t i)"
apply (induct s arbitrary: i)
apply simp
apply (rule iffI)
apply (erule linorder_neqE)
apply (rename_tac nat a, rule_tac x = "Var nat" in exI)
apply simp
apply (rename_tac nat a, 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 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 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)"
by (auto simp add: not_free_iff_lifted)
subsection ‹Eta-postponement theorem›
text ‹
Based on a paper proof due to Andreas Abel.
Unlike the proof by Masako Takahashi \<^cite>‹"Takahashi-IandC"›, it does not
use parallel eta reduction, which only seems to complicate matters unnecessarily.
›
theorem eta_case:
fixes s :: dB
assumes free: "¬ free s 0"
and s: "s[dummy/0] => u"
shows "∃t'. Abs (s ° Var 0) => t' ∧ t' →⇩η⇧* u"
proof -
from s have "lift (s[dummy/0]) 0 => lift u 0" by (simp del: lift_subst)
with free have "s => lift u 0" by (simp add: lift_subst_dummy del: lift_subst)
hence "Abs (s ° Var 0) => Abs (lift u 0 ° Var 0)" by simp
moreover have "¬ free (lift u 0) 0" by simp
hence "Abs (lift u 0 ° Var 0) →⇩η lift u 0[dummy/0]"
by (rule eta.eta)
hence "Abs (lift u 0 ° Var 0) →⇩η⇧* u" by simp
ultimately show ?thesis by iprover
qed
theorem eta_par_beta:
assumes st: "s →⇩η t"
and tu: "t => u"
shows "∃t'. s => t' ∧ t' →⇩η⇧* u" using tu st
proof (induct arbitrary: s)
case (var n)
thus ?case by (iprover intro: par_beta_refl)
next
case (abs s' t)
note abs' = this
from ‹s →⇩η Abs s'› show ?case
proof cases
case (eta s'' dummy)
from abs have "Abs s' => Abs t" by simp
with eta have "s''[dummy/0] => Abs t" by simp
with ‹¬ free s'' 0› have "∃t'. Abs (s'' ° Var 0) => t' ∧ t' →⇩η⇧* Abs t"
by (rule eta_case)
with eta show ?thesis by simp
next
case (abs r)
from ‹r →⇩η s'›
obtain t' where r: "r => t'" and t': "t' →⇩η⇧* t" by (iprover dest: abs')
from r have "Abs r => Abs t'" ..
moreover from t' have "Abs t' →⇩η⇧* Abs t" by (rule rtrancl_eta_Abs)
ultimately show ?thesis using abs by simp iprover
qed
next
case (app u u' t t')
from ‹s →⇩η u ° t› show ?case
proof cases
case (eta s' dummy)
from app have "u ° t => u' ° t'" by simp
with eta have "s'[dummy/0] => u' ° t'" by simp
with ‹¬ free s' 0› have "∃r. Abs (s' ° Var 0) => r ∧ r →⇩η⇧* u' ° t'"
by (rule eta_case)
with eta show ?thesis by simp
next
case (appL s')
from ‹s' →⇩η u›
obtain r where s': "s' => r" and r: "r →⇩η⇧* u'" by (iprover dest: app)
from s' and app have "s' ° t => r ° t'" by simp
moreover from r have "r ° t' →⇩η⇧* u' ° t'" by (simp add: rtrancl_eta_AppL)
ultimately show ?thesis using appL by simp iprover
next
case (appR s')
from ‹s' →⇩η t›
obtain r where s': "s' => r" and r: "r →⇩η⇧* t'" by (iprover dest: app)
from s' and app have "u ° s' => u' ° r" by simp
moreover from r have "u' ° r →⇩η⇧* u' ° t'" by (simp add: rtrancl_eta_AppR)
ultimately show ?thesis using appR by simp iprover
qed
next
case (beta u u' t t')
from ‹s →⇩η Abs u ° t› show ?case
proof cases
case (eta s' dummy)
from beta have "Abs u ° t => u'[t'/0]" by simp
with eta have "s'[dummy/0] => u'[t'/0]" by simp
with ‹¬ free s' 0› have "∃r. Abs (s' ° Var 0) => r ∧ r →⇩η⇧* u'[t'/0]"
by (rule eta_case)
with eta show ?thesis by simp
next
case (appL s')
from ‹s' →⇩η Abs u› show ?thesis
proof cases
case (eta s'' dummy)
have "Abs (lift u 1) = lift (Abs u) 0" by simp
also from eta have "… = s''" by (simp add: lift_subst_dummy del: lift_subst)
finally have s: "s = Abs (Abs (lift u 1) ° Var 0) ° t" using appL and eta by simp
from beta have "lift u 1 => lift u' 1" by simp
hence "Abs (lift u 1) ° Var 0 => lift u' 1[Var 0/0]"
using par_beta.var ..
hence "Abs (Abs (lift u 1) ° Var 0) ° t => lift u' 1[Var 0/0][t'/0]"
using ‹t => t'› ..
with s have "s => u'[t'/0]" by simp
thus ?thesis by iprover
next
case (abs r)
from ‹r →⇩η u›
obtain r'' where r: "r => r''" and r'': "r'' →⇩η⇧* u'" by (iprover dest: beta)
from r and beta have "Abs r ° t => r''[t'/0]" by simp
moreover from r'' have "r''[t'/0] →⇩η⇧* u'[t'/0]"
by (rule rtrancl_eta_subst')
ultimately show ?thesis using abs and appL by simp iprover
qed
next
case (appR s')
from ‹s' →⇩η t›
obtain r where s': "s' => r" and r: "r →⇩η⇧* t'" by (iprover dest: beta)
from s' and beta have "Abs u ° s' => u'[r/0]" by simp
moreover from r have "u'[r/0] →⇩η⇧* u'[t'/0]"
by (rule rtrancl_eta_subst'')
ultimately show ?thesis using appR by simp iprover
qed
qed
theorem eta_postponement':
assumes eta: "s →⇩η⇧* t" and beta: "t => u"
shows "∃t'. s => t' ∧ t' →⇩η⇧* u" using eta beta
proof (induct arbitrary: u)
case base
thus ?case by blast
next
case (step s' s'' s''')
then obtain t' where s': "s' => t'" and t': "t' →⇩η⇧* s'''"
by (auto dest: eta_par_beta)
from s' obtain t'' where s: "s => t''" and t'': "t'' →⇩η⇧* t'" using step
by blast
from t'' and t' have "t'' →⇩η⇧* s'''" by (rule rtranclp_trans)
with s show ?case by iprover
qed
theorem eta_postponement:
assumes "(sup beta eta)⇧*⇧* s t"
shows "(beta⇧*⇧* OO eta⇧*⇧*) s t" using assms
proof induct
case base
show ?case by blast
next
case (step s' s'')
from step(3) obtain t' where s: "s →⇩β⇧* t'" and t': "t' →⇩η⇧* s'" by blast
from step(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'' →⇩η⇧* s''"
by (auto dest: eta_postponement')
from par_beta_subset_beta st have "t' →⇩β⇧* t''" ..
with s have "s →⇩β⇧* t''" by (rule rtranclp_trans)
thus ?thesis using tu ..
next
assume "s' →⇩η s''"
with t' have "t' →⇩η⇧* s''" ..
with s show ?thesis ..
qed
qed
end