new example

--- a/src/HOL/IsaMakefile	Sat May 31 00:34:04 2008 +0200
+++ b/src/HOL/IsaMakefile	Sun Jun 01 17:39:21 2008 +0200
@@ -826,6 +826,7 @@
   Nominal/Examples/SN.thy \
   Nominal/Examples/SOS.thy \
   Nominal/Examples/Support.thy \
+  Nominal/Examples/Type_Preservation.thy \
   Nominal/Examples/VC_Condition.thy \
   Nominal/Examples/W.thy \
   Nominal/Examples/Weakening.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/Type_Preservation.thy	Sun Jun 01 17:39:21 2008 +0200
@@ -0,0 +1,219 @@
+theory Type_Preservation
+  imports Nominal
+begin
+
+atom_decl name
+
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam" 
+| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._")
+
+text {* Capture-Avoiding Substitution *}
+
+consts 
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]")
+
+nominal_primrec
+  "(Var x)[y::=s] = (if x=y then s else (Var x))"
+  "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
+  "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
+apply(finite_guess)+
+apply(rule TrueI)+
+apply(simp add: abs_fresh)
+apply(fresh_guess)+
+done
+
+lemma  subst_eqvt[eqvt]:
+  fixes pi::"name prm"
+  shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"
+by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)
+   (auto simp add: perm_bij fresh_atm fresh_bij)
+
+lemma fresh_fact:
+  fixes z::"name"
+  shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]"
+by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
+   (auto simp add: abs_fresh fresh_prod fresh_atm)
+
+text {* Types *}
+
+nominal_datatype ty =
+    TVar "string"
+  | TArr "ty" "ty" ("_ \<rightarrow> _")
+
+lemma ty_fresh:
+  fixes x::"name"
+  and   T::"ty"
+  shows "x\<sharp>T"
+by (induct T rule: ty.induct)
+   (auto simp add: fresh_string)
+
+text {* Typing Contexts *}
+
+types ctx = "(name\<times>ty) list"
+
+abbreviation
+  "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<subseteq> _") 
+where
+  "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^isub>1 \<longrightarrow> x \<in> set \<Gamma>\<^isub>2"
+
+text {* Validity of typing contexts *}
+
+inductive
+  valid :: "(name\<times>ty) list \<Rightarrow> bool"
+where
+    v1[intro]: "valid []"
+  | v2[intro]: "\<lbrakk>valid \<Gamma>; x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,T)#\<Gamma>)"
+
+equivariance valid
+
+lemma valid_elim[dest]:
+  assumes a: "valid ((x,T)#\<Gamma>)"
+  shows "x\<sharp>\<Gamma> \<and> valid \<Gamma>"
+using a by (cases) (auto)
+
+lemma valid_insert:
+  assumes a: "valid (\<Delta>@[(x,T)]@\<Gamma>)"
+  shows "valid (\<Delta> @ \<Gamma>)" 
+using a
+by (induct \<Delta>)
+   (auto simp add:  fresh_list_append fresh_list_cons dest!: valid_elim)
+
+lemma fresh_set: 
+  shows "y\<sharp>xs = (\<forall>x\<in>set xs. y\<sharp>x)"
+by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)
+
+lemma context_unique:
+  assumes a1: "valid \<Gamma>"
+  and     a2: "(x,T) \<in> set \<Gamma>"
+  and     a3: "(x,U) \<in> set \<Gamma>"
+  shows "T = U" 
+using a1 a2 a3
+by (induct) (auto simp add: fresh_set fresh_prod fresh_atm)
+
+text {* typing relation *}
+
+inductive
+  typing :: "ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _") 
+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> t\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t\<^isub>1 t\<^isub>2 : T\<^isub>2"
+| t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2"
+
+equivariance typing
+nominal_inductive typing
+  by (simp_all add: abs_fresh ty_fresh)
+
+lemma t_Lam_inversion[dest]:
+  assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 
+  and     fc: "x\<sharp>\<Gamma>" 
+  shows "\<exists>T\<^isub>1 T\<^isub>2. T = T\<^isub>1 \<rightarrow> T\<^isub>2 \<and> (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2"
+using ty fc 
+by (cases rule: typing.strong_cases) 
+   (auto simp add: alpha lam.inject abs_fresh ty_fresh)
+
+lemma t_App_inversion[dest]:
+  assumes ty: "\<Gamma> \<turnstile> App t1 t2 : T" 
+  shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'"
+using ty 
+by (cases) (auto simp add: lam.inject)
+
+lemma weakening: 
+  fixes \<Gamma>1 \<Gamma>2::"ctx"
+  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
+by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
+   (auto | atomize)+
+
+lemma type_substitution_aux:
+  assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T"
+  and     b: "\<Gamma> \<turnstile> e' : T'"
+  shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 
+using a b 
+proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
+  case (t_Var \<Gamma>' y T x e' \<Delta>)
+  then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 
+       and  a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 
+       and  a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
+  from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
+  { assume eq: "x=y"
+    from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
+    with a3 have "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" using eq a4 by (auto intro: weakening)
+  }
+  moreover
+  { assume ineq: "x\<noteq>y"
+    from a2 have "(y,T) \<in> set (\<Delta>@\<Gamma>)" using ineq by simp
+    then have "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto
+  }
+  ultimately show "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" by blast
+qed (force simp add: fresh_list_append fresh_list_cons)+
+
+corollary type_substitution:
+  assumes a: "(x,T')#\<Gamma> \<turnstile> e : T"
+  and     b: "\<Gamma> \<turnstile> e' : T'"
+  shows "\<Gamma> \<turnstile> e[x::=e'] : T"
+using a b
+by (auto intro: type_substitution_aux[where \<Delta>="[]",simplified])
+
+text {* Beta reduction *}
+
+inductive 
+  "beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _")
+where
+  b1[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> App t1 s \<longrightarrow>\<^isub>\<beta> App t2 s"
+| b2[intro]: "s1 \<longrightarrow>\<^isub>\<beta> s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^isub>\<beta> App t s2"
+| b3[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>\<^isub>\<beta> Lam [x].t2"
+| b4[intro]: "x\<sharp>s \<Longrightarrow> App (Lam [x].t) s \<longrightarrow>\<^isub>\<beta> t[x::=s]"
+
+equivariance beta
+nominal_inductive beta
+  by (auto simp add: abs_fresh fresh_fact)
+
+
+theorem type_preservation:
+  assumes a: "t \<longrightarrow>\<^isub>\<beta> t'"
+  and     b: "\<Gamma> \<turnstile> t : T" 
+  shows "\<Gamma> \<turnstile> t' : T" 
+using a b
+proof (nominal_induct avoiding: \<Gamma> T rule: beta.strong_induct)
+  case (b1 t1 t2 s \<Gamma> T)
+  have "\<Gamma> \<turnstile> App t1 s : T" by fact
+  then obtain T' where a1: "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s : T'" by auto
+  have ih: "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<Longrightarrow> \<Gamma> \<turnstile> t2 : T' \<rightarrow> T" by fact
+  with a1 a2 show "\<Gamma> \<turnstile> App t2 s : T" by auto
+next 
+  case (b2 s1 s2 t \<Gamma> T)
+  have "\<Gamma> \<turnstile> App t s1 : T" by fact
+  then obtain T' where a1: "\<Gamma> \<turnstile> t : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s1 : T'" by auto
+  have ih: "\<Gamma> \<turnstile> s1 : T' \<Longrightarrow> \<Gamma> \<turnstile> s2 : T'" by fact
+  with a1 a2 show "\<Gamma> \<turnstile> App t s2 : T" by auto
+next 
+  case (b3 t1 t2 x \<Gamma> T)
+  have vc: "x\<sharp>\<Gamma>" by fact
+  have "\<Gamma> \<turnstile> Lam [x].t1 : T" by fact
+  then obtain T1 T2 where a1: "(x,T1)#\<Gamma> \<turnstile> t1 : T2" and a2: "T = T1 \<rightarrow> T2" using vc by auto
+  have ih: "(x,T1)#\<Gamma> \<turnstile> t1 : T2 \<Longrightarrow> (x,T1)#\<Gamma> \<turnstile> t2 : T2" by fact
+  with a1 a2 show "\<Gamma> \<turnstile> Lam [x].t2 : T" using vc by auto
+next
+  case (b4 x s t \<Gamma> T)
+  have vc: "x\<sharp>\<Gamma>" by fact
+  have "\<Gamma> \<turnstile> App (Lam [x].t) s : T" by fact
+  then obtain T' where a1: "\<Gamma> \<turnstile> Lam [x].t : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s : T'" by auto
+  from a1 obtain T1 T2 where a3: "(x,T')#\<Gamma> \<turnstile> t : T" using vc by (auto simp add: ty.inject)
+  from a3 a2 show "\<Gamma> \<turnstile> t[x::=s] : T" by (simp add: type_substitution)
+qed
+
+
+theorem type_preservation_automatic:
+  assumes a: "t \<longrightarrow>\<^isub>\<beta> t'"
+  and     b: "\<Gamma> \<turnstile> t : T" 
+  shows "\<Gamma> \<turnstile> t' : T"
+using a b
+by (nominal_induct avoiding: \<Gamma> T rule: beta.strong_induct)
+   (auto dest!: t_Lam_inversion t_App_inversion simp add: ty.inject type_substitution)
+
+end