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