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+
−
+
−
+
−
+
−