Quelle CR_Takahashi.thy Sprache: Isabelle

(* Authors: Christian Urban and Mathilde Arnaud                   *)
(*                                                                *)
(* A formalisation of the Church-Rosser proof by Masako Takahashi.*)
(* This formalisation follows with some very slight exceptions    *)
(* the version of this proof given by Randy Pollack in the paper: *)
(*                                                                *)
(*  Polishing Up the Tait-Martin Löf Proof of the                 *)
(*  Church-Rosser Theorem (1995).                                 *)

theory CR_Takahashi
  imports "HOL-Nominal.Nominal"
begin

atom_decl name

nominal_datatype lam =
    Var "name"
  | App "lam" "lam"
  | Lam "\name\lam" (\Lam [_]._\ [100,100] 100)

nominal_primrec
  subst :: "lam \ name \ lam \ lam" (\_[_::=_]\ [100,100,100] 100)
where
  "(Var x)[y::=s] = (if x=y then s else (Var x))"
| "(App t\<^sub>1 t\<^sub>2)[y::=s] = App (t\<^sub>1[y::=s]) (t\<^sub>2[y::=s])"
| "x\(y,s) \ (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(fresh_guess)+
done

section \<open>Lemmas about Capture-Avoiding Substitution\<close>

lemma  subst_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi\(t1[x::=t2]) = (pi\t1)[(pi\x)::=(pi\t2)]"
by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)
   (auto simp add: perm_bij fresh_atm fresh_bij)

lemma forget:
  shows "x\t \ t[x::=s] = t"
by (nominal_induct t avoiding: x s rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_atm)

lemma fresh_fact:
  fixes z::"name"
  shows "\z\s; (z=y \ z\t)\ \ z\t[y::=s]"
by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_prod fresh_atm)

lemma substitution_lemma:
  assumes a: "x\y" "x\u"
  shows "t[x::=s][y::=u] = t[y::=u][x::=s[y::=u]]"
using a
by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)
   (auto simp add: fresh_fact forget)

lemma subst_rename:
  assumes a: "y\t"
  shows "t[x::=s] = ([(y,x)]\t)[y::=s]"
using a
by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
   (auto simp add: swap_simps fresh_atm abs_fresh)

section \<open>Beta-Reduction\<close>

inductive
  "Beta" :: "lam\lam\bool" (\ _ \\<^sub>\ _\ [80,80] 80)
where
  b1[intro]: "t1 \\<^sub>\ t2 \ App t1 s \\<^sub>\ App t2 s"
| b2[intro]: "s1 \\<^sub>\ s2 \ App t s1 \\<^sub>\ App t s2"
| b3[intro]: "t1 \\<^sub>\ t2 \ Lam [x].t1 \\<^sub>\ Lam [x].t2"
| b4[intro]: "App (Lam [x].t) s \\<^sub>\ t[x::=s]"

section \<open>Transitive Closure of Beta\<close>

inductive
  "Beta_star" :: "lam\lam\bool" (\ _ \\<^sub>\\<^sup>* _\ [80,80] 80)
where
  bs1[intro]: "t \\<^sub>\\<^sup>* t"
| bs2[intro]: "t \\<^sub>\ s \ t \\<^sub>\\<^sup>* s"
| bs3[intro,trans]: "\t1\\<^sub>\\<^sup>* t2; t2 \\<^sub>\\<^sup>* t3\ \ t1 \\<^sub>\\<^sup>* t3"

section \<open>One-Reduction\<close>

inductive
  One :: "lam\lam\bool" (\ _ \\<^sub>1 _\ [80,80] 80)
where
  o1[intro]: "Var x\\<^sub>1 Var x"
| o2[intro]: "\t1\\<^sub>1t2; s1\\<^sub>1s2\ \ App t1 s1 \\<^sub>1 App t2 s2"
| o3[intro]: "t1\\<^sub>1t2 \ Lam [x].t1 \\<^sub>1 Lam [x].t2"
| o4[intro]: "\x\(s1,s2); t1\\<^sub>1t2; s1\\<^sub>1s2\ \ App (Lam [x].t1) s1 \\<^sub>1 t2[x::=s2]"

