Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Contexts.thy Sprache: Isabelle

Original von: Isabelle^©

theory Contexts
imports "HOL-Nominal.Nominal"
begin

text \<open>

  We show here that the Plotkin-style of defining
  beta-reduction (based on congruence rules) is
  equivalent to the Felleisen-Hieb-style representation
  (based on contexts).

  The interesting point in this theory is that contexts
  do not contain any binders. On the other hand the operation
  of filling a term into a context produces an alpha-equivalent
  term.

\<close>

atom_decl name

text \<open>
  Lambda-Terms - the Lam-term constructor binds a name
\<close>

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

text \<open>
  Contexts - the lambda case in contexts does not bind
  a name, even if we introduce the notation [_]._ for CLam.
\<close>

nominal_datatype ctx =
    Hole ("\" 1000)
  | CAppL "ctx" "lam"
  | CAppR "lam" "ctx"
  | CLam "name" "ctx"  ("CLam [_]._" [100,100] 100)

text \<open>Capture-Avoiding Substitution\<close>

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

text \<open>
  Filling is the operation that fills a term into a hole.
  This operation is possibly capturing.
\<close>

nominal_primrec
  filling :: "ctx \ lam \ lam" ("_\_\" [100,100] 100)
where
  "\\t\ = t"
| "(CAppL E t')\t\ = App (E\t\) t'"
| "(CAppR t' E)\t\ = App t' (E\t\)"
| "(CLam [x].E)\t\ = Lam [x].(E\t\)"
by (rule TrueI)+

text \<open>
  While contexts themselves are not alpha-equivalence classes, the
  filling operation produces an alpha-equivalent lambda-term.
\<close>

lemma alpha_test:
  shows "x\y \ (CLam [x].\) \ (CLam [y].\)"
  and   "(CLam [x].\)\Var x\ = (CLam [y].\)\Var y\"
by (auto simp add: alpha ctx.inject lam.inject calc_atm fresh_atm)

text \<open>The composition of two contexts.\<close>

nominal_primrec
ctx_compose :: "ctx \ ctx \ ctx" ("_ \ _" [100,100] 100)
where
  "\ \ E' = E'"
| "(CAppL E t') \ E' = CAppL (E \ E') t'"
| "(CAppR t' E) \ E' = CAppR t' (E \ E')"
| "(CLam [x].E) \ E' = CLam [x].(E \ E')"
by (rule TrueI)+

lemma ctx_compose:
  shows "(E1 \ E2)\t\ = E1\E2\t\\"
by (induct E1 rule: ctx.induct) (auto)

text \<open>Beta-reduction via contexts in the Felleisen-Hieb style.\<close>

inductive
  ctx_red :: "lam\lam\bool" ("_ \x _" [80,80] 80)
where
  xbeta[intro]: "E\App (Lam [x].t) t'\ \x E\t[x::=t']\"

text \<open>Beta-reduction via congruence rules in the Plotkin style.\<close>

inductive
  cong_red :: "lam\lam\bool" ("_ \o _" [80,80] 80)
where
  obeta[intro]: "App (Lam [x].t) t' \o t[x::=t']"
| oapp1[intro]: "t \o t' \ App t t2 \o App t' t2"
| oapp2[intro]: "t \o t' \ App t2 t \o App t2 t'"
| olam[intro]:  "t \o t' \ Lam [x].t \o Lam [x].t'"

text \<open>The proof that shows both relations are equal.\<close>

lemma cong_red_in_ctx:
  assumes a: "t \o t'"
  shows "E\t\ \o E\t'\"
using a
by (induct E rule: ctx.induct) (auto)

lemma ctx_red_in_ctx:
  assumes a: "t \x t'"
  shows "E\t\ \x E\t'\"
using a
by (induct) (auto simp add: ctx_compose[symmetric])

theorem ctx_red_implies_cong_red:
  assumes a: "t \x t'"
  shows "t \o t'"
using a by (induct) (auto intro: cong_red_in_ctx)

theorem cong_red_implies_ctx_red:
  assumes a: "t \o t'"
  shows "t \x t'"
using a
proof (induct)
  case (obeta x t' t)
  have "\\App (Lam [x].t) t'\ \x \\t[x::=t']\" by (rule xbeta)
  then show  "App (Lam [x].t) t' \x t[x::=t']" by simp
qed (metis ctx_red_in_ctx filling.simps)+ (* found by SledgeHammer *)

lemma ctx_existence:
  assumes a: "t \o t'"
  shows "\C s s'. t = C\s\ \ t' = C\s'\ \ s \o s'"
using a
by (induct) (metis cong_red.intros filling.simps)+

end

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.