Quelle LocalWeakening.thy Sprache: Isabelle

(* Formalisation of weakening using locally nameless    *)
(* terms; the nominal infrastructure can also derive    *)
(* strong induction principles for such representations *)
(*                                                      *)
(* Authors: Christian Urban and Randy Pollack           *)
theory LocalWeakening
  imports "HOL-Nominal.Nominal"
begin

atom_decl name

text \<open>
  Curry-style lambda terms in locally nameless
  representation without any binders
\<close>
nominal_datatype llam =
    lPar "name"
  | lVar "nat"
  | lApp "llam" "llam"
  | lLam "llam"

text \<open>definition of vsub - at the moment a bit cumbersome\<close>

lemma llam_cases:
  "(\a. t = lPar a) \ (\n. t = lVar n) \ (\t1 t2. t = lApp t1 t2) \
   (\<exists>t1. t = lLam t1)"
by (induct t rule: llam.induct)
   (auto simp add: llam.inject)

nominal_primrec
  llam_size :: "llam \ nat"
where
  "llam_size (lPar a) = 1"
| "llam_size (lVar n) = 1"
| "llam_size (lApp t1 t2) = 1 + (llam_size t1) + (llam_size t2)"
| "llam_size (lLam t) = 1 + (llam_size t)"
by (rule TrueI)+

function
  vsub :: "llam \ nat \ llam \ llam"
where
   vsub_lPar: "vsub (lPar p) x s = lPar p"
| vsub_lVar: "vsub (lVar n) x s = (if n < x then (lVar n)
                      else (if n = x then s else (lVar (n - 1))))"
| vsub_lApp: "vsub (lApp t u) x s = (lApp (vsub t x s) (vsub u x s))"
| vsub_lLam: "vsub (lLam t) x s = (lLam (vsub t (x + 1) s))"
using llam_cases
apply(auto simp add: llam.inject)
apply(rotate_tac 4)
apply(drule_tac x="a" in meta_spec)
apply(blast)
done
termination by (relation "measure (llam_size \ fst)") auto

lemma vsub_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi\(vsub t n s) = vsub (pi\t) (pi\n) (pi\s)"
by (induct t arbitrary: n rule: llam.induct)
   (simp_all add: perm_nat_def)

definition freshen :: "llam \ name \ llam" where
  "freshen t p \ vsub t 0 (lPar p)"

lemma freshen_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi\(freshen t p) = freshen (pi\t) (pi\p)"
by (simp add: vsub_eqvt freshen_def perm_nat_def)

text \<open>types\<close>

nominal_datatype ty =
    TVar "nat"
  | TArr "ty" "ty" (infix \<open>\<rightarrow>\<close> 200)

lemma ty_fresh[simp]:
  fixes x::"name"
  and   T::"ty"
  shows "x\T"
by (induct T rule: ty.induct)
   (simp_all add: fresh_nat)

text \<open>valid contexts\<close>

type_synonym cxt = "(name\ty) list"

inductive
  valid :: "cxt \ bool"
where
  v1[intro]: "valid []"
| v2[intro]: "\valid \;a\\\\ valid ((a,T)#\)"

equivariance valid

lemma v2_elim:
  assumes a: "valid ((a,T)#\)"
  shows   "a\\ \ valid \"
using a by (cases) (auto)

text \<open>"weak" typing relation\<close>

inductive
  typing :: "cxt\llam\ty\bool" (\ _ \ _ : _ \ [60,60,60] 60)
where
  t_lPar[intro]: "\valid \; (x,T)\set \\\ \ \ lPar x : T"
| t_lApp[intro]: "\\ \ t1 : T1\T2; \ \ t2 : T1\\ \ \ lApp t1 t2 : T2"
| t_lLam[intro]: "\x\t; (x,T1)#\ \ freshen t x : T2\\ \ \ lLam t : T1\T2"

equivariance typing

lemma typing_implies_valid:
  assumes a: "\ \ t : T"
  shows "valid \"
using a by (induct) (auto dest: v2_elim)

text \<open>
  we have to explicitly state that nominal_inductive should strengthen
  over the variable x (since x is not a binder)
\<close>
nominal_inductive typing
  avoids t_lLam: x
  by (auto simp add: fresh_prod dest: v2_elim typing_implies_valid)

text \<open>strong induction principle for typing\<close>
thm typing.strong_induct

text \<open>sub-contexts\<close>

abbreviation
  "sub_context" :: "cxt \ cxt \ bool" (\_ \ _\ [60,60] 60)
where
  "\1 \ \2 \ \x T. (x,T)\set \1 \ (x,T)\set \2"

lemma weakening_almost_automatic:
  fixes \<Gamma>1 \<Gamma>2 :: cxt
  assumes a: "\1 \ t : T"
  and     b: "\1 \ \2"
  and     c: "valid \2"
shows "\2 \ t : T"
using a b c
apply(nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
apply(auto)
apply(drule_tac x="(x,T1)#\2" in meta_spec)
apply(auto intro!: t_lLam)
done

lemma weakening_in_more_detail:
  fixes \<Gamma>1 \<Gamma>2 :: cxt
  assumes a: "\1 \ t : T"
  and     b: "\1 \ \2"
  and     c: "valid \2"
shows "\2 \ t : T"
using a b c
proof(nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
  case (t_lPar \<Gamma>1 x T \<Gamma>2)  (* variable case *)
  have "\1 \ \2" by fact
  moreover
  have "valid \2" by fact
  moreover
  have "(x,T)\ set \1" by fact
  ultimately show "\2 \ lPar x : T" by auto
next
  case (t_lLam x t T1 \<Gamma>1 T2 \<Gamma>2) (* lambda case *)
  have vc: "x\\2" "x\t" by fact+ (* variable convention *)
  have ih: "\(x,T1)#\1 \ (x,T1)#\2; valid ((x,T1)#\2)\ \ (x,T1)#\2 \ freshen t x : T2" by fact
  have "\1 \ \2" by fact
  then have "(x,T1)#\1 \ (x,T1)#\2" by simp
  moreover
  have "valid \2" by fact
  then have "valid ((x,T1)#\2)" using vc by (simp add: v2)
  ultimately have "(x,T1)#\2 \ freshen t x : T2" using ih by simp
  with vc show "\2 \ lLam t : T1\T2" by auto
next
  case (t_lApp \<Gamma>1 t1 T1 T2 t2 \<Gamma>2)
  then show "\2 \ lApp t1 t2 : T2" by auto
qed

end

quality91%

¤ Dauer der Verarbeitung: 0.8 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.