(* 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