Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Nominal/Examples/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 4 kB

Quellcode-Bibliothek Contexts.thy Sprache: 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 (\<open>\<box>\<close> 1000)
  | CAppL "ctx" "lam"
  | CAppR "lam" "ctx"
  | CLam "name" "ctx"  (\<open>CLam [_]._\<close> [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

quality100%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.