equivariance One
nominal_inductive One
  by (simp_all add: abs_fresh fresh_fact)

lemma One_refl:
  shows "t \\<^sub>1 t"
by (nominal_induct t rule: lam.strong_induct) (auto)

lemma One_subst:
  assumes a: "t1 \\<^sub>1 t2" "s1 \\<^sub>1 s2"
  shows "t1[x::=s1] \\<^sub>1 t2[x::=s2]"
using a
by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
   (auto simp add: substitution_lemma fresh_atm fresh_fact)

lemma better_o4_intro:
  assumes a: "t1 \\<^sub>1 t2" "s1 \\<^sub>1 s2"
  shows "App (Lam [x].t1) s1 \\<^sub>1 t2[x::=s2]"
proof -
  obtain y::"name" where fs: "y\(x,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp, blast)
  have "App (Lam [x].t1) s1 = App (Lam [y].([(y,x)]\t1)) s1" using fs
    by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
  also have "\ \\<^sub>1 ([(y,x)]\t2)[y::=s2]" using fs a by (auto simp add: One.eqvt)
  also have "\ = t2[x::=s2]" using fs by (simp add: subst_rename[symmetric])
  finally show "App (Lam [x].t1) s1 \\<^sub>1 t2[x::=s2]" by simp
qed

lemma One_Var:
  assumes a: "Var x \\<^sub>1 M"
  shows "M = Var x"
using a by (cases rule: One.cases) (simp_all)

lemma One_Lam:
  assumes a: "Lam [x].t \\<^sub>1 s" "x\s"
  shows "\t'. s = Lam [x].t' \ t \\<^sub>1 t'"
using a
by (cases rule: One.strong_cases)
   (auto simp add: lam.inject abs_fresh alpha)

lemma One_App:
  assumes a: "App t s \\<^sub>1 r"
  shows "(\t' s'. r = App t' s' \ t \\<^sub>1 t' \ s \\<^sub>1 s') \
         (\<exists>x p p' s'. r = p'[x::=s'] \<and> t = Lam [x].p \<and> p \<longrightarrow>\<^sub>1 p' \<and> s \<longrightarrow>\<^sub>1 s' \<and> x\<sharp>(s,s'))"
using a by (cases rule: One.cases) (auto simp add: lam.inject)

lemma One_Redex:
  assumes a: "App (Lam [x].t) s \\<^sub>1 r" "x\(s,r)"
  shows "(\t' s'. r = App (Lam [x].t') s' \ t \\<^sub>1 t' \ s \\<^sub>1 s') \
         (\<exists>t' s'. r = t'[x::=s'] \<and> t \<longrightarrow>\<^sub>1 t' \<and> s \<longrightarrow>\<^sub>1 s')"
using a
by (cases rule: One.strong_cases)
   (auto dest: One_Lam simp add: lam.inject abs_fresh alpha fresh_prod)

section \<open>Transitive Closure of One\<close>

inductive
  "One_star" :: "lam\lam\bool" (\ _ \\<^sub>1\<^sup>* _\ [80,80] 80)
where
  os1[intro]: "t \\<^sub>1\<^sup>* t"
| os2[intro]: "t \\<^sub>1 s \ t \\<^sub>1\<^sup>* s"
| os3[intro]: "\t1\\<^sub>1\<^sup>* t2; t2 \\<^sub>1\<^sup>* t3\ \ t1 \\<^sub>1\<^sup>* t3"

section \<open>Complete Development Reduction\<close>

inductive
  Dev :: "lam \ lam \ bool" (\ _ \\<^sub>d _\ [80,80]80)
where
  d1[intro]: "Var x \\<^sub>d Var x"
| d2[intro]: "t \\<^sub>d s \ Lam [x].t \\<^sub>d Lam[x].s"
| d3[intro]: "\\(\y t'. t1 = Lam [y].t'); t1 \\<^sub>d t2; s1 \\<^sub>d s2\ \ App t1 s1 \\<^sub>d App t2 s2"
| d4[intro]: "\x\(s1,s2); t1 \\<^sub>d t2; s1 \\<^sub>d s2\ \ App (Lam [x].t1) s1 \\<^sub>d t2[x::=s2]"

