src/HOL/Nominal/Examples/LocalWeakening.thy

Mirabelle: actions are responsible for handling exceptions,
Mirabelle core logs only structural information,
measuring running times for sledgehammer and subsequent metis invocation,
Mirabelle produces reports for every theory (only for sledgehammer at the moment)

(* 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 "../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:
  "(\<exists>a. t = lPar a) \<or> (\<exists>n. t = lVar n) \<or> (\<exists>t1 t2. t = lApp t1 t2) \<or> 
   (\<exists>t1. t = lLam t1)"
by (induct t rule: llam.induct)
   (auto simp add: llam.inject)

nominal_primrec
  llam_size :: "llam \<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> llam \<Rightarrow> 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 \<circ> fst)") auto

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

constdefs
  freshen :: "llam \<Rightarrow> name \<Rightarrow> llam"
  "freshen t p \<equiv> vsub t 0 (lPar p)"

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

text {* types *}

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

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

text {* valid contexts *}

types cxt = "(name\<times>ty) list"

inductive
  valid :: "cxt \<Rightarrow> bool"
where
  v1[intro]: "valid []"
| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,T)#\<Gamma>)"

equivariance valid

lemma v2_elim:
  assumes a: "valid ((a,T)#\<Gamma>)"
  shows   "a\<sharp>\<Gamma> \<and> valid \<Gamma>"
using a by (cases) (auto)

text {* "weak" typing relation *}

inductive
  typing :: "cxt\<Rightarrow>llam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60)
where
  t_lPar[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lPar x : T"
| t_lApp[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lApp t1 t2 : T2"
| t_lLam[intro]: "\<lbrakk>x\<sharp>t; (x,T1)#\<Gamma> \<turnstile> freshen t x : T2\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lLam t : T1\<rightarrow>T2"

equivariance typing

lemma typing_implies_valid:
  assumes a: "\<Gamma> \<turnstile> t : T"
  shows "valid \<Gamma>"
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 \<Rightarrow> cxt \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 
where
  "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2"

lemma weakening_almost_automatic:
  fixes \<Gamma>1 \<Gamma>2 :: cxt
  assumes a: "\<Gamma>1 \<turnstile> t : T"
  and     b: "\<Gamma>1 \<subseteq> \<Gamma>2"
  and     c: "valid \<Gamma>2"
shows "\<Gamma>2 \<turnstile> 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)#\<Gamma>2" in meta_spec)
apply(auto intro!: t_lLam)
done

lemma weakening_in_more_detail:
  fixes \<Gamma>1 \<Gamma>2 :: cxt
  assumes a: "\<Gamma>1 \<turnstile> t : T"
  and     b: "\<Gamma>1 \<subseteq> \<Gamma>2"
  and     c: "valid \<Gamma>2"
shows "\<Gamma>2 \<turnstile> 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 "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 
  moreover  
  have "valid \<Gamma>2" by fact 
  moreover 
  have "(x,T)\<in> set \<Gamma>1" by fact
  ultimately show "\<Gamma>2 \<turnstile> lPar x : T" by auto
next
  case (t_lLam x t T1 \<Gamma>1 T2 \<Gamma>2) (* lambda case *)
  have vc: "x\<sharp>\<Gamma>2" "x\<sharp>t" by fact+  (* variable convention *)
  have ih: "\<lbrakk>(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2; valid ((x,T1)#\<Gamma>2)\<rbrakk> \<Longrightarrow> (x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" by fact
  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
  then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp
  moreover
  have "valid \<Gamma>2" by fact
  then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2)
  ultimately have "(x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" using ih by simp
  with vc show "\<Gamma>2 \<turnstile> lLam t : T1\<rightarrow>T2" by auto
next 
  case (t_lApp \<Gamma>1 t1 T1 T2 t2 \<Gamma>2)
  then show "\<Gamma>2 \<turnstile> lApp t1 t2 : T2" by auto
qed

end