section \<open>Basic definitions of Lambda-calculus\<close>
theory Lambda imports Main begin
declare [[syntax_ambiguity_warning = false]]
subsection \<open>Lambda-terms in de Bruijn notation and substitution\<close>
datatype dB =
Var nat
| App dB dB (infixl\<open>\<degree>\<close> 200)
| Abs dB
primrec
lift :: "[dB, nat] => dB" where "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
| "lift (s \ t) k = lift s k \ lift t k"
| "lift (Abs s) k = Abs (lift s (k + 1))"
primrec
subst :: "[dB, dB, nat] => dB" (\<open>_[_'/_]\<close> [300, 0, 0] 300) where(* FIXME base names *)
subst_Var: "(Var i)[s/k] =
(if k < i then Var (i - 1) else if i = k then s else Var i)"
| subst_App: "(t \ u)[s/k] = t[s/k] \ u[s/k]"
| subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
declare subst_Var [simp del]
text\<open>Optimized versions of \<^term>\<open>subst\<close> and \<^term>\<open>lift\<close>.\<close>
primrec
liftn :: "[nat, dB, nat] => dB" where "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
| "liftn n (s \ t) k = liftn n s k \ liftn n t k"
| "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
primrec
substn :: "[dB, dB, nat] => dB" where "substn (Var i) s k =
(if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
| "substn (t \ u) s k = substn t s k \ substn u s k"
| "substn (Abs t) s k = Abs (substn t s (k + 1))"
subsection \<open>Beta-reduction\<close>
inductive beta :: "[dB, dB] => bool" (infixl\<open>\<rightarrow>\<^sub>\<beta>\<close> 50) where
beta [simp, intro!]: "Abs s \ t \\<^sub>\ s[t/0]"
| appL [simp, intro!]: "s \\<^sub>\ t \ s \ u \\<^sub>\ t \ u"
| appR [simp, intro!]: "s \\<^sub>\ t \ u \ s \\<^sub>\ u \ t"
| abs [simp, intro!]: "s \\<^sub>\ t \ Abs s \\<^sub>\ Abs t"
abbreviation
beta_reds :: "[dB, dB] => bool" (infixl\<open>\<rightarrow>\<^sub>\<beta>\<^sup>*\<close> 50) where "s \\<^sub>\\<^sup>* t == beta\<^sup>*\<^sup>* s t"
inductive_cases beta_cases [elim!]: "Var i \\<^sub>\ t" "Abs r \\<^sub>\ s" "s \ t \\<^sub>\ u"
lemma rtrancl_beta_Abs [intro!]: "s \\<^sub>\\<^sup>* s' \ Abs s \\<^sub>\\<^sup>* Abs s'" by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
lemma rtrancl_beta_AppL: "s \\<^sub>\\<^sup>* s' \ s \ t \\<^sub>\\<^sup>* s' \ t" by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
lemma rtrancl_beta_AppR: "t \\<^sub>\\<^sup>* t' \ s \ t \\<^sub>\\<^sup>* s \ t'" by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
lemma rtrancl_beta_App [intro]: "\s \\<^sub>\\<^sup>* s'; t \\<^sub>\\<^sup>* t'\ \ s \ t \\<^sub>\\<^sup>* s' \ t'" by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
lemma subst_gt [simp]: "i < j \ (Var j)[u/i] = Var (j - 1)" by (simp add: subst_Var)
lemma subst_lt [simp]: "j < i \ (Var j)[u/i] = Var j" by (simp add: subst_Var)
lemma lift_lift: "i < k + 1 \ lift (lift t i) (Suc k) = lift (lift t k) i" by (induct t arbitrary: i k) auto
lemma lift_subst [simp]: "j < i + 1 \ lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]" by (induct t arbitrary: i j s)
(simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
lemma lift_subst_lt: "i < j + 1 \ lift (t[s/j]) i = (lift t i) [lift s i / j + 1]" by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift)
lemma subst_lift [simp]: "(lift t k)[s/k] = t" by (induct t arbitrary: k s) simp_all
lemma subst_subst: "i < j + 1 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]" by (induct t arbitrary: i j u v)
(simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
split: nat.split)
subsection \<open>Equivalence proof for optimized substitution\<close>
lemma liftn_0 [simp]: "liftn 0 t k = t" by (induct t arbitrary: k) (simp_all add: subst_Var)
lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k" by (induct t arbitrary: k) (simp_all add: subst_Var)
lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]" by (induct t arbitrary: n) (simp_all add: subst_Var)
theorem substn_subst_0: "substn t s 0 = t[s/0]" by simp
subsection \<open>Preservation theorems\<close>
text\<open>Not used in Church-Rosser proof, but in Strong
Normalization. \medskip\<close>
theorem subst_preserves_beta [simp]: "r \\<^sub>\ s \ r[t/i] \\<^sub>\ s[t/i]" by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
theorem subst_preserves_beta': "r \\<^sub>\\<^sup>* s \ r[t/i] \\<^sub>\\<^sup>* s[t/i]" proof (induct set: rtranclp) case base thenshow ?case by (iprover intro: rtrancl_refl) next case (step y z) thenshow ?case by (iprover intro: rtranclp.simps subst_preserves_beta) qed
theorem lift_preserves_beta [simp]: "r \\<^sub>\ s \ lift r i \\<^sub>\ lift s i" by (induct arbitrary: i set: beta) auto
theorem lift_preserves_beta': "r \\<^sub>\\<^sup>* s \ lift r i \\<^sub>\\<^sup>* lift s i" proof (induct set: rtranclp) case base thenshow ?case by (iprover intro: rtrancl_refl) next case (step y z) thenshow ?case by (iprover intro: lift_preserves_beta rtranclp.simps) qed
theorem subst_preserves_beta2 [simp]: "r \\<^sub>\ s \ t[r/i] \\<^sub>\\<^sup>* t[s/i]" proof (induct t arbitrary: r s i) case (Var x) thenshow ?case by (simp add: subst_Var r_into_rtranclp) next case (App t1 t2) thenshow ?case by (simp add: rtrancl_beta_App) next case (Abs t) thenshow ?caseby (simp add: rtrancl_beta_Abs) qed
theorem subst_preserves_beta2': "r \\<^sub>\\<^sup>* s \ t[r/i] \\<^sub>\\<^sup>* t[s/i]" proof (induct set: rtranclp) case base thenshow ?caseby (iprover intro: rtrancl_refl) next case (step y z) thenshow ?case by (iprover intro: rtranclp_trans subst_preserves_beta2) qed
end
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