equivariance Dev
nominal_inductive Dev
  by (simp_all add: abs_fresh fresh_fact)

lemma better_d4_intro:
  assumes a: "t1 \\<^sub>d t2" "s1 \\<^sub>d s2"
  shows "App (Lam [x].t1) s1 \\<^sub>d t2[x::=s2]"
proof -
  obtain y::"name" where fs: "y\(x,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp,blast)
  have "App (Lam [x].t1) s1 = App (Lam [y].([(y,x)]\t1)) s1" using fs
    by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
  also have "\ \\<^sub>d ([(y,x)]\t2)[y::=s2]" using fs a by (auto simp add: Dev.eqvt)
  also have "\ = t2[x::=s2]" using fs by (simp add: subst_rename[symmetric])
  finally show "App (Lam [x].t1) s1 \\<^sub>d t2[x::=s2]" by simp
qed

lemma Dev_preserves_fresh:
  fixes x::"name"
  assumes a: "M\\<^sub>d N"
  shows "x\M \ x\N"
using a
by (induct) (auto simp add: abs_fresh fresh_fact)

lemma Dev_Lam:
  assumes a: "Lam [x].M \\<^sub>d N"
  shows "\N'. N = Lam [x].N' \ M \\<^sub>d N'"
proof -
  from a have "x\Lam [x].M" by (simp add: abs_fresh)
  with a have "x\N" by (simp add: Dev_preserves_fresh)
  with a show "\N'. N = Lam [x].N' \ M \\<^sub>d N'"
    by (cases rule: Dev.strong_cases)
       (auto simp add: lam.inject abs_fresh alpha)
qed

lemma Development_existence:
  shows "\M'. M \\<^sub>d M'"
by (nominal_induct M rule: lam.strong_induct)
   (auto dest!: Dev_Lam intro: better_d4_intro)

lemma Triangle:
  assumes a: "t \\<^sub>d t1" "t \\<^sub>1 t2"
  shows "t2 \\<^sub>1 t1"
using a
proof(nominal_induct avoiding: t2 rule: Dev.strong_induct)
  case (d4 x s1 s2 t1 t1' t2)
  have  fc: "x\t2" "x\s1" by fact+
  have "App (Lam [x].t1) s1 \\<^sub>1 t2" by fact
  then obtain t' s' where reds:
             "(t2 = App (Lam [x].t') s' \ t1 \\<^sub>1 t' \ s1 \\<^sub>1 s') \
              (t2 = t'[x::=s'] \<and> t1 \<longrightarrow>\<^sub>1 t' \<and> s1 \<longrightarrow>\<^sub>1 s')"
  using fc by (auto dest!: One_Redex)
  have ih1: "t1 \\<^sub>1 t' \ t' \\<^sub>1 t1'" by fact
  have ih2: "s1 \\<^sub>1 s' \ s' \\<^sub>1 s2" by fact
  { assume "t1 \\<^sub>1 t'" "s1 \\<^sub>1 s'"
    then have "App (Lam [x].t') s' \\<^sub>1 t1'[x::=s2]"
      using ih1 ih2 by (auto intro: better_o4_intro)
  }
  moreover
  { assume "t1 \\<^sub>1 t'" "s1 \\<^sub>1 s'"
    then have "t'[x::=s'] \\<^sub>1 t1'[x::=s2]"
      using ih1 ih2 by (auto intro: One_subst)
  }
  ultimately show "t2 \\<^sub>1 t1'[x::=s2]" using reds by auto
qed (auto dest!: One_Lam One_Var One_App)

lemma Diamond_for_One:
  assumes a: "t \\<^sub>1 t1" "t \\<^sub>1 t2"
  shows "\t3. t2 \\<^sub>1 t3 \ t1 \\<^sub>1 t3"
proof -
  obtain tc where "t \\<^sub>d tc" using Development_existence by blast
  with a have "t2 \\<^sub>1 tc" and "t1 \\<^sub>1 tc" by (simp_all add: Triangle)
  then show "\t3. t2 \\<^sub>1 t3 \ t1 \\<^sub>1 t3" by blast
qed

lemma Rectangle_for_One:
  assumes a:  "t \\<^sub>1\<^sup>* t1" "t \\<^sub>1 t2"
  shows "\t3. t1 \\<^sub>1 t3 \ t2 \\<^sub>1\<^sup>* t3"
using a Diamond_for_One by (induct arbitrary: t2) (blast)+

lemma CR_for_One_star:
  assumes a: "t \\<^sub>1\<^sup>* t1" "t \\<^sub>1\<^sup>* t2"
    shows "\t3. t2 \\<^sub>1\<^sup>* t3 \ t1 \\<^sub>1\<^sup>* t3"
using a Rectangle_for_One by (induct arbitrary: t2) (blast)+

section \<open>Establishing the Equivalence of Beta-star and One-star\<close>

lemma Beta_Lam_cong:
  assumes a: "t1 \\<^sub>\\<^sup>* t2"
  shows "Lam [x].t1 \\<^sub>\\<^sup>* Lam [x].t2"
using a by (induct) (blast)+

lemma Beta_App_cong_aux:
  assumes a: "t1 \\<^sub>\\<^sup>* t2"
  shows "App t1 s\\<^sub>\\<^sup>* App t2 s"
    and "App s t1 \\<^sub>\\<^sup>* App s t2"
using a by (induct) (blast)+

lemma Beta_App_cong:
  assumes a: "t1 \\<^sub>\\<^sup>* t2" "s1 \\<^sub>\\<^sup>* s2"
  shows "App t1 s1 \\<^sub>\\<^sup>* App t2 s2"
using a by (blast intro: Beta_App_cong_aux)

lemmas Beta_congs = Beta_Lam_cong Beta_App_cong

lemma One_implies_Beta_star:
  assumes a: "t \\<^sub>1 s"
  shows "t \\<^sub>\\<^sup>* s"
using a by (induct) (auto intro!: Beta_congs)

lemma One_congs:
  assumes a: "t1 \\<^sub>1\<^sup>* t2"
  shows "Lam [x].t1 \\<^sub>1\<^sup>* Lam [x].t2"
  and   "App t1 s \\<^sub>1\<^sup>* App t2 s"
  and   "App s t1 \\<^sub>1\<^sup>* App s t2"
using a by (induct) (auto intro: One_refl)

lemma Beta_implies_One_star:
  assumes a: "t1 \\<^sub>\ t2"
  shows "t1 \\<^sub>1\<^sup>* t2"
using a by (induct) (auto intro: One_refl One_congs better_o4_intro)

lemma Beta_star_equals_One_star:
  shows "t1 \\<^sub>1\<^sup>* t2 = t1 \\<^sub>\\<^sup>* t2"
proof
  assume "t1 \\<^sub>1\<^sup>* t2"
  then show "t1 \\<^sub>\\<^sup>* t2" by (induct) (auto intro: One_implies_Beta_star)
next
  assume "t1 \\<^sub>\\<^sup>* t2"
  then show "t1 \\<^sub>1\<^sup>* t2" by (induct) (auto intro: Beta_implies_One_star)
qed

section \<open>The Church-Rosser Theorem\<close>

theorem CR_for_Beta_star:
  assumes a: "t \\<^sub>\\<^sup>* t1" "t\\<^sub>\\<^sup>* t2"
  shows "\t3. t1 \\<^sub>\\<^sup>* t3 \ t2 \\<^sub>\\<^sup>* t3"
proof -
  from a have "t \\<^sub>1\<^sup>* t1" and "t\\<^sub>1\<^sup>* t2" by (simp_all add: Beta_star_equals_One_star)
  then have "\t3. t1 \\<^sub>1\<^sup>* t3 \ t2 \\<^sub>1\<^sup>* t3" by (simp add: CR_for_One_star)
  then show "\t3. t1 \\<^sub>\\<^sup>* t3 \ t2 \\<^sub>\\<^sup>* t3" by (simp add: Beta_star_equals_One_star)
qed

end

quality98%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.