# HG changeset patch
# User urbanc
# Date 1213257388 -7200
# Node ID 8d747de5c73ee60e26d33acd07c1c4920f6516fc
# Parent  21154312296df3534a88fe8ba4151522e9492486
soundness and completeness proofs for a CK machine as
well as proofs for type preservation

diff -r 21154312296d -r 8d747de5c73e src/HOL/Nominal/Examples/CK_Machine.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Thu Jun 12 09:56:28 2008 +0200
@@ -0,0 +1,550 @@
+(* $Id$ *)
+
+theory CK_Machine 
+  imports "../Nominal" 
+begin
+
+text {* 
+  
+  This theory establishes soundness and completeness for a CK-machine
+  with respect to a cbv-big-step semantics. The language includes 
+  functions, recursion, booleans and numbers. In the soundness proof 
+  the small-step cbv-reduction relation is used to get the induction
+  through. Type preservation is proved for the machine and also for
+  the small- and big-step semantics.
+
+  The theory is inspired by notes of Roshan James from Indiana University
+  and the lecture notes by Andy Pitts for his semantics course. See
+  
+  http://www.cs.indiana.edu/~rpjames/lm.pdf
+  http://www.cl.cam.ac.uk/teaching/2001/Semantics/
+
+*}
+
+atom_decl name
+
+nominal_datatype lam =
+  VAR "name"
+| APP "lam" "lam" 
+| LAM "\<guillemotleft>name\<guillemotright>lam" ("LAM [_]._")
+| NUM "nat"
+| DIFF "lam" "lam" ("_ -- _")
+| PLUS "lam" "lam" ("_ ++ _")
+| TRUE
+| FALSE
+| IF "lam" "lam" "lam"
+| FIX "\<guillemotleft>name\<guillemotright>lam" ("FIX [_]._")  
+| ZET "lam"                      (* zero test *)
+| EQI "lam" "lam"                (* equality test on numbers *)
+
+section {* Capture-Avoiding Substitution *}
+
+consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
+
+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])"
+  "(NUM n)[y::=s] = NUM n"
+  "(t\<^isub>1 -- t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) -- (t\<^isub>2[y::=s])"
+  "(t\<^isub>1 ++ t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) ++ (t\<^isub>2[y::=s])"
+  "x\<sharp>(y,s) \<Longrightarrow> (FIX [x].t)[y::=s] = FIX [x].(t[y::=s])"
+  "TRUE[y::=s] = TRUE"
+  "FALSE[y::=s] = FALSE"
+  "(IF t1 t2 t3)[y::=s] = IF (t1[y::=s]) (t2[y::=s]) (t3[y::=s])"
+  "(ZET t)[y::=s] = ZET (t[y::=s])"
+  "(EQI t1 t2)[y::=s] = EQI (t1[y::=s]) (t2[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 fresh_nat)
+
+lemma subst_rename: 
+  assumes a: "y\<sharp>t"
+  shows "t[x::=s] = ([(y,x)]\<bullet>t)[y::=s]"
+using a 
+by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
+   (auto simp add: calc_atm fresh_atm abs_fresh perm_nat_def)
+
+section {* Evaluation Contexts *}
+
+datatype ctx = 
+    Hole ("\<box>")  
+  | CAPPL "ctx" "lam"
+  | CAPPR "lam" "ctx"
+  | CDIFFL "ctx" "lam"
+  | CDIFFR "lam" "ctx"
+  | CPLUSL "ctx" "lam"
+  | CPLUSR "lam" "ctx"
+  | CIF "ctx" "lam" "lam"
+  | CZET "ctx"
+  | CEQIL "ctx" "lam"
+  | CEQIR "lam" "ctx"
+
+fun
+  filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>")
+where
+  "\<box>\<lbrakk>t\<rbrakk> = t"
+| "(CAPPL E t')\<lbrakk>t\<rbrakk> = APP (E\<lbrakk>t\<rbrakk>) t'"
+| "(CAPPR t' E)\<lbrakk>t\<rbrakk> = APP t' (E\<lbrakk>t\<rbrakk>)"
+| "(CDIFFL E t')\<lbrakk>t\<rbrakk> = (E\<lbrakk>t\<rbrakk>) -- t'"
+| "(CDIFFR t' E)\<lbrakk>t\<rbrakk> = t' -- (E\<lbrakk>t\<rbrakk>)"
+| "(CPLUSL E t')\<lbrakk>t\<rbrakk> = (E\<lbrakk>t\<rbrakk>) ++ t'"
+| "(CPLUSR t' E)\<lbrakk>t\<rbrakk> = t' ++ (E\<lbrakk>t\<rbrakk>)"
+| "(CIF E t1 t2)\<lbrakk>t\<rbrakk> = IF (E\<lbrakk>t\<rbrakk>) t1 t2"
+| "(CZET E)\<lbrakk>t\<rbrakk> = ZET (E\<lbrakk>t\<rbrakk>)"
+| "(CEQIL E t')\<lbrakk>t\<rbrakk> = EQI (E\<lbrakk>t\<rbrakk>) t'"
+| "(CEQIR t' E)\<lbrakk>t\<rbrakk> = EQI t' (E\<lbrakk>t\<rbrakk>)"
+
+fun 
+ ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _")
+where
+  "\<box> \<circ> E' = E'"
+| "(CAPPL E t') \<circ> E' = CAPPL (E \<circ> E') t'"
+| "(CAPPR t' E) \<circ> E' = CAPPR t' (E \<circ> E')"
+| "(CDIFFL E t') \<circ> E' = CDIFFL (E \<circ> E') t'"
+| "(CDIFFR t' E) \<circ> E' = CDIFFR t' (E \<circ> E')"
+| "(CPLUSL E t') \<circ> E' = CPLUSL (E \<circ> E') t'"
+| "(CPLUSR t' E) \<circ> E' = CPLUSR t' (E \<circ> E')"
+| "(CIF E t1 t2) \<circ> E' = CIF (E \<circ> E') t1 t2"
+| "(CZET E) \<circ> E' = CZET (E \<circ> E')"
+| "(CEQIL E t') \<circ> E' = CEQIL (E \<circ> E') t'"
+| "(CEQIR t' E) \<circ> E' = CEQIR t' (E \<circ> E')"
+
+lemma ctx_compose:
+  shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
+by (induct E1 rule: ctx.induct) (auto)
+
+fun
+  ctx_composes :: "ctx list \<Rightarrow> ctx" ("_\<down>")
+where
+    "[]\<down> = \<box>"
+  | "(E#Es)\<down> = (Es\<down>) \<circ> E"
+
+section {* CK Machine *}
+
+inductive
+  val :: "lam\<Rightarrow>bool" 
+where
+  v_LAM[intro]:   "val (LAM [x].e)"
+| v_NUM[intro]:   "val (NUM n)"  
+| v_FALSE[intro]: "val FALSE"
+| v_TRUE[intro]:  "val TRUE"
+
+equivariance val 
+
+inductive
+  machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto> <_,_>")
+where
+  m1[intro]: "<APP e1 e2,Es> \<mapsto> <e1,(CAPPL \<box> e2)#Es>"
+| m2[intro]: "val v \<Longrightarrow> <v,(CAPPL \<box> e2)#Es> \<mapsto> <e2,(CAPPR v \<box>)#Es>"
+| m3[intro]: "val v \<Longrightarrow> <v,(CAPPR (LAM [y].e) \<box>)#Es> \<mapsto> <e[y::=v],Es>"
+| m4[intro]: "<e1 -- e2, Es> \<mapsto> <e1,(CDIFFL \<box> e2)#Es>"
+| m5[intro]: "<NUM n1,(CDIFFL \<box> e2)#Es> \<mapsto> <e2,(CDIFFR (NUM n1) \<box>)#Es>"
+| m6[intro]: "<NUM n2,(CDIFFR (NUM n1) \<box>)#Es> \<mapsto> <NUM (n1 - n2),Es>"
+| m4'[intro]:"<e1 ++ e2, Es> \<mapsto> <e1,(CPLUSL \<box> e2)#Es>"
+| m5'[intro]:"<NUM n1,(CPLUSL \<box> e2)#Es> \<mapsto> <e2,(CPLUSR (NUM n1) \<box>)#Es>"
+| m6'[intro]:"<NUM n2,(CPLUSR (NUM n1) \<box>)#Es> \<mapsto> <NUM (n1+n2),Es>"
+| m7[intro]: "<IF e1 e2 e3,Es> \<mapsto> <e1,(CIF \<box> e2 e3)#Es>"
+| m8[intro]: "<TRUE,(CIF \<box> e1 e2)#Es> \<mapsto> <e1,Es>"
+| m9[intro]: "<FALSE,(CIF \<box> e1 e2)#Es> \<mapsto> <e2,Es>"
+| mA[intro]: "<FIX [x].t,Es> \<mapsto> <t[x::=FIX [x].t],Es>"
+| mB[intro]: "<ZET e,Es> \<mapsto> <e,(CZET \<box>)#Es>"
+| mC[intro]: "<NUM 0,(CZET \<box>)#Es> \<mapsto> <TRUE,Es>"
+| mD[intro]: "0 < n \<Longrightarrow> <NUM n,(CZET \<box>)#Es> \<mapsto> <FALSE,Es>"
+| mE[intro]: "<EQI e1 e2,Es> \<mapsto> <e1,(CEQIL \<box> e2)#Es>"
+| mF[intro]: "<NUM n1,(CEQIL \<box> e2)#Es> \<mapsto> <e2,(CEQIR (NUM n1) \<box>)#Es>"
+| mG[intro]: "<NUM n,(CEQIR (NUM n) \<box>)#Es> \<mapsto> <TRUE,Es>"
+| mH[intro]: "n1\<noteq>n2 \<Longrightarrow> <NUM n1,(CEQIR (NUM n2) \<box>)#Es> \<mapsto> <FALSE,Es>"
+
+inductive 
+  "machine_star" :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto>* <_,_>")
+where
+  ms1[intro]: "<e,Es> \<mapsto>* <e,Es>"
+| ms2[intro]: "\<lbrakk><e1,Es1> \<mapsto> <e2,Es2>; <e2,Es2> \<mapsto>* <e3,Es3>\<rbrakk> \<Longrightarrow> <e1,Es1> \<mapsto>* <e3,Es3>"
+
+lemma ms3[intro,trans]:
+  assumes a: "<e1,Es1> \<mapsto>* <e2,Es2>" "<e2,Es2> \<mapsto>* <e3,Es3>"
+  shows "<e1,Es1> \<mapsto>* <e3,Es3>"
+using a by (induct) (auto) 
+
+lemma ms4[intro]:
+  assumes a: "<e1,Es1> \<mapsto> <e2,Es2>" 
+  shows "<e1,Es1> \<mapsto>* <e2,Es2>"
+using a by (rule ms2) (rule ms1)
+
+section {* Evaluation Relation *}
+
+inductive
+  eval :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<Down> _") 
+where
+  eval_NUM[intro]:  "NUM n \<Down> NUM n" 
+| eval_DIFF[intro]: "\<lbrakk>t1 \<Down> (NUM n1); t2 \<Down> (NUM n2)\<rbrakk> \<Longrightarrow> t1 -- t2 \<Down> NUM (n1 - n2)"
+| eval_PLUS[intro]: "\<lbrakk>t1 \<Down> (NUM n1); t2 \<Down> (NUM n2)\<rbrakk> \<Longrightarrow> t1 ++ t2 \<Down> NUM (n1 + n2)"
+| eval_LAM[intro]:  "LAM [x].t \<Down> LAM [x].t"
+| eval_APP[intro]:  "\<lbrakk>t1\<Down> LAM [x].t; t2\<Down> t2'; t[x::=t2']\<Down> t'\<rbrakk> \<Longrightarrow> APP t1 t2 \<Down> t'"
+| eval_FIX[intro]:  "t[x::= FIX [x].t] \<Down> t' \<Longrightarrow> FIX [x].t \<Down> t'"
+| eval_IF1[intro]:  "\<lbrakk>t1 \<Down> TRUE; t2 \<Down> t'\<rbrakk> \<Longrightarrow> IF t1 t2 t3 \<Down> t'"
+| eval_IF2[intro]:  "\<lbrakk>t1 \<Down> FALSE; t3 \<Down> t'\<rbrakk> \<Longrightarrow> IF t1 t2 t3 \<Down> t'"
+| eval_TRUE[intro]: "TRUE \<Down> TRUE"
+| eval_FALSE[intro]:"FALSE \<Down> FALSE"
+| eval_ZET1[intro]: "t \<Down> NUM 0 \<Longrightarrow> ZET t \<Down> TRUE"
+| eval_ZET2[intro]: "\<lbrakk>t \<Down> NUM n; 0 < n\<rbrakk> \<Longrightarrow> ZET t \<Down> FALSE"
+| eval_EQ1[intro]:  "\<lbrakk>t1 \<Down> NUM n; t2 \<Down> NUM n\<rbrakk> \<Longrightarrow> EQI t1 t2 \<Down> TRUE"
+| eval_EQ2[intro]:  "\<lbrakk>t1 \<Down> NUM n1; t2 \<Down> NUM n2; n1\<noteq>n2\<rbrakk> \<Longrightarrow> EQI t1 t2 \<Down> FALSE"
+
+declare lam.inject[simp]
+inductive_cases eval_elim:
+  "APP t1 t2 \<Down> t'"
+  "IF t1 t2 t3 \<Down> t'"
+  "ZET t \<Down> t'"
+  "EQI t1 t2 \<Down> t'"
+  "t1 ++ t2 \<Down> t'"
+  "t1 -- t2 \<Down> t'"
+  "(NUM n) \<Down> t"
+  "TRUE \<Down> t"
+  "FALSE \<Down> t"
+declare lam.inject[simp del]
+
+lemma eval_to:
+  assumes a: "t \<Down> t'"
+  shows "val t'"
+using a by (induct) (auto)
+
+lemma eval_val:
+  assumes a: "val t"
+  shows "t \<Down> t"
+using a by (induct) (auto)
+
+theorem eval_implies_machine_star_ctx:
+  assumes a: "t \<Down> t'"
+  shows "<t,Es> \<mapsto>* <t',Es>"
+using a
+by (induct arbitrary: Es)
+   (metis eval_to machine.intros ms1 ms2 ms3 ms4 v_LAM)+
+
+text {* Completeness Property *}
+
+corollary eval_implies_machine_star:
+  assumes a: "t \<Down> t'"
+  shows "<t,[]> \<mapsto>* <t',[]>"
+using a by (auto dest: eval_implies_machine_star_ctx)
+
+section {* CBV Reduction Relation *}
+
+lemma less_eqvt[eqvt]:
+  fixes pi::"name prm"
+  and   n1 n2::"nat"
+  shows "(pi\<bullet>(n1 < n2)) = ((pi\<bullet>n1) < (pi\<bullet>n2))"
+by (simp add: perm_nat_def perm_bool)
+
+inductive
+  cbv :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>cbv _") 
+where
+  cbv1': "\<lbrakk>val v; x\<sharp>v\<rbrakk> \<Longrightarrow> APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]"
+| cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> APP t t2 \<longrightarrow>cbv APP t' t2"
+| cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> APP t2 t \<longrightarrow>cbv APP t2 t'"
+| cbv4[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t -- t2 \<longrightarrow>cbv t' -- t2"
+| cbv5[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t2 -- t \<longrightarrow>cbv t2 -- t'"
+| cbv6[intro]: "(NUM n1) -- (NUM n2) \<longrightarrow>cbv NUM (n1 - n2)"
+| cbv4'[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t ++ t2 \<longrightarrow>cbv t' ++ t2"
+| cbv5'[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t2 ++ t \<longrightarrow>cbv t2 ++ t'"
+| cbv6'[intro]:"(NUM n1) ++ (NUM n2) \<longrightarrow>cbv NUM (n1 + n2)"
+| cbv7[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> IF t t1 t2 \<longrightarrow>cbv IF t' t1 t2"
+| cbv8[intro]: "IF TRUE t1 t2 \<longrightarrow>cbv t1"
+| cbv9[intro]: "IF FALSE t1 t2 \<longrightarrow>cbv t2"
+| cbvA[intro]: "FIX [x].t \<longrightarrow>cbv t[x::=FIX [x].t]"
+| cbvB[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> ZET t \<longrightarrow>cbv ZET t'"
+| cbvC[intro]: "ZET (NUM 0) \<longrightarrow>cbv TRUE"
+| cbvD[intro]: "0 < n \<Longrightarrow> ZET (NUM n) \<longrightarrow>cbv FALSE"
+| cbvE[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> EQI t t2 \<longrightarrow>cbv EQI t' t2"
+| cbvF[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> EQI t2 t \<longrightarrow>cbv EQI t2 t'"
+| cbvG[intro]: "EQI (NUM n) (NUM n) \<longrightarrow>cbv TRUE"
+| cbvH[intro]: "n1\<noteq>n2 \<Longrightarrow> EQI (NUM n1) (NUM n2) \<longrightarrow>cbv FALSE"
+
+equivariance cbv
+nominal_inductive cbv
+ by (simp_all add: abs_fresh fresh_fact)
+
+lemma cbv1[intro]: 
+  assumes a: "val v" 
+  shows "APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]"
+proof -
+  obtain y::"name" where fs: "y\<sharp>(x,t,v)" by (rule exists_fresh, rule fin_supp, blast)
+  have "APP (LAM [x].t) v = APP (LAM [y].([(y,x)]\<bullet>t)) v" using fs
+    by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
+  also have "\<dots> \<longrightarrow>cbv  ([(y,x)]\<bullet>t)[y::=v]" using fs a by (auto simp add: cbv.eqvt cbv1')
+  also have "\<dots> = t[x::=v]" using fs by (simp add: subst_rename[symmetric])
+  finally show "APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]" by simp
+qed
+
+inductive 
+  "cbv_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>cbv* _")
+where
+  cbvs1[intro]: "e \<longrightarrow>cbv* e"
+| cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
+
+lemma cbvs3[intro,trans]:
+  assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
+  shows "e1 \<longrightarrow>cbv* e3"
+using a by (induct) (auto) 
+
+lemma cbv_in_ctx:
+  assumes a: "t \<longrightarrow>cbv t'"
+  shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>"
+using a by (induct E) (auto)
+
+lemma machine_implies_cbv_star_ctx:
+  assumes a: "<e,Es> \<mapsto> <e',Es'>"
+  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
+using a by (induct) (auto simp add: ctx_compose intro: cbv_in_ctx)
+
+lemma machine_star_implies_cbv_star_ctx:
+  assumes a: "<e,Es> \<mapsto>* <e',Es'>"
+  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
+using a 
+by (induct) (auto dest: machine_implies_cbv_star_ctx)
+
+lemma machine_star_implies_cbv_star:
+  assumes a: "<e,[]> \<mapsto>* <e',[]>"
+  shows "e \<longrightarrow>cbv* e'"
+using a by (auto dest: machine_star_implies_cbv_star_ctx)
+
+lemma cbv_eval:
+  assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3"
+  shows "t1 \<Down> t3"
+using a
+by (induct arbitrary: t3)
+   (auto elim!: eval_elim intro: eval_val)
+
+lemma cbv_star_eval:
+  assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"
+  shows "t1 \<Down> t3"
+using a by (induct) (auto simp add: cbv_eval)
+
+lemma cbv_star_implies_eval:
+  assumes a: "t \<longrightarrow>cbv* v" "val v"
+  shows "t \<Down> v"
+using a
+by (induct)
+   (auto simp add: eval_val cbv_star_eval dest: cbvs2)
+
+text {* Soundness Property *}
+
+theorem machine_star_implies_eval:
+  assumes a: "<t1,[]> \<mapsto>* <t2,[]>" 
+  and     b: "val t2" 
+  shows "t1 \<Down> t2"
+proof -
+  from a have "t1 \<longrightarrow>cbv* t2" by (simp add: machine_star_implies_cbv_star)
+  then show "t1 \<Down> t2" using b by (simp add: cbv_star_implies_eval)
+qed
+
+section {* Typing *}
+
+nominal_datatype ty =
+  tVAR "string"
+| tBOOL 
+| tINT
+| tARR "ty" "ty" ("_ \<rightarrow> _")
+
+declare ty.inject[simp]
+
+lemma ty_fresh:
+  fixes x::"name"
+  and   T::"ty"
+  shows "x\<sharp>T"
+by (induct T rule: ty.induct)
+   (auto simp add: fresh_string)
+
+types tctx = "(name\<times>ty) list"
+
+abbreviation
+  "sub_tctx" :: "tctx \<Rightarrow> tctx \<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"
+
+inductive
+  valid :: "tctx \<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)
+
+section {* Typing Relation *}
+
+inductive
+  typing :: "tctx \<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"
+| t_NUM[intro]:  "\<Gamma> \<turnstile> (NUM n) : tINT"
+| t_DIFF[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^isub>1 : tINT; \<Gamma> \<turnstile> t\<^isub>2 : tINT\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 -- t\<^isub>2 : tINT"
+| t_PLUS[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^isub>1 : tINT; \<Gamma> \<turnstile> t\<^isub>2 : tINT\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 ++ t\<^isub>2 : tINT"
+| t_TRUE[intro]:  "\<Gamma> \<turnstile> TRUE : tBOOL"
+| t_FALSE[intro]: "\<Gamma> \<turnstile> FALSE : tBOOL"
+| t_IF[intro]:    "\<lbrakk>\<Gamma> \<turnstile> t1 : tBOOL; \<Gamma> \<turnstile> t2 : T; \<Gamma> \<turnstile> t3 : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> IF t1 t2 t3 : T"
+| t_ZET[intro]:   "\<Gamma> \<turnstile> t : tINT \<Longrightarrow> \<Gamma> \<turnstile> ZET t : tBOOL"
+| t_EQI[intro]:   "\<lbrakk>\<Gamma> \<turnstile> t1 : tINT; \<Gamma> \<turnstile> t2 : tINT\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> EQI t1 t2 : tBOOL"
+| t_FIX[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T)#\<Gamma> \<turnstile> t : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> FIX [x].t : T"  
+
+declare lam.inject[simp]
+inductive_cases typing_inversion[elim]:
+  "\<Gamma> \<turnstile> t\<^isub>1 -- t\<^isub>2 : T"
+  "\<Gamma> \<turnstile> t\<^isub>1 ++ t\<^isub>2 : T"
+  "\<Gamma> \<turnstile> IF t1 t2 t3 : T"
+  "\<Gamma> \<turnstile> ZET t : T"
+  "\<Gamma> \<turnstile> EQI t1 t2 : T"
+  "\<Gamma> \<turnstile> APP t1 t2 : T"
+declare lam.inject[simp del]
+
+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_FIX_inversion[dest]:
+  assumes ty: "\<Gamma> \<turnstile> FIX [x].t : T" 
+  and     fc: "x\<sharp>\<Gamma>" 
+  shows "(x,T)#\<Gamma> \<turnstile> t : T"
+using ty fc 
+by (cases rule: typing.strong_cases) 
+   (auto simp add: alpha lam.inject abs_fresh ty_fresh)
+
+section {* Type Preservation for the CBV Reduction Relation *}
+
+lemma weakening: 
+  fixes \<Gamma>1 \<Gamma>2::"tctx"
+  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 (auto | 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])
+
+theorem cbv_type_preservation:
+  assumes a: "t \<longrightarrow>cbv t'"
+  and     b: "\<Gamma> \<turnstile> t : T" 
+  shows "\<Gamma> \<turnstile> t' : T"
+using a b
+apply(nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
+apply(auto elim!: typing_inversion dest: t_LAM_inversion simp add: type_substitution)
+apply(frule t_FIX_inversion)
+apply(auto simp add: type_substitution)
+done
+
+corollary cbv_star_type_preservation:
+  assumes a: "t \<longrightarrow>cbv* t'"
+  and     b: "\<Gamma> \<turnstile> t : T" 
+  shows "\<Gamma> \<turnstile> t' : T"
+using a b
+by (induct) (auto intro: cbv_type_preservation)
+
+section {* Type Preservation for the Machine and Evaluation Relation *}
+
+theorem machine_type_preservation:
+  assumes a: "<t,[]> \<mapsto>* <t',[]>"
+  and     b: "\<Gamma> \<turnstile> t : T" 
+  shows "\<Gamma> \<turnstile> t' : T"
+proof -
+  from a have "t \<longrightarrow>cbv* t'" by (simp add: machine_star_implies_cbv_star)
+  then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbv_star_type_preservation)
+qed
+
+theorem eval_type_preservation:
+  assumes a: "t \<Down> t'"
+  and     b: "\<Gamma> \<turnstile> t : T" 
+  shows "\<Gamma> \<turnstile> t' : T"
+proof -
+  from a have "<t,[]> \<mapsto>* <t',[]>" by (simp add: eval_implies_machine_star)
+  then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)
+qed
+
+end    
+   
+
+
+
+  
+
+  
+  
+
+