Theory Weakening

theory Weakening 
  imports "HOL-Nominal.Nominal" 
begin

text ‹
  A simple proof of the Weakening Property in the simply-typed 
  lambda-calculus. The proof is simple, because we can make use
  of the variable convention.›

atom_decl name 

text ‹Terms and Types›

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

nominal_datatype ty =
    TVar "string"
  | TArr "ty" "ty" ("_ → _" [100,100] 100)

lemma ty_fresh:
  fixes x::"name"
  and   T::"ty"
  shows "x♯T"
by (nominal_induct T rule: ty.strong_induct)
   (auto simp add: fresh_string)

text ‹
  Valid contexts (at the moment we have no type for finite 
  sets yet, therefore typing-contexts are lists).›

inductive
  valid :: "(name×ty) list ⇒ bool"
where
    v1[intro]: "valid []"
  | v2[intro]: "⟦valid Γ;x♯Γ⟧⟹ valid ((x,T)#Γ)"

equivariance valid

text‹Typing judgements›

inductive
  typing :: "(name×ty) list⇒lam⇒ty⇒bool" ("_ ⊢ _ : _" [60,60,60] 60) 
where
    t_Var[intro]: "⟦valid Γ; (x,T)∈set Γ⟧ ⟹ Γ ⊢ Var x : T"
  | t_App[intro]: "⟦Γ ⊢ t1 : T1→T2; Γ ⊢ t2 : T1⟧ ⟹ Γ ⊢ App t1 t2 : T2"
  | t_Lam[intro]: "⟦x♯Γ;(x,T1)#Γ ⊢ t : T2⟧ ⟹ Γ ⊢ Lam [x].t : T1→T2"

text ‹
  We derive the strong induction principle for the typing 
  relation (this induction principle has the variable convention 
  already built-in).›

equivariance typing
nominal_inductive typing
  by (simp_all add: abs_fresh ty_fresh)

text ‹Abbreviation for the notion of subcontexts.›

abbreviation
  "sub_context" :: "(name×ty) list ⇒ (name×ty) list ⇒ bool" ("_ ⊆ _" [60,60] 60) 
where
  "Γ1 ⊆ Γ2 ≡ ∀x T. (x,T)∈set Γ1 ⟶ (x,T)∈set Γ2"

text ‹Now it comes: The Weakening Lemma›

text ‹
  The first version is, after setting up the induction, 
  completely automatic except for use of atomize.›

lemma weakening_version1: 
  fixes Γ1 Γ2::"(name×ty) list"
  assumes a: "Γ1 ⊢ t : T" 
  and     b: "valid Γ2" 
  and     c: "Γ1 ⊆ Γ2"
  shows "Γ2 ⊢ t : T"
using a b c
by (nominal_induct Γ1 t T avoiding: Γ2 rule: typing.strong_induct)
   (auto | atomize)+

text ‹
  The second version gives the details for the variable
  and lambda case.›

lemma weakening_version2: 
  fixes Γ1 Γ2::"(name×ty) list"
  and   t ::"lam"
  and   τ ::"ty"
  assumes a: "Γ1 ⊢ t : T"
  and     b: "valid Γ2" 
  and     c: "Γ1 ⊆ Γ2"
  shows "Γ2 ⊢ t : T"
using a b c
proof (nominal_induct Γ1 t T avoiding: Γ2 rule: typing.strong_induct)
  case (t_Var Γ1 x T)  (* variable case *)
  have "Γ1 ⊆ Γ2" by fact 
  moreover  
  have "valid Γ2" by fact 
  moreover 
  have "(x,T)∈ set Γ1" by fact
  ultimately show "Γ2 ⊢ Var x : T" by auto
next
  case (t_Lam x Γ1 T1 t T2) (* lambda case *)
  have vc: "x♯Γ2" by fact   (* variable convention *)
  have ih: "⟦valid ((x,T1)#Γ2); (x,T1)#Γ1 ⊆ (x,T1)#Γ2⟧ ⟹ (x,T1)#Γ2 ⊢ t: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 ⊢ t : T2" using ih by simp
  with vc show "Γ2 ⊢ Lam [x].t : T1→T2" by auto
qed (auto) (* app case *)

text‹
  The original induction principle for the typing relation
  is not strong enough - even this simple lemma fails to be 
  simple ;o)›

lemma weakening_not_straigh_forward: 
  fixes Γ1 Γ2::"(name×ty) list"
  assumes a: "Γ1 ⊢ t : T"
  and     b: "valid Γ2" 
  and     c: "Γ1 ⊆ Γ2"
  shows "Γ2 ⊢ t : T"
