theory Lambda

imports "../Nominal2" 

begin

atom_decl name

nominal_datatype lam =

  Var "name"

| App "lam" "lam"

| Lam x::"name" l::"lam"  bind x in l

thm lam.distinct

thm lam.induct

thm lam.exhaust lam.strong_exhaust

thm lam.fv_defs

thm lam.bn_defs

thm lam.perm_simps

thm lam.eq_iff

thm lam.fv_bn_eqvt

thm lam.size_eqvt

section {* Typing *}

nominal_datatype ty =

  TVar string

| TFun ty ty ("_ \<rightarrow> _") 

lemma ty_fresh:

  fixes x::"name"

  and   T::"ty"

  shows "atom x \<sharp> T"

apply (nominal_induct T rule: ty.strong_induct)

apply (simp_all add: ty.fresh pure_fresh)

done

inductive

  valid :: "(name \<times> ty) list \<Rightarrow> bool"

where

  v_Nil[intro]: "valid []"

| v_Cons[intro]: "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"

inductive

  typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 

where

    t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"

  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"

  | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"

thm typing.intros

thm typing.induct

equivariance valid

equivariance typing

nominal_inductive typing

  avoids t_Lam: "x"

  by (simp_all add: fresh_star_def ty_fresh lam.fresh)

thm typing.strong_induct

abbreviation

  "sub_context" :: "(name \<times> ty) list \<Rightarrow> (name \<times> ty) list \<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"

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_version2: 

  fixes \<Gamma>1 \<Gamma>2::"(name \<times> ty) list"

  and   t ::"lam"

  and   \<tau> ::"ty"

  assumes a: "\<Gamma>1 \<turnstile> t : T"

  and     b: "valid \<Gamma>2" 

  and     c: "\<Gamma>1 \<subseteq> \<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_Var \<Gamma>1 x T)  (* 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> Var x : T" by auto

next

  case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)

  have vc: "atom x \<sharp> \<Gamma>2" by fact   (* variable convention *)

  have ih: "\<lbrakk>valid ((x, T1) # \<Gamma>2); (x, T1) # \<Gamma>1 \<subseteq> (x, T1) # \<Gamma>2\<rbrakk> \<Longrightarrow> (x, T1) # \<Gamma>2 \<turnstile> t : 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: v_Cons)

  ultimately have "(x, T1) # \<Gamma>2 \<turnstile> t : T2" using ih by simp

  with vc show "\<Gamma>2 \<turnstile> Lam x t : T1 \<rightarrow> T2" by auto

qed (auto) (* app case *)

lemma weakening_version1: 

  fixes \<Gamma>1 \<Gamma>2::"(name \<times> ty) list"

  assumes a: "\<Gamma>1 \<turnstile> t : T" 

  and     b: "valid \<Gamma>2" 

  and     c: "\<Gamma>1 \<subseteq> \<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 | atomize)+

done

inductive

  Acc :: "('a::pt \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"

where

  AccI: "(\<And>y. R y x \<Longrightarrow> Acc R y) \<Longrightarrow> Acc R x"

lemma Acc_eqvt [eqvt]:

  fixes p::"perm"

  assumes a: "Acc R x"

  shows "Acc (p \<bullet> R) (p \<bullet> x)"

using a

apply(induct)

apply(rule AccI)

apply(rotate_tac 1)

apply(drule_tac x="-p \<bullet> y" in meta_spec)

apply(simp)

apply(drule meta_mp)

apply(rule_tac p="p" in permute_boolE)

apply(perm_simp add: permute_minus_cancel)

apply(assumption)

apply(assumption)

done

nominal_inductive Acc .

thm Acc.strong_induct

end