(* 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 ‹
Curry-style lambda terms
in locally nameless
representation without any binders
›
nominal_datatype llam =
lPar
"name"
| lVar
"nat"
| lApp
"llam" "llam"
| lLam
"llam"
text ‹definition of vsub - at the moment a bit cumbersome
›
lemma llam_cases:
"(\a. t = lPar a) \ (\n. t = lVar n) \ (\t1 t2. t = lApp t1 t2) \
(
∃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 ‹types›
nominal_datatype ty =
TVar
"nat"
| TArr
"ty" "ty" (
infix ‹→› 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 ‹valid contexts
›
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 ‹"weak" typing relation
›
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 ‹
we
have to explicitly state that
nominal_inductive should strengthen
over the variable x (since x
is not a
binder)
›
nominal_inductive typing
avoids t_lLam: x
by (auto simp add: fresh_prod dest: v2_elim typing_implies_valid)
text ‹strong
induction principle
for typing
›
thm typing.strong_induct
text ‹sub-contexts
›
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 Γ1 Γ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 Γ1 t T avoiding: Γ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 Γ1 Γ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 Γ1 t T avoiding: Γ2 rule: typing.strong_induct)
case (t_lPar Γ1 x T Γ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 Γ1 T2 Γ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 Γ1 t1 T1 T2 t2 Γ2)
then show "\2 \ lApp t1 t2 : T2" by auto
qed
end