using a b c
proof (induct arbitrary: Γ2)
  case (t_Var Γ1 x T) (* variable case still works *)
  have "Γ1 ⊆ Γ2" by fact
  moreover
  have "valid Γ2" by fact
  moreover
  have "(x,T) ∈ (set Γ1)" by fact 
  ultimately show "Γ2 ⊢ Var x : T" by auto
next
  case (t_Lam x Γ1 T1 t T2) (* lambda case *)
  (* These are all assumptions available in this case*)
  have a0: "x♯Γ1" by fact
  have a1: "(x,T1)#Γ1 ⊢ t : T2" by fact
  have a2: "Γ1 ⊆ Γ2" by fact
  have a3: "valid Γ2" by fact
  have ih: "⋀Γ3. ⟦valid Γ3; (x,T1)#Γ1 ⊆ Γ3⟧ ⟹ Γ3 ⊢ t : T2" by fact
  have "(x,T1)#Γ1 ⊆ (x,T1)#Γ2" using a2 by simp
  moreover
  have "valid ((x,T1)#Γ2)" using v2 (* fails *) 
    oops
  
text‹
  To show that the proof with explicit renaming is not simple, 
  here is the proof without using the variable convention. It
  crucially depends on the equivariance property of the typing
  relation.

›

lemma weakening_with_explicit_renaming: 
  fixes Γ1 Γ2::"(name×ty) list"
  assumes a: "Γ1 ⊢ t : T"
  and     b: "valid Γ2" 
  and     c: "Γ1 ⊆ Γ2"
  shows "Γ2 ⊢ t : T"
using a b c
proof (induct arbitrary: Γ2)
  case (t_Lam x Γ1 T1 t T2) (* lambda case *)
  have fc0: "x♯Γ1" by fact
  have ih: "⋀Γ3. ⟦valid Γ3; (x,T1)#Γ1 ⊆ Γ3⟧ ⟹ Γ3 ⊢ t : T2" by fact
  obtain c::"name" where fc1: "c♯(x,t,Γ1,Γ2)"  (* we obtain a fresh name *)
    by (rule exists_fresh) (auto simp add: fs_name1)
  have "Lam [c].([(c,x)]∙t) = Lam [x].t" using fc1 (* we then alpha-rename the lambda-abstraction *)
    by (auto simp add: lam.inject alpha fresh_prod fresh_atm)
  moreover
  have "Γ2 ⊢ Lam [c].([(c,x)]∙t) : T1 → T2" (* we can then alpha-rename our original goal *)
  proof - 
    (* we establish (x,T1)#Γ1 ⊆ (x,T1)#([(c,x)]∙Γ2) and valid ((x,T1)#([(c,x)]∙Γ2)) *)
    have "(x,T1)#Γ1 ⊆ (x,T1)#([(c,x)]∙Γ2)" 
    proof -
      have "Γ1 ⊆ Γ2" by fact
      then have "[(c,x)]∙((x,T1)#Γ1 ⊆ (x,T1)#([(c,x)]∙Γ2))" using fc0 fc1 
        by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
      then show "(x,T1)#Γ1 ⊆ (x,T1)#([(c,x)]∙Γ2)" by (rule perm_boolE)
    qed
    moreover 
    have "valid ((x,T1)#([(c,x)]∙Γ2))" 
    proof -
      have "valid Γ2" by fact
      then show "valid ((x,T1)#([(c,x)]∙Γ2))" using fc1
        by (auto intro!: v2 simp add: fresh_left calc_atm eqvts)
    qed
    (* these two facts give us by induction hypothesis the following *)
    ultimately have "(x,T1)#([(c,x)]∙Γ2) ⊢ t : T2" using ih by simp 
    (* we now apply renamings to get to our goal *)
    then have "[(c,x)]∙((x,T1)#([(c,x)]∙Γ2) ⊢ t : T2)" by (rule perm_boolI)
    then have "(c,T1)#Γ2 ⊢ ([(c,x)]∙t) : T2" using fc1 
      by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
    then show "Γ2 ⊢ Lam [c].([(c,x)]∙t) : T1 → T2" using fc1 by auto
  qed
  ultimately show "Γ2 ⊢ Lam [x].t : T1 → T2" by simp
qed (auto) (* var and app cases *)

text ‹
  Moral: compare the proof with explicit renamings to weakening_version1 
  and weakening_version2, and imagine you are proving something more substantial 
  than the weakening lemma.›

